Trustworthy Software
Our world relies on software, so it is key for that software to be trustworthy and function correctly. This is particularly crucial for software in safety-critical applications such as drones and autonomous vehicles, financial applications such as blockchain smart contracts, but is important for all kinds of software.
Our research group is working on ensuring software correctness and trustworthiness using a variety of techniques, including formal software verification, static analysis of programs, and symbolic execution. The gold standard for software verification is machine-checked formal proof of correctness, followed by verified refinement down to the executable machine code or bytecode. We have several projects that are exploring this approach, using interactive theorem provers such as Isabelle or automated reasoning solvers such as Z3.
Current Projects
Verifying GraalVM Optimization Passes (Oracle, 2020-2026)
Compilers are an essential ingredient of the computing base, and the GraalVM compiler is a widely-used optimizing compiler for Java and other languages. The focus of this project is on the verification of compiler optimization passes because these are commonly the source of compiler errors. The GraalVM compiler uses a sophisticated ‘sea of nodes’ intermediate representation (IR) that combines the control-flow and data-flow graphs, and optimizations are complex transformations of these IR graphs. We are modelling and verifying these optimizations using the Isabelle interactive theorem prover, to ensure that the optimizations preserve correctness under all circumstances.
Researchers: Prof. Ian Hayes, A/Prof. Mark Utting, Brae Webb.
Design and verification of correct, efficient and secure concurrent systems (ARC DP, 2019-2022)
Today’s software must be correct and secure, but it must also be fast: written to take advantage of modern multi-core architectures. Complex interactions between concurrent processes are needed to achieve efficiency but can easily compromise correctness and security. For software deplyed on millions of devices, or that is used to control critical infrastructure, the consequences can be devastating. Traditional development methods cannot cope with the complexity and scale of such software applications. The project aims to provide methods for the design and verification of correct, secure and efficient concurrent software that are scalable and mechanised. They are expected to reduce the prevalence of failures in efficient, modern software.
Researchers: Prof. Ian Hayes, Dr Larissa Meinicke, Dr Callum Bannister
Verifying Concurrent Data Structures for Multicore seL4 (DSTG with ANU, 2021–2024)
This project aims to develop a framework for specifying and verifying concurrent data structures (CDS) running on hardware with weak memory in the proof assistant Isabelle/HOL, focusing on the inclusion of weak memory models, the support of CDSs required by software running in parallel within the kernel and on top of a kernel, as well as the needs of a multicore extension of seL4. The main issues over the earlier “sequential” verification of the uniprocessor kernel are handling parallel execution of the kernel itself on multiple processors, and the complications that arise due to the weak memory models, which give rise to out-of-order execution. The project also considers concurrent user software running on arbitrary operating systems. The specification language to be used for specifying and verification should be based on existing technology, such as Complx [1] and the language used in [2]. CDSs include both blocking (locking) data structures and non- blocking structures, such as read-copy-update data structures and locking mechanisms, such as ticket lock and CLH lock.
Researchers: Prof. Ian Hayes, Dr Larissa Meinicke, Dr Robert Colvin (DSTG), A/Prof. Peter Höfner (ANU), Prof. Tony Hosking (ANU), Dr Peter Gammie (ANU).
Program Analysis Cell (DSTG, 2018–)
The DSTG Program Analysis Cell investigates the use of formal methods and program analysis for detecting software security vulnerabilities. The aim is to develop advanced tools and techniques for the simultaneous development of cyber-secure systems and the associated assurance evidence necessary to prove the systems’ lack of vulnerabilities and flaws, and resistance to attacks. The emphasis of the research is on general techniques, rather than specific solutions, allowing for a diversity of solutions and innovation to be supported. This will lead to cybersecurity principles that will endure as systems and attacks evolve into the future.
Areas of research include:
Formal security foundations - developing a formal understanding of the effects of multicore hardware, operating systems, and compilation processes on information security.
Advanced program analysis - developing automated techniques for finding security vulnerabilities during software development and evolution.
Secure software development - establishing a tool/language ecosystem supporting vulnerability analysis of software at the source code, binary and intermediate levels.
Researchers: A/Prof. Graeme Smith, Dr Kirsten Winter, Dr Robert Colvin, Nicholas Coughlin, Katrina Lam
BASIL: Boogie Analysis for Secure Information-Flow Logics (DSTG, 2022–2024)
This project is implementing an information-flow security analysis logic (previously developed by DSTG) on top of the Boogie intermediate language for software verification. This will increase the automation of the approach, and integrate support for the generation of annotations. The analysis technique has been designed by DSTG to provide higher assurance than is available through existing analysis tools. The focus on automation in this project will ensure the tool can be incorporated into current software development processes with minimal cost and effort.
Researchers: A/Prof. Mark Utting, Dr Kirsten Winter, Mr Liam Kent, Mr Harrison Van Roy, Mr James Tobler
AVESC: Automated Verification of Ethereum Smart-Contracts (UQ Cyber Seed Funding, 2022):
Blockchains and smart contracts are a promising technology for distributed finance applications. The correctness of smart contracts is crucial, since their code is public, they cannot easily be updated, and bugs can lead to millions of dollars being lost. This project will investigate a new approach to verifying the correctness of smart contracts that goes all the way from high-level financial properties down to the correctness of the low-level blockchain bytecode that implements the smart contract. The verification process will use automated SMT solvers that do not require theorem prover expertise, so the resulting verification tools will be widely usable.
Researchers: A/Prof. Mark Utting, Dr Naipeng Dong, Dr Marten Risius, Dr Franck Cassez, Mr Daniel Cumming, Mr Sadra Bayat Tork.
BAP ARMv8 Lifter Extension (DSTG, 2022)
To enable the analysis of binary code, an analysis tool needs to be paired with a lifter which disassembles the binaries and lifts the resulting assembly into an intermediate representation suitable for further processing by the analysis tool. Such a prototypical lifter exists in the Binary Analysis Platform (BAP) but requires extensions for the ARMv8 instruction set architecture. This project aims to build on the existing infrastructure of the BAP framework and extend its scope.
As an alternative the project also investigates the partial evaluation of the ARM machine-readable specification language to automatically derive a lifter. This approach builds on the existing open-source implementation of ARM Specification Language interpreter (ASLi), a library of tools to parse and manipulate the machine-readable hardware specification.
Researchers: A/Prof. John Williams, Dr Kirsten Winter, Adriel Efendy, Thomas Malcolm, Kaitlyn Lake, Thomas Le, James Paterson, Alastair Michael, Andrew Brown