Abstract
The possession of secrets is a recurrent theme in security literature and practice. We present a refinement type system, based on indexed intuitonist S4 necessity, for an object calculus with explicit locations (corresponding to principals) to control the principals that may possess a secret. Type safety ensures that if the execution of a well-typed program leads to a configuration with an object p located at principal a, then a possesses the capability to p. We illustrate the type system with simple examples drawn from web applications, including an illustration of how Cross-Site Request Forgery (CSRF) vulnerabilities may manifest themselves as absurd refinements on object declarations during type checking.
A fuller version of the paper is available at fpl.cs.depaul.edu/jriely/papers/2012-aplas.pdf.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M.: Access control in a core calculus of dependency. ENTCS 172, 5–31 (2007)
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148, 36–47 (1999)
Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. Program. Lang. Syst. 17(3), 507–535 (1995)
Abadi, M.: Secrecy by typing in security protocols. Journal of the ACM 46, 611–638 (1998)
Anderson, M., Pose, R.D., Wallace, C.S.: A password-capability system. Comput. J. 29(1), 1–8 (1986)
Bierman, G.M., de Paiva, V.C.V.: On an intuitionistic modal logic. Studia Logica 65 (2001)
Cardelli, L.: A language with distributed scope. In: POPL, pp. 286–297 (1995)
Castellani, I.: Process algebras with localities. In: Handbook of Process Algebra, ch. 15, pp. 945–1045 (2001)
Cirillo, A., Jagadeesan, R., Pitcher, C., Riely, J.: Tapido: Trust and Authorization Via Provenance and Integrity in Distributed Objects (Extended Abstract). In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 208–223. Springer, Heidelberg (2008)
DeYoung, H., Pfenning, F.: Reasoning about the consequences of authorization policies in a linear epistemic logic. Tech. Rep. 1213, CMU (2009)
Drossopoulou, S.: Ten years of ownership types or the benefits of putting objects into boxes, invited talk at BCS (2008), Talk available at http://www.doc.ic.ac.uk/~scd/BCS.pdf
E: Open source distributed capabilities, http://www.erights.org
Feil, R., Nyffenegger, L.: Evolution of cross site request forgery attacks. Journal in Computer Virology 4(1), 61–71 (2007)
Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization in distributed systems. In: CSF (2007)
Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization policies. ACM Trans. Program. Lang. Syst. 29(5) (2007)
Freeman, T., Pfenning, F.: Refinement types for ML. In: PLDI 1991, pp. 268–277. ACM, New York (1991)
Garg, D., Bauer, L., Bowers, K.D., Pfenning, F., Reiter, M.K.: A Linear Logic of Authorization and Knowledge. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 297–312. Springer, Heidelberg (2006)
Garg, D., Pfenning, F.: Non-interference in constructive authorization logic. In: CSFW, pp. 283–296 (2006)
Gong, L., Mueller, M., Prafullch, H.: Going beyond the sandbox: An overview of the new security architecture in the Java Development Kit 1.2. In: USENIX Symposium on Internet Technologies and Systems, pp. 103–112 (1997)
Gordon, A.D., Hankin, P.D.: A concurrent object calculus: Reduction and typing. In: Proceedings HLCL 1998 (1998)
Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. Journal of Computer Security 11(4), 451–520 (2003)
Hardy, N.: The confused deputy: (or why capabilities might have been invented). SIGOPS Oper. Syst. Rev. 22, 36–38 (1988)
Hardy, N.: KeyKOS architecture. SIGOPS Oper. Syst. Rev. 19, 8–25 (1985)
Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. Information and Computation 173, 2002 (1998)
Jagadeesan, R., Pitcher, C., Riely, J.: Non interference for intuitionist necessity. Tech. Rep. 12-003, School of Computing, DePaul University (2012)
Maffeis, S., Mitchell, J.C., Taly, A.: Object capabilities and isolation of untrusted web applications. In: IEEE Symposium on Security and Privacy, pp. 125–140 (2010)
Nicola, R.D., Ferrari, G., Pugliese, R.: Klaim: a kernel language for agents interaction and mobility. IEEE Transactions on Software Engineering 24, 315–330 (1997)
Pfenning, F., Wong, H.C.: On a modal λ-calculus for S4. In: Proceedings of MFOS, New Orleans, Louisiana. ENTCS, vol. 1. Elsevier (March 1995)
Shapiro, J.S., Smith, J.M., Farber, D.J.: EROS: a fast capability system. SIGOPS Oper. Syst. Rev. 33, 170–185 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jagadeesan, R., Pitcher, C., Riely, J. (2012). Succour to the Confused Deputy. In: Jhala, R., Igarashi, A. (eds) Programming Languages and Systems. APLAS 2012. Lecture Notes in Computer Science, vol 7705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35182-2_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-35182-2_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35181-5
Online ISBN: 978-3-642-35182-2
eBook Packages: Computer ScienceComputer Science (R0)