Trusted ← Trustworthy ← Proof Position Paper

  • Gernot Heiser


Trusted computing is important, but we argue that it remains an illusion as long as the underlying trusted computing base (TCB) is not trustworthy. We observe that present approaches to trusted computing do not really address this issue, but are trusting TCBs which have not been shown to deserve this trust. We argue that only mathematical proof can ensure the trustworthiness of the TCB. In short: trust requires trustworthiness, which in turn requires proof. We also show that this is achievable.


Trust Platform Module Trust Computing Base High Evaluation Level Pruh WKDQ Formal Formal Formal 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Alves-Foss, Jim; Oman, Paul W.; Taylor, Carol; Harrison, Scott: The MILS architecture for high-assurance embedded systems. In International Journal on Embedded Systems, 2:239247, 2006.Google Scholar
  2. Cock, David; Klein, Gerwin; Sewell, Thomas: Secure microkernels, state monads and scalable refinement. In Otmane Ait Mohamed, Cesar Munoz and Sofiène Tahar, editors, Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs’08), volume 5170 of Lecture Notes in Computer Science. Springer, 2008.Google Scholar
  3. Elkaduwe, Dhammika; Klein, Gerwin; Elphinstone, Kevin: Verified protection model of the seL4 microkernel. Technical report, NICTA, October 2007. Available from
  4. US Information Assurance Directorate: U.S. Government Protection Profile for Separation Kernels in Environments Requiring High Robustness, June 2007. Version 1.03.
  5. International Standards Organization: Common Criteria for IT Security Evaluation, 1999. ISO Standard 15408.
  6. Liedtke, Jochen; Elphinstone, Kevin; Schönberg, Sebastian; Härtig, Herrman; Heiser, Gemot; Islam, Nayeem; Jaeger, Trent: Achieved IPC performance (still the foundation for extensibility). In Proceedings of the 6th Workshop on Hot Topics in Operating Systems, pages 28–31, Cape Cod, MA, USA, May 1997.Google Scholar
  7. Nipkow, Tobias; Paulson, Lawrence; Wenzel, Markus: Isabelle/HOL–a proof assistant for higher-order logic. In Volume 2283 of LNCS. Springer, 2002.Google Scholar
  8. National Security Agency: The Common Criteria evaluation and validation scheme. evaluation/. Accessed May 2008.
  9. O’Dowd, Dan: Linux security controversy.

Copyright information

© Vieweg+Teubner | GWV Fachverlage GmbH 2009

Authors and Affiliations

  • Gernot Heiser
    • 1
  1. 1.Open Kernel Labs and NICTA and University of New South WalesSydneyAustralia

Personalised recommendations