Abstract

NICTA has completed the machine-checked, code-level formal verification of the full functional correctness of the seL4 operating system microkernel. This outcome confirms that it is feasible to perform this kind of detailed formal verification in real software engineering projects. However, although seL4 is complex, it is not a very large system (8700 lines of C code).

Our next broad challenge is to make it feasible to complete the code-level formal verification of key security and safety properties of very large highly-critical software-intensive systems. We expect that seL4 will provide a foundation for this. In this talk I will give an overview of three areas of recent ongoing research that I am involved with that help to address this broad challenge.

The first area is on better understanding of the software process and management for large-scale formal methods projects. The second area is on approaches to define and analyse software architectures for large trustworthy systems built using trusted and untrusted components. The final area is more methodological and philosophical: how should we establish the empirical validity of the formal models used in formal verification?

Bio: Mark Staples is a Principal Researcher in the Software Systems Research Group at NICTA , and a Conjoint Senior Lecturer at the University of New South Wales. He is conducting research at the borders between software engineering, formal methods, and systems.

Earlier at NICTA he was a member of, then led, NICTA ’s empirical software engineering group. He was the founding leader of the Fraunhofer Project Centre in Transport and Logistics at NICTA , a strategic collaboration between NICTA and Fraunhofer IESE . In conjunction with Fraunhofer IESE and SAP Research, he led the creation of the Future Logistics Living Lab facility and industry network.

Prior to joining NICTA , he worked in the software industry for several years, first on a safety-critical SCADA system, and then on a business-critical web payments infrastructure product. He completed undergraduate degrees in computer science and cognitive science at the University of Queensland, and a PhD on theorem proving and formal methods at the University of Cambridge.