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)
Personal Author(s):
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.
Descriptors:
Subject Categories:
- Computer Programming and Software
- Computer Systems Management and Standards