article

A design and verification methodology for secure isolated regions

Authors:

Sriram Rajamani,

Sanjit A. Seshia,

Kapil VaswaniAuthors Info & Claims

ACM SIGPLAN Notices, Volume 51, Issue 6

Pages 665 - 681

https://doi.org/10.1145/2980983.2908113

Published: 02 June 2016 Publication History

Abstract

Hardware support for isolated execution (such as Intel SGX) enables development of applications that keep their code and data confidential even while running in a hostile or compromised host. However, automatically verifying that such applications satisfy confidentiality remains challenging. We present a methodology for designing such applications in a way that enables certifying their confidentiality. Our methodology consists of forcing the application to communicate with the external world through a narrow interface, compiling it with runtime checks that aid verification, and linking it with a small runtime that implements the narrow interface. The runtime includes services such as secure communication channels and memory management. We formalize this restriction on the application as Information Release Confinement (IRC), and we show that it allows us to decompose the task of proving confidentiality into (a) one-time, human-assisted functional verification of the runtime to ensure that it does not leak secrets, (b) automatic verification of the application's machine code to ensure that it satisfies IRC and does not directly read or corrupt the runtime's internal state. We present /CONFIDENTIAL: a verifier for IRC that is modular, automatic, and keeps our compiler out of the trusted computing base. Our evaluation suggests that the methodology scales to real-world applications.

References

[1]

https://slashconfidential.github.io.

[2]

M. Abadi, M. Budiu, U. Erlingsson, and J. Ligatti. Control-flow integrity. In CCS, 2005.

Digital Library

[3]

ARM Security Technology - Building a Secure System using Trust-Zone Technology. ARM Technical White Paper.

[4]

M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In FMCO, 2005.

Digital Library

[5]

C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi´c, T. King, A. Reynolds, and C. Tinelli. CVC4. In CAV, 2011.

Digital Library

[6]

S. Bauer, P. Cuoq, and J. Regehr. Deniable backdoors using compiler bugs. International Journal of PoC||GTFO, 0x08:7–9, June 2015.

[7]

D. E. Bell and L. J. LaPadula. Secure computer system: Unified exposition and multics interpretation. Technical Report MTR-2997, MITRE Corp., 1975.

[8]

K. J. Biba. Integrity considerations for secure computer systems. Technical Report ESD-TR-76-372, USAF Electronic Systems Division, 1977.

[9]

J. Black, J. Rogaway, and T. Shrimpton. Encryption-scheme security in the presence of key-dependent messages. In SAC, 2002.

Digital Library

[10]

D. Brumley, I. Jager, T. Avgerinos, and E. J. Schwartz. BAP: A binary analysis platform. In CAV, 2011.

Digital Library

[11]

X. Chen, T. Garfinkel, E. C. Lewis, P. Subrahmanyam, C. A. Waldspurger, D. Boneh, J. Dwoskin, and D. R. Ports. Overshadow: A virtualization-based approach to retrofitting protection in commodity operating systems. In ASPLOS, 2008.

Digital Library

[12]

M. R. Clarkson and F. B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157–1210, Sept. 2010.

Digital Library

[13]

J. Criswell, N. Dautenhahn, and V. Adve. Virtual ghost: Protecting applications from hostile operating systems. In ASPLOS, 2014.

Digital Library

[14]

L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, 2008.

Digital Library

[15]

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.

[16]

D. E. Denning. A lattice model of secure information flow. Communications of the ACM, 19(5):236–243, 1976.

Digital Library

[17]

D. E. Denning and P. J. Denning. Certification of programs for secure information flow. Communications of the ACM, 20(7):504–513, 1977.

Digital Library

[18]

U. Erlingsson, M. Abadi, M. Vrable, M. Budiu, and G. Necula. XFI: software guards for system address spaces. In OSDI, 2006.

Digital Library

[19]

A. Fontaine, P. Chifflier, and T. Coudray. Picon : Control flow integrity on llvm ir. In SSTIC, 2015.

[20]

O. S. Hofmann, S. Kim, A. M. Dunn, M. Z. Lee, and E. Witchel. InkTag: Secure applications on an untrusted operating system. In ASPLOS, 2013.

Digital Library

[21]

Intel Software Guard Extensions Programming Reference. Available at https://software.intel.com/sites/default/ files/329298-001.pdf, 2014.

[22]

B. Lampson. A note on the confinment problem. Communications of the ACM, 16(10), 1976.

Digital Library

[23]

V. Le, M. Afshari, and Z. Su. Compiler validation via equivalence modulo inputs. In PLDI, 2014.

Digital Library

[24]

D. Lie, C. Thekkath, M. Mitchell, P. Lincoln, D. Boneh, J. Mitchell, and M. Horowitz. Architectural support for copy and tamper resistant software. In ASPLOS, 2000.

Digital Library

[25]

C. Liu, A. Harris, M. Maas, M. Hicks, M. Tiwari, and E. Shi. Ghostrider: A hardware-software system for memory trace oblivious computation. In ASPLOS, 2015.

Digital Library

[26]

N. P. Lopes, D. Menendez, S. Nagarakatte, and J. Regehr. Provably correct peephole optimizations with Alive. In PLDI, 2015.

Digital Library

[27]

S. McCamant and G. Morrisett. Evaluating SFI for a CISC architecture. In Usenix Security, 2008.

Digital Library

[28]

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 HASP, 2013.

Digital Library

[29]

R. Morisset, P. Pawan, and F. Z. Nardelli. Compiler testing via a theory of sound optimisations in the C11/C++11 memory model. In PLDI, 2013.

Digital Library

[30]

G. Morrisett, G. Tan, J. Tassarotti, J.-B. Tristan, and E. Gan. RockSalt: better, faster, stronger SFI for the x86. In PLDI, 2012.

Digital Library

[31]

A. C. Myers and B. Liskov. A decentralized model for information flow control. In SOSP, 1997.

Digital Library

[32]

G. C. Necula. Translation validation for an optimizing compiler. In PLDI, 2000.

Digital Library

[33]

B. Niu and G. Tan. Modular control flow integrity. In PLDI, 2014.

Digital Library

[34]

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 zerosoftware trusted computing base. In USENIX Security, 2013.

Digital Library

[35]

A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In TACAS, 1998.

Digital Library

[36]

A. Sabelfeld and A. C. Myers. Language-based information-flow security. Selected Areas in Communications, IEEE Journal on, 21(1):5– 19, 2003.

Digital Library

[37]

J. H. Saltzer and M. D. Schroeder. Formal verification of a realistic compiler. Proceedings of the IEEE, 63(9):1278–1308, 1975.

[38]

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 S&P, 2015.

Digital Library

[39]

D. Sehr, R. Muth, C. L. Biffle, V. Khimenko, E. Pasko, B. Yee, K. Schimpf, and B. Chen. Adapting software fault isolation to contemporary CPU architectures. In Usenix Security, 2010.

Digital Library

[40]

R. Sinha, S. Rajamani, S. Seshia, and K. Vaswani. Moat: Verifying confidentiality of enclave programs. In CCS, 2015.

Digital Library

[41]

M. Stepp, R. Tate, and S. Lerner. Equality-based translation validator for LLVM. In CAV, 2011.

Digital Library

[42]

J.-B. Tristan, P. Govereau, and G. Morrisett. Evaluating value-graph translation validation for LLVM. In PLDI, 2011.

Digital Library

[43]

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.

Digital Library

[44]

R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham. Efficient software-based fault isolation. In SOSP, 1993.

Digital Library

[45]

J. Yang and K. G. Shin. Using hypervisor to provide data secrecy for user applications on a per-page basis. In VEE, 2008.

Digital Library

[46]

X. Yang, Y. Chen, E. Eide, and J. Regehr. Finding and understanding bugs in C compilers. In PLDI, 2011.

Digital Library

[47]

B. Yee, D. Sehr, G. Dardyk, B. Chen, R. Muth, T. Ormandy, S. Okasaka, N. Narula, and N. Fullagar. Native client: A sandbox for portable, untrusted x86 native code. In S&P, 2009.

Digital Library

[48]

B. Zeng, G. Tan, and G. Morrisett. Combining control-flow integrity and static analysis for efficient and validated data sandboxing. In CCS, 2011.

Digital Library

[49]

L. Zhao, G. Li, B. D. Sutter, and J. Regehr. Armor: Fully verified software fault isolation. In EMSOFT, 2011.

Digital Library

Cited By

Derakhshan FZhang ZVasudevan AJia L(2023)Towards End-to-End Verified TEEs via Verified Interface Conformance and Certified Compilers2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00021(324-339)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00021
Guo YWang ZZhong BZeng Q(2022)Formal Modeling and Security Analysis for Intra-level Privilege SeparationProceedings of the 38th Annual Computer Security Applications Conference10.1145/3564625.3567984(88-101)Online publication date: 5-Dec-2022
https://dl.acm.org/doi/10.1145/3564625.3567984
Yang LChen YHajiesmaili MHerbster MTowsley D(2022)Hierarchical Learning Algorithms for Multi-scale Expert ProblemsProceedings of the ACM on Measurement and Analysis of Computing Systems10.1145/35309006:2(1-29)Online publication date: 6-Jun-2022
https://dl.acm.org/doi/10.1145/3530900
Show More Cited By

Recommendations

A Formal Foundation for Secure Remote Execution of Enclaves
CCS '17: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security

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 ...
Moat: Verifying Confidentiality of Enclave Programs
CCS '15: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security

Security-critical applications constantly face threats from exploits in lower computing layers such as the operating system, virtual machine monitors, or even attacks from malicious administrators. To help protect application secrets from such attacks, ...
A design and verification methodology for secure isolated regions
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation

Hardware support for isolated execution (such as Intel SGX) enables development of applications that keep their code and data confidential even while running in a hostile or compromised host. However, automatically verifying that such applications ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 51, Issue 6

PLDI '16

June 2016

726 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2980983

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2016
726 pages
ISBN:9781450342612
DOI:10.1145/2908080
General Chair:
Chandra Krintz
University of California at Santa Barbara, USA
,
Program Chair:
Emery Berger
University of Massachusetts at Amherst, USA

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 June 2016

Published in SIGPLAN Volume 51, Issue 6

Check for updates

Author Tags

Qualifiers

Article

Funding Sources

NSF
SRC

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

53
Total Citations
View Citations
581
Total Downloads

Downloads (Last 12 months)18
Downloads (Last 6 weeks)5

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Derakhshan FZhang ZVasudevan AJia L(2023)Towards End-to-End Verified TEEs via Verified Interface Conformance and Certified Compilers2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00021(324-339)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00021
Guo YWang ZZhong BZeng Q(2022)Formal Modeling and Security Analysis for Intra-level Privilege SeparationProceedings of the 38th Annual Computer Security Applications Conference10.1145/3564625.3567984(88-101)Online publication date: 5-Dec-2022
https://dl.acm.org/doi/10.1145/3564625.3567984
Yang LChen YHajiesmaili MHerbster MTowsley D(2022)Hierarchical Learning Algorithms for Multi-scale Expert ProblemsProceedings of the ACM on Measurement and Analysis of Computing Systems10.1145/35309006:2(1-29)Online publication date: 6-Jun-2022
https://dl.acm.org/doi/10.1145/3530900
Xiao YVarvello MKuzmanovic A(2022)Monetizing Spare BandwidthProceedings of the ACM on Measurement and Analysis of Computing Systems10.1145/35308996:2(1-27)Online publication date: 6-Jun-2022
https://dl.acm.org/doi/10.1145/3530899
Hsieh HJiang JYang THu RWu C(2022)Predicting the Success of Mediation Requests Using Case Properties and Textual Information for Reducing the Burden on the CourtDigital Government: Research and Practice10.1145/34692332:4(1-18)Online publication date: 6-Jan-2022
https://dl.acm.org/doi/10.1145/3469233
Anthopoulos LSirakoulis KReddick C(2022)Conceptualizing Smart Government: Interrelations and Reciprocities with Smart CityDigital Government: Research and Practice10.1145/34650612:4(1-28)Online publication date: 6-Jan-2022
https://dl.acm.org/doi/10.1145/3465061
Antonino PWoloszyn WRoscoe AZhang Yvan Dijk M(2021)GuardianProceedings of the 2021 on Cloud Computing Security Workshop10.1145/3474123.3486755(111-123)Online publication date: 15-Nov-2021
https://dl.acm.org/doi/10.1145/3474123.3486755
Sabogal SGeorge ACrum G(2021)Reconfigurable Framework for Resilient Semantic Segmentation for Space ApplicationsACM Transactions on Reconfigurable Technology and Systems10.1145/347277014:4(1-32)Online publication date: 13-Sep-2021
https://dl.acm.org/doi/10.1145/3472770
Romero Hung JLi CWang PShao CGuo JWang JShi G(2021)ACE-GCN: A Fast Data-driven FPGA Accelerator for GCN EmbeddingACM Transactions on Reconfigurable Technology and Systems10.1145/347053614:4(1-23)Online publication date: 13-Sep-2021
https://dl.acm.org/doi/10.1145/3470536
Liu WWang WChen HWang XLu YChen KWang XShen QChen YTang H(2021)Practical and Efficient in-Enclave Verification of Privacy Compliance2021 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)10.1109/DSN48987.2021.00052(413-425)Online publication date: Jun-2021
https://doi.org/10.1109/DSN48987.2021.00052
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents