ABI-aware verification for system-level software
|
Supervisor |
|
|
Suitable for |
Abstract
Software model checkers, such as CBMC and SatAbs (created by Daniel Kroening, and maintained by the Formal Verification group at Oxford) are typically written according to a programming language standard, e.g. the ANSI standard for C. However, low-level systems software often relies on platform-specific features that are not part of the compiler, but are guaranteed by a particular compiler for a given target architecture. Examples include the size and alignment of data-types, layout of stack-frames, layout of structures, order of evaluation of function arguments, and endianness. Details of these features are left up to the compiler, and form the "application binary interface" (ABI) of the compiler. An ABI-agnostic model checker must not make assumptions about such non-standard features, representing program execution at an abstract level catering for all possible implementations. While this is desirable for high-level software, it renders much system-level software "un-verifiable". This type of software does depend on specific ABI features: if these features are not assumed, a model checker will produce bug reports that are spurious, in the sense that they would not actually occur on the target architecture of interest, assuming code had been compiled with the appropriate compiler. The project would remedy this program by parameterising the model checker by a given compiler, such that the compiler is queried whenever ABI-specific information is required. A concrete implementation of this would be produced for CBMC and/or SatAbs. The resulting ABI-aware model checker would then be applied to a range of examples, including device-drivers, source code for the Cell BE processor, and source code for the SPIN model checker. The project's outcome would make these previously elusive, yet important, applications amenable to verification by model checking.Background needed: This project would suit a student with an interest in low-level issues related to memory layout. Strong programming skills and basic knowledge of model checking techniques would be desirable.