A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code

This paper presents our solutions to some problems we encountered in an ongoing attempt to verify the micro-hypervisor currently developed within the Robin project. The problems that we discuss are (1) efficient automatic reasoning for type-correct programs in virtual memory, and (2) modeling memory...

Full description

Saved in:
Bibliographic Details
Published in:Electronic notes in theoretical computer science 2008-07, Vol.217, p.79-96
Main Authors: Tews, Hendrik, Weber, Tjark, Völp, Marcus
Format: Article
Language:English
Subjects:
formal verification
memory-mapped devices
micro-hypervisor
operating-system kernel
virtual memory
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper presents our solutions to some problems we encountered in an ongoing attempt to verify the micro-hypervisor currently developed within the Robin project. The problems that we discuss are (1) efficient automatic reasoning for type-correct programs in virtual memory, and (2) modeling memory-mapped devices with alignment requirements. The discussed solutions are integrated in our verification environment for operating-system kernels in the interactive theorem prover PVS. This verification environment will ultimately be used for the verification of the Robin micro-hypervisor. As a proof of concept we include an example verification of a very simple piece of code in our environment.
ISSN:1571-0661
1571-0661
DOI:10.1016/j.entcs.2008.06.043