Paper Info
Title
Integrated semantics of intermediate-language c and macro-assembler for pervasive formal verification of operating systems and hypervisors from VerisoftXT
Abstract
Pervasive formal verification of operating systems and hypervisors is, due to their safety-critical aspects, a highly relevant area of research. Many implementations consist of both assembler and C functions. Formal verification of their correctness must consider the correct interaction of code written in these languages, which is, in practice, ensured by using matching application binary interfaces (ABIs). Also, these programs must be able to interact with hardware. We present an integrated operational small-step semantics model of intermediate-language C and Macro-Assembler code execution for pervasive operating systems and hypervisor verification. Our semantics is based on a compiler calling convention that defines callee- and caller-save registers. We sketch a theory connecting this semantic layer with an ISA-model executing the compiled code for use in a pervasive verification context. This forms a basis for soundness proofs of tools used in the VerisoftXT project and is a crucial step towards arguing formal correctness of execution of the verified code on a gate-level hardware model.
Year
DOI
Venue
2012
10.1007/978-3-642-27705-4_3
VSTTE
Keywords
Field
DocType
c function,macro-assembler code execution,pervasive verification context,pervasive formal verification,pervasive operating system,integrated semantics,formal correctness,gate-level hardware model,intermediate-language c,integrated operational small-step semantics,hypervisor verification,formal verification
Programming language,Computer science,Correctness,Theoretical computer science,Compiler,Assembly language,Compiled language,Calling convention,Soundness,Macro,Operating system,Formal verification
Conference
Volume
ISSN
Citations 
7152
0302-9743
2
PageRank 
References 
Authors
0.39
11
2
Name
Order
Citations
PageRank
Sabine Schmaltz1803.63
Andrey Shadrin2723.35