Soundness-guided security analysis for android applications. This project aims to develop a soundness-guided programme analysis to mitigate security threats caused by reflection and dynamic class loading in Android apps, without compromising precision and scalability. Both dynamic code update techniques are widely used in benign and malware apps, but state-of-the-art malware analysis tools ignore or mishandle them, missing security threats and vulnerabilities. The resulting open-source security ....Soundness-guided security analysis for android applications. This project aims to develop a soundness-guided programme analysis to mitigate security threats caused by reflection and dynamic class loading in Android apps, without compromising precision and scalability. Both dynamic code update techniques are widely used in benign and malware apps, but state-of-the-art malware analysis tools ignore or mishandle them, missing security threats and vulnerabilities. The resulting open-source security analysis tool will allow software industries and enterprises (from national security, finance, banking to healthcare, retail, telecommunications) to test their mobile software effectively for code defects or security threats early at software development time at significantly reduced cost.Read moreRead less
Micro Compilers: An Extensible Compiler Architecture for Increased Flexibility and Safety. Programming languages specialised to a particular application domain can cut software development costs and reduce programming errors. Unfortunately, most application domains cannot sustain the costly development and maintenance of the specialised compilers required to implement specialised languages. We address this problem by introducing a novel customisable compiler architecture that can be adapted to ....Micro Compilers: An Extensible Compiler Architecture for Increased Flexibility and Safety. Programming languages specialised to a particular application domain can cut software development costs and reduce programming errors. Unfortunately, most application domains cannot sustain the costly development and maintenance of the specialised compilers required to implement specialised languages. We address this problem by introducing a novel customisable compiler architecture that can be adapted to specialised languages and other special-purpose compiler requirements. Customisable compilers are especially important to a country like Australia that has only limited resources for special purpose developments. Moreover, we will train students at undergraduate and postgraduate level in the area of programming languages and compilers.Read moreRead less
Finding concurrency bugs in multithreaded software. This project aims to develop sound and practical techniques for detecting and eliminating concurrency bugs for object-oriented languages like Java, enabled by a new model for concurrent effects. The expected outcome is a novel technology that will significantly improve the safety, productivity and efficiency of large-scale concurrent programming.
Foundations of Executable Temporal Logic. In many computer applications, including those of temporal reasoning, distributed computations and knowledge representations, the concept of time is of central importance. Multiple granularity of time also plays a critical role as not all events are necessarily defined over a uniform model of time. This project will develop the foundations of executable logical representations, supporting multiple granularity of time. This will allow system developers a ....Foundations of Executable Temporal Logic. In many computer applications, including those of temporal reasoning, distributed computations and knowledge representations, the concept of time is of central importance. Multiple granularity of time also plays a critical role as not all events are necessarily defined over a uniform model of time. This project will develop the foundations of executable logical representations, supporting multiple granularity of time. This will allow system developers access to powerful logical techniques in those applications. In the process, fundamental problems in modelling multiple granularity of time will be identified, and application-independent solutions to those problems will be provided.Read moreRead less
Verified concurrent memory management on modern processors. This project aims to formally verify automatic memory managers in the presence of concurrency and the weakly ordered memory of modern processors. A new framework for verifying memory managers, reusable for a wide range of managed programming languages, target hardware, policies, and algorithms will be developed. Expected technical outcomes include improved techniques to ensure trustworthiness of the foundations on which critical softwar ....Verified concurrent memory management on modern processors. This project aims to formally verify automatic memory managers in the presence of concurrency and the weakly ordered memory of modern processors. A new framework for verifying memory managers, reusable for a wide range of managed programming languages, target hardware, policies, and algorithms will be developed. Expected technical outcomes include improved techniques to ensure trustworthiness of the foundations on which critical software infrastructures are built. This will significantly enhance the security of public and private cyber assets, and deliver applications that are more robust and trustworthy, across a range of critical infrastructure such as transportation, communication, energy and defence.Read moreRead less
Automating data placement and movement for explicitly managed memory hierarchies. Efficient management of explicitly managed memory hierarchies is essential, making a difference often by one order of magnitude in performance. Compiler-directed techniques promise to take the burden of memory management from the programmer and enable significant performance potential for a broader community, resulting in higher productivity.
Portable High-Performance Computing Based on Flattening and Fusion. We aim at simplifying the development and improving the portability of computing intensive applications, such as those from computational science and engineering, which are of growing scientific and economic relevance (e.g., drug synthesis, virtual wind tunnel, and geologic surveys). Our focus is on achieving portable high-performance for a particularly expressive high-level notation supporting irregular algorithms (like sparse ....Portable High-Performance Computing Based on Flattening and Fusion. We aim at simplifying the development and improving the portability of computing intensive applications, such as those from computational science and engineering, which are of growing scientific and economic relevance (e.g., drug synthesis, virtual wind tunnel, and geologic surveys). Our focus is on achieving portable high-performance for a particularly expressive high-level notation supporting irregular algorithms (like sparse matrices and hierarchical N-body codes). We will develop a set of program transformations and integrate them into a compiler implementing an aggressive fusion strategy optimising for the memory hierarchy. We do not propose a new programming language, but work within an existing one.Read moreRead less
Securing systems against code-reuse attacks with modular pointer analysis. This project aims to build secure defences against code-reuse attacks in large-scale C++ applications with millions of lines of code, by enforcing control flow integrity with modular pointer analysis. The state-of-the-art mitigation techniques that are deployed in mainstream computer operating systems can all be bypassed by advanced code-reuse attacks, resulting in security exploits in all major web browsers. The outcomes ....Securing systems against code-reuse attacks with modular pointer analysis. This project aims to build secure defences against code-reuse attacks in large-scale C++ applications with millions of lines of code, by enforcing control flow integrity with modular pointer analysis. The state-of-the-art mitigation techniques that are deployed in mainstream computer operating systems can all be bypassed by advanced code-reuse attacks, resulting in security exploits in all major web browsers. The outcomes of this project will be an exploit mitigation technology and an open-source tool that can significantly raise the bar against advanced code-reuse attacks, thereby providing a foundation for eliminating such security threats.Read moreRead less
A Programming Model of Object Validity for Secure and Efficient Concurrency. To provide improved performance and security for software applications, Australia's ICT industry must adapt to the complex programming demands of modern multicore processors. The programming model developed in the project represents a breakthrough solution. A seamless integration of concurrency and object orientation leads to a simple yet powerful programming style that is compatible with today's premier approach to bui ....A Programming Model of Object Validity for Secure and Efficient Concurrency. To provide improved performance and security for software applications, Australia's ICT industry must adapt to the complex programming demands of modern multicore processors. The programming model developed in the project represents a breakthrough solution. A seamless integration of concurrency and object orientation leads to a simple yet powerful programming style that is compatible with today's premier approach to building large-scale software systems with significantly improved performance and security. The product will reduce development time for compute-intensive applications in many industry sectors, including health care (e.g. patient monitoring), finance, defence, environment, mining, manufacturing and computer games.Read moreRead less
Sparse Demand-Driven Analysis to Improve Software Reliability and Security. Current static analysis tools can eliminate many bugs missed by traditional testing but they are still imprecise or inefficient. This project aims to develop precise pointer analyses that enable -finding clients to detect bugs efficiently in large-scale programs in C/C++ and Java, where pointers are used pervasively. The novelty lies in performing these analyses sparsely (allowing data-flow information to move directly f ....Sparse Demand-Driven Analysis to Improve Software Reliability and Security. Current static analysis tools can eliminate many bugs missed by traditional testing but they are still imprecise or inefficient. This project aims to develop precise pointer analyses that enable -finding clients to detect bugs efficiently in large-scale programs in C/C++ and Java, where pointers are used pervasively. The novelty lies in performing these analyses sparsely (allowing data-flow information to move directly from variable definitions to their potential uses) based on Context-Free-Language-reachability (enabling client queries to be answered on-demand). The outcomes aim to significantly improve the reliability and security of industrial-sized software.Read moreRead less