We have developed a stack of semantics for a high-level C-like language and low-level assembly code, which has been carefully crafted to support the pervasive verification of system software. It can handle mixed-language implementations and concurrently operating devices, and permits the transferral of properties to the target architecture while obeying its resource restrictions. We demonstrate the applicability of our framework by proving the correct virtualization of user memory in our microkernel, which implements demand paging. This verification target is of particular interest because it has a relatively simple top-level specification and it exercises all parts of our semantics stack. At the bottom level a disk driver written in assembly implements page transfers via a swap disk. A page-fault handler written in~C uses the driver to implement the paging algorithm. It guarantees that a step of the currently executing user can be simulated at the architecture level. Besides the mere theoretical and technical difficulties the project also bore the social challenge to manage the large verification effort, spread over many sites and people, concurrently contributing to and maintaining a common theory corpus. We share our experiences and elaborate on lessons learned.

Online Copy

Preprint available as PDF-File

BibTeX Entry

@article{Alkassar:JAR-42-2-38, AUTHOR = {Alkassar, E. and Hillebrand, M. A. and Leinenbach, D. C. and Schirmer, N. W. and Starostin, A. and Tsyban, A.}, TITLE = {Balancing the Load: Leveraging Semantics Stack for Systems Verification}, VOLUME = {42, Numbers 2-4}, YEAR = {2009}, PAGES = {389-454}, BOOKTITLE = {Journal of Automated Reasoning: Special Issue on Operating Systems Verification}, PUBLISHER = {Springer}, EDITOR = {Klein, Gerwin and Huuck, Ralf and Schlich, Bastian}, EE = {http://dx.doi.org/10.1007/s10817-009-9123-z}, } }