nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Formal Abstractions for Attested Execution Secure Processors

verfasst von : Rafael Pass, Elaine Shi, Florian Tramèr

Erschienen in: Advances in Cryptology – EUROCRYPT 2017

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Realistic secure processors, including those built for academic and commercial purposes, commonly realize an “attested execution” abstraction. Despite being the de facto standard for modern secure processors, the “attested execution” abstraction has not received adequate formal treatment. We provide formal abstractions for “attested execution” secure processors and rigorously explore its expressive power. Our explorations show both the expected and the surprising.

On one hand, we show that just like the common belief, attested execution is extremely powerful, and allows one to realize powerful cryptographic abstractions such as stateful obfuscation whose existence is otherwise impossible even when assuming virtual blackbox obfuscation and stateless hardware tokens. On the other hand, we show that surprisingly, realizing composable two-party computation with attested execution processors is not as straightforward as one might anticipate. Specifically, only when both parties are equipped with a secure processor can we realize composable two-party computation. If one of the parties does not have a secure processor, we show that composable two-party computation is impossible. In practice, however, it would be desirable to allow multiple legacy clients (without secure processors) to leverage a server’s secure processor to perform a multi-party computation task. We show how to introduce minimal additional setup assumptions to enable this. Finally, we show that fair multi-party computation for general functionalities is impossible if secure processors do not have trusted clocks. When secure processors have trusted clocks, we can realize fair two-party computation if both parties are equipped with a secure processor; but if only one party has a secure processor (with a trusted clock), then fairness is still impossible for general functionalities.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Improved Private Set Intersection Against Malicious Adversaries

Nächstes Kapitel One-Shot Verifiable Encryption from Lattices

Trusted computing group. http://www.trustedcomputinggroup.org/

Abadi, M., Jürjens, J.: Formal eavesdropping and its computational interpretation. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 82–94. Springer, Heidelberg (2001). doi:10.1007/3-540-45500-0_4 CrossRef

Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptol. 20(3), 395 (2007)CrossRefMATH

Adão, P., Bana, G., Herzog, J., Scedrov, A.: Soundness of formal encryption in the presence of key-cycles. In: Vimercati, S.C., Syverson, P., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 374–396. Springer, Heidelberg (2005). doi:10.1007/11555827_22 CrossRef

Alves, T., Felton, D.: Trustzone: integrated hardware and software security. Inf. Q. 3(4), 18–24 (2004)

Anati, I., Gueron, S., Johnson, S.P., Scarlata, V.R.: Innovative technology for CPU based attestation and sealing. In: HASP (2013)

ARM Limited: ARM Security Technology Building a Secure System using TrustZone\(\textregistered \) Technology, April 2009. Reference no. PRD29-GENC-009492C

Asharov, G., Beimel, A., Makriyannis, N., Omri, E.: Complete characterization of fairness in secure two-party computation of Boolean functions. In: Dodis, Y., Nielsen, J.B. (eds.) TCC 2015. LNCS, vol. 9014, pp. 199–228. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46494-6_10

Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library. IACR Cryptology ePrint Archive, 2003:15 (2003)

10.

Barbosa, M., Portela, B., Scerri, G., Warinschi, B.: Foundations of hardware-based attested computation and application to SGX. In: IEEE European Symposium on Security and Privacy, pp. 245–260 (2016)

11.

Baumann, A., Peinado, M., Hunt, G.: Shielding applications from an untrusted cloud with haven. In: OSDI (2014)

12.

Berger, S., Cáceres, R., Goldman, K.A., Perez, R., Sailer, R., van Doorn, L.: vTPM: virtualizing the trusted platform module. In: USENIX Security (2006)

13.

Bohl, F., Unruh, D.: Symbolic universal composability. In: IEEE Computer Security Foundations Symposium, pp. 257–271 (2013)

14.

Boneh, D., Naor, M.: Timed commitments. In: Bellare, M. (ed.) CRYPTO 2000. LNCS, vol. 1880, pp. 236–254. Springer, Heidelberg (2000). doi:10.1007/3-540-44598-6_15 CrossRef

15.

Brickell, E., Camenisch, J., Chen, L.: Direct anonymous attestation. In: CCS (2004)

16.

