More Web Proxy on the site http://driver.im/

research-article

Open access

The high-level benefits of low-level sandboxing

Authors:

Michael Sammler,

Tadeusz LitakAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 4, Issue POPL

Article No.: 32, Pages 1 - 32

https://doi.org/10.1145/3371100

Published: 20 December 2019 Publication History

Abstract

Sandboxing is a common technique that allows low-level, untrusted components to safely interact with trusted code. However, previous work has only investigated the low-level memory isolation guarantees of sandboxing, leaving open the question of the end-to-end guarantees that sandboxing affords programmers. In this paper, we fill this gap by showing that sandboxing enables reasoning about the known concept of robust safety, i.e., safety of the trusted code even in the presence of arbitrary untrusted code. To do this, we first present an idealized operational semantics for a language that combines trusted code with untrusted code. Sandboxing is built into our semantics. Then, we prove that safety properties of the trusted code (as enforced through a rich type system) are upheld in the presence of arbitrary untrusted code, so long as all interactions with untrusted code occur at the “any” type (a type inhabited by all values). Finally, to alleviate the burden of having to interact with untrusted code at only the “any” type, we formalize and prove safe several wrappers, which automatically convert values between the “any” type and much richer types. All our results are mechanized in the Coq proof assistant.

Supplementary Material

WEBM File (a32-sammler.webm)

Download
91.38 MB

References

[1]

Martín Abadi. 1997. Secrecy by typing in security protocols. In Theoretical Aspects of Computer Software, Third International Symposium, TACS ’97, Sendai, Japan, September 23-26, 1997, Proceedings (Lecture Notes in Computer Science), Martín Abadi and Takayasu Ito (Eds.), Vol. 1281. Springer, 611–638.

[2]

Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Catalin Hritcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, and Andrew Tolmach. 2018. When good components go bad: Formally secure compilation despite dynamic compromise. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018. 1351–1368.

Digital Library

[3]

R.P. Abbott, J. S. Chin, J. E. Donnelley, W. L. Konigsford, S. Tokubo, and D. A. Webb. 1976. Security analysis and enhancements of computer operating systems. Technical Report. Institute for Computer Sciences and Technology, National Bureau of Standards, Washington,D.C. https://nvlpubs.nist.gov/nistpubs/Legacy/IR/nbsir76- 1041.pdf

[4]

Amal Ahmed, Andrew W. Appel, Christopher D. Richards, Kedar N. Swadi, Gang Tan, and Daniel C. Wang. 2010. Semantic foundations for typed assembly languages. ACM Trans. Program. Lang. Syst. 32, 3 (2010), 7:1–7:67.

Digital Library

[5]

ARM Limited. 2009. ARM Security Technology. Technical Report. http://infocenter.arm.com/help/topic/com.arm.doc.prd29-genc- 009492c/PRD29- GENC- 009492C_trustzone_security_whitepaper.pdf

[6]

David A. Basin, Vincent Jugé, Felix Klaedtke, and Eugen Zalinescu. 2013. Enforceable security policies revisited. ACM Trans. Inf. Syst. Secur. 16, 1 (2013), 3:1–3:26.

Digital Library

[7]

Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas P. Jensen, and Pierre Wilke. 2019. Compiling sandboxes: Formally verified software fault isolation. In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings. 499–524.

[8]

Matthias Blume and David A. McAllester. 2004. A sound (and complete) model of contracts. In Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, ICFP 2004, Snow Bird, UT, USA, September 19-21, 2004, Chris Okasaki and Kathleen Fisher (Eds.). ACM, 189–200.

Digital Library

[9]

Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, and Matteo Maffei. 2011. Resource-aware authorization policies for statically typed cryptographic protocols. In Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, 27-29 June, 2011. IEEE Computer Society, 83–98.

Digital Library

[10]

Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Catalin Hritcu, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. 2015. Micro-policies: Formally verified, tag-based security monitors. In 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015. IEEE Computer Society, 813–830.

Digital Library

[11]

Arthur Azevedo de Amorim, Catalin Hritcu, and Benjamin C. Pierce. 2018. The meaning of memory safety. In Principles of Security and Trust - 7th International Conference, POST 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings (Lecture Notes in Computer Science), Lujo Bauer and Ralf Küsters (Eds.), Vol. 10804. Springer, 79–105.

[12]

Akram El-Korashy. 2016. A Formal Model for Capability Machines: An Illustrative Case Study towards Secure Compilation to CHERI. Master’s thesis. Universität des Saarlandes. http://hdl.handle.net/11858/00- 001M- 0000- 002C- 41CA- B

[13]

Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for higher-order functions. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002., Mitchell Wand and Simon L. Peyton Jones (Eds.). ACM, 48–59.

Digital Library

[14]

Cormac Flanagan. 2006. Hybrid type checking. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, J. Gregory Morrisett and Simon L. Peyton Jones (Eds.). ACM, 245–256.

Digital Library

[15]

Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. 2007. A type discipline for authorization policies. ACM Trans. Program. Lang. Syst. 29, 5 (2007), 25.

Digital Library

[16]

Timothy S. Freeman and Frank Pfenning. 1991. Refinement types for ML. In Proceedings of the ACM SIGPLAN’91 Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28, 1991, David S. Wise (Ed.). ACM, 268–277.

Digital Library

[17]

Google. 2019. Sandboxed Api. https://github.com/google/sandboxed- api .

[18]

Andrew D. Gordon and Alan Jeffrey. 2001. Authenticity by typing for security protocols. In 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada. 145–159.

[19]

Orna Grumberg and David E. Long. 1994. Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16, 3 (1994), 843–871.

Digital Library

[20]

Norman Hardy. 1988. The confused deputy (or why capabilities might have been invented). Operating Systems Review 22, 4 (1988), 36–38.

Digital Library

[21]

Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. 2017. On polymorphic gradual typing. PACMPL 1, ICFP (2017), 40:1–40:29.

Digital Library

[22]

Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Boris Eng, and Benjamin C. Pierce. 2016. Beyond good and evil: Formalizing the security guarantees of compartmentalizing compilation. In IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016. 45–60.

[23]

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018a. Rustbelt: Securing the foundations of the Rust programming language. PACMPL 2, POPL (2018), 66:1–66:34.

Digital Library

[24]

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018b. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018), e20.

[25]

Koen Koning, Xi Chen, Herbert Bos, Cristiano Giuffrida, and Elias Athanasopoulos. 2017. No need to hide: Protecting safe regions on commodity hardware. In Proceedings of the Twelfth European Conference on Computer Systems, EuroSys 2017, Belgrade, Serbia, April 23-26, 2017, Gustavo Alonso, Ricardo Bianchini, and Marko Vukolic (Eds.). ACM, 437–452.

Digital Library

[26]

Benjamin Lamowski, Carsten Weinhold, Adam Lackorzynski, and Hermann Härtig. 2017. Sandcrust: Automatic sandboxing of unsafe components in Rust. In Proceedings of the 9th Workshop on Programming Languages and Operating Systems, Shanghai, China, October 28, 2017, Julia Lawall (Ed.). ACM, 51–57.

Digital Library

[27]

Nico Lehmann and Éric Tanter. 2017. Gradual refinement types. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. 775–788. http://dl.acm.org/citation. cfm?id=3009856

[28]

Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. 2012. The CompCert Memory Model, Version 2. Research report RR-7987. INRIA. http://hal.inria.fr/hal- 00703441

[29]

James Litton, Anjo Vahldiek-Oberwagner, Eslam Elnikety, Deepak Garg, Bobby Bhattacharjee, and Peter Druschel. 2016. Light-weight contexts: An OS abstraction for safety and performance. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016., Kimberly Keeton and Timothy Roscoe (Eds.). USENIX Association, 49–64. https://www.usenix.org/conference/osdi16/technical- sessions/presentation/litton

[30]

