Trustworthy Systems

Final report for AOARD grant #FA2386-11-1-4070, formal system verification — extension

Authors

June Andronick, Andrew Boyton and Gerwin Klein

NICTA

UNSW

Abstract

The AOARD project #FA2386-11-1-4070 aims at providing a provably correct initialiser of componentised systems. Taking as input a description of the desired components and the desired authorised communication between them, the initialiser sets up the system and provides a proof that the resulting concrete machine state of the system matches the desired authority state. Within the scope of this project, we provide (1) a formal specification of the initialiser, in terms of the steps needed to create the components and their communication channels; and (2) substantial progress towards a formal proof that this specification is correct in that it either fails safely or produces the desired state. This document is the final report of the project, presenting its scientific outcomes. Namely, we have completed the initialiser specification, we have created a verification framework enabling modular reasoning and proofs about the initialiser, and we have progressed substantially on the proof itself, demonstrating that such proofs are feasible.

BibTeX Entry

  @techreport{Andronick_BK_12:tr,
    address          = {Sydney, Australia},
    author           = {Andronick, June and Boyton, Andrew and Klein, Gerwin},
    institution      = {NICTA},
    issn             = {1833-9646-6408},
    keywords         = {sel4, isabelle/hol, system initialisation},
    month            = oct,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/6408.pdf},
    title            = {Final Report for {AOARD} Grant \#{FA2386}-11-1-4070, Formal System Verification --- Extension},
    year             = {2012}
  }

Download