Virtual Computer Science joint ICE-TCS/GSSI seminars: Helgi Kristvin Sigurbjarnarson
Push-Button Verification of Systems Software
Schedule: 22 June, 16:00 GMT/17:00 BST/18:00 Italian time
Virtual link: https://accounts.eyeson.team/rooms/XpWCVrLlnc1BsF
Speaker: Helgi Kristvin Sigurbjarnarson (Synthetic Minds, Seattle, USA; https://synthetic-minds.com/)
WWW: https://homes.cs.washington.edu/~helgi/
Title: Push-Button Verification of Systems Software
Abstract: Systems software interfaces with hardware, multiplexes resources, and provides common abstractions for modern applications to build on. The correctness and reliability of these systems are critical for the applications and users that depend on them. While formal verification of systems software can be effective at eliminating bugs, it is a non-trivial task, requiring developers to write many lines of proof code for every line of implementation code. This is a considerable engineering effort that requires a high degree of expertise to achieve.
In this talk, which is based on work presented in my doctoral dissertation defended last February, I will present a new approach to designing, specifying, implementing, and verifying systems software in a push-button fashion. By co-designing systems software with automation, I argue it is possible to build correct and reliable systems with substantially less effort. I developed four systems to demonstrate the effectiveness of this approach, using the Z3 satisfiability modulo theories (SMT) solver:
- Yggdrasil, a toolkit for writing file systems,
- an OS kernel named Hyperkernel, which has a high degree of proof automation and low proof burden,
- Nickel, a framework that helps developers design and verify information flow control systems by systematically eliminating covert channels inherent in the interface, and
- Ratatoskr, showing the feasibility of applying push-button verification to distributed protocols.
I argue that these contributions demonstrate the effectiveness of treating automation as a first-class design principle, letting developers build verified systems software with substantially less effort.
--
Seminars Computer Science
Gran Sasso Science Institute (GSSI), L’Aquila, Italy
URL: http://cs.gssi.it
