Michele Bugliesi
Abstract
Recent research has shown that it is possible to leverage general-purpose theorem-proving techniques to develop powerful type systems for the verification of a wide range of security properties on application code. Although successful in many respects, these type systems fall short of capturing resource-conscious properties that are crucial in large classes of modern distributed applications. In this article, we propose the first type system that statically enforces the safety of cryptographic protocol implementations with respect to authorization policies expressed in affine logic. Our type system draws on a novel notion of “exponential serialization” of affine formulas, a general technique to protect affine formulas from the effect of duplication. This technique allows formulate of an expressive logical encoding of the authentication mechanisms underpinning distributed resource-aware authorization policies. We discuss the effectiveness of our approach on two case studies: the EPMO e-commerce protocol and the Kerberos authentication protocol. We finally devise a sound and complete type-checking algorithm, which is the key to achieving an efficient implementation of our analysis technique.
- Martín Abadi and Cédric Fournet. 2001. Mobile values, new names, and secure communication. In Proceedings of the 28th Symposium on Principles of Programming Languages (POPL). ACM, 104--115. Google Scholar
Digital Library
- Alessandro Armando, David A. Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuéllar, Paul Hankes Drielsma, Pierre-Cyrille Héam, Olga Kouchnarenko, Jacopo Mantovani, Sebastian Mödersheim, David von Oheimb, Michaël Rusinowitch, Judson Santiago, Mathieu Turuani, Luca Viganò, and Laurent Vigneron. 2005. The AVISPA tool for the automated validation of Internet security protocols and applications. In Proceedings Computer Aided Verification’05 (CAV) (LNCS). 281--285. Google ScholarDigital Library
- Michael Backes, Agostino Cortesi, Riccardo Focardi, and Matteo Maffei. 2007b. A calculus of challenges and responses. In Formal Methods in Security Engineering 2007 (FMSE’07 ). ACM, 101--116. Google ScholarDigital Library
- Michael Backes, Agostino Cortesi, and Matteo Maffei. 2007a. Causality-based abstraction of multiplicity in cryptographic protocols. In Proceedings of the 20th IEEE Symposium on Computer Security Foundations (CSF). IEEE, 355--369. Google ScholarDigital Library
- Michael Backes, Martin P. Grochulla, Catalin Hritcu, and Matteo Maffei. 2009. Achieving security despite compromise using zero-knowledge. In Computer Security Foundations 2009 (CSF’09). IEEE, 308--323. Google ScholarDigital Library
- Michael Backes, Cătălin Hriţcu, and Matteo Maffei. 2008. Type-checking Zero-knowledge. In 15th ACM Conference on Computer and Communications Security (CCS). ACM Press, 357--370. Google ScholarDigital Library
- Michael Backes, Catalin Hriţcu, and Matteo Maffei. 2011. Union and intersection types for secure protocol implementations. In TOSCA’11 (LNCS). Springer, 1--28. Google ScholarDigital Library
- Michael Backes, Catalin Hriţcu, and Matteo Maffei. 2014. Union and intersection types for secure protocol implementations. JCS 22, 2, 301--353. Google ScholarDigital Library
- Michael Backes, Matteo Maffei, and Dominique Unruh. 2010. Computationally sound verification of source code. In Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS). ACM, 387--398. Google ScholarDigital Library
- Patrick Baillot and Martin Hofmann. 2010. Type inference in intuitionistic linear logic. In Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming 2010 (PPDP’10). ACM, 219--230. Google ScholarDigital Library
- Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. 2011. Refinement types for secure implementations. Transactions on Programming Languages and Systems 33, 2, Article 8, 45 pages. Google ScholarDigital Library
- Karthikeyan Bhargavan, Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, and James J. Leifer. 2009. Cryptographic protocol synthesis and verification for multiparty sessions. In Computer Security Foundations 2009 (CSF’09). IEEE, 124--140. Google ScholarDigital Library
- Karthikeyan Bhargavan, Cédric Fournet, and Andrew D. Gordon. 2010. Modular verification of security protocol code by typing. In 37th ACM SIGT-SIGPLAN Symposium on Principles of Programming Languages (POPL’10). ACM, 445--456. Google ScholarDigital Library
- Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Stephen Tse. 2008. Verified interoperable implementations of security protocols. Transactions on Programming Languages and Systems 31, 1, Article 5, 61 pages. Google ScholarDigital Library
- Kevin Bierhoff and Jonathan Aldrich. 2007. Modular typestate checking of aliased objects. In 22nd International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’07). ACM, 301--320. Google ScholarDigital Library
- Bruno Blanchet. 2001. An efficient cryptographic protocol verifier based on prolog rules. In 14th IEEE Computer Security Foundations Workshop (CSFW’01). IEEE, 82--96. Google ScholarDigital Library
- Bruno Blanchet. 2011. Using horn clauses for analyzing security protocols. In Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security, Vol. 5. IOS Press, Amsterdam, The Netherlands, 86--111.Google Scholar
- Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, and Matteo Maffei. 2011. Resource-aware authorization policies for statically typed cryptographic protocols. In Computer Security Foundations 2001 (CSF’11). IEEE, 83--98. Google ScholarDigital Library
- Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, and Matteo Maffei. 2012. Affine refinement types for authentication and authorization. In TGC’12. Springer, 19--33.Google Scholar
- Michele Bugliesi, Stefano Calzavara, Fabienne Eigner, and Matteo Maffei. 2013. Logical foundations of secure resource management in protocol implementations. In 2nd International Conference on Principles of Security and Trust 2013 (POST’13). Springer, 105--125. Google ScholarDigital Library
- Michele Bugliesi, Riccardo Focardi, and Matteo Maffei. 2004a. Authenticity by tagging and typing. In Formal Methods in Security Engineering 2004 (FMSE’04). ACM, 1--12. Google ScholarDigital Library
- Michele Bugliesi, Riccardo Focardi, and Matteo Maffei. 2004b. Compositional analysis of authentication protocols. In 13th European Symposium on Programming 2004 (ESOP’04) (LNCS), Vol. 2986. Springer, 140--154.Google ScholarCross Ref
- Michele Bugliesi, Riccardo Focardi, and Matteo Maffei. 2005. Analysis of typed analyses of authentication protocols. In Computer Security Foundations Workshop 2005 (CSFW’05). IEEE, 112--125. Google ScholarDigital Library
- Michele Bugliesi, Riccardo Focardi, and Matteo Maffei. 2007. Dynamic types for authentication. JCS 15, 6, 563--617. Google ScholarDigital Library
- Peter C. Chapin, Christian Skalka, and Xiaoyang Sean Wang. 2008. Authorization in trust management: Features and foundations. Comput Surveys 40, 3, Article 9, 48 pages. Google ScholarDigital Library
- Cas J. F. Cremers. 2008. The scyther tool: Verification, falsification, and analysis of security protocols. In Proceedings of Computer Aided Verification 2008 (CAV’08) (LNCS). Springer, 414--418. Google ScholarDigital Library
- Nicholaas G. de Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings) 75, 5, 381--392.Google ScholarCross Ref
- Manuel Fähndrich and Robert DeLine. 2002. Adoption and focus: Practical linear types for imperative programming. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation 2002 (PLDI’02). ACM, 13--24. Google ScholarDigital Library
- Riccardo Focardi and Matteo Maffei. 2011. Types for security protocols. In Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security, Vol. 5. IOS Press, Amsterdam, The Netherlands 143--181.Google Scholar
- Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. 2005. A type discipline for authorization policies. In 14th European Symposium on Programming 2005 (ESOP’05) (LNCS). Springer, 141--156. Google ScholarDigital Library
- Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. 2007. A type discipline for authorization in distributed systems. In Computer Security Foundations (CSF’07). IEEE, 31--45. Google ScholarDigital Library
- Cédric Fournet, Markulf Kohlweiss, and Pierre-Yves Strub. 2011. Modular code-based cryptographic verification. In ACM Conference on Computer and Communications Security 2011 (CCS’11). ACM, 341--350. Google ScholarDigital Library
- Jean-Yves Girard. 1995. Linear logic: Its syntax and semantics. In Advances in Linear Logic (London Mathematical Society LNS), Vol. 22. Cambridge University Press, 1--42. Google ScholarDigital Library
- Andrew D. Gordon and Alan Jeffrey. 2003. Authenticity by typing for security protocols. JCS 11, 4, 451--519. Google ScholarDigital Library
- Andrew D. Gordon and Alan Jeffrey. 2004. Types and effects for asymmetric cryptographic protocols. JCS 12, 3, 435--484. Google ScholarDigital Library
- Joshua D. Guttman, F. Javier Thayer, Jay A. Carlson, Jonathan C. Herzog, John D. Ramsdell, and Brian T. Sniffen. 2004. Trust management in strand spaces: A rely-guarantee method. In 13th European Symposium on Programming 2004 (ESOP’04) (LNCS). Springer, 325--339.Google Scholar
- Matteo Maffei. 2004. Tags for multi-protocol authentication. In Proceedings of the 2nd International Workshop on Security Issues in Coordination Models, Languages, and Systems (SECCO’04) (Electronic Notes on Theoretical Computer Science). Elsevier Science Publishers Ltd., 55--63. Google ScholarDigital Library
- Yitzhak Mandelbaum, David Walker, and Robert Harper. 2003. An effective theory of type refinements. In 8th ACM SIGPLAN International Conference on Functional Programming (ICFP’03). ACM, 213--225. Google ScholarDigital Library
- Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. 2013. The TAMARIN prover for the symbolic analysis of security protocols. In Proceedings of Computer Aided Verification 2013 (CAV’13) (LNCS). Springer, 696--701. Google ScholarDigital Library
- Robin Milner. 1992. Functions as processes. MSCS 2, 2, 119--141.Google Scholar
- James H. Morris. 1973. Protection in programming languages. CACM 16, 1, 15--21. Google ScholarDigital Library
- Karl Naden, Robert Bocchino, Jonathan Aldrich, and Kevin Bierhoff. 2012. A type system for borrowing permissions. In 39th ACM SIGT-SIGPLAN Symposium on Principles of Programming Languages (POPL’12). ACM, 557--570. Google ScholarDigital Library
- Jennifer G. Steiner, Clifford Neuman, and Jeffrey I. Schiller. 1988. Kerberos: An authentication service for open network systems. In USENIX’88. USENIX Association, 191--202.Google Scholar
- Eijiro Sumii and Benjamin C. Pierce. 2007. A bisimulation for dynamic sealing. TCS 375, 1--3, 169--192. Google ScholarDigital Library
- Joshua Sunshine, Karl Naden, Sven Stork, Jonathan Aldrich, and Éric Tanter. 2011. First-class state change in plaid. In 26th International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’11). ACM, 713--732. Google ScholarDigital Library
- Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011. Secure distributed programming with value-dependent types. In 16th ACM SIGPLAN International Conference on Functional Programming (ICFP’11). ACM, 266--278. Google ScholarDigital Library
- Alwen Tiu and Alberto Momigliano. 2012. Cut elimination for a logic with induction and co-induction. Journal of Applied Logic 10, 4, 330--367.Google ScholarCross Ref
- Naoyuki Tomura. 1995. llprover - A Linear Logic Prover. Retrieved June 2, 2015 from http://bach.istc.kobe-u.ac.jp/llprover/.Google Scholar
- Jesse Tov and Riccardo Pucella. 2010. Stateful contracts for affine types. In 19th European Symposium on Programming 2010 (ESOP’10). Springer, 550--569. Google ScholarDigital Library
- Anne S. Troelstra. 1992. Lectures on Linear Logic. Center for the Study of Language and Information, Stanford, CA, LNS, vol. 29.Google Scholar
Index Terms
- Affine Refinement Types for Secure Distributed Programming
Recommendations
Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations
Foundational Aspects of SecurityWe present a new type system for verifying the security of reference implementations of cryptographic protocols written in a core functional programming language. The type system combines prior work on refinement types, with union, intersection, and ...
Practical affine types
POPL '11Alms is a general-purpose programming language that supports practical affine types. To offer the expressiveness of Girard's linear logic while keeping the type system light and convenient, Alms uses expressive kinds that minimize notation while ...
Modeling abstract types in modules with open existential types
POPL '09We propose F-zip, a calculus of open existential types that is an extension of System F obtained by decomposing the introduction and elimination of existential types into more atomic constructs. Open existential types model modular type abstraction as ...
Reviews
Markus Wolf
Security of communication in modern applications is an increasingly important issue. Although there are strong cryptographic techniques, security is often broken nevertheless due to weaknesses in the implementation or in the exchange protocols. Advances in verification and theorem-proving techniques have led to techniques for encapsulating proofs of properties in the type of a program, leading to programs that, by typing alone, satisfy certain properties. This paper extends such techniques to affine logics, which are resource aware, that is, where the number of times information is used can be restricted. This can help prevent, for example, man-in-the-middle attacks. The paper starts with a general overview of the techniques of refinement types (dependent type packaging a type with a logical formula expressing properties of the values of the type). Some motivating examples illustrate that current techniques cannot easily capture bounds on resource usage. The following sections introduce the resource aware logic (affine logic) chosen as the basis for the later techniques, together with some key definitions and theorems. Next, the functional programming system RCF is extended by constructs and a type system based on affine logic and some basic properties of this formalism are proved. The third part of the paper presents a basic protocol library based on this system and analyzes two existing security protocols (EPMO and Kerberos) with the tools previously defined. The paper closes with a detailed analysis of type checking containing the structure of an algorithm for type checking. Finally, the usual overview of related work is given. Several appendices contain detailed proofs of several formal results stated in the paper. The paper is well structured, very thorough, and detailed, while still a good read. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments