A Formal Foundation for Secure Remote Execution of Enclaves.

IACR Cryptology ePrint Archive, (2017): 2435-2450

Cited by: 78|Views317
EI

Abstract

Recent proposals for trusted hardware platforms, such as Intel SGX and the MIT Sanctum processor, offer compelling security features but lack formal guarantees. We introduce a verification methodology based on a trusted abstract platform (TAP), a formalization of idealized enclave platforms along with a parameterized adversary. We also fo...More

Code:

Data:

Introduction
  • An application executing on a typical computing platform contains large privileged software layers in its trusted computing base (TCB), which includes the operating system (OS), hypervisor and firmware.
  • Vulnerabilities in these privileged software layers have been exploited to enable the execution of privileged malware with disastrous consequences [1, 26, 35, 52, 64]
  • To address this problem, processor designers and vendors are developing CPUs with hardware primitives, such as Intel SGX and MIT Sanctum, which isolate sensitive code and data within protected memory regions, called enclaves, that are inaccessible to other software running on the machine.
  • Hardware designers cannot formally state security properties of their architectures and are unable to reason about potential vulnerabilities of enclaves running on their hardware
Highlights
  • An application executing on a typical computing platform contains large privileged software layers in its trusted computing base (TCB), which includes the operating system (OS), hypervisor and firmware
  • We develop formal models of SGX and Sanctum and present machine-checked proofs showing that SGX and Sanctum are refinements of our idealized trusted abstract platform: every operation on SGX and Sanctum can be mapped to a corresponding trusted abstract platform operation
  • We present a set of machine-checked proofs showing that the trusted abstract platform satisfies the properties required for secure remote execution: (i) secure measurement, integrity and confidentiality
  • This paper introduced a framework and methodology to reason about the security guarantees provided by enclave platforms
  • We introduced the Trusted Abstract Platform (TAP), and performed proofs demonstrating that trusted abstract platform satisfies the three properties required for secure remote execution (SRE): secure measurement, integrity and confidentiality
  • We presented machine-checked proofs stating that models of Intel SGX and Sanctum are refinements of trusted abstract platform under certain adversarial conditions
Methods
  • The authors say that Impl refines TAP, or equivalently TAP simulates Impl, if there exists a simulation relation R ⊆ (ΣL × Σ) with the following property:.
  • The initial states of Impl and TAP must be related by R.
  • This is illustrated in Figure 5.
  • The properties the authors consider are 2-safety properties [77] that are variants of observational determinism [48, 62]
  • These are properties are preserved by refinement.
  • The SRE properties proven on the TAP hold for SGX and Sanctum, as the authors show that these architectures refine the TAP
Results
  • This section discusses the models and machine-checked proofs. The authors' models of the TAP, Intel SGX and MIT Sanctum are constructed using the BoogiePL [7, 24] intermediate verification language.
  • BoogiePL programs can be annotated with assertions, loop invariants and pre-/post-conditions for procedures.
  • The validity of these annotations are checked using the Boogie Verification Condition Generator [7], which in turn uses the Z3 SMT solver [23].
  • The verification times for the TAP, MMU Model and Sanctum rows is for proving that procedures in these models satisfy their post conditions, which specify behavior and system invariants.
  • The total computation time in checking validity of the proofs once the correct annotations are specified is only a few minutes
Conclusion
  • Suppose that the version of Sanctum supports demand paging through the use of oblivious RAM to maintain TAP’s confidentiality guarantee
  • Reasoning about these more complex enclave platforms is infeasible without a verification methodology and TAP-like specification of the platform’s primitives.This paper introduced a framework and methodology to reason about the security guarantees provided by enclave platforms.
  • The authors presented machine-checked proofs stating that models of Intel SGX and Sanctum are refinements of TAP under certain adversarial conditions
  • These platforms satisfy the properties required for SRE.
  • This paper took a step towards a unified, extensible framework for reasoning about enclave programs and platforms
Tables
  • Table1: Description of TAP State Variables
  • Table2: Fields of the enc_metadata record
  • Table3: Description of TAP Operations
  • Table4: BoogiePL Models and Verification Results
  • Table5: Glossary of Symbols
Download tables as Excel
Related work
  • Secure Processors: There have been several commercial deployments of secure processors. ARM TrustZone [2] implements a secure and normal mode of execution to effectively create a single privileged enclave in an isolated address space. TPM+TXT [29] enables attestation of the platform’s state, but includes all privileged software layers in the trusted computing base. Most recently, Intel SGX [3, 20, 32, 47] implements unprivileged enclaves protecting the integrity of memory and enclave state against software adversaries and certain physical access attacks. Academic work seeking to improve the security of aspects of conventional processors is also abundant [25, 43, 44].

    Several clean-slate academic projects have been seeking to build a trusted system. The XOM [42] architecture introduced the concept of isolated software containers managed by untrusted host software, and employed encryption and HMAC to protect DRAM. Aegis [76] showed how a security kernel could measure and sign enclaves, and employed counter-mode memory encryption and a Merkle tree to guarantee freshness of data in DRAM. Bastion [16] encrypts and HMACs DRAM and employs a trusted (and authenticated as part of remote attestation) hypervisor which is invoked at each TLB miss to check address translation against a policy. Fides [74] uses a small trusted hypervisor to provide security guarantees for so-called protected modules; protected modules offer very similar programming abstractions and security guarantees as enclaves. Sancus [54] builds upon Fides, and proposes hardware extensions that ensure security of protected modules in the context of resourceconstrained embedded processors. Ascend [27] and Phantom [46] ensure privacy and integrity of all CPU memory accesses through a hardware ORAM primitive. Attacks on Secure Processors: Secure systems often expose complex threat models in practice, leading to vulnerabilities in the application layers. Side channel observations, such as attacks observing cache timing, are known to compromise cryptographic keys used by numerous cryptosystems [11, 14, 15, 37]. Attacks exploiting other shared resources exist as well, such as those observing a core’s branch history buffers [38]. These attacks are viable at any privilege, separated by arbitrary protection boundaries [34, 45, 56]. Similar attacks apply on trusted hardware, as shown on SGX with attacks observing shared caches [12, 49, 66], and shared page tables [69, 83]. Formal Models/Verification of Enclave Platforms: A formal cryptographic model of SGX’s anonymous attestation scheme is presented in [58]. Barbosa et al [6] present a formal analysis of cryptographic protocols for secure outsourced computation using enclave platforms. In contrast to these efforts, which reason about cryptographic protocols in the context of enclaves, our work formalizes the security guarantees of enclave platforms themselves. Patrignani et al [60, 61] develop abstract trace semantics for lowlevel code (not including side-channels) on protected module architectures – Fides [74] and Sancus [54] – in order to build secure compilers for these platforms [59]. This is complementary to our work which focuses on formalizing the security guarantees of enclave platforms in presence of a precisely modelled adversary (including side-channel observations).
Funding
  • Funding for this research was partially provided by the National Science Foundation under grants CNS-1413920 and CNS-1528108, by the Intel ADEPT Center, by Delta Electronics, and by TerraSwarm, one of six centers of STARnet, a Semiconductor Research Corporation program sponsored by MARCO and DARPA
Reference
  • Lenovo ThinkPad System Management Mode Arbitrary Code Execution 0day Exploit. Available at https://github.com/Cr4sh/ThinkPwn.git.
    Findings
  • T. Alves and D. Felton. TrustZone: Integrated Hardware and Software Security. Information Quarterly, 3(4):18–24, 2004.
    Google ScholarLocate open access versionFindings
  • I. Anati, S. Gueron, S. P. Johnson, and V. R. Scarlata. Innovative Technology for CPU Based Attestation and Sealing. In Proceedings of the 2nd International Workshop on Hardware and Architectural Support for Security and Privacy, HASP, volume 13, 2013.
    Google ScholarLocate open access versionFindings
  • K. Asanovic, R. Avizienis, J. Bachrach, S. Beamer, D. Biancolin, C. Celio, H. Cook, D. Dabbelt, J. Hauser, A. Izraelevitz, et al. The Rocket Chip Generator. EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2016-17, 2016.
    Google ScholarFindings
  • K. Asanović and D. A. Patterson. Instruction Sets Should Be Free: The Case For RISC-V. EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS2014-146, 2014.
    Google ScholarFindings
  • M. Barbosa, B. Portela, G. Scerri, and B. Warinschi. Foundations of HardwareBased Attested Computation and Application to SGX. In IEEE European Symposium on Security and Privacy, EuroS&P 2016, Saarbrücken, Germany, March 21-24, 2016, pages 245–260, 2016.
    Google ScholarLocate open access versionFindings
  • M. Barnett, B. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In FMCO ’05, LNCS 4111, pages 364–387, 2005.
    Google ScholarLocate open access versionFindings
  • G. Barthe, P. R. D’Argenio, and T. Rezk. Secure information flow by selfcomposition. Mathematical Structures in Computer Science, 21(6):1207–1252, 2011.
    Google ScholarLocate open access versionFindings
  • Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer Science & Business Media, 2013.
    Google ScholarFindings
  • K. Bhargavan, C. Fournet, and M. Kohlweiss. miTLS: Verifying Protocol Implementations against Real-World Attacks. IEEE Security & Privacy, 14(6):18–25, 2016.
    Google ScholarLocate open access versionFindings
  • J. Bonneau and I. Mironov. Cache-Collision Timing Attacks Against AES, pages 201–215. Springer Berlin Heidelberg, Berlin, Heidelberg, 2006.
    Google ScholarFindings
  • F. Brasser, U. Müller, A. Dmitrienko, K. Kostiainen, S. Capkun, and A. Sadeghi. Software Grand Exposure: SGX Cache Attacks Are Practical. CoRR, abs/1702.07521, 2017.
    Findings
  • M. C. Browne, E. M. Clarke, and O. Grumberg. Characterizing Finite Kripke Structures in Propositional Temporal Logic. Theoretical Computer Science, 59:115– 131, 1988.
    Google ScholarLocate open access versionFindings
  • B. B. Brumley and N. Tuveri. Remote Timing Attacks Are Still Practical. In Proceedings of the 16th European Conference on Research in Computer Security, ESORICS’11, pages 355–371, Berlin, Heidelberg, 2011. Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • D. Brumley and D. Boneh. Remote Timing Attacks Are Practical. In Proceedings of the 12th Conference on USENIX Security Symposium - Volume 12, SSYM’03, pages 1–1, Berkeley, CA, USA, 2003. USENIX Association.
    Google ScholarLocate open access versionFindings
  • D. Champagne and R. B. Lee. Scalable architectural support for trusted software. In High Performance Computer Architecture (HPCA), 2010 IEEE 16th International Symposium on, pages 1–12. IEEE, 2010.
    Google ScholarLocate open access versionFindings
  • A. Chaudhuri. Language-based security on Android. In Proceedings of the 2009 Workshop on Programming Languages and Analysis for Security, PLAS 2009, Dublin, Ireland, 15-21 June, 2009, pages 1–7, 2009.
    Google ScholarLocate open access versionFindings
  • C.-T. Chou, P. K. Mannava, and S. Park. A simple method for parameterized verification of cache coherence protocols. In A. J. Hu and A. K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in ComputerAided Design, pages 382–398, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.
    Google ScholarLocate open access versionFindings
  • M. R. Clarkson and F. B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157–1210, Sept. 2010.
    Google ScholarLocate open access versionFindings
  • V. Costan and S. Devadas. Intel SGX Explained. Cryptology ePrint Archive, Report 2016/086, 2016. http://eprint.iacr.org/2016/086.
    Findings
  • V. Costan, I. Lebedev, and S. Devadas. Sanctum: Minimal Hardware Extensions for Strong Software Isolation. In 25th USENIX Security Symposium (USENIX Security 16), pages 857–874, Austin, TX, 2016. USENIX Association.
    Google ScholarLocate open access versionFindings
  • A. Datta, J. Franklin, D. Garg, and D. Kaynar. A Logic of Secure Systems and Its Application to Trusted Computing. In Proceedings of the 2009 30th IEEE Symposium on Security and Privacy, SP ’09, pages 221–236, Washington, DC, USA, 2009. IEEE Computer Society.
    Google ScholarLocate open access versionFindings
  • L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In TACAS ’08, pages 337–340, 2008.
    Google ScholarLocate open access versionFindings
  • R. DeLine and K. R. M. Leino. BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research, 2005.
    Google ScholarFindings
  • L. Domnitser, A. Jaleel, J. Loew, N. Abu-Ghazaleh, and D. Ponomarev. Nonmonopolizable caches: Low-complexity mitigation of cache side channel attacks. Transactions on Architecture and Code Optimization (TACO), 2012.
    Google ScholarLocate open access versionFindings
  • S. Embleton, S. Sparks, and C. C. Zou. SMM rootkit: a new breed of OS independent malware. Security and Communication Networks, 6(12):1590–1605, 2013.
    Google ScholarLocate open access versionFindings
  • C. W. Fletcher, M. v. Dijk, and S. Devadas. A Secure Processor Architecture for Encrypted Computation on Untrusted Programs. In Proceedings of the Seventh ACM Workshop on Scalable Trusted Computing, pages 3–8. ACM, 2012.
    Google ScholarLocate open access versionFindings
  • J. A. Goguen and J. Meseguer. Security Policies and Security Models. In 1982 IEEE Symposium on Security and Privacy, Oakland, CA, USA, April 26-28, 1982, pages 11–20, 1982.
    Google ScholarLocate open access versionFindings
  • D. Grawrock. Dynamics of a Trusted Platform: A building block approach. Intel Press, 2009.
    Google ScholarFindings
  • 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 Proceedings of the 11th USENIX conference on Operating Systems Design and Implementation, pages 165–181, 2014.
    Google ScholarLocate open access versionFindings
  • M. P. Herlihy and J. M. Wing. Linearizability: A Correctness Condition for Concurrent Objects. ACM Transactions on Programming Languages and Systems, 12(3):463–492, July 1990.
    Google ScholarLocate open access versionFindings
  • M. Hoekstra, R. Lal, P. Pappachan, V. Phegade, and J. Del Cuvillo. Using Innovative Instructions to Create Trustworthy Software Solutions. In Proceedings of the 2nd International Workshop on Hardware and Architectural Support for Security and Privacy, HASP, volume 13, 2013.
    Google ScholarLocate open access versionFindings
  • Intel Software Guard Extensions Programming Reference. Available at https:
    Google ScholarFindings
  • G. Irazoqui, T. Eisenbarth, and B. Sunar. SA: A Shared Cache Attack That Works across Cores and Defies VM Sandboxing – and Its Application to AES. In IEEE Symposium on Security and Privacy, pages 591–604, May 2015.
    Google ScholarLocate open access versionFindings
  • Joanna Rutkowska. Red Pill... or how to detect VMM using (almost) one CPU instruction. https://github.com/Cr4sh/ThinkPwn.git.
    Findings
  • G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal Verification of an OS Kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP ’09, pages 207–220, New York, USA, 2009.
    Google ScholarLocate open access versionFindings
  • P. C. Kocher. Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In Proceedings of the 16th Annual International Cryptology Conference on Advances in Cryptology, CRYPTO ’96, pages 104–113, London, UK, UK, 1996. Springer-Verlag.
    Google ScholarLocate open access versionFindings
  • S. Lee, M. Shih, P. Gera, T. Kim, H. Kim, and M. Peinado. Inferring Fine-grained Control Flow Inside SGX Enclaves with Branch Shadowing. CoRR, abs/1611.06952, 2016.
    Findings
  • R. Leslie-Hurd, D. Caspi, and M. Fernandez. Verifying Linearizability of Intel® Software Guard Extensions. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, pages 144–160, 2015.
    Google ScholarLocate open access versionFindings
  • X. Li, V. Kashyap, J. K. Oberg, M. Tiwari, V. R. Rajarathinam, R. Kastner, T. Sherwood, B. Hardekopf, and F. T. Chong. Sapper: A Language for Hardware-Level Security Policy Enforcement. In Architectural Support for Programming Languages and Operating Systems, ASPLOS ’14, Salt Lake City, UT, USA, March 1-5, 2014, pages 97–112, 2014.
    Google ScholarFindings
  • X. Li, M. Tiwari, J. Oberg, V. Kashyap, F. T. Chong, T. Sherwood, and B. Hardekopf. Caisson: A Hardware Description Language for Secure Information Flow. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, pages 109–120, 2011.
    Google ScholarLocate open access versionFindings
  • D. Lie, C. Thekkath, M. Mitchell, P. Lincoln, D. Boneh, J. Mitchell, and M. Horowitz. Architectural support for copy and tamper resistant software. ACM SIGPLAN Notices, 35(11):168–177, 2000.
    Google ScholarLocate open access versionFindings
  • F. Liu, Q. Ge, Y. Yarom, F. Mckeen, C. Rozas, G. Heiser, and R. B. Lee. CATalyst: Defeating Last-Level Cache Side Channel Attacks in Cloud Computing. In 2016 IEEE International Symposium on High Performance Computer Architecture (HPCA), Mar 2016.
    Google ScholarLocate open access versionFindings
  • F. Liu and R. B. Lee. Random Fill Cache Architecture. In 2014 47th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO). IEEE, 2014.
    Google ScholarLocate open access versionFindings
  • F. Liu, Y. Yarom, Q. Ge, G. Heiser, and R. B. Lee. Last-Level Cache Side-Channel Attacks Are Practical. In Proceedings of the 2015 IEEE Symposium on Security and Privacy, pages 605–622, Washington, DC, USA, 2015. IEEE Computer Society.
    Google ScholarLocate open access versionFindings
  • M. Maas, E. Love, E. Stefanov, M. Tiwari, E. Shi, K. Asanovic, J. Kubiatowicz, and D. Song. Phantom: Practical oblivious computation in a secure processor. In Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security, pages 311–324. ACM, 2013.
    Google ScholarLocate open access versionFindings
  • 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. HASP, 13:10, 2013.
    Google ScholarLocate open access versionFindings
  • J. Mclean. Proving Noninterference and Functional Correctness Using Traces. Journal of Computer Security, 1:37–58, 1992.
    Google ScholarLocate open access versionFindings
  • A. Moghimi, G. Irazoqui, and T. Eisenbarth. CacheZoom: How SGX Amplifies The Power of Cache Attacks. CoRR, abs/1703.06986, 2017.
    Findings
  • G. Morrisett, G. Tan, J. Tassarotti, J. Tristan, and E. Gan. RockSalt: better, faster, stronger SFI for the x86. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, Beijing, China - June 11 - 16, 2012, pages 395–404, 2012.
    Google ScholarLocate open access versionFindings
  • 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 Security and Privacy (SP), 2013 IEEE Symposium on, pages 415–429. IEEE, 2013.
    Google ScholarLocate open access versionFindings
  • M. Neugschwandtner, C. Platzer, P. M. Comparetti, and U. Bayer. dAnubis Dynamic Device Driver Analysis Based on Virtual Machine Introspection. In Detection of Intrusions and Malware, and Vulnerability Assessment, 7th International Conference, DIMVA 2010, Bonn, Germany, July 8-9, 2010. Proceedings, pages 41–60, 2010.
    Google ScholarLocate open access versionFindings
  • T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283. Springer Science & Business Media, 2002.
    Google ScholarLocate open access versionFindings
  • J. Noorman, P. Agten, W. Daniels, R. Strackx, A. Van Herrewege, C. Huygens, B. Preneel, I. Verbauwhede, and F. Piessens. Sancus: Low-cost Trustworthy Extensible Networked Devices with a Zero-software Trusted Computing Base. In Proceedings of the 22Nd USENIX Conference on Security, SEC’13, pages 479–494, Berkeley, CA, USA, 2013. USENIX Association.
    Google ScholarLocate open access versionFindings
  • 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 (USENIX Security 16), pages 619–636, Austin, TX, 2016. USENIX Association.
    Google ScholarLocate open access versionFindings
  • Y. Oren, V. P. Kemerlis, S. Sethumadhavan, and A. D. Keromytis. The Spy in the Sandbox - Practical Cache Attacks in Javascript. CoRR, abs/1502.07373, 2015.
    Findings
  • B. Parno, J. R. Lorch, J. R. Douceur, J. Mickens, and J. M. McCune. Memoir: Practical State Continuity for Protected Modules. In Proceedings of the 2011 IEEE Symposium on Security and Privacy, SP ’11, pages 379–394, Washington, DC, USA, 2011. IEEE Computer Society.
    Google ScholarLocate open access versionFindings
  • R. Pass, E. Shi, and F. Tramèr. Formal Abstractions for Attested Execution Secure Processors. IACR Cryptology ePrint Archive, 2016:1027, 2016.
    Google ScholarLocate open access versionFindings
  • M. Patrignani, P. Agten, R. Strackx, B. Jacobs, D. Clarke, and F. Piessens. Secure Compilation to Protected Module Architectures. ACM Trans. Program. Lang. Syst., 37(2):6:1–6:50, 2015.
    Google ScholarLocate open access versionFindings
  • M. Patrignani and D. Clarke. Fully abstract trace semantics for low-level isolation mechanisms. In Symposium on Applied Computing, SAC 2014, Gyeongju, Republic of Korea - March 24 - 28, 2014, pages 1562–1569, 2014.
    Google ScholarLocate open access versionFindings
  • M. Patrignani and D. Clarke. Fully abstract trace semantics for protected module architectures. Computer Languages, Systems & Structures, 42:22–45, 2015.
    Google ScholarLocate open access versionFindings
  • A. W. Roscoe. CSP and determinism in security modelling. In Proceedings of the 1995 IEEE Symposium on Security and Privacy, Oakland, California, USA, May 8-10, 1995, pages 114–127, 1995.
    Google ScholarLocate open access versionFindings
  • J. M. Rushby. Proof of separability: A verification technique for a class of a security kernels. In International Symposium on Programming, 5th Colloquium, Torino, Italy, April 6-8, 1982, Proceedings, pages 352–367, 1982.
    Google ScholarLocate open access versionFindings
  • [65] A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5–19, 2003.
    Google ScholarLocate open access versionFindings
  • [66] M. Schwarz, S. Weiser, D. Gruss, C. Maurice, and S. Mangard. Malware Guard Extension: Using SGX to Conceal Cache Attacks. CoRR, abs/1702.08719, 2017.
    Findings
  • [67] J. Seo, B. Lee, S. Kim, M.-W. Shih, I. Shin, D. Han, and T. Kim. SGX-Shield: Enabling address space layout randomization for SGX programs. In 23nd Annual Network and Distributed System Security Symposium, NDSS 2017, San Diego, California, USA, February 26-Marc 1, 2017, 2017.
    Google ScholarLocate open access versionFindings
  • [68] M.-W. Shih, S. Lee, T. Kim, and M. Peinado. T-SGX: Eradicating ControlledChannel Attacks Against Enclave Programs. In Proceedings of the 2017 Annual Network and Distributed System Security Symposium (NDSS), San Diego, CA, Feb. 2017.
    Google ScholarLocate open access versionFindings
  • [69] S. Shinde, Z. L. Chua, V. Narayanan, and P. Saxena. Preventing Page Faults from Telling Your Secrets. In Proceedings of the 11th ACM on Asia Conference on Computer and Communications Security, AsiaCCS 2016, Xi’an, China, May 30 June 3, 2016, pages 317–328, 2016.
    Google ScholarLocate open access versionFindings
  • [70] R. Sinha, M. Costa, A. Lal, N. P. Lopes, S. K. Rajamani, S. A. Seshia, and K. Vaswani. A Design and Verification Methodology for Secure Isolated Regions. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 665–681, 2016.
    Google ScholarLocate open access versionFindings
  • [71] R. Sinha, S. K. Rajamani, S. A. Seshia, and K. Vaswani. Moat: Verifying Confidentiality of Enclave Programs. In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, Denver, CO, USA, October 12-6, 2015, pages 1169–1184, 2015.
    Google ScholarLocate open access versionFindings
  • [72] T. Skolem. Logico-combinatorial investigations in the satisfiability or provability of mathematical propositions: a simplified proof of a theorem by L. Löwenheim and generalizations of the theorem. From Frege to Gödel. A Source Book in Mathematical Logic, 1879-1931, pages 252–263, 1967.
    Google ScholarLocate open access versionFindings
  • [73] G. Smith and D. M. Volpano. Secure Information Flow in a Multi-Threaded Imperative Language. In POPL ’98, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 19-21, 1998, pages 355–364, 1998.
    Google ScholarLocate open access versionFindings
  • [74] R. Strackx and F. Piessens. Fides: Selectively Hardening Software Application Components Against Kernel-level or Process-level Malware. In Proceedings of the 2012 ACM Conference on Computer and Communications Security, CCS ’12, pages 2–13, New York, NY, USA, 2012. ACM.
    Google ScholarLocate open access versionFindings
  • [75] P. Subramanyan, R. Sinha, I. Lebedev, S. Devadas, and S. A. Seshia. Models and https://github.com/0tcb/TAP.
    Locate open access versionFindings
  • [76] G. E. Suh, D. Clarke, B. Gassend, M. Van Dijk, and S. Devadas. AEGIS: architecture for tamper-evident and tamper-resistant processing. In Proceedings of the 17th annual international conference on Supercomputing, pages 160–171. ACM, 2003.
    Google ScholarLocate open access versionFindings
  • [77] T. Terauchi and A. Aiken. Secure Information Flow as a Safety Problem. In Static Analysis Symposium (SAS ’05), LNCS 3672, pages 352–367, 2005.
    Google ScholarLocate open access versionFindings
  • [78] E. Tromer, D. A. Osvik, and A. Shamir. Efficient Cache Attacks on AES, and Countermeasures. J. Cryptology, 23(1):37–71, 2010.
    Google ScholarLocate open access versionFindings
  • [79] M. Vijayaraghavan, A. Chlipala, Arvind, and N. Dave. Modular Deductive Verification of Multiprocessor Hardware Designs. In Computer Aided Verification 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, pages 109–127, 2015.
    Google ScholarLocate open access versionFindings
  • [80] D. Volpano, C. Irvine, and G. Smith. A Sound Type System for Secure Flow Analysis. Journal of Computer Security, 4(2-3):167–187, Jan. 1996.
    Google ScholarLocate open access versionFindings
  • [81] A. Waterman, Y. Lee, R. Avizienis, D. A. Patterson, and K. Asanović. The RISC-V Instruction Set Manual Volume II: Privileged Architecture Version 1.9.1. Technical Report UCB/EECS-2016-161, EECS Department, University of California, Berkeley, Nov 2016.
    Google ScholarFindings
  • [82] A. Waterman, Y. Lee, D. A. Patterson, and K. Asanović. The RISC-V Instruction 2014-54, EECS Department, University of California, Berkeley, May 2014.
    Google ScholarFindings
  • [83] Y. Xu, W. Cui, and M. Peinado. Controlled-Channel Attacks: Deterministic Side Channels for Untrusted Operating Systems. In 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015, pages 640–656, 2015.
    Google ScholarLocate open access versionFindings
  • [84] Y. Yarom and K. Falkner. FLUSH+RELOAD: A High Resolution, Low Noise, L3 Cache Side-Channel Attack. In Proceedings of the 23rd USENIX Security Symposium, San Diego, CA, USA, August 20-22, 2014., pages 719–732, 2014.
    Google ScholarLocate open access versionFindings
  • [85] D. Zhang, Y. Wang, G. E. Suh, and A. C. Myers. A Hardware Design Language for Timing-Sensitive Information-Flow Security. In Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS ’15, Istanbul, Turkey, March 14-18, 2015, pages 503–516, 2015.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科