Skip to main content


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


June Andronick, Gerwin Klein and Toby Murray




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

    author           = {Andronick, June and Klein, Gerwin and Murray, Toby},
    issn             = {1833-9646-5617},
    month            = nov,
    year             = {2011},
    title            = {Formal System Verification for Trustworthy Embedded Systems, Final Report Option 1 --- {AOARD}
    institution      = {NICTA},
    address          = {Sydney, Australia}