Abstract
Trusted computing relies on formally verified trusted computing platforms to achieve high security assurance. In practice, however, new platforms are often proposed without a comprehensive formal evaluation and explicitly defined underlying assumptions. In this work, we propose TRUSTFOUND, a formal foundation and framework for model checking trusted computing platforms. TRUSTFOUND includes a logic for formally modeling platforms, a model of trusted computing techniques and a broad spectrum of threat models. It can be used to check platforms on security properties (e.g., confidentiality and attestability) and uncover the implicit assumptions that must be satisfied to guarantee the security properties. In our experiments, TRUSTFOUND is used to encode and model check two trusted platforms. It has identified a total of six implicit assumptions and two severe previously-unknown logic flaws from them.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
BitLocker, http://technet.microsoft.com/en-us/library/ee449438%28v=ws.10%29.aspx
TPM Reset Attack, http://www.cs.dartmouth.edu/~pkilab/sparks/
The AVISPA project homepage, http://www.avispa-project.org/
Trusted Boot, http://sourceforge.net/projects/tboot/
Trusted Platform Module (TPM): Built-in Authentication, http://www.trustedcomputinggroup.org/solutions/authentication
TrustFound, http://www.comp.nus.edu.sg/~a0091939/TrustFound/
Abadi, M., Gordon, A.D.: A Calculus for Cryptographic Protocols: The spi Calculus. Information and Computation 148(1), 1–70 (1999)
Ables, K., Ryan, M.D.: Escrowed Data and the Digital Envelope. In: Acquisti, A., Smith, S.W., Sadeghi, A.-R. (eds.) TRUST 2010. LNCS, vol. 6101, pp. 246–256. Springer, Heidelberg (2010)
Berger, S., Cáceres, R., Goldman, K.A., Perez, R., Sailer, R., van Doorn, L.: vTPM: Virtualizing the Trusted Platform Module. In: USENIX Security Symposium (2006)
Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: IEEE Computer Security Foundations Workshop (CSFW) (2001)
Bruschi, D., Cavallaro, L., Lanzi, A., Monga, M.: Replay Attack in TCG Specification and Solution. In: Annual Computer Security Applications Conference (ACSAC) (2005)
Burrows, M., Abadi, M., Needham, R.: A Logic of Authentication. ACM Transactions on Computer Systems 8, 18–36 (1990)
Chen, L., Li, J.: Flexible and Scalable Digital Signatures in TPM 2.0. In: ACM Conference on Computer and Communications Security (CCS) (2013)
Chen, L., Ryan, M.: Offline Dictionary Attack on TCG TPM Weak Authorisation Data, and Solution. In: Future of Trust in Computing (2008)
Cooper, A., Martin, A.: Towards a Secure, Tamper-Proof Grid Platform. In: IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing (CCGRID) (2006)
Datta, A., Franklin, J., Garg, D., Kaynar, D.: A Logic of Secure Systems and Its Application to Trusted Computing. In: IEEE Symposium on Security and Privacy (S&P) (2009)
Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: A Formal Analysis of Authentication in the TPM. In: Degano, P., Etalle, S., Guttman, J. (eds.) FAST 2010. LNCS, vol. 6561, pp. 111–125. Springer, Heidelberg (2011)
Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: Formal Analysis of Protocols Based on TPM State Registers. In: IEEE Computer Security Foundations Symposium (CSF) (2011)
Dolev, D., Yao, A.C.: On the Security of Public Key Protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
T. C. Group. TPM Specification 1.2 (2013), http://www.trustedcomputinggroup.org/resources/tpm_main_specification
T. C. Group. TPM Specification 2.0 (2013), https://www.trustedcomputinggroup.org/resources/tpm_library_specification
Gürgens, S., Rudolph, C., Scheuermann, D., Atts, M., Plaga, R.: Security Evaluation of Scenarios Based on the TCG’s TPM Specification. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 438–453. Springer, Heidelberg (2007)
Hendricks, J., van Doorn, L.: Secure Bootstrap is Not Enough: Shoring Up the Trusted Computing Base. In: ACM SIGOPS European Workshop (2004)
Kauer, B.: OSLO: Improving the Security of Trusted Computing. In: USENIX Security (2007)
Kursawe, K., Schellekens, D., Preneel, B.: Analyzing Trusted Platform Communication. In: ECRYPT Workshop, CRASH-CRyptographic Advances in Secure Hardware (2005)
Mackie, K.: Wave Outlines Windows 8 Mobile Device Management Alternative
McCune, J.M., Parno, B.J., Perrig, A., Reiter, M.K., Isozaki, H.: Flicker: an Execution Infrastructure for TCB Minimization. In: ACM SIGOPS/EuroSys European Conference on Computer Systems (Eurosys) (2008)
Mukhamedov, A., Gordon, A.D., Ryan, M.: Towards a Verified Reference Implementation of a Trusted Platform Module. In: Christianson, B., Malcolm, J.A., Matyáš, V., Roe, M. (eds.) Security Protocols 2009. LNCS, vol. 7028, pp. 69–81. Springer, Heidelberg (2013)
Namiluko, C., Martin, A.: An Abstract Model of a Trusted Platform. In: Chen, L., Yung, M. (eds.) INTRUST 2010. LNCS, vol. 6802, pp. 47–66. Springer, Heidelberg (2011)
Parno, B., Lorch, J.R., Douceur, J.R., Mickens, J., McCune, J.M.: Memoir: Practical State Continuity for Protected Modules. In: IEEE Symposium on Security and Privacy (S&P) (2011)
Sadeghi, A.-R., Selhorst, M., Stüble, C., Wachsmann, C., Winandy, M.: TCG Inside?: A Note on TPM Specification Compliance. In: ACM Workshop on Scalable Trusted Computing (STC) (2006)
Sailer, R., Zhang, X., Jaeger, T., van Doorn, L.: Design and Implementation of a TCG-Based Integrity Measurement Architecture. In: USENIX Security Symposium (2004)
Sparks, E.R.: A Security Assessment of Trusted Platform Modules. Technical Report TR2007-597, Dartmouth College, Computer Science (2007)
Stumpf, F., Tafreschi, O., Röder, P., Eckert, C.: A Robust Integrity Reporting Protocol for Remote Attestation. In: Workshop on Advances in Trusted Computing (WATC) (2006)
Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating Specification and Programs for System Modeling and Verification. In: International Symposium on Theoretical Aspects of Software Engineering (TASE) (2009)
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)
Wojtczuk, R., Rutkowska, J.: Attacking Intel Trusted Execution Technology. In: Black Hat DC (2009)
Wojtczuk, R., Rutkowska, J., Tereshkin, A.: Another Way to Circumvent Intel Trusted Execution Technology. Invisible Things Lab (2009)
Woo, T.Y.C., Lam, S.S.: A Semantic Model for Authentication Protocols. In: IEEE Symposium on Security and Privacy (S&P) (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Bai, G., Hao, J., Wu, J., Liu, Y., Liang, Z., Martin, A. (2014). TrustFound: Towards a Formal Foundation for Model Checking Trusted Computing Platforms. In: Jones, C., Pihlajasaari, P., Sun, J. (eds) FM 2014: Formal Methods. FM 2014. Lecture Notes in Computer Science, vol 8442. Springer, Cham. https://doi.org/10.1007/978-3-319-06410-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-06410-9_8
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06409-3
Online ISBN: 978-3-319-06410-9
eBook Packages: Computer ScienceComputer Science (R0)