Frank McKeen, Ilya Alexandrovich, Alex Berenzon, Carlos V. Rozas, Hisham Shafi, Vedvyas Shanbhogue, and Uday R. Savagaonkar. 2013. Innovative instructions and software model for isolated execution. In HASP 2013, The Second Workshop on Hardware and Architectural Support for Security and Privacy, Tel-Aviv, Israel, June 23-24, 2013, Ruby B. Lee and Weidong Shi (Eds.). ACM, 10.

Digital Library

[31]

James H. Morris, Jr. 1973. Protection in programming languages. Commun. ACM 16, 1 (1973), 15–21.

Digital Library

[32]

Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, and Edward Gan. 2012. 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. 395–404.

Digital Library

[33]

Mozilla. 2019. Script security. Technical Report. https://developer.mozilla.org/en- US/docs/Mozilla/Gecko/Script_security

[34]

Max S. New and Amal Ahmed. 2018. Graduality from embedding-projection pairs. PACMPL 2, ICFP (2018), 73:1–73:30.

Digital Library

[35]

Michael Sammler, Deepak Garg, Derek Dreyer, and Tadeusz Litak. 2019. The high-level benefits of low-level sandboxing – Artifact.

Digital Library

[36]

Fred B. Schneider. 2000. Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3, 1 (2000), 30–50.

Digital Library

[37]

Jeremy G. Siek and Walid Taha. 2006. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, Vol. 6. 81–92.

[38]

David Swasey, Deepak Garg, and Derek Dreyer. 2017. Robust and compositional verification of object capability patterns. PACMPL 1, OOPSLA (2017), 89:1–89:26.

Digital Library

[39]

The Rust Developers. 2019. The Rust programming language. https://rust- lang.org .

[40]

Jesse A. Tov and Riccardo Pucella. 2010. Stateful contracts for affine types. In Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings (Lecture Notes in Computer Science), Andrew D. Gordon (Ed.), Vol. 6012. Springer, 550–569.

Digital Library

[41]

Anjo Vahldiek-Oberwagner, Eslam Elnikety, Nuno O. Duarte, Michael Sammler, Peter Druschel, and Deepak Garg. 2019. ERIM: Secure, efficient in-process isolation with protection keys (MPK). In 28th USENIX Security Symposium, USENIX Security 2019, Santa Clara, CA, USA, August 14-16, 2019, Nadia Heninger and Patrick Traynor (Eds.). USENIX Association, 1221–1238. https://www.usenix.org/conference/usenixsecurity19/presentation/vahldiek- oberwagner

[42]

Thomas Van Strydonck, Frank Piessens, and Dominique Devriese. 2019. Linear capabilities for fully abstract compilation of separation-logic-verified code. Proc. ACM Program. Lang. 3, ICFP, Article 84 (July 2019), 29 pages.

Digital Library

[43]

Philip Wadler and Robert Bruce Findler. 2009. Well-typed programs can’t be blamed. In Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. 1–16.

Digital Library

[44]

Hongwei Xi and Frank Pfenning. 1998. Eliminating array bound checking through dependent types. In Proceedings of the ACM SIGPLAN ’98 Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada, June 17-19, 1998, Jack W. Davidson, Keith D. Cooper, and A. Michael Berman (Eds.). ACM, 249–257.

Digital Library

[45]

Bennet Yee, David Sehr, Gregory Dardyk, J. Bradley Chen, Robert Muth, Tavis Ormandy, Shiki Okasaka, Neha Narula, and Nicholas Fullagar. 2009. Native Client: A sandbox for portable, untrusted x86 native code. In 30th IEEE Symposium on Security and Privacy (S&P 2009), 17-20 May 2009, Oakland, California, USA. IEEE Computer Society, 79–93.

Digital Library

Cited By