Brickell, E., Li, J.: Enhanced privacy id from bilinear pairing. IACR Cryptology ePrint Archive, 2009:95 (2009)

17.

Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: FOCS (2001)

18.

Canetti, R., Dodis, Y., Pass, R., Walfish, S.: Universally composable security with global setup. In: Vadhan, S.P. (ed.) TCC 2007. LNCS, vol. 4392, pp. 61–85. Springer, Heidelberg (2007). doi:10.1007/978-3-540-70936-7_4 CrossRef

19.

Canetti, R., Fischlin, M.: Universally composable commitments. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol. 2139, pp. 19–40. Springer, Heidelberg (2001). doi:10.1007/3-540-44647-8_2 CrossRef

20.

Canetti, R., Herzog, J.: Universally composable symbolic security analysis. J. Cryptol. 24(1), 83–147 (2011)MathSciNetCrossRefMATH

21.

Canetti, R., Rabin, T.: Universal composition with joint state. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 265–281. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45146-4_16 CrossRef

22.

Champagne, D., Lee, R.B.: Scalable architectural support for trusted software. In: HPCA (2010)

23.

Chen, C., Raj, H., Saroiu, S., Wolman, A.: cTPM: a cloud TPM for cross-device trusted applications. In: NSDI (2014)

24.

Chung, K.-M., Katz, J., Zhou, H.-S.: Functional encryption from (small) hardware tokens. In: Sako, K., Sarkar, P. (eds.) ASIACRYPT 2013. LNCS, vol. 8270, pp. 120–139. Springer, Heidelberg (2013). doi:10.1007/978-3-642-42045-0_7 CrossRef

25.

Cleve, R.: Limits on the security of coin flips when half the processors are faulty. In: STOC 1986, pp. 364–369 (1986)

26.

Costan, V., Devadas, S.: Intel SGX explained. Manuscript (2015)

27.

Costan, V., Lebedev, I., Devadas, S.: Sanctum: minimal hardware extensions for strong software isolation. In: USENIX Security (2016)

28.

Dinh, T.T.A., Saxena, P., Chang, E.-C., Ooi, B.C., Zhang, C.: M2R: enabling stronger privacy in MapReduce computation. In: USENIX Security (2015)

29.

Döttling, N., Mie, T., Müller-Quade, J., Nilges, T.: Basing obfuscation on simple tamper-proof hardware assumptions. IACR Cryptology ePrint Archive 2011:675 (2011)

30.

Even, S., Goldreich, O., Lempel, A.: A randomized protocol for signing contracts. Commun. ACM 28(6), 637–647 (1985)MathSciNetCrossRefMATH

31.

Ferraiuolo, A., Wang, Y., Rui, X., Zhang, D., Myers, A., Edward, G.S.: Full-processor timing channel protection with applications to secure hardware compartments (2015)

32.

Fletcher, C.W., van Dijk, M., Devadas, S.: A secure processor architecture for encrypted computation on untrusted programs. In: STC (2012)

33.

Fletcher, C.W., Ren, L., Kwon, A., van Dijk, M., Stefanov, E., Devadas, S.: RAW Path ORAM: a low-latency, low-area hardware ORAM controller with integrity verification. IACR Cryptology ePrint Archive 2014:431 (2014)

34.

Fletcher, C.W., Ren, L., Xiangyao, Y., van Dijk, M., Khan, O., Devadas, S.: Suppressing the oblivious RAM timing channel while making information leakage and program efficiency trade-offs. In: HPCA, pp. 213–224 (2014)

35.

Garay, J., MacKenzie, P., Prabhakaran, M., Yang, K.: Resource fairness and composability of cryptographic protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 404–428. Springer, Heidelberg (2006). doi:10.1007/11681878_21 CrossRef

36.

Genkin, D., Pachmanov, L., Pipman, I., Shamir, A., Tromer, E.: Physical key extraction attacks on PCs. Commun. ACM 59(6), 70–79 (2016)CrossRefMATH

37.

Goldwasser, S., Kalai, Y.T., Rothblum, G.N.: One-time programs. In: Wagner, D. (ed.) CRYPTO 2008. LNCS, vol. 5157, pp. 39–56. Springer, Heidelberg (2008). doi:10.1007/978-3-540-85174-5_3 CrossRef

