Formal System Verification - Extension 2
Abstract
The goal of this project is to provide an initial framework prototype for efficient performing formal proofs of targeted security or safety properties about large, complex software systems, which is generic in terms of the targeted property for the system and minimizes the verification effort while providing high-assurance guarantees at the source code level. The framework takes as input the concrete implementation (translated into formal logic) of any system made of a set of components running on top of an OS microkernel. It explicitly identifies and formally states all theorems required for a given property to hold about the system. In particular, it assumes that the system follows the strategy of a formally verified minimal computing base, i.e. that the system is made of a minimal set of trusted components, isolated from untrusted ones by an OS kernel which we can formally reason about.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 08, 2012
- Accession Number
- ADA570949
Entities
People
- Gerwin Klein
- June Andronick
Organizations
- University of New South Wales