Abstract
Object capabilities are increasingly used to reason informally about the properties of secure systems. But can capabilities also aid in formal reasoning? To answer this question, we examine a calculus that uses effects to capture resource use and extend it to support capability-based reasoning. We demonstrate that capabilities provide a way to reason about effects: we can bound the effects of an expression based on the capabilities to which it has access. This reasoning is “free” in that it relies only on type-checking (not effect-checking), does not require the programmer to add effect annotations within the expression, and does not require the expression to be analysed for its effects. Our result sheds light on the essence of what capabilities provide and suggests ways of integrating lightweight capability-based reasoning into languages.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
\(\mathtt {Unit}\) is a singleton type, like \(\mathtt {void}\) in C and Java.
- 2.
Note that the resource literal is \(\mathtt {File}\), while the type of the resource literal is \(\mathtt {\{File\}}\).
- 3.
or automatically—but if the automation produces an unexpected result we must fall back to manual reasoning to understand why.
- 4.
Our formalisation only permits a single capability to be imported, but this discussion leads to a generalisation needed for the rules to be safe when multiple capabilities can be imported. In any case, importing multiple capabilities can be handled with an encoding of pairs.
References
Coker, Z., Maass, M., Ding, T., Le Goues, C., Sunshine, J.: Evaluating the flexibility of the Java sandbox. In: Proceedings of the 31st Annual Computer Security Applications Conference, ACSAC 2015, USA, pp. 1–10 (2015)
Craig, A., Potanin, A., Groves, L., Aldrich, J.: Capabilities: effects for free. Technical report, School of Engineering and Computer Science, Victoria University of Wellington, Wellington, New Zealand (2018). https://ecs.victoria.ac.nz/Main/TechnicalReportSeries
Dennis, J.B., Van Horn, E.C.: Programming semantics for multiprogrammed computations. Commun. ACM 9(3), 143–155 (1966)
Devriese, D., Birkedal, L., Piessens, F.: Reasoning about object capabilities with logical relations and effect parametricity. In: IEEE European Symposium on Security and Privacy (2016)
Dimoulas, C., Moore, S., Askarov, A., Chong, S.: Declarative policies for capability control. In: Computer Security Foundations Symposium (2014)
Drossopoulou, S., Noble, J., Miller, M.S., Murray, T.: Reasoning about risk and trust in an open world. In: ECOOP, pp. 451–475 (2007)
Hunt, G., et al.: Sealing OS processes to improve dependability and safety. SIGOPS OS Rev. 41(3), 341–354 (2007)
Kiniry, J.R.: Exceptions in Java and Eiffel: two extremes in exception design and application. In: Dony, C., Knudsen, J.L., Romanovsky, A., Tripathi, A. (eds.) Advanced Topics in Exception Handling Techniques. LNCS, vol. 4119, pp. 288–300. Springer, Heidelberg (2006). https://doi.org/10.1007/11818502_16
Leijen, D.: Koka: programming with row polymorphic effect types. In: Mathematically Structured Functional Programming 2014. EPTCS, March 2014
Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: POPL, POPL 1988, USA, pp. 47–57 (1988)
Maass, M.: A theory and tools for applying sandboxes effectively. Ph.D. thesis, Carnegie Mellon University (2016)
Madhavapeddy, A., et al.: Unikernels: library operating systems for the cloud. SIGPLAN Not. 48(4), 461–472 (2013)
Maffeis, S., Mitchell, J.C., Taly, A.: Object capabilities and isolation of untrusted web applications. In: Proceedings of the 2010 IEEE Symposium on Security and Privacy, SP 2010, pp. 125–140. IEEE Computer Society (2010)
Melicher, D., Shi, Y., Potanin, A., Aldrich, J.: A capability-based module system. In: 31st European Conference on Object-Oriented Programming (ECOOP 2017), pp 20:1–20:27 (2017). Article No. 20
Melicher, D., Shi, Y., Zhao, V., Potanin, A., Aldrich, J.: Using object capabilities and effects to build an authority-safe module system: poster. In: Proceedings of the 5th Annual Symposium and Bootcamp on Hot Topics in the Science of Security, HoTSoS 2018, Raleigh, North Carolina, USA, 10–11 April 2018
Miller, M., Yee, K.P., Shapiro, J.: Capability myths demolished. Technical report SRL2003-02, Systems Research Laboratory, Johns Hopkins University (2003)
Miller, M.S.: Robust composition: towards a unified approach to access control and concurrency control. Ph.D. thesis, Johns Hopkins University (2006)
Nielson, F., Nielson, H.R.: Type and effect systems. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 114–136. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48092-7_6
Rytz, L., Odersky, M., Haller, P.: Lightweight polymorphic effects. In: Noble, J. (ed.) ECOOP 2012. LNCS, vol. 7313, pp. 258–282. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31057-7_13
Talpin, J.P., Jouvelot, P.: The type and effect discipline. Inf. Comput. 111(2), 245–296 (1994)
Tang, Y.M.: Control-flow analysis by effect systems and abstract interpretation. Ph.D. thesis, Ecole des Mines de Paris (1994)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Craig, A., Potanin, A., Groves, L., Aldrich, J. (2018). Capabilities: Effects for Free. In: Sun, J., Sun, M. (eds) Formal Methods and Software Engineering. ICFEM 2018. Lecture Notes in Computer Science(), vol 11232. Springer, Cham. https://doi.org/10.1007/978-3-030-02450-5_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-02450-5_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02449-9
Online ISBN: 978-3-030-02450-5
eBook Packages: Computer ScienceComputer Science (R0)