Trustworthy Systems

Formal system verification for trustworthy embedded systems, final report option 1 — AOARD 104105

Authors

June Andronick, Gerwin Klein and Toby Murray

NICTA

UNSW

Abstract

This report summarises the work done in Option 1 of AOARD project 104105, Formal System Verification for Trustworthy Embedded Systems. It describes the progress made in formalising a general framework that allows us to prove invariant properties about a system consisting of a microkernel, user-level trusted components, and user-level untrusted components. It explains how the different parts of this framework would be put together to obtain invariant properties of system execution, reducing the necessary reasoning about system composition, kernel access control, and trusted component behaviour.

BibTeX Entry

  @techreport{Andronick_KM_11:tr,
    address          = {Sydney, Australia},
    author           = {Andronick, June and Klein, Gerwin and Murray, Toby},
    institution      = {NICTA},
    issn             = {1833-9646-5617},
    month            = nov,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/5617.pdf},
    title            = {Formal System Verification for Trustworthy Embedded Systems, Final Report Option 1 --- {AOARD}
                        104105},
    year             = {2011}
  }

Download