Nothing Special   »   [go: up one dir, main page]

skip to main content
research-article
Open access

Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types

Published: 08 October 2024 Publication History

Abstract

Modern software needs fine-grained compartmentalization, i.e., intra-process isolation. A particularly important reason for it are supply-chain attacks, the need for which is aggravated by modern applications depending on hundreds or even thousands of libraries. Object capabilities are a particularly salient approach to compartmentalization, but they require the entire program to assume a lack of ambient authority. Most of existing code was written under no such assumption; effectively, existing applications need to undergo a rewrite-the-world migration to reap the advantages of ocap. We propose gradual compartmentalization, an approach which allows gradually migrating an application to object capabilities, component by component in arbitrary order, all the while continuously enjoying security guarantees. The approach relies on runtime authority enforcement and tracking the authority of objects the type system. We present Gradient, a proof-of-concept gradual compartmentalization extension to Scala which uses Enclosures and Capture Tracking as its key components. We evaluate our proposal by migrating the standard XML library of Scala to Gradient.

References

[1]
Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object Types. In A List of Successes That Can Change the World. Springer, 249–272.
[2]
Nada Amin, Tiark Rompf, and Martin Odersky. 2014. Foundations of Path-Dependent Types. ACM SIGPLAN Notices, 49, 10 (2014), Oct., 233–249. issn:0362-1340 https://doi.org/10.1145/2714064.2660216
[3]
A.W. Appel. 2001. Foundational Proof-Carrying Code. In Proceedings 16th Annual IEEE Symposium on Logic in Computer Science. 247–256. issn:1043-6871 https://doi.org/10.1109/LICS.2001.932501
[4]
Yechan Bae, Youngsuk Kim, Ammar Askar, Jungwon Lim, and Taesoo Kim. 2021. Rudra: Finding Memory Safety Bugs in Rust at the Ecosystem Scale. In Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles (SOSP ’21). Association for Computing Machinery, New York, NY, USA. 84–99. isbn:978-1-4503-8709-5 https://doi.org/10.1145/3477132.3483570
[5]
Andrea Bittau, Petr Marchenko, Mark Handley, and Brad Karp. 2008. Wedge: Splitting Applications into Reduced-Privilege Compartments. In 5th USENIX Symposium on Networked Systems Design & Implementation, NSDI 2008, April 16-18, 2008, San Francisco, CA, USA, Proceedings, Jon Crowcroft and Michael Dahlin (Eds.). USENIX Association, 309–322. http://www.usenix.org/events/nsdi08/tech/full_papers/bittau/bittau.pdf
[6]
Aleksander Boruch-Gruszecki, Adrien Ghosn, Mathias Payer, and Clément Pit-Claudel. 2024. Gradient: benchmark code. https://doi.org/10.5281/zenodo.13385386
[7]
Aleksander Boruch-Gruszecki, Adrien Ghosn, Mathias Payer, and Clément Pit-Claudel. 2024. Gradient: migrated scala-xml. https://doi.org/10.5281/zenodo.13385375
[8]
Aleksander Boruch-Gruszecki, Martin Odersky, Edward Lee, Ondřej Lhoták, and Jonathan Brachthäuser. 2023. Capturing Types. ACM Transactions on Programming Languages and Systems, Sept., issn:0164-0925 https://doi.org/10.1145/3618003
[9]
Aleksander Boruch-Gruszecki, Radosł aw Waśko, Yichen Xu, and Lionel Parreaux. 2022. A Case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-style Reasoning. Proceedings of the ACM on Programming Languages, 6, OOPSLA2 (2022), Oct., 179:1526–179:1555. https://doi.org/10.1145/3563342
[10]
Gilad Bracha, Peter von der Ahé, Vassili Bykov, Yaron Kashai, William Maddox, and Eliot Miranda. 2010. Modules as Objects in Newspeak. In ECOOP 2010 – Object-Oriented Programming, Theo D’Hondt (Ed.) (Lecture Notes in Computer Science). Springer, Berlin, Heidelberg. 405–428. isbn:978-3-642-14107-2 https://doi.org/10.1007/978-3-642-14107-2_20
[11]
Jonathan Immanuel Brachthäuser, Philipp Schuster, Edward Lee, and Aleksander Boruch-Gruszecki. 2022. Effects, Capabilities, and Boxes: From Scope-Based Reasoning to Type-Based Reasoning and Back. Proceedings of the ACM on Programming Languages, 6, OOPSLA1 (2022), April, 76:1–76:30. https://doi.org/10.1145/3527320
[12]
Partha Das Chowdhury, Mohammad Tahaei, and Awais Rashid. 2022. Better Call Saltzer & Schroeder: A Retrospective Security Analysis of SolarWinds & Log4j. CoRR, abs/2211.02341 (2022), https://doi.org/10.48550/arXiv.2211.02341 arXiv:2211.02341.
[13]
Chromium. 2023. Chromium sandboxing documentation. https://chromium.googlesource.com/chromium/src/+/refs/heads/main/docs/design/sandbox.md
[14]
Jack B. Dennis and Earl C. Van Horn. 1966. Programming Semantics for Multiprogrammed Computations. Commun. ACM, 9, 3 (1966), 143–155.
[15]
Matthew Flatt and Matthias Felleisen. 1998. Units: Cool Modules for HOT Languages. In Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation (PLDI ’98). Association for Computing Machinery, New York, NY, USA. 236–248. isbn:978-0-89791-987-6 https://doi.org/10.1145/277650.277730
[16]
Adrien Ghosn, Marios Kogias, Mathias Payer, James R. Larus, and Edouard Bugnion. 2021. Enclosure: Language-Based Restriction of Untrusted Libraries. In Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’21). Association for Computing Machinery, New York, NY, USA. 255–267. isbn:978-1-4503-8317-2 https://doi.org/10.1145/3445814.3446728
[17]
Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. 2017. Bringing the Web up to Speed with WebAssembly. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). Association for Computing Machinery, New York, NY, USA. 185–200. isbn:978-1-4503-4988-8 https://doi.org/10.1145/3062341.3062363
[18]
John Hannan. 1998. A Type-Based Escape Analysis for Functional Languages. Journal of Functional Programming, 8, 3 (1998), May, 239–273. issn:1469-7653, 0956-7968 https://doi.org/10.1017/S0956796898003025
[19]
Norm Hardy. 1988. The Confused Deputy: (Or Why Capabilities Might Have Been Invented). ACM SIGOPS Operating Systems Review, 22, 4 (1988), Oct., 36–38. issn:0163-5980 https://doi.org/10.1145/54289.871709
[20]
Mohammad Hedayati, Spyridoula Gravani, Ethan Johnson, John Criswell, Michael L. Scott, Kai Shen, and Mike Marty. 2019. Hodor: Intra-Process Isolation for High-Throughput Data Plane Libraries. In 2019 USENIX Annual Technical Conference, USENIX ATC 2019, Renton, WA, USA, July 10-12, 2019, Dahlia Malkhi and Dan Tsafrir (Eds.). USENIX Association, 489–504. https://www.usenix.org/conference/atc19/presentation/hedayati-hodor
[21]
Raphael Hiesgen, Marcin Nawrocki, Thomas C. Schmidt, and Matthias Wählisch. 2022. The Race to the Vulnerable: Measuring the Log4j Shell Incident. CoRR, abs/2205.02544 (2022), https://doi.org/10.48550/arXiv.2205.02544 arXiv:2205.02544.
[22]
Terry Ching-Hsiang Hsu, Kevin Hoffman, Patrick Eugster, and Mathias Payer. 2016. Enforcing Least Privilege Memory Views for Multithreaded Applications. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS ’16). Association for Computing Machinery, New York, NY, USA. 393–405. isbn:978-1-4503-4139-4 https://doi.org/10.1145/2976749.2978327
[23]
2020. Intel 64 and IA-32 Architectures Software Developer’s Manual.
[24]
Java. 2021. JEP 411: Deprecate the Security Manager for Removal. https://openjdk.org/jeps/411
[25]
Ben Laurie. 2007. Safer Scripting Through Precompilation. In Security Protocols, Bruce Christianson, Bruno Crispo, James A. Malcolm, and Michael Roe (Eds.) (Lecture Notes in Computer Science). Springer, Berlin, Heidelberg. 289–294. isbn:978-3-540-77156-2 https://doi.org/10.1007/978-3-540-77156-2_36
[26]
Joshua Lind, Christian Priebe, Divya Muthukumaran, Dan O’Keeffe, Pierre-Louis Aublin, Florian Kelbert, Tobias Reiher, David Goltzsche, David M. Eyers, Rüdiger Kapitza, Christof Fetzer, and Peter R. Pietzuch. 2017. Glamdring: Automatic Application Partitioning for Intel SGX. In 2017 USENIX Annual Technical Conference, USENIX ATC 2017, Santa Clara, CA, USA, July 12-14, 2017, Dilma Da Silva and Bryan Ford (Eds.). USENIX Association, 285–298. https://www.usenix.org/conference/atc17/technical-sessions/presentation/lind
[27]
Linux. 2023. Seccomp BPF. https://kernel.org/doc/html/latest/userspace-api/seccomp_filter.html
[28]
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 Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI’16). USENIX Association, USA. 49–64. isbn:978-1-931971-33-1
[29]
J. M. Lucassen and D. K. Gifford. 1988. Polymorphic Effect Systems. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’88). Association for Computing Machinery, New York, NY, USA. 47–57. isbn:978-0-89791-252-5 https://doi.org/10.1145/73560.73564
[30]
Guillaume Martres. 2023. Type-Preserving Compilation of Class-Based Languages. Jan., https://doi.org/10.5075/epfl-thesis-8218 arxiv:2307.05557.
[31]
Steven McCanne and Van Jacobson. 1993. The BSD Packet Filter: A New Architecture for User-level Packet Capture. In Proceedings of the Usenix Winter 1993 Technical Conference, San Diego, California, USA, January 1993. USENIX Association, 259–270. https://www.usenix.org/conference/usenix-winter-1993-conference/bsd-packet-filter-new-architecture-user-level-packet
[32]
Darya Melicher. 2020. Controlling Module Authority Using Programming Language Design. Ph. D. Dissertation. Carnegie Mellon University.
[33]
Darya Melicher, Yangqingwei Shi, Alex Potanin, and Jonathan Aldrich. 2017. A Capability-Based Module System for Authority Control. In 31st European Conference on Object-Oriented Programming (ECOOP 2017), Peter Müller (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 74). Schloss Dagstuhl– Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 20:1–20:27. isbn:978-3-95977-035-4 https://doi.org/10.4230/LIPIcs.ECOOP.2017.20
[34]
Samuel Mergendahl, Nathan Burow, and Hamed Okhravi. 2022. Cross-Language Attacks. Proceedings 2022 Network and Distributed System Security Symposium, isbn:9781891562747 https://doi.org/10.14722/ndss.2022.24078
[35]
Adrian Mettler, David A. Wagner, and Tyler Close. 2010. Joe-E: A Security-Oriented Subset of Java. In Network and Distributed System Security Symposium. 10, 357–374.
[36]
Mark Miller. 2006. Robust Composition: Towards a Unifed Approach to Access Control and Concurrency Control. Ph. D. Dissertation. Johns Hopkins University. https://jscholarship.library.jhu.edu/handle/1774.2/873
[37]
Mark S. Miller, Mike Samuel, Ben Laurie, Ihab Awad, and Mike Stay. 2008. Safe Active Content in Sanitized JavaScript. https://google-code-archive-downloads.storage.googleapis.com/v2/code.google.com/google-caja/caja-spec-2008-06-06.pdf
[38]
J. C. Mitchell and R. Harper. 1988. The Essence of ML. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’88). Association for Computing Machinery, New York, NY, USA. 28–46. isbn:978-0-89791-252-5 https://doi.org/10.1145/73560.73563
[39]
James H. Morris. 1973. Protection in Programming Languages. Commun. ACM, 16, 1 (1973), Jan., 15–21. issn:0001-0782 https://doi.org/10.1145/361932.361937
[40]
Mozilla. 2023. Firefox sandboxing documentation. https://wiki.mozilla.org/Security/Sandbox
[41]
George C. Necula. 1997. Proof-Carrying Code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’97). Association for Computing Machinery, New York, NY, USA. 106–119. isbn:978-0-89791-853-4 https://doi.org/10.1145/263699.263712
[42]
Nick Nikiforakis, Luca Invernizzi, Alexandros Kapravelos, Steven Van Acker, Wouter Joosen, Christopher Kruegel, Frank Piessens, and Giovanni Vigna. 2012. You Are What You Include: Large-Scale Evaluation of Remote Javascript Inclusions. In Proceedings of the 2012 ACM Conference on Computer and Communications Security (CCS ’12). Association for Computing Machinery, New York, NY, USA. 736–747. isbn:978-1-4503-1651-4 https://doi.org/10.1145/2382196.2382274
[43]
Leo Osvald, Grégory Essertel, Xilun Wu, Lilliam I. González Alayón, and Tiark Rompf. 2016. Gentrification Gone Too Far? Affordable 2Nd-class Values for Fun and (Co-)Effect. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016). ACM, New York, NY, USA. 234–251. isbn:978-1-4503-4444-9 https://doi.org/10.1145/2983990.2984009
[44]
Vineet Rajani, Deepak Garg, and Tamara Rezk. 2016. On Access Control, Capabilities, Their Equivalence, and Confused Deputy Attacks. In 2016 IEEE 29th Computer Security Foundations Symposium (CSF). 150–163. issn:2374-8303 https://doi.org/10.1109/CSF.2016.18
[45]
Marianna Rapoport and Ondřej Lhoták. 2019. A Path To DOT: Formalizing Fully-Path-Dependent Types. arXiv:1904.07298 [cs], April, arxiv:1904.07298. arxiv:1904.07298
[46]
Jonathan A. Rees. 1996. A Security Kernel Based on the Lambda-Calculus. https://dspace.mit.edu/handle/1721.1/5944
[47]
Lukas Rytz, Martin Odersky, and Philipp Haller. 2012. Lightweight Polymorphic Effects. In ECOOP 2012 – Object-Oriented Programming, James Noble (Ed.) (Lecture Notes in Computer Science). Springer, Berlin, Heidelberg. 258–282. isbn:978-3-642-31057-7 https://doi.org/10.1007/978-3-642-31057-7_13
[48]
Jerome H. Saltzer. 1974. Protection and the Control of Information Sharing in Multics. Commun. ACM, 17, 7 (1974), July, 388–402. issn:0001-0782 https://doi.org/10.1145/361011.361067
[49]
Sandboxdb. 2023. Sandboxdb.org. https://sandboxdb.org
[50]
ScalaXML. 2023. Scala XML: the standard Scala XML library. https://github.com/scala/scala-xml
[51]
Gabriel Scherer and Jan Hoffmann. 2013. Tracking Data-Flow with Open Closure Types. In Logic for Programming, Artificial Intelligence, and Reasoning, Ken McMillan, Aart Middeldorp, and Andrei Voronkov (Eds.) (Lecture Notes in Computer Science). Springer, Berlin, Heidelberg. 710–726. isbn:978-3-642-45221-5 https://doi.org/10.1007/978-3-642-45221-5_47
[52]
Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop. https://www.semanticscholar.org/paper/Gradual-Typing-for-Functional-Languages-Siek/b7ca4b0e6d3119aa341af73964dbe38d341061dd
[53]
Fred Spiessens and Peter Van Roy. 2005. The Oz-E Project: Design Guidelines for a Secure Multiparadigm Programming Language. In Multiparadigm Programming in Mozart/Oz, Peter Van Roy (Ed.) (Lecture Notes in Computer Science). Springer, Berlin, Heidelberg. 21–40. isbn:978-3-540-31845-3 https://doi.org/10.1007/978-3-540-31845-3_3
[54]
Marc Stiegler. 2007. Emily: A High Performance Language for Enabling Secure Cooperation. In Fifth International Conference on Creating, Connecting and Collaborating through Computing (C5 ’07). 163–169. https://doi.org/10.1109/C5.2007.13
[55]
Marc Stiegler and Mark Miller. 2006. How Emily Tamed the Caml. https://www.hpl.hp.com/techreports/2006/HPL-2006-116.pdf
[56]
Mads Tofte and Jean-Pierre Talpin. 1997. Region-Based Memory Management. Information and Computation, 132, 2 (1997), Feb., 109–176. issn:0890-5401 https://doi.org/10.1006/inco.1996.2613
[57]
R. Uhlig, G. Neiger, D. Rodgers, A.L. Santoni, F.C.M. Martins, A.V. Anderson, S.M. Bennett, A. Kagi, F.H. Leung, and L. Smith. 2005. Intel Virtualization Technology. Computer, 38, 5 (2005), May, 48–56. issn:1558-0814 https://doi.org/10.1109/MC.2005.163
[58]
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
[59]
Philip Wadler. 2015. A Complement to Blame. In 1st Summit on Advances in Programming Languages (SNAPL 2015), Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 32). Schloss Dagstuhl– Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 309–320. isbn:978-3-939897-80-4 issn:1868-8969 https://doi.org/10.4230/LIPIcs.SNAPL.2015.309
[60]
Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can’t Be Blamed. In Programming Languages and Systems, Giuseppe Castagna (Ed.) (Lecture Notes in Computer Science). Springer, Berlin, Heidelberg. 1–16. isbn:978-3-642-00590-9 https://doi.org/10.1007/978-3-642-00590-9_1
[61]
WASI. 2023. Webassembly: WASI. https://github.com/WebAssembly/WASI
[62]
WASM-JS. 2023. Webassembly: JavaScript API. https://webassembly.github.io/spec/js-api/index.html
[63]
WASM-Web. 2023. Webassembly: Web API. https://webassembly.github.io/spec/web-api/index.html
[64]
Emmett Witchel, Josh Cates, and Krste Asanović. 2002. Mondrian Memory Protection. In Proceedings of the 10th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS X). Association for Computing Machinery, New York, NY, USA. 304–316. isbn:978-1-58113-574-9 https://doi.org/10.1145/605397.605429
[65]
Jonathan Woodruff, Robert N. M. Watson, David Chisnall, Simon W. Moore, Jonathan Anderson, Brooks Davis, Ben Laurie, Peter G. Neumann, Robert Norton, and Michael Roe. 2014. The CHERI Capability Model: Revisiting RISC in an Age of Risk. In 2014 ACM/IEEE 41st International Symposium on Computer Architecture (ISCA). 457–468. issn:1063-6897 https://doi.org/10.1109/ISCA.2014.6853201
[66]
A. K. Wright and M. Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation, 115, 1 (1994), Nov., 38–94. issn:0890-5401 https://doi.org/10.1006/inco.1994.1093
[67]
Yichen Xu and Martin Odersky. 2023. Formalizing Box Inference for Capture Calculus. arXiv. https://doi.org/10.48550/arXiv.2306.06496 arxiv:2306.06496.
[68]
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 2009 30th IEEE Symposium on Security and Privacy. 79–93. issn:2375-1207 https://doi.org/10.1109/SP.2009.25

Recommendations

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 8, Issue OOPSLA2
October 2024
2691 pages
EISSN:2475-1421
DOI:10.1145/3554319
Issue’s Table of Contents
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: 08 October 2024
Published in PACMPL Volume 8, Issue OOPSLA2

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. compartmentalization
  2. object capabilities
  3. security
  4. type systems

Qualifiers

  • Research-article

Funding Sources

  • MEYS
  • SNSF

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • 0
    Total Citations
  • 156
    Total Downloads
  • Downloads (Last 12 months)156
  • Downloads (Last 6 weeks)68
Reflects downloads up to 14 Dec 2024

Other Metrics

Citations

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media