June Andronick
Data61/CSIRO and UNSW

Is formally verified software more secure? Well, it depends: more secure than what? If a software system is secure already, then formal verification simply supplies the evidence (and in fact the strongest possible evidence) that it actually is secure. Most developed software systems, however, even when built with security in mind, will inevitably still contain errors that lead to vulnerabilities. The process of providing a formal proof of the system’s security will reveal these vulnerabilities, and it reveals all of them — as opposed to testing (as long as you can clearly define what security means, of course). In the extreme case where the system has no built-in security, then formal verification is not of much help to magically add security as an afterthought; it cannot, for instance, suggest a redesign of the implementation.

In this talk I’ll present the approach we advocate for building software that is provably secure; and I will give evidence of its success, and of its impact on systems that have been built on our formally verified seL4 microkernel.

Bio: June Andronick leads the Trustworthy Systems group, world-leading in verified operating systems software, known worldwide for the formal verification of the seL4 microkernel. She is a Principal Research Scientist at Data61|CSIRO, and conjoint Associate Professor at UNSW Sydney, Australia.