This Article 
 Bibliographic References 
 Add to: 
It's Time for Trustworthy Systems
March/April 2012 (vol. 10 no. 2)
pp. 67-70
Toby Murray, NICTA
Gerwin Klein, NICTA
The time has arrived for truly trustworthy systems, backed by machine-checked proofs of security and reliability. Research demonstrates that formal whole-system analysis that applies to the C and binary implementation level is feasible, including proofs of integrity, authority confinement, confidentiality, and worst-case execution time. Because these proofs build on previous results, they become easier each year. However, they do have some limitations.

1. G. Klein et al., "seL4: Formal Verification of an Operating System Kernel," Comm. ACM, vol. 53, no. 6, 2010, pp. 107–115.
2. J. Andronick, D. Greenaway, and K. Elphinstone, "Towards Proving Security in the Presence of Large Untrusted Components," Proc. 5th Int'l Workshop Systems Software Verification, Usenix Assoc., 2010; full_papersAndronick.pdf.
3. T. Sewell et al., "seL4 Enforces Integrity," Proc. 2nd Int'l Conf. Interactive Theorem Proving, LNCS 6898, Springer, 2011, pp. 325–340.
4. B. Blackham, Y. Shi, and G. Heiser, "Improving Interrupt Response Time in a Verifiable Protected Microkernel," Proc. 7th EuroSys Conf., 2012; Blackham_SH_12.pdf.

Index Terms:
trustworthy systems, verification and analysis, seL4 microkernel, integrity, confidentiality, worst-case execution time, safety, security, computer security, functional correctness, authority confinement, noninterference
Gernot Heiser, Toby Murray, Gerwin Klein, "It's Time for Trustworthy Systems," IEEE Security & Privacy, vol. 10, no. 2, pp. 67-70, March-April 2012, doi:10.1109/MSP.2012.41
Usage of this product signifies your acceptance of the Terms of Use.