Timany AKrebbers RDreyer DBirkedal L(2024)A Logical Approach to Type SoundnessJournal of the ACM10.1145/367695471:6(1-75)Online publication date: 11-Nov-2024
https://dl.acm.org/doi/10.1145/3676954
Zhang JLuo BLiao XXu JKirda ELie D(2024)Language-based SandboxingProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3690866(5122-5124)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3690866
Mainas CPlakas INtoutsos GNanos A(2024)Sandboxing Functions for Efficient and Secure Multi-tenant Serverless DeploymentsProceedings of the 2nd Workshop on SErverless Systems, Applications and MEthodologies10.1145/3642977.3652096(25-31)Online publication date: 22-Apr-2024
https://dl.acm.org/doi/10.1145/3642977.3652096
Show More Cited By

Index Terms

The high-level benefits of low-level sandboxing
1. Security and privacy
  1. Formal methods and theory of security
    1. Logic and verification
2. Theory of computation
  1. Logic
    1. Programming logic

Recommendations

Gradual typing embedded securely in JavaScript
POPL '14

JavaScript's flexible semantics makes writing correct code hard and writing secure code extremely difficult. To address the former problem, various forms of gradual typing have been proposed, such as Closure and TypeScript. However, supporting all ...
Mechanized logical relations for termination-insensitive noninterference

We present an expressive information-flow control type system with recursive types, existential types, label polymorphism, and impredicative type polymorphism for a higher-order programming language with higher-order state. We give a novel semantic model ...
Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris

The metatheory of Scala’s core type system—the Dependent Object Types (DOT) calculus—is hard to extend, like the metatheory of other type systems combining subtyping and dependent types. Soundness of important Scala features therefore remains an open ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 4, Issue POPL

January 2020

1984 pages

EISSN:2475-1421

DOI:10.1145/3377388

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 December 2019

Published in PACMPL Volume 4, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Horizon 2020 Framework Programme
Deutsche Forschungsgemeinschaft

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
1,880
Total Downloads

Downloads (Last 12 months)927
Downloads (Last 6 weeks)24

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Timany AKrebbers RDreyer DBirkedal L(2024)A Logical Approach to Type SoundnessJournal of the ACM10.1145/367695471:6(1-75)Online publication date: 11-Nov-2024
https://dl.acm.org/doi/10.1145/3676954
Zhang JLuo BLiao XXu JKirda ELie D(2024)Language-based SandboxingProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3690866(5122-5124)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3690866
Mainas CPlakas INtoutsos GNanos A(2024)Sandboxing Functions for Efficient and Secure Multi-tenant Serverless DeploymentsProceedings of the 2nd Workshop on SErverless Systems, Applications and MEthodologies10.1145/3642977.3652096(25-31)Online publication date: 22-Apr-2024
https://dl.acm.org/doi/10.1145/3642977.3652096
Georges AGuéneau AVan Strydonck TTimany ATrieu ADevriese DBirkedal L(2024)Cerise: Program Verification on a Capability Machine in the Presence of Untrusted CodeJournal of the ACM10.1145/362351071:1(1-59)Online publication date: 11-Feb-2024
https://dl.acm.org/doi/10.1145/3623510
Yin JChen SLv YZhu H(2024)Enhancement and formal verification of the ICC mechanism with a sandbox approach in android systemSoftware Quality Journal10.1007/s11219-024-09684-232:3(1175-1202)Online publication date: 1-Sep-2024
https://dl.acm.org/doi/10.1007/s11219-024-09684-2
Cho MSong YLee DGäher LDreyer D(2023)Stuttering for FreeProceedings of the ACM on Programming Languages10.1145/36228577:OOPSLA2(1677-1704)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622857
Patterson DWagner AAhmed ACong YDagand P(2023)Semantic Encapsulation using Linking TypesProceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3609027.3609405(14-28)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3609027.3609405
Johnson ELaufer EZhao ZGohman DNarayan SSavage SStefan DBrown F(2023)WaVe: a verifiably secure WebAssembly sandboxing runtime2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179357(2940-2955)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179357
Patrignani MBlackshear S(2023)Robust Safety for Move2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00045(308-323)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00045
Mackay JEisenbach SNoble JDrossopoulou S(2022)Necessity specifications for robustnessProceedings of the ACM on Programming Languages10.1145/35633176:OOPSLA2(811-840)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563317
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents