Trustworthy Systems

Formal system verification for trustworthy embedded systems, final report AOARD 094160

Authors

June Andronick and Gerwin Klein

NICTA

UNSW

Abstract

This report summarises the work done in AOARD project 094160, Formal System Verification for Trustworthy Embedded Systems. We begin by revisiting the original motivation and work plan, which is of a verification framework that allows us to combine proofs from different levels of abstraction into one final, verifiable formal statement. We then present a high-level summary of the project outcomes: a fully formal, high-level architecture specification of a case study system; a formal behaviour specification of the main trusted component in the case study system; a high-level interleaving semantics for the execution of the whole system; and a formal security proof of the case study system, that examines all possible executions of the high-level system.

BibTeX Entry

  @techreport{Andronick_Klein_11:tr,
    address          = {Sydney, Australia},
    author           = {Andronick, June and Klein, Gerwin},
    institution      = {NICTA},
    issn             = {1833-9646-5614},
    month            = apr,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/5614.pdf},
    title            = {Formal System Verification for Trustworthy Embedded Systems, Final Report {AOARD} 094160},
    year             = {2011}
  }

Download