A Capability-Based Module System for Authority Control

Authors Darya Melicher, Yangqingwei Shi, Alex Potanin, Jonathan Aldrich



PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2017.20.pdf
  • Filesize: 0.71 MB
  • 27 pages

Document Identifiers

Author Details

Darya Melicher
Yangqingwei Shi
Alex Potanin
Jonathan Aldrich

Cite AsGet BibTex

Darya Melicher, Yangqingwei Shi, Alex Potanin, and Jonathan Aldrich. A Capability-Based Module System for Authority Control. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 20:1-20:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ECOOP.2017.20

Abstract

The principle of least authority states that each component of the system should be given authority to access only the information and resources that it needs for its operation. This principle is fundamental to the secure design of software systems, as it helps to limit an application's attack surface and to isolate vulnerabilities and faults. Unfortunately, current programming languages do not provide adequate help in controlling the authority of application modules, an issue that is particularly acute in the case of untrusted third-party extensions. In this paper, we present a language design that facilitates controlling the authority granted to each application module. The key technical novelty of our approach is that modules are first-class, statically typed capabilities. First-class modules are essentially objects, and so we formalize our module system by translation into an object calculus and prove that the core calculus is type-safe and authority-safe. Unlike prior formalizations, our work defines authority non-transitively, allowing engineers to reason about software designs that use wrappers to provide an attenuated version of a more powerful capability. Our approach allows developers to determine a module's authority by examining the capabilities passed as module arguments when the module is created, or delegated to the module later during execution. The type system facilitates this by identifying which objects provide capabilities to sensitive resources, and by enabling security architects to examine the capabilities passed into and out of a module based only on the module's interface, without needing to examine the module's implementation code. An implementation of the module system and illustrative examples in the Wyvern programming language suggest that our approach can be a practical way to control module authority.
Keywords
  • Language-based security
  • capabilities
  • authority
  • modules

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. John Boyland, James Noble, and William Retert. Capabilities for Sharing: A Generalisation of Uniqueness and Read-Only. In European Conference on Object-Oriented Programming, 2001. Google Scholar
  2. Gilad Bracha, Peter von der Ahé, Vassili Bykov, Yaron Kashai, William Maddox, and Eliot Miranda. Modules as Objects in Newspeak. In European Conference on Object-Oriented Programming, 2010. Google Scholar
  3. Shuo Chen, David Ross, and Yi-Min Wang. An Analysis of Browser Domain-isolation Bugs and a Light-weight Transparent Defense Mechanism. In Conference on Computer and Communications Security, 2007. Google Scholar
  4. Zack Coker, Michael Maass, Tianyuan Ding, Claire Le Goues, and Joshua Sunshine. Evaluating the Flexibility of the Java Sandbox. In Annual Computer Security Applications Conference, 2015. Google Scholar
  5. Jack B. Dennis and Earl C. Van Horn. Programming Semantics for Multiprogrammed Computations. Communications of the ACM, 9(3):143-155, 1966. Google Scholar
  6. Dominique Devriese, Frank Piessens, and Lars Birkedal. Reasoning about Object Capabilities with Logical Relations and Effect Parametricity. In European Symposium on Security and Privacy, 2016. Google Scholar
  7. Christos Dimoulas, Scott Moore, Aslan Askarov, and Stephen Chong. Declarative Policies for Capability Control. In Computer Security Foundations Symposium, 2014. Google Scholar
  8. Sophia Drossopoulou and James Noble. The Need for Capability Policies. In Workshop on Formal Techniques for Java-like Programs, 2013. Google Scholar
  9. Sophia Drossopoulou and James Noble. How to Break the Bank: Semantics of Capability Policies. In Integrated Formal Methods, 2014. Google Scholar
  10. Sophia Drossopoulou and James Noble. Towards Capability Policy Specification and Verification. Technical report, Victoria University of Wellington, 2014. Google Scholar
  11. Sophia Drossopoulou, James Noble, and Mark S. Miller. Swapsies on the Internet: First Steps Towards Reasoning About Risk and Trust in an Open World. In Workshop on Programming Languages and Analysis for Security, 2015. Google Scholar
  12. Sophia Drossopoulou, James Noble, Toby Murray, and Mark S. Miller. Reasoning about Risk and Trust in an Open World. Technical report, Victoria University of Wellington, 2015. Google Scholar
  13. Matthew Flatt and Matthias Felleisen. Units: Cool Modules for HOT Languages. In Programming Language Design and Implementation, 1998. Google Scholar
  14. Google, Inc. Caja. URL: https://code.google.com/p/google-caja/.
  15. Michael Homer, Kim B. Bruce, James Noble, and Andrew P. Black. Modules As Gradually-typed Objects. In Workshop on Dynamic Languages and Applications, 2013. Google Scholar
  16. Darya Kurilova, Alex Potanin, and Jonathan Aldrich. Modules in Wyvern: Advanced Control over Security and Privacy. In Symposium and Bootcamp on the Science of Security, 2016. Google Scholar
  17. Ben Laurie. Safer Scripting Through Precompilation. In Security Protocols, 2007. Google Scholar
  18. Michael Maass. A Theory and Tools for Applying Sandboxes Effectively. PhD thesis, Carnegie Mellon University, 2016. Google Scholar
  19. David MacQueen. Modules for Standard ML. In ACM Symposium on LISP and Functional Programming, 1984. Google Scholar
  20. Sergio Maffeis, John C. Mitchell, and Ankur Taly. Object Capabilities and Isolation of Untrusted Web Applications. In IEEE Symposium on Security and Privacy, 2010. Google Scholar
  21. Darya Melicher, Yangqingwei Shi, Alex Potanin, and Jonathan Aldrich. A Capability-Based Module System for Authority Control. Technical Report CMU-ISR-17-106, Carnegie Mellon University, 2017. URL: http://reports-archive.adm.cs.cmu.edu/anon/isr2017/abstracts/17-106.html.
  22. Adrian Mettler, David Wagner, and Tyler Close. Joe-E: A Security-Oriented Subset of Java. In Network and Distributed System Security Symposium, 2010. Google Scholar
  23. Heather Miller, Philipp Haller, and Martin Odersky. Spores: A Type-Based Foundation for Closures in the Age of Concurrency and Distribution. In European Conference on Object-Oriented Programming, 2014. Google Scholar
  24. Mark S. Miller. The E Language. URL: http://erights.org/elang/.
  25. Mark S. Miller. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. PhD thesis, Johns Hopkins University, 2006. Google Scholar
  26. Mark S. Miller, Mike Samuel, Ben Laurie, Ihab Awad, and Mike Stay. Caja: Safe Active Content in Sanitized JavaScript. Technical report, Google, Inc., 2008. Google Scholar
  27. Scott Moore, Christos Dimoulas, Dan King, and Stephen Chong. SHILL: A Secure Shell Scripting Language. In USENIX Symposium on Operating Systems Design and Implementation, 2014. Google Scholar
  28. James H. Morris, Jr. Protection in Programming Languages. Communications of the ACM, 16(1):15-21, 1973. Google Scholar
  29. Ligia Nistor, Darya Kurilova, Stephanie Balzer, Benjamin Chung, Alex Potanin, and Jonathan Aldrich. Wyvern: A Simple, Typed, and Pure Object-Oriented Language. In Workshop on Mechanisms for Specialization, Generalization and Inheritance, 2013. Google Scholar
  30. James Noble and Sophia Drossopoulou. Rationally Reconstructing the Escrow Example. In Workshop on Formal Techniques for Java-like Programs, 2014. Google Scholar
  31. Martin Odersky, Philippe Altherr, Vincent Cremet, Gilles Dubochet, Burak Emir, Philipp Haller, Stéphane Micheloud, Nikolay Mihaylov, Adriaan Moors, Lukas Rytz, Michel Schinz, Erik Stenman, and Matthias Zenger. Scala Language Specification. http://scala-lang.org/files/archive/spec/2.11/. Last accessed: May 2017.
  32. Jonathan A. Rees. A Security Kernel Based on the Lambda-Calculus. Technical report, Massachusetts Institute of Technology, 1996. Google Scholar
  33. John M. Rushby. Design and Verification of Secure Systems. In Symposium on Operating Systems Principles, 1981. Google Scholar
  34. Jerome H. Saltzer. Protection and the Control of Information Sharing in Multics. Communications of the ACM, 17(7):388-402, 1974. Google Scholar
  35. Z. Cliffe Schreuders, Tanya Mcgill, and Christian Payne. The State of the Art of Application Restrictions and Sandboxes: A Survey of Application-oriented Access Controls and Their Shortfalls. Computers and Security, 32:219-241, 2013. Google Scholar
  36. Fred Spiessens and Peter Van Roy. The Oz-E Project: Design Guidelines for a Secure Multiparadigm Programming Language. In Multiparadigm Programming in Mozart/Oz, 2005. Google Scholar
  37. Marc Stiegler. Emily: A High Performance Language for Enabling Secure Cooperation. In International Conference on Creating, Connecting and Collaborating through Computing, 2007. Google Scholar
  38. Mike Ter Louw, Prithvi Bisht, and V Venkatakrishnan. Analysis of Hypertext Isolation Techniques for XSS Prevention. Web 2.0 Security and Privacy, 2008. Google Scholar
  39. Tom Van Cutsem, Elisa Gonzalez Boix, Christophe Scholliers, Andoni Lombide Carreton, Dries Harnie, Kevin Pinte, and Wolfgang De Meuter. AmbientTalk: Programming Responsive Mobile Peer-to-peer Applications with Actors. Computer Languages, Systems and Structures, 40(3–4):112-136, 2014. Google Scholar
  40. David Wagner and Dean Tribble. A Security Analysis of the Combex DarpaBrowser Architecture. http://combex.com/papers/darpa-review/security-review.pdf, March 2002.
  41. Esther Wang and Jonathan Aldrich. Capability Safe Reflection for the Wyvern Language. In Workshop on Meta-Programming Techniques and Reflection, 2016. Google Scholar
  42. Robert N. M. Watson. Exploiting Concurrency Vulnerabilities in System Call Wrappers. In USENIX Workshop on Offensive Technologies, 2007. Google Scholar
  43. William A. Wulf, Ellis S. Cohen, William M. Corwin, Anita K. Jones, Roy Levin, C. Pierson, and Fred J. Pollack. HYDRA: The Kernel of a Multiprocessor Operating System. Communications of the ACM, 17(6):337-345, 1974. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail