Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
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.
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.
Elkaduwe, Dhammika; Klein, Gerwin; Elphinstone, Kevin: Verified protection model of the seL4 microkernel. Technical report, NICTA, October 2007. Available from http://ertos.nicta.com.au/publica-tions/papers/Elkaduwe_GE_07.pdf
US Information Assurance Directorate: U.S. Government Protection Profile for Separation Kernels in Environments Requiring High Robustness, June 2007. Version 1.03. http://www.niap-ccevs.org/cc-scheme/pp/pp.cfm/id/pp_skpp_hr_v1.03/.
International Standards Organization: Common Criteria for IT Security Evaluation, 1999. ISO Standard 15408. http://csrc.nist.gov/cc/.
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.
Nipkow, Tobias; Paulson, Lawrence; Wenzel, Markus: Isabelle/HOL–a proof assistant for higher-order logic. In Volume 2283 of LNCS. Springer, 2002.
National Security Agency: The Common Criteria evaluation and validation scheme. http://www.niap-ccevs.org/cc-scheme/in evaluation/. Accessed May 2008.
O’Dowd, Dan: Linux security controversy. http://www.ghs.com/linux/unfit.html.AccessedMay2008.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2009 Vieweg+Teubner | GWV Fachverlage GmbH
About this chapter
Cite this chapter
Heiser, G. (2009). Trusted ← Trustworthy ← Proof Position Paper. In: Gawrock, D., Reimer, H., Sadeghi, AR., Vishik, C. (eds) Future of Trust in Computing. Vieweg+Teubner. https://doi.org/10.1007/978-3-8348-9324-6_6
Download citation
DOI: https://doi.org/10.1007/978-3-8348-9324-6_6
Publisher Name: Vieweg+Teubner
Print ISBN: 978-3-8348-0794-6
Online ISBN: 978-3-8348-9324-6
eBook Packages: Computer ScienceComputer Science (R0)