38.

Dov Gordon, S., Katz, J.: Complete fairness in multi-party computation without an honest majority. In: Reingold, O. (ed.) TCC 2009. LNCS, vol. 5444, pp. 19–35. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00457-5_2 CrossRef

39.

Dov Gordon, S., Hazay, C., Katz, J., Lindell, Y.: Complete fairness in secure two-party computation. J. ACM 58(6), 24:1–24:37 (2011)MathSciNetMATH

40.

Goyal, V., Ishai, Y., Sahai, A., Venkatesan, R., Wadia, A.: Founding cryptography on tamper-proof hardware tokens. In: Micciancio, D. (ed.) TCC 2010. LNCS, vol. 5978, pp. 308–326. Springer, Heidelberg (2010). doi:10.1007/978-3-642-11799-2_19 CrossRef

41.

Gupta, D., Mood, B., Feigenbaum, J., Butler, K., Traynor, P.: Using intel software guard extensions for efficient two-party secure function evaluation. In: Clark, J., Meiklejohn, S., Ryan, P.Y.A., Wallach, D., Brenner, M., Rohloff, K. (eds.) FC 2016. LNCS, vol. 9604, pp. 302–318. Springer, Heidelberg (2016). doi:10.1007/978-3-662-53357-4_20 CrossRef

42.

Hazay, C., Polychroniadou, A., Venkitasubramaniam, M.: Composable security in the tamper-proof hardware model under minimal complexity. In: Hirt, M., Smith, A. (eds.) TCC 2016. LNCS, vol. 9985, pp. 367–399. Springer, Heidelberg (2016). doi:10.1007/978-3-662-53641-4_15 CrossRef

43.

Horvitz, O., Gligor, V.: Weak key authenticity and the computational completeness of formal encryption. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 530–547. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45146-4_31 CrossRef

44.

Janvier, R., Lakhnech, Y., Mazaré, L.: Completing the picture: soundness of formal encryption in the presence of active adversaries. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 172–185. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31987-0_13 CrossRef

45.

Katz, J.: Universally composable multi-party computation using tamper-proof hardware. In: Naor, M. (ed.) EUROCRYPT 2007. LNCS, vol. 4515, pp. 115–128. Springer, Heidelberg (2007). doi:10.1007/978-3-540-72540-4_7 CrossRef

46.

Kauer, B.: TPM reset attack. http://www.cs.dartmouth.edu/~pkilab/sparks/

47.

Kocher, P., Jaffe, J., Jun, B.: Differential power analysis. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 388–397. Springer, Heidelberg (1999). doi:10.1007/3-540-48405-1_25 CrossRef

48.

Lie, D., Thekkath, C., Mitchell, M., Lincoln, P., Boneh, D., Mitchell, J., Horowitz, M.: Architectural support for copy and tamper resistant software. ACM SIGPLAN Not. 35(11), 168–177 (2000)CrossRef

49.

Maas, M., Love, E., Stefanov, E., Tiwari, M., Shi, E., Asanovic, K., Kubiatowicz, J., Song, D.: Phantom: practical oblivious computation in a secure processor. In: CCS (2013)

50.

Martignoni, L., Poosankam, P., Zaharia, M., Han, J., McCamant, S., Song, D., Paxson, V., Perrig, A., Shenker, S., Stoica, I.: Cloud terminal: secure access to sensitive applications from untrusted systems. In: USENIX ATC (2012)

51.

McKeen, F., Alexandrovich, I., Berenzon, A., Rozas, C.V., Shafi, H., Shanbhogue, V., Savagaonkar, U.R.: Innovative instructions and software model for isolated execution. In: HASP 2013: 10 (2013)

52.

Mechler, J., Mller-Quade, J., Nilges, T.: Universally composable (non-interactive) two-party computation from untrusted reusable hardware tokens. Cryptology ePrint Archive, Report 2016/615 (2016). http://eprint.iacr.org/2016/615

53.

Micciancio, D., Warinschi, B.: Completeness theorems for the Abadi-Rogaway language of encrypted expressions. J. Comput. Secur. 12(1), 99–129 (2004)CrossRef

54.

Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 133–151. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24638-1_8 CrossRef

55.

Ohrimenko, O., Schuster, F., Fournet, C., Mehta, A., Nowozin, S., Vaswani, K., Costa, M.: Oblivious multi-party machine learning on trusted processors. In: USENIX Security, August 2016

56.

Pass, R., Shi, E., Tramèr, F.: Formal abstractions for attested execution secure processors. IACR Cryptology ePrint Archive 2016:1027 (2016)

57.

Petcher, A., Morrisett, G.: The foundational cryptography framework. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 53–72. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46666-7_4

58.

Petcher, A., Morrisett, G.: A mechanized proof of security for searchable symmetric encryption. In: CSF (2015)

59.

Sailer, R., Zhang, X., Jaeger, T., van Doorn, L.: Design and implementation of a TCG-based integrity measurement architecture. In: USENIX Security (2004)

60.

Santos, N., Raj, H., Saroiu, S., Wolman, A.: Using arm trustzone to build a trusted language runtime for mobile applications. SIGARCH Comput. Archit. News 42(1), 67–80 (2014)

61.

Santos, N., Rodrigues, R., Gummadi, K.P., Saroiu, S.: Policy-sealed data: a new abstraction for building trusted cloud services. In: USENIX Security, pp. 175–188 (2012)

62.

Schuster, F., Costa, M., Fournet, C., Gkantsidis, C., Peinado, M., Mainar-Ruiz, G., Russinovich, M.: VC3: trustworthy data analytics in the cloud. In: IEEE S&P (2015)

63.

Shi, E., Perrig, A., Van Doorn, L.: BIND: a fine-grained attestation service for secure distributed systems. In: IEEE S&P (2005)

64.

Shi, E., Zhang, F., Pass, R., Devadas, S., Song, D., Liu, C.: Systematization of knowledge: trusted hardware: life, the composable universe, and everything. Manuscript (2015)

65.

Smith, S.W., Austel, V.: Trusting trusted hardware: towards a formal model for programmable secure coprocessors. In: Proceedings of the 3rd Conference on USENIX Workshop on Electronic Commerce, WOEC 1998, vol. 3 (1998)

66.

Suh, G.E., Clarke, D., Gassend, B., Van Dijk, M., Devadas, S.: AEGIS: architecture for tamper-evident and tamper-resistant processing. In: Proceedings of the 17th Annual International Conference on Supercomputing, pp. 160–171. ACM (2003)

67.

Szczys, M.: TPM crytography cracked. http://hackaday.com/2010/02/09/tpm-crytography-cracked/

68.

Lie, D., Thekkath, C., Mitchell, M., Lincoln, P., Boneh, D., Mitchell, J., Horowitz, M.: Architectural support for copy and tamper resistant software. SIGOPS Oper. Syst. Rev. 34(5), 168–177 (2000)CrossRef

69.

Thompson, K.: Reflections on trusting trust. Commun. ACM 27(8), 761–763 (1984)CrossRef

70.

Tramèr, F., Zhang, F., Lin, H., Hubaux, J.-P., Juels, A., Shi, E.: Sealed-glass proofs: using transparent enclaves to prove and sell knowledge. In: IEEE European Symposium on Security and Privacy (2017)

71.

Yuanzhong, X., Cui, W., Peinado, M.: Controlled-channel attacks: deterministic side channels for untrusted operating systems. In: IEEE S&P (2015)

72.

Zhang, D., Yao Wang, G., Suh, E., Myers, A.C.: A hardware design language for timing-sensitive information-flow security. In: ASPLOS (2015)

73.

Zhang, F., Cecchetti, E., Croman, K., Juels, A., Shi, E.: Town crier: an authenticated data feed for smart contracts. In: ACM CCS (2016)

74.

Zhuang, X., Zhang, T., Pande, S.: Hide: an infrastructure for efficiently protecting information leakage on the address bus. SIGARCH Comput. Archit. News 32(5), 72–84 (2004)CrossRef

Titel: Formal Abstractions for Attested Execution Secure Processors
verfasst von: Rafael Pass
Elaine Shi
Florian Tramèr
Verlag: Springer International Publishing
Buch: Advances in Cryptology – EUROCRYPT 2017
Print ISBN: 978-3-319-56619-1

Electronic ISBN: 978-3-319-56620-7

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-56620-7_10

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"