Info

MPI Audience

English

60 Minutes

The correctness of low-level systems software like operating systems or
hypervisors is crucial to the reliability and security of modern systems.
One approach for ensuring the correctness of such low-level programs is
formal verification, which can show the absence of large classes of bugs.
However, to apply formal verification to low-level software, we must
deal with three challenges:
1) handling realistic programming languages and systems code, which is
often idiomatic and nuanced, and not written with the intention of being
verified,
2) ensuring the soundness of the verification technique, ideally via
foundational proofs (i.e. proofs that are machine-checked by a theorem
prover with a small trusted computing base, such as Coq), and
3) automating the verification effort as much as possible.

In my thesis, I present a verification framework for low-level systems
code that advances the state of the art along these three dimensions.
This framework consists of three components:
The first component is RefinedC, a new Coq-based approach to verifying C
code, combining foundational proofs with a high degree of automation.
The second component, Islaris, complements RefinedC by scaling the
verification of assembly code to realistic models of modern instruction
set architectures like Armv8-A and RISC-V.
The third component, DimSum, combines the two in a new "decentralized"
approach to reasoning about multi-language programs.
Overall, this results in a framework that can verify multi-language (C
and assembly) programs with a high degree of realism, foundational
proofs, and automation.

--email hidden

Zoom

923 6785 8852

passcode not visible

logged in users only