A Bottom-Up Verification Approach for Systems Software
Abstract
We propose to develop a bottom-up verification methodology for verifying systems software at the assembly code level,by relying on a shallow embedding of the denotational semantics of the C programming language and using an algebra process-like refinement for the program under verification. Our approach involves manually encoding, in higher order logic, a behavioral specification of the target program, which also contains a shallow embedding of a formallanguage that describes the denotational semantics of the C language. We propose to develop a translator that takes the program in assembly code, as well as the formal language as inputs, and embeds the code in the formal language. In addition, the translator willautomatically produce an abstraction of the embedded code, and generate proofs showing that this generatedabstraction is an instantiation of the behavioral system specification. To increase the trust on program s execution semantics and its execution environment, we propose to conduct formal testing: behavioral refinement rules and symbolic execution calculi based on deductive proofs will be used to systematically generate a test set. The target program is executed on the test cases to establish a conformance relationship between the program and the verifiedfunctional specification.Our verification methodology will be folded into a tool-chain infrastructure and integrated into the Isabelle/HOL theoremprover, and will be demonstrated by verifying a select subset of the Linux Memory Manager.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Mar 03, 2017
- Source ID
- N000141712297
Entities
People
- Binoy Ravindran
Organizations
- Office of Naval Research
- United States Navy
- Virginia Tech