There has been considerable recent interest in verifying operating systems [1,2]. One of the difficulties with this form of software verification is simply stating the verification problem formally and succinctly. This, combined with the fact that some of the critical parts of an operating system depend on services provided by a processor and programmed in assembly language, makes the task even more daunting.
This paper presents the verification of a separation kernel, which provides a “Chinese wall” between two virtual machines. The specification of such a kernel is formulated as a set of operational semantic rules. This specification can be seen to be “correct by construction” with respect to the Chinese-wall properties that a separation kernel ought to satisfy. The authors construct a refinement relation between this ideal machine and the real kernel implemented in ARM assembly language.
One of the highlights of the paper is the use of a formalization of the ARM instruction set architecture within the HOL4 higher-order logic system. This allows expression of both the ideal and real kernel in the same platform, and enables the construction and verification of a bisimulation relation between the two. The authors have tried to achieve a high degree of automation in the verification effort by, for example, building custom tools to iterate through the ARM instruction set and proving clauses of the bisimulation relation in HOL4. The use of tools for the automatic construction of pre-post condition pairs for the interrupt handler and bootstrap code from the ideal specification is also quite ingenious.