Whole-system assurance

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

• 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:
  

  • 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;
  • 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

Publications

		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
		June Andronick and Gerwin Klein Formal system verification — extension 2, final report AOARD #FA2386-12-1-4022 Technical Report, NICTA, August, 2012
		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