Advertisement

Understanding Attestation: Analyzing Protocols that Use Quotes

  • Joshua D. GuttmanEmail author
  • John D. Ramsdell
Conference paper
  • 144 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11738)

Abstract

Attestation protocols use digital signatures and other cryptographic values to convey evidence of hardware state, program code, and associated keys. They require hardware support such as Trusted Execution Environments. Conclusions about attestations thus depend jointly on protocols, hardware services, and program behavior.

We present a mechanized approach to modeling these properties, combining protocol analysis with axioms, that formalize hardware and software properties. Here, we model aspects of Intel’s SGX mechanism. Above the underlying manufacturer-provided protocols, we build a modular user-level that uses its attestations to make trust decisions.

References

  1. 1.
    Barbosa, M., Portela, B., Scerri, G., Warinschi, B.: Foundations of hardware-based attested computation and application to SGX. In: IEEE EuroS&P, pp. 245–260 (2016)Google Scholar
  2. 2.
    Bhargavan, K., Corin, R., Deniélou, P.-M., Fournet, C., Leifer, J.J.: Cryptographic protocol synthesis and verification for multiparty sessions. In: IEEE Computer Security Foundations Symposium (2009)Google Scholar
  3. 3.
    Bhargavan, K., Corin, R., Fournet, C., Gordon, A.D.: Secure sessions for web services. ACM Trans. Inf. Syst. Secur. 10(2), 8 (2007)CrossRefGoogle Scholar
  4. 4.
    Blanchet, B.: An efficient protocol verifier based on prolog rules. In: IEEE CSFW, pp. 82–96. IEEE CS Press, June 2001Google Scholar
  5. 5.
    Blanchet, B., Pointcheval, D.: Automated security proofs with sequences of games. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol. 4117, pp. 537–554. Springer, Heidelberg (2006).  https://doi.org/10.1007/11818175_32CrossRefGoogle Scholar
  6. 6.
    Brickell, E., Li, J.: Enhanced privacy ID: a direct anonymous attestation scheme with enhanced revocation capabilities. In: ACM Workshop on Privacy in the Electronic Society, pp. 21–30. ACM (2007)Google Scholar
  7. 7.
    Van Bulck, J., et al.: Foreshadow: extracting the keys to the intel SGX kingdom with transient out-of-order execution. In: USENIX Security, pp. 991–1008 (2018)Google Scholar
  8. 8.
    Chadha, R., Cheval, V., Ciobâc, Ş., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log. 17(4), 23:1–23:32 (2016)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Coker, G., et al.: Principles of remote attestation. IJIS 10(2), 63–81 (2011)CrossRefGoogle Scholar
  10. 10.
    Costan, V., Lebedev, I.A., Devadas, S.: Sanctum: minimal hardware extensions for strong software isolation. In: USENIX Security Symposium, pp. 857–874 (2016)Google Scholar
  11. 11.
    Cremers, C., Mauw, S.: Operational Semantics and Verification of Security Protocols. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-540-78636-8CrossRefzbMATHGoogle Scholar
  12. 12.
    Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Trans. Inf. Theory 29, 198–208 (1983)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Dougherty, D.J., Guttman, J.D., Ramsdell, J.D.: Security protocol analysis in context: computing minimal executions using SMT and CPSA. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 130–150. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-98938-9_8CrossRefGoogle Scholar
  14. 14.
    Dyckhoff, R., Negri, S.: Geometrisation of first-order logic. Bull. Symb. Logic 21(2), 123–163 (2015)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-03829-7_1CrossRefzbMATHGoogle Scholar
  16. 16.
    Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization policies. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 141–156. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-31987-0_11CrossRefGoogle Scholar
  17. 17.
    Gollamudi, A., Chong, S.: Automatic enforcement of expressive security policies using enclaves. In: OOPSLA, pp. 494–513 (2016)CrossRefGoogle Scholar
  18. 18.
    Guttman, J.D.: Shapes: surveying crypto protocol runs. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols, Cryptology and Information Security Series. IOS Press (2011)Google Scholar
  19. 19.
    Guttman, J.D.: Establishing and preserving protocol security goals. J. Comput. Secur. 22(2), 201–267 (2014)CrossRefGoogle Scholar
  20. 20.
    Guttman, J.D., Herzog, J.C., Ramsdell, J.D., Sniffen, B.T.: Programming cryptographic protocols. In: De Nicola, R., Sangiorgi, D. (eds.) TGC 2005. LNCS, vol. 3705, pp. 116–145. Springer, Heidelberg (2005).  https://doi.org/10.1007/11580850_8CrossRefGoogle Scholar
  21. 21.
    Guttman, J.D., Ramsdell, J.D.: CPSA inputs for understanding attestation, April 2019. https://web.cs.wpi.edu/~guttman/pubs/understanding_attestation_example/
  22. 22.
    Intel. Intel® Software Guard Extensions (Intel® SGX) (2016). https://software.intel.com/en-us/sgx
  23. 23.
    Intel. Intel® Software Guard Extensions (Intel® SGX) data center attestation primitives: ECDSA quote library API, November 2018. https://download.01.org/intel-sgx/dcap-1.0.1/docs/Intel_SGX_ECDSA_QuoteGenReference_DCAP_API_Linux_1.0.1.pdf
  24. 24.
    Kaplan, D., Powell, J., Woller, T.: AMD memory encryption, April 2016. https://developer.amd.com/wordpress/media/2013/12/AMD_Memory_Encryption_Whitepaper_v7-Public.pdf
  25. 25.
    Kremer, S., Künnemann, R.: Automated analysis of security protocols with global state. J. Comput. Secur. 24(5), 583–616 (2016)CrossRefGoogle Scholar
  26. 26.
    Lampson, B., Abadi, M., Burrows, M., Wobber, E.: Authentication in distributed systems: theory and practice. ACM Trans. Comput. Syst. 10(4), 265–310 (1992)CrossRefGoogle Scholar
  27. 27.
    Li, N., Mitchell, J.C., Winsborough, W.H.: Design of a role-based trust management framework. In: Proceedings, 2002 IEEE Symposium on Security and Privacy, pp. 114–130. IEEE CS Press, May 2002Google Scholar
  28. 28.
    Liskov, M.D., Guttman, J.D., Ramsdell, J.D., Rowe, P.D., Thayer, F.J.: Enrich-by-need protocol analysis for Diffie-Hellman. In: Guttman, J.D., Landwehr, C.E., Meseguer, J., Pavlovic, D. (eds.) Foundations of Security, Protocols, and Equational Reasoning. LNCS, vol. 11565, pp. 135–155. Springer, Cham (2019).  https://doi.org/10.1007/978-3-030-19052-1_10CrossRefGoogle Scholar
  29. 29.
    Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_48CrossRefGoogle Scholar
  30. 30.
    Murray, T., van Oorschot, P.C.: Formal proofs, the fine print and side effects. In: IEEE SecDev, September 2018Google Scholar
  31. 31.
    Noorman, J., et al.: Sancus 2.0: a low-cost security architecture for IoT devices. ACM Trans. Priv. Secur. 20(3), 7:1–7:33 (2017)CrossRefGoogle Scholar
  32. 32.
    Ramsdell, J.D., Guttman, J.D.: CPSA4: a cryptographic protocol shapes analyzer with geometric rules. The MITRE Corporation (2018). https://github.com/ramsdell/cpsa
  33. 33.
    Ramsdell, J.D., Guttman, J.D., Liskov, M.: CPSA: A cryptographic protocol shapes analyzer (2016). http://hackage.haskell.org/package/cpsa
  34. 34.
    Rescorla, E., Ray, M., Dispensa, S., Oskov, N.: Transport Layer Security (TLS) Renegotiation Indication Extension. RFC 5746 (Proposed Standard) (2010)Google Scholar
  35. 35.
    Rowe, P.D., Guttman, J.D., Liskov, M.D.: Measuring protocol strength with security goals. Int. J. Inf. Secur. (2016).  https://doi.org/10.1007/s10207-016-0319-z. http://web.cs.wpi.edu/~guttman/pubs/ijis_measuring-security.pdfCrossRefGoogle Scholar
  36. 36.
    Saghafi, S., Danas, R., Dougherty, D.J.: Exploring theories with a model-finding assistant. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 434–449. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21401-6_30CrossRefGoogle Scholar
  37. 37.
    Schuster, F., et al.: VC3: trustworthy data analytics in the cloud using SGX. In: 2015 IEEE S&P, pp. 38–54 (2015)Google Scholar
  38. 38.
    Sinha, R., et al.: A design and verification methodology for secure isolated regions. In: PLDI (2016)Google Scholar
  39. 39.
    Sinha, R., Rajamani, S., Seshia, S., Vaswani, K.: Moat: verifying confidentiality of enclave programs. In: ACM CCS, Moat (2015)Google Scholar
  40. 40.
    Subramanyan, P., Sinha, R., Lebedev, I.A. Devadas, S., Seshia, S.A.: A formal foundation for secure remote execution of enclaves. In: ACM CCS (2017)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.The MITRE CorporationBedfordUSA

Personalised recommendations