Skip to main content

Whole-system assurance

Whole-system assurance

Whole-system assurance is one activity of the Trustworthy Systems project.

Kernel-based, componentised system
  • Aim: formal proof, holding at the source code level, of a system comprising million LoC.

  • Scope:

    • The "system" is a kernel-based, componentised system, with minimal set of trusted components
    • The "property" is an invariant that needs to be preserved at each execution step
    • The kernel has a proof of functional correctness , enabling verification at an abstract level
    • The kernel has a proof of access control , isolating untrusted code
  • Approach: Execution automaton

    • Automatically decompose the proof;
    • Invoke the kernel's access control proof to avoid verifying untrusted code;
    • Invoke the kernel's functional correctness proof, to carry most of the reasoning at an abstract level; Framework
    • Require a minimal set of system-specific, one-time-off proofs.
  • Status:

    • generic framework formalised in Isabelle/HOL, and instantiated to seL4's specific proofs of functional correctness and access control.
    • modelling of trusted user code linked to low-level ARM model of execution.
    • successful instantiation to very simple systems of 2 components with restricted communication between them.
  • Ongoing work:

    • intantiation to more complex system, as a seL4-based multi-level terminal.
    • explore links with proving whole-system information flow properties.
  • Contact: June Andronick , june.andronick<at>nicta.com.au

People

Current

Past

  • Andrew Skelton
  • David Greenaway
  • Dean Garden
  • Matthew Brassil
  • Matthew Fernandez
  • Nelson Billing

Publications

Abstract PDF June Andronick, Gerwin Klein and Toby Murray
Formal system verification for trustworthy embedded systems, final report for AOARD grant #FA2386-10-1-4105
Technical Report, NICTA, October, 2012
Abstract PDF June Andronick and Gerwin Klein
Formal system verification - extension 2, final report AOARD #FA2386-12-1-4022
Technical Report, NICTA, August, 2012
Abstract PDF June Andronick, Gerwin Klein and Toby Murray
Formal system verification for trustworthy embedded systems, final report option 1 – AOARD 104105
Technical Report, NICTA, November, 2011