Trustworthy Systems

Automated verification of a component platform

Authors

Matthew Fernandez, June Andronick, Gerwin Klein and Ihor Kuz

NICTA

UNSW

Abstract

This document outlines various criteria defining the correctness of a component platform, and describes a process for automatic verification of some of these criteria for the CAmkES component platform. Generated proofs are provided for a sample system as an example of the output artefacts and their relationship to both hand written formal reasoning and generated code. Our correctness properties depend upon an interactive theorem prover and some straightforward translation tools. We consider our assumptions and resulting trusted computing base to be acceptable in a high assurance software environment.

This report is an extension to previous reports on the formalisation of the CAmkES component platform and a familiarity with these previous documents is assumed.

BibTeX Entry

  @techreport{Fernandez_AKK_15:tr,
    address          = {Sydney, Australia},
    author           = {Fernandez, Matthew and Andronick, June and Klein, Gerwin and Kuz, Ihor},
    institution      = {NICTA and UNSW},
    issn             = {1833-9646-9034},
    keywords         = {camkes, sel4, autocorres},
    month            = aug,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/9034.pdf},
    title            = {Automated Verification of a Component Platform},
    year             = {2015}
  }

Download