Verification and formal methods
Verification and Formal Methods are powerful techniques to demonstrate the trustworthiness and security of computer systems and software. Software especially is increasingly exposed to sophisticated attack, while being increasingly relied upon as critical infrastructure across many sectors. In this environment, software security vulnerabilities can be incredibly harmful. Verification and formal methods can produce rigorous arguments about the absence of entire classes of security vulnerability, and are an incredibly powerful tool to build highly secure software systems.
This group of researchers focuses on:
Automated program analysis
Building techniques for automatically analysing software to determine whether it is correct and trustworthy. These techniques can be used by everyday software developers to help them write more secure software by detecting common forms of security vulnerabilities.
Secure embedded devices
Focuses on applying formal methods and formally verified software components to build highly secure embedded devices.
Proof methods for securing concurrent software
Examines the problem of how to ensure that software that is composed of multiple concurrently executing threads of execution is secure. Concurrency is ubiquitous in everyday software, yet makes the problem of detecting security vulnerabilities very challenging. This pillar focuses on building new techniques to prove that concurrent software doesn’t leak sensitive information.
Understanding the costs and benefits of formal methods
Looks at verification and formal methods in the context of software engineering to better understand its benefits as well as its costs. While verification and formal methods have produced incredibly trustworthy systems, they remain relatively few in number and poorly understood by outsiders. This pillar aims to improve our understanding of these techniques to better inform decision about their adoption.
Key research projects
Some of our key research projects are:Cross domain desktop compositor
A collaboration between DST Group and Data61 to develop a new kind of embedded device to enable highly secure access to multiple classified workstations simultaneously while ensuring that sensitive information is not exposed to attackers.The COVERN project: compositional verification and refinement of non-interference
A collaboration with Data61, University of New South Wales and Chalmers University of Technology (Sweden) to develop new techniques to prove that concurrent software can keep confidential information secure.
Understanding the benefits and drawbacks of proofs for secure software
A collaboration with Carleton University (Canada) to understand how proofs of software security relate to traditional software engineering.
