Portal de Periódicos da CAPES

Correct Microkernel Primitives

2008; Elsevier BV; Volume: 217; Linguagem: Inglês

10.1016/j.entcs.2008.06.048

1571-0661

A. N. Starostin, Alexandra Tsyban,

Distributed systems and fault tolerance

Primitives are basic means provided by a microkernel to implementors of operating system services. Intensively used within every OS and commonly implemented in a mixture of high-level and assembly programming languages, primitives are meaningful and challenging candidates for formal verification. We report on the accomplished correctness proof of academic microkernel primitives. We describe how a novel approach to verification of programs written in C with inline assembler is successfully applied to a piece of realistic system software. Necessary and sufficient criteria covering functional correctness and requirements for the integration into a formal model of memory virtualization are determined and formally proven. The presented results are important milestones on the way to a pervasively verified operating system.