Paper Info
Title
Completing the automated verification of a small hypervisor - assembler code verification
Abstract
In [1] the almost complete formal verification of a small hypervisor with the automated C code verifier VCC [2] was reported: the correctness of the C portions of the hypervisor and of the guest simulation was established; the verification of the assembler portions of the code was left as future work. Suitable methodology for the verification of Macro Assembler programs in VCC was given without soundness proof in [3]. A joint semantics of C + Macro Assembler necessary for such a soundness proof was introduced in [4]. In this paper i) we observe that for two instructions (that manipulate stack pointers) of the hypervisor code the C + Macro Assembler semantics does not suffice; therefore we extend it to C + Macro Assembler + assembler, ii) we argue the soundness of the methodology from [3] with respect to this new semantics, iii) we apply the methodology from [3] to formally verify the Macro Assembler + assembler portions of the hypervisor from [1], completing the formal verification of the small hypervisor in the automated tool VCC.
Year
DOI
Venue
2012
10.1007/978-3-642-33826-7_13
SEFM
Keywords
Field
DocType
automated c code verifier,c portion,assembler portion,macro assembler semantics,hypervisor code,assembler code verification,macro assembler,automated verification,small hypervisor,macro assembler program,soundness proof,formal verification
Pointer (computer programming),Programming language,Computer science,Correctness,Inline assembler,Hypervisor,Assembly language,Soundness,Macro,Operating system,Formal verification
Conference
Citations 
PageRank 
References 
6
0.54
15
Authors
3
Name
Order
Citations
PageRank
Wolfgang Paul1454.39
Sabine Schmaltz2803.63
Andrey Shadrin3723.35