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):

• Andronick, June
• Klein, Gerwin

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:

• *COMPUTER PROGRAMS
• *SECURITY
• EFFICIENCY
• INPUT
• LOGIC
• PROTOTYPES
• SAFETY
• STRATEGY
• VERIFICATION

Subject Categories:

• Computer Programming and Software
• Computer Systems Management and Standards

Distribution Statement:

APPROVED FOR PUBLIC RELEASE