Johanna Polzin is working on her Bachelor’s Thesis at ETH Zürich Switzerland in David Basin’s group, working with Matthias Brun (ETH), Andrea Lattuada (MPI-SWS), and Reto Achermann (UBC) on OS specification and verification using semi-automated verification tools.

AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI   Info

AG Audience

English

60 Minutes

Saarbrücken

For complex, concurrent programs testing has proven insufficient to catch most bugs before a system is deployed. Formal verification addresses this issue by proving that bad behavior cannot ever happen, rather than relying on individual tests that demonstrate the program behaves correctly on specific inputs. The community has developed verified operating systems and verified user-space programs, but the two are generally disconnected: user-space programs still need to be verified against a manually derived, error-prone environment specification representing the execution environment that the user space program experiences.

In contrast to OS specifications that only verify integrity and confidentiality, a process-centric OS specification enables the construction of end-to-end verified software. In this talk, I will discuss the specification of page tables in a concurrent OS as a case study for process-centric OS specification. I will address the role of concurrency and of correctly modeling and handling of the hardware’s address translation caches, and I will demonstrate how such a specification can then be used to verify a (model of) a simple user-space program.

Annika Meiser

+49 681 9303 9105

--email hidden

Zoom

966 8141 4048

passcode not visible

logged in users only