IEEE Secure Development Conference

September 25 - 27, 2019
Hilton McLean Tysons Corner
McLean, VA

Sponsored by the IEEE Computer Society Technical Committee on Security and Privacy

2019 June

Posted on: June 10th, 2019 by Shelby Allen

June Andronick
Data61/CSIRO and UNSW

Componentise, Isolate, Prove; The seL4 Security Story

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.