Trustworthy Systems

Formal system verification for trustworthy embedded systems, final report for AOARD grant #FA2386-10-1-4105

Authors

June Andronick, Gerwin Klein and Toby Murray

NICTA

UNSW

Abstract

The aim of AOARD project #FA2386-10-1-4105 is to investigate the creation of a framework enabling the formal verification of trustworthy embedded systems, leading to formal guarantees, holding at the source code level, about the security of large, complex systems. The key to make formal verification scale to systems consisting of million lines of code lies in minimising the verification effort by combining proofs of various components of the system in a provably correct way, and by concentrating effort on trusted components. This approach is enabled by designing trustworthy systems as componentised systems running on a small, verified microkernel such as seL4.

The project, running for 27 months from 16 June 2010 to 15 September 2012, consisted of three phases: • Base, running for 8 months from 16 June 2010 to 15 February 2011; • Option 1, running for 7 months, from 16 February 2011 to 15 September 2011; and • Option 2, running for 12 months, from 16 September 2011 to 15 September 2012.

In the Base phase, we identified three main research areas required to achieve the end objective, namely: (a) proving component isolation, (b) proving trusted components correctness, and (c) proving the correctness of the whole-system semantics. In this phase, we also made significant progress in the isolation proof by showing that the seL4 kernel enforces integrity. We also worked on trusted components correctness by providing an intermediate design specification for a case-study trusted component. In the second phase (Option 1), we worked on the definition of the whole system semantics, by developing an informal, yet detailed plan for achieving the decomposition of the overall theorem into proofs about the various part of the kernel-based, componentised system.

In the last phase (Option 2), we addressed the dual property of integrity for component isolation, that is confidentiality. We proved confidentiality enforcement for about 98% of seL4, and explain why the remaining functions will require some changes in seL4. In this last phase, we also formalised our plan for overall system proofs in an common, initial framework in the Isabelle/HOL [15] theorem prover. This work was in part additionally funded by the AOARD extension grant #FA2386-12-1- 4022 [4]. The formal framework we developed 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 kernel. It explicitly identifies and formally states all theorems required for a given property to hold about the system. It then combines, in a provably correct way, these proofs to provide a formal proof that the property holds at the source code level of the whole system.

BibTeX Entry

  @techreport{Andronick_KM_12:tr,
    address          = {Sydney, Australia},
    author           = {Andronick, June and Klein, Gerwin and Murray, Toby},
    institution      = {NICTA},
    issn             = {1833-9646-6324},
    keywords         = {aoard, isabelle/hol, trustworthy systems},
    month            = oct,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/6324.pdf},
    title            = {Formal System Verification for Trustworthy Embedded Systems, Final Report for {AOARD} Grant
                        \#{FA2386}-10-1-4105},
    year             = {2012}
  }

Download