Trustworthy Systems

Formal system verification — extension 2, final report AOARD #FA2386-12-1-4022

Authors

June Andronick and Gerwin Klein

NICTA

UNSW

Abstract

The aim of AOARD project #FA2386-12-1-4022 (“Formal System Verification - Extension 2”, running from 9 February 2012 to 8 August 2012) is to provide an initial framework prototype for efficiently performing formal proofs of targeted security or safety properties about large, complex software systems. The framework is meant to be generic in terms of the targeted property for the system and to minimise the verification effort while providing high-assurance guarantees at the source code level.

This document is the final report of the project, presenting our initial framework, formalised in the theorem prover Isabelle/HOL [7]. 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. The framework explicitly identifies and formally states all theorems required for a given property to hold about the system. In particular, the framework 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. The framework therefore requires as input a proof of the kernel’s correctness and isolation properties, and a proof that the trusted components satisfy the targeted property. The former proof can be performed once for any system built on a given kernel. The latter proof is specific to the system and its trusted components’ behaviour and must be provided for each instance. The framework then combines these proofs to provide a formal proof that the property holds at the source code level of the whole system.

BibTeX Entry

  @techreport{Andronick_Klein_12:tr,
    address          = {Sydney, Australia},
    author           = {Andronick, June and Klein, Gerwin},
    institution      = {NICTA},
    issn             = {1833-9646-6302},
    keywords         = {isabelle/hol, trustworthy systems},
    month            = aug,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/6302.pdf},
    title            = {Formal System Verification --- Extension 2, Final Report {AOARD} \#{FA2386}-12-1-4022},
    year             = {2012}
  }

Download