This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
It's Time for Trustworthy Systems
March/April 2012 (vol. 10 no. 2)
pp. 67-70
ASCII Text
x 
 
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.
 
 
BibTex
x
 
@article{ 10.1109/MSP.2012.41,
author = {Gernot Heiser and Toby Murray and Gerwin Klein},
title = {It's Time for Trustworthy Systems},
journal ={IEEE Security & Privacy},
volume = {10},
number = {2},
issn = {1540-7993},
year = {2012},
pages = {67-70},
doi = {http://doi.ieeecomputersociety.org/10.1109/MSP.2012.41},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - MGZN
JO - IEEE Security & Privacy
TI - It's Time for Trustworthy Systems
IS - 2
SN - 1540-7993
SP67
EP70
EPD - 67-70
A1 - Gernot Heiser,
A1 - Toby Murray,
A1 - Gerwin Klein,
PY - 2012
KW - trustworthy systems
KW - verification and analysis
KW - seL4 microkernel
KW - integrity
KW - confidentiality
KW - worst-case execution time
KW - safety
KW - security
KW - computer security
KW - functional correctness
KW - authority confinement
KW - noninterference
VL - 10
JA - IEEE Security & Privacy
ER -
 
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; http://static.usenix.org/events/ssv10/tech/ 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; www.ssrg.nicta.com.au/publications/papers 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
Citation:
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.