DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click
HERE to register or log in.
Accession Number:
ADA570949
Title:
Formal System Verification - Extension 2
Descriptive Note:
Final rept. 8 Jan 2011-8 Aug 2012
Corporate Author:
NEW SOUTH WALES UNIV SYDNEY (AUSTRALIA)
Report Date:
2012-08-08
Pagination or Media Count:
28.0
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.
Distribution Statement:
APPROVED FOR PUBLIC RELEASE