Komodo: Using verification to disentangle secure-enclave hardware from software

ABSTRACT

Intel SGX promises powerful security: an arbitrary number of user-mode enclaves protected against physical attacks and privileged software adversaries. However, to achieve this, Intel extended the x86 architecture with an isolation mechanism approaching the complexity of an OS microkernel, implemented by an inscrutable mix of silicon and microcode. While hardware-based security can offer performance and features that are difficult or impossible to achieve in pure software, hardware-only solutions are difficult to update, either to patch security flaws or introduce new features.

Komodo illustrates an alternative approach to attested, on-demand, user-mode, concurrent isolated execution. We decouple the core hardware mechanisms such as memory encryption, address-space isolation and attestation from the management thereof, which Komodo delegates to a privileged software monitor that in turn implements enclaves. The monitor's correctness is ensured by a machine-checkable proof of both functional correctness and high-level security properties of enclave integrity and confidentiality. We show that the approach is practical and performant with a concrete implementation of a prototype in verified assembly code on ARM TrustZone. Our ultimate goal is to achieve security equivalent to or better than SGX while enabling deployment of new enclave features independently of CPU upgrades.

The Komodo specification, prototype implementation, and proofs are available at https://github.com/Microsoft/Komodo.

References

1. PrimeCell Infrastructure AMBA 3 TrustZone Protection Controller (BP147) Technical Overview. ARM Limited, Nov. 2004. Ref. DTO 0015A.
2. Building a Secure System using TrustZone Technology. ARM Limited, Apr. 2009. Ref. PRD29-GENC-009492C.
3. ARM Architecture Reference Manual, ARMv7-A and ARMv7-R edition. ARM Limited, May 2014. Ref. DDI 0406C.c.
4. ARM CoreLink TZC-400 TrustZone Address Space Controller Technical Reference Manual. ARM Limited, Feb. 2014. Ref. DDI 0504C.
5. S. Arnautov, B. Trach, F. Gregor, T. Knauth, A. Martin, C. Priebe, J. Lind, D. Muthukumaran, D. O'Keeffe, M. L. Stillwell, D. Goltzsche, D. Eyers, R. Kapitza, P. Pietzuch, and C. Fetzer. SCONE: Secure Linux containers with Intel SGX. In 12th USENIX Symposium on Operating Systems Design and Implementation, pages 689--703, 2016. ISBN 978-1-931971-33-1. URL https://www.usenix.org/conference/osdi16/technical-sessions/presentation/arnautov.
6. A. M. Azab, P. Ning, J. Shah, Q. Chen, R. Bhutkar, G. Ganesh, J. Ma, and W. Shen. Hypervision across worlds: Real-time kernel protection from the ARM TrustZone secure world. In 21st ACM Conference on Computer and Communications Security, pages 90--102, 2014. ISBN 978-1-4503-2957-6.
7. A. Baumann. Hardware is the new software. In 16th Workshop on Hot Topics in Operating Systems, HotOS '17, pages 132--137, 2017. ISBN 978-1-4503-5068-6.
8. A. Baumann, M. Peinado, and G. Hunt. Shielding applications from an untrusted cloud with Haven. In 11th USENIX Symposium on Operating Systems Design and Implementation, pages 267--283, Oct. 2014. ISBN 978-1-931971-16-4. URL https://www.usenix.org/conference/osdi14/technical-sessions/presentation/baumann.
9. J. Behl, T. Distler, and R. Kapitza. Hybrids on steroids: SGX-based high performance BFT. In EuroSys Conference, pages 222--237, 2017. ISBN 978-1-4503-4938-3.
10. K. J. Biba. Integrity considerations for secure computer systems. Technical Report ESD-TR-76-372, USAF Electronic Systems Division, 1977.
11. R. Boivie. SecureBlue++: CPU support for secure execution. Technical Report RC25287, IBM Research, May 2012. URL http://researcher.watson.ibm.com/researcher/view_group.php?id=7253.
12. B. Bond, C. Hawblitzel, M. Kapritsos, K. R. M. Leino, J. R. Lorch, B. Parno, A. Rane, S. Setty, and L. Thompson. Vale: Verifying high-performance cryptographic assembly code. In 26th USENIX Security Symposium, Aug. 2017. URL https://www.usenix.org/conference/usenixsecurity17/technical-sessions/presentation/bond.
13. F. Brasser, U. Müller, A. Dmitrienko, K. Kostiainen, S. Capkun, and A.-R. Sadeghi. Software grand exposure: SGX cache attacks are practical. In 11th USENIX Workshop on Offensive Technologies (WOOT 17), Aug. 2017. URL https://www.usenix.org/conference/woot17/workshop-program/presentation/brasser.
14. S. Brenner, C. Wulf, D. Goltzsche, N. Weichbrodt, M. Lorenz, C. Fetzer, P. Pietzuch, and R. Kapitza. SecureKeeper: Confidential ZooKeeper using Intel SGX. In 17th International Middleware Conference, pages 14:1--14:13, 2016. ISBN 978-1-4503-4300-8.
15. D. Champagne and R. B. Lee. Scalable architectural support for trusted software. In 16th IEEE International Symposium on High-Performance Computer Architecture, Jan. 2010.
16. S. Chhabra, B. Rogers, Y. Solihin, and M. Prvulovic. SecureME: a hardware-software approach to full system security. In International Conference on Supercomputing, pages 108--119, 2011. ISBN 978-1-4503-0102-2.
17. P. Colp, J. Zhang, J. Gleeson, S. Suneja, E. de Lara, H. Raj, S. Saroiu, and A. Wolman. Protecting data on smartphones and tablets from memory attacks. In 20th International Conference on Architectural Support for Programming Languages and Operating Systems, pages 177--189, 2015. ISBN 978-1-4503-2835-7.
18. V. Costan and S. Devadas. Intel SGX explained. Cryptology ePrint Archive, Report 2016/086, Feb. 2016. http://eprint.iacr.org/2016/086.
19. V. Costan, I. Lebedev, and S. Devadas. Sanctum: Minimal hardware extensions for strong software isolation. In 25th USENIX Security Symposium, pages 857--874, Aug. 2016. ISBN 978-1-931971-32-4. URL https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/costan.
20. D. Costanzo, Z. Shao, and R. Gu. End-to-end verificationof information-flow security for C and assembly programs. In 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 648--664, 2016. ISBN 978-1-4503-4261-2.
21. S. Crosby. Using Intel SGX to protect on-line credentials, Aug. 2016. URL https://blogs.bromium.com/2016/08/09/using-intel-sgx-to-protect-on-line-credentials/.
22. I. Cutress. Intel's 'Tick-Tock' seemingly dead, becomes 'Process-Architecture-Optimization'. AnandTech, Mar. 2016. URL http//:www.anandtech.com/show/10183.
23. L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 337--340, Mar. 2008. ISBN 978-3-540-78800-3.
24. PALcode for Alpha Microprocessors System Design Guide. Digital Equipment Corp., May 1996. Order No. EC-QFGLC-TE.
25. K. Elphinstone, A. Zarrabi, A. Danis, Y. Shen, and G. Heiser. An evaluation of coarse-grained locking for multicore microkernels. CoRR, abs/1609.08372, Oct. 2016. URL http://arxiv.org/abs/1609.08372.
26. D. Evtyushkin, J. Elwell, M. Ozsoy, D. Ponomarev, N. A. Ghazaleh, and R. Riley. Iso-X: A flexible architecture for hardware-managed isolated execution. In 47th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO-47, pages 190--202, 2014. ISBN 978-1-4799-6998-2.
27. C. W. Fletcher, M. v. Dijk, and S. Devadas. A secure processor architecture for encrypted computation on untrusted programs. In 7th ACM Workshop on Scalable Trusted Computing, pages 3--8, 2012. ISBN 978-1-4503-1662-0.
28. P. Fonseca, K. Zhang, X. Wang, and A. Krishnamurthy. An empirical study on the correctness of formally verified distributed systems. In EuroSys Conference, Apr. 2017.
29. A. Fox and M. O. Myreen. A trustworthy monadic formalization of the ARMv7 instruction set architecture. In 1st International Conference on Interactive Theorem Proving, pages 243--258, July 2010. ISBN 978-3-642-14052-5.
30. GlobalPlatform Device Technology TEE System Architecture v1.1. GlobalPlatform, Jan. 2017. Ref. GPD_SPE_009.
31. A. Goel, S. Krstić, R. Leslie, and M. R. Tuttle. SMT-based system verification with DVF. In 10th International Workshop on Satisfiability Modulo Theories, pages 32--43, 2012. URL http://smt2012.loria.fr/paper2.pdf.
32. J. A. Goguen and J. Meseguer. Security policies and security models. In IEEE Symposium on Security and Privacy, 1982.
33. A. Gollamudi and S. Chong. Automatic enforcement of expressive security policies using enclaves. In 2016 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA 2016, pages 494--513, 2016. ISBN 978-1-4503-4444-9.
34. R. Gu, J. Koenig, T. Ramananandro, Z. Shao, X. N. Wu, S.-C. Weng, H. Zhang, and Y. Guo. Deep specifications and certified abstraction layers. In 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 595--608, 2015. ISBN 978-1-4503-3300-9.
35. R. Gu, Z. Shao, H. Chen, X. N. Wo, J. Kim, V. Sjöberg, and D. Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, Nov. 2016.
36. J. A. Halderman, S. D. Schoen, N. Heninger, W. Clarkson, W. Paul, J. A. Calandrino, A. J. Feldman, J. Appelbaum, and E. W. Felten. Lest we remember: Cold boot attacks on encryption keys. In 17th USENIX Security Symposium, pages 45--60, July 2008. URL https://www.usenix.org/legacy/event/sec08/tech/full_papers/halderman/halderman.pdf.
37. S. M. Hand. Self-paging in the Nemesis operating system. In 3rd USENIX Symposium on Operating Systems Design and Implementation, pages 73--86, New Orleans, Louisiana, USA, 1999. ISBN 1-880446-39-1. URL https://www.usenix.org/events/osdi99/hand.html.
38. C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno, D. Zhang, and B. Zill. Ironclad apps: End-to-end security via automated full-system verification. In 11th USENIX Symposium on Operating Systems Design and Implementation, pages 165--181, Oct. 2014. ISBN 978-1-931971-16-4. URL https://www.usenix.org/conference/osdi14/technical-sessions/presentation/hawblitzel.
39. C. Hawblitzel, J. Howell, M. Kapritsos, J. R. Lorch, B. Parno, M. L. Roberts, S. Setty, and B. Zill. IronFleet: Proving practical distributed systems correct. In 25th ACM Symposium on Operating Systems Principles, pages 1--17, 2015. ISBN 978-1-4503-3834-9.
40. J. Howell, B. Parno, and J. R. Douceur. Embassies: Radically refactoring the web. In 10th USENIX Symposium on Networked Systems Design and Implementation, pages 529--545, 2013. ISBN 978-1-931971-00-3. URL https://www.usenix.org/conference/nsdi13/technical-sessions/presentation/howell.
41. G. Hunt, G. Letey, and E. Nightingale. The seven properties of highly secure devices. Technical Report MSR-TR-2017-16, Microsoft Research, Mar. 2017. URL https://www.microsoft.com/en-us/research/publication/seven-properties-highly-secure-devices/.
42. T. Hunt, Z. Zhu, Y. Xu, S. Peter, and E. Witchel. Ryoan: A distributed sandbox for untrusted computation on secret data. In 12th USENIX Symposium on Operating Systems Design and Implementation, pages 533--549, 2016. ISBN 978-1-931971-33-1. URL https://www.usenix.org/conference/osdi16/technical-sessions/presentation/hunt.
43. Software Guard Extensions Programming Reference. Intel Corp., Oct. 2014. Ref. #329298-002 https://software.intel.com/sites/default/files/managed/48/88/329298-002.pdf.
44. SGX Tutorial at ISCA 2015. Intel Corp., June 2015. Ref. #332680-002 https://software.intel.com/sites/default/files/332680-002.pdf.
45. Intel 64 and IA-32 Architectures Software Developer's Manual. Intel Corp., Dec. 2016. Ref. #325462-061US.
46. S. P. Johnson, U. R. Savagaonkar, V. R. Scarlata, F. X. McKeen, and C. V. Rozas. Technique for supporting multiple secure enclaves, Dec. 2010. US Patent 8,972,746.
47. U. Kanonov and A. Wool. Secure containers in Android: The Samsung KNOX case study. In 6th Workshop on Security and Privacy in Smart-phones and Mobile Devices, pages 3--12, 2016. ISBN 978-1-4503-4564-4.
48. D. Kaplan, J. Powell, and T. Woller. AMD memory encryption. http://developer.amd.com/wordpress/media/2013/12/AMD_Memory_Encryption_Whitepaper_v7-Public.pdf, Apr. 2016.
49. G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski, and G. Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, 32(1):2:1--2:70, Feb. 2014. ISSN 0734-2071.
50. R. B. Lee, P. C. S. Kwan, J. P. McGregor, J. Dwoskin, and Z. Wang. Architecture for protecting critical secrets in microprocessors. In 32nd International Symposium on Computer Architecture, pages 2--13, 2005. ISBN 0-7695-2270-X.
51. K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-16), pages 348--370, Apr. 2010. ISBN 978-3-642-17511-4.
52. R. Leslie-Hurd, D. Caspi, and M. Fernandez. Verifying linearizability of Intel software guard extensions. In 27th International Conference on Computer Aided Verification, pages 144--160, July 2015. ISBN 978-3-319-21668-3.
53. D. Lie, C. Thekkath, M. Mitchell, P. Lincoln, D. Boneh, J. Mitchell, and M. Horowitz. Architectural support for copy and tamper resistant software. In 9th International Conference on Architectural Support for Programming Languages and Operating Systems, Nov. 2000.
54. L. Maranget, S. Sarkar, and P. Sewell. A tutorial introduction to the ARM and POWER relaxed memory models. Draft revision 120, Oct. 2012. URL http//:www.cl.cam.ac.uk/~pes20/weakmemory/.
55. B. D. Marsh, M. L. Scott, T. J. LeBlanc, and E. P. Markatos. First-class user-level threads. In 13th ACM Symposium on Operating Systems Principles, pages 110--121, 1991. ISBN 0-89791-447-3.
56. J. M. McCune, B. Parno, A. Perrig, M. K. Reiter, and A. Seshadri. Minimal TCB code execution (extended abstract). In Proceedings of the IEEE Symposium on Security and Privacy, May 2007.
57. J. M. McCune, B. J. Parno, A. Perrig, M. K. Reiter, and H. Isozaki. Flicker: an execution infrastructure for TCB minimization. In EuroSys Conference, pages 315--328, 2008. ISBN 978-1-60558-013-5.
58. J. M. McCune, Y. Li, N. Qu, Z. Zhou, A. Datta, V. Gligor, and A. Perrig. TrustVisor: Efficient TCB reduction and attestation. In IEEE Symposium on Security and Privacy, pages 143--158, May 2010.
59. F. McKeen, I. Alexandrovich, A. Berenzon, C. V. Rozas, H. Shafi, V. Shanbhogue, and U. R. Savagaonkar. Innovative instructions and software model for isolated execution. In 2nd International Workshop on Hardware and Architectural Support for Security and Privacy, 2013. ISBN 978-1-4503-2118-1.
60. F. X. McKeen, C. V. Rozas, U. R. Savagaonkar, S. P. Johnson, V. Scarlata, M. A. Goldsmith, E. Brickell, et al. Method and apparatus to provide secure application execution, Dec. 2009. US Patent 9,087,200.
61. MITRE. CVE-2017-5691, July 2017. URL https://nvd.nist.gov/vuln/detail/CVE-2017-5691.
62. T. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke, S. Seefried, C. Lewis, X. Gao, and G. Klein. seL4: From general purpose to a proof of information flow enforcement. In IEEE Symposium on Security and Privacy, pages 415--429, May 2013.
63. K. T. Nguyen. Introduction to Cache Allocation Technology in the Intel Xeon Processor E5 v4 family, Feb. 2016. https://software.intel.com/en-us/articles/introduction-to-cache-allocation-technology.
64. NXP. i.MX 7Solo, i.MX 7Dual applications processors, 2017. URL http//:www.nxp.com/iMX7.
65. O. Ohrimenko, F. Schuster, C. Fournet, A. Mehta, S. Nowozin, K. Vaswani, and M. Costa. Oblivious multi-party machine learning on trusted processors. In 25th USENIX Security Symposium, pages 619--636, 2016. ISBN 978-1-931971-32-4. URL https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/ohrimenko.
66. M. Orenbach, P. Lifshits, M. Minkin, and M. Silberstein. Eleos: ExitLess OS services for SGX enclaves. In EuroSys Conference, Apr. 2017.
67. E. Owusu, J. Guajardo, J. McCune, J. Newsome, A. Perrig, and A. Vasudevan. OASIS: On achieving a sanctuary for integrity and secrecy on untrusted platforms. In 20th ACM Conference on Computer and Communications Security, pages 13--24, 2013. ISBN 978-1-4503-2477-9.
68. R. Pires, M. Pasin, P. Felber, and C. Fetzer. Secure content-based routing using Intel software guard extensions. In 17th International Middleware Conference, pages 10:1--10:10, 2016. ISBN 978-1-4503-4300-8.
69. H. Raj, D. Robinson, T. B. Tariq, P. England, S. Saroiu, and A. Wolman. Credo: Trusted computing for guest VMs with a commodity hypervisor. Technical Report MSR-TR-2011-130, Microsoft Research, Dec. 2011.
70. H. Raj, S. Saroiu, A. Wolman, R. Aigner, J. Cox, P. England, C. Fenner, K. Kinshumann, J. Loeser, D. Mattoon, M. Nystrom, D. Robinson, R. Spiger, S. Thom, and D. Wooten. fTPM: A software-only implementation of a TPM chip. In 25th USENIX Security Symposium, pages 841--856, 2016. ISBN 978-1-931971-32-4. URL https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/raj.
71. A. Reid. Trustworthy specifications of ARM v8-A and v8-M system level architecture. In Formal Methods in Computer-Aided Design, pages 161--168, Oct. 2016.
72. A. Reid, R. Chen, A. Deligiannis, D. Gilday, D. Hoyes, W. Keen, A. Pathirane, O. Shepherd, P. Vrabel, and A. Zaidi. End-to-end verification of ARM processors with ISA-formal. In 28th International Conference on Computer Aided Verification, pages 42--58, July 2016. ISBN 978-3-319-41540-6.
73. A. Sabelfeld and A. C. Myers. A Model for Delimited Information Release, pages 174--191. Springer, Oct. 2004. ISBN 978-3-540-37621-7.
74. N. Santos, H. Raj, S. Saroiu, and A. Wolman. Using ARM TrustZone to build a trusted language runtime for mobile applications. In 19th International Conference on Architectural Support for Programming Languages and Operating Systems, pages 67--80, 2014. ISBN 978-1-4503-2305-5.
75. F. Schuster, M. Costa, C. Fournet, C. Gkantsidis, M. Peinado, G. Mainar-Ruiz, and M. Russinovich. VC3: Trustworthy data analytics in the cloud using SGX. In IEEE Symposium on Security and Privacy, May 2015.
76. M. Schwarz, S. Weiser, D. Gruss, C. Maurice, and S. Mangard. Malware guard extension: Using SGX to conceal cache attacks. In 14th International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment (DIMVA), pages 3--24. Springer, July 2017. ISBN 978-3-319-60876-1.
77. M.-W. Shih, S. Lee, T. Kim, and M. Peinado. T-SGX: Eradicating controlled-channel attacks against enclave programs. In Annual Network and Distributed System Security Symposium (NDSS), Feb. 2017.
78. S. Shinde, Z. L. Chua, V. Narayanan, and P. Saxena. Preventing page faults from telling your secrets. In 11th ACM Asia Conference on Computer and Communications Security, pages 317--328, 2016. ISBN 978-1-4503-4233-9.
79. T. Simonite. Intel puts the brakes on Moore's Law. MIT Technology Review, Mar. 2016. URL https://www.technologyreview.com/s/601102.
80. R. Sinha, S. Rajamani, S. Seshia, and K. Vaswani. Moat: Verifying confidentiality of enclave programs. In 22nd ACM Conference on Computer and Communications Security, pages 1169--1184, 2015. ISBN 978-1-4503-3832-5.
81. R. Sinha, M. Costa, A. Lal, N. P. Lopes, S. Rajamani, S. A. Seshia, and K. Vaswani. A design and verification methodology for secure isolated regions. In 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '16, pages 665--681, 2016. ISBN 978-1-4503-4261-2.
82. J. Szefer and R. B. Lee. Architectural support for hypervisor-secure virtualization. In 17th International Conference on Architectural Support for Programming Languages and Operating Systems, pages 437--450, 2012. ISBN 978-1-4503-0759-8.
83. TPM Main Specification Level 2. Trusted Computing Group, Mar. 2011. Version 1.2, Revision 116.
84. A. Vasudevan, S. Chaki, P. Maniatis, L. Jia, and A. Datta. überspark: Enforcing verifiable object abstractions for automated compositional security analysis of a hypervisor. In 25th USENIX Security Symposium, pages 87--104, 2016. ISBN 978-1-931971-32-4. URL https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/vasudevan.
85. A. Waterman, Y. Lee, R. Avizienis, D. A. Patterson, and K. Asanović. The RISC-V instruction set manual volume II: Privileged architecture version 1.7. Technical Report UCB/EECS-2015-49, UC Berkeley EECS, May 2015.
86. R. Wojtczuk and J. Rutkowska. Attacking Intel TXT via SINIT code execution hijacking. http://invisiblethingslab.com/resources/2011/Attacking_Intel_TXT_via_SINIT_hijacking.pdf, Nov. 2011.
87. R. Wojtczuk, J. Rutkowska, and A. Tereshkin. Another way to circumvent Intel Trusted Execution Technology. http://invisiblethingslab.com/resources/misc09/Another%20TXT%20Attack.pdf, Dec. 2009.
88. Y. Xu, W. Cui, and M. Peinado. Controlled-channel attacks: Deterministic side-channels for untrusted operating systems. In IEEE Symposium on Security and Privacy, May 2015.
89. J. Yang and C. Hawblitzel. Safe to the last instruction: Automated verification of a type-safe operating system. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 99--110, 2010. ISBN 978-1-4503-0019-3.