Name
Abstract | ||
|---|---|---|
We extend the existing formal verification of the seL4 operating system microkernel from 9500 lines of C source code to the binary level. We handle all functions that were part of the previous verification. Like the original verification, we currently omit the assembly routines and volatile accesses used to control system hardware. More generally, we present an approach for proving refinement between the formal semantics of a program on the C source level and its formal semantics on the binary level, thus checking the validity of compilation, including some optimisations, and linking, and extending static properties proved of the source code to the executable. We make use of recent improvements in SMT solvers to almost fully automate this process. We handle binaries generated by unmodified gcc 4.5.1 at optimisation level 1, and can handle most of seL4 even at optimisation level 2. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1145/2491956.2462183 | PLDI |
Keywords | Field | DocType |
previous verification,optimisation level,os kernel,translation validation,c source level,original verification,source code,sel4 operating system microkernel,binary level,existing formal verification,c source code,formal semantics,verification | Programming language,Source code,Computer science,Parallel computing,Microkernel,Real-time computing,Os kernel,Control system,High-level verification,Binary number,Executable,Formal verification | Conference |
Volume | Issue | ISSN |
48 | 6 | 0362-1340 |
Citations | PageRank | References |
41 | 1.26 | 28 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thomas Sewell | 1 | 914 | 37.60 |
| Magnus O. Myreen | 2 | 621 | 35.67 |
| Gerwin Klein | 3 | 1450 | 87.47 |