MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Automated and Foundational Verification of Low-Level Programs

Michael Sammler
MPI-SWS
SWS Student Defense Talks - Thesis Defense

Michael Sammler is a PhD student at the Max Planck Institute for Software Systems under the supervision of Deepak Garg and Derek Dreyer. His research focuses on developing techniques for formal verification of realistic low-level systems software that combine machine-checked proofs with a high degree of automation. He has received multiple awards for his research, including Distinguished Paper awards at PLDI and POPL and a Google PhD fellowship.
SWS  
AG Audience
English

Date, Time and Location

Monday, 4 December 2023
17:00
60 Minutes
E1 5
029
Saarbrücken

Abstract

Formal verification is a promising technique to ensure the reliability of low-level programs like operating systems and hypervisors, since it can show the absence of whole classes of bugs and prevent critical vulnerabilities.
To realize the full potential of formal verification for real-world low-level programs, however one has to overcome several challenges, including:
(1) dealing with the complexities of realistic models of real-world programming languages;
(2) ensuring the trustworthiness of the verification, ideally by providing foundational proofs (i.e., proofs that can be checked by a general-purpose proof assistant);
and (3) minimizing the manual effort required for verification by providing a high degree of automation.

This dissertation presents multiple projects that advance formal verification along these three axes:
RefinedC provides the first approach for verifying C code that combines foundational proofs with a high degree of automation via a novel refinement and ownership type system.
Islaris shows how to scale verification of assembly code to realistic models of modern instruction set architectures-in particular, Armv8-A and RISC-V.
DimSum develops a decentralized approach for reasoning about programs that consist of components written in multiple different languages (e.g., assembly and C), as is common for low-level programs.
RefinedC and Islaris rest on Lithium, a novel proof engine for separation logic that combines automation with foundational proofs.

Contact

Gretchen Gravelle
+49 681 9303 9102
--email hidden

Video Broadcast

Yes
Kaiserslautern
G26
113
passcode not visible
logged in users only

Gretchen Gravelle, 11/14/2023 13:09 -- Created document.