The seL4 verification journey: how have the challenges and opportunities evolved
ABSTRACT: The formal verification journey of the seL4 microkernel is nearing two decades, and still has an busy roadmap for the years ahead. It started as a research project aiming for a highly challenging problem with the potential of significant impact. Today, a whole ecosystem of developers, researchers, adopters and supporters are part of the seL4 community. With increasing uptake and adoption, seL4 is evolving, supporting more platforms, architectures, configurations, and features. This creates both opportunities and challenges: verification is what makes seL4 unique; as the seL4 code evolves, so must its formal proofs. With more than a million lines of formal, machine-checked proofs, seL4 is the most highly assured OS kernel, with proofs of an increasing number of properties (functional correctness, binary correctness, security –integrity and confidentiality– and system initialisation) and for an increasing number of hardware architectures: Arm (32-bit), x86 (64-bit) and RISC-V (64-bit), with proofs now starting for Arm (64-bit). In this talk we will reflect on the evolution of the challenges and opportunities the seL4 verification faced along its long, and continuing, journey.
BIO: June Andronick is CEO and co-founder of Proofcraft, providing commercial support for software verification in general and the seL4 microkernel verification in particular. She is also CEO of the seL4 Foundation, and conjoint Professor at UNSW Sydney. Her technical expertise is in increasing the reliability of critical software systems, by mathematically proving that the code behaves as expected and satisfies security and safety requirements. She previously led the Trustworthy Systems group, world-leading in the area of verified operating systems software, known worldwide for the formal verification of the seL4 microkernel. She was recognised in 2011 by MIT’s Technology Review as one of the world’s top young innovators (TR35). She holds a PhD in Computer Science from the University of Paris-Sud, France.
Why do things go wrong (or right)? Applications of causal reasoning to verification
ABSTRACT: In this talk I will look at the connections between causality and learning from one side, and verification and synthesis from the other side. I will introduce the relevant concepts and discuss how causality and learning can help to improve the quality of systems and reduce the amount of human effort in designing and verifying systems. I will (briefly) introduce the theory of actual causality as defined by Halpern and Pearl. This theory turns out to be extremely useful in various areas of computer science due to a good match between the results it produces and our intuition. I will illustrate the definitions by examples from formal verification. I will also argue that active learning can be viewed as a type of causal discovery. Tackling the problem of reducing the human effort from the other direction, I will discuss ways to improve the quality of specifications and will focus in particular on synthesis.
BIO: Hana Chockler is a Principal Scientist at a startup company causaLens and a Reader (Associate Professor) in Formal Methods in the Department of Informatics at King’s College London (KCL). Prior to joining KCL in 2013, Hana worked at IBM Research in the formal verification and software engineering departments. Her research interests span a wide variety of topics, including formal verification and synthesis of hardware and software, fundamental concepts in causality and its applications to a variety of domains, learning, and explainable AI.