research-article

Open access

Affine Refinement Types for Secure Distributed Programming

Authors:

Michele Bugliesi,

Stefano Calzavara,

Fabienne Eigner,

Matteo MaffeiAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 37, Issue 4

Article No.: 11, Pages 1 - 66

https://doi.org/10.1145/2743018

Published: 13 August 2015 Publication History

PDF eReader

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.

References

[1]

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.

Digital Library

Google Scholar

[2]

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.

Digital Library

Google Scholar

[3]

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.

Digital Library

Google Scholar

[4]

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.

Digital Library

Google Scholar

[5]

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.

Digital Library

Google Scholar

[6]

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.

Digital Library

Google Scholar

[7]

Michael Backes, Catalin Hriţcu, and Matteo Maffei. 2011. Union and intersection types for secure protocol implementations. In TOSCA’11 (LNCS). Springer, 1--28.

Digital Library

Google Scholar

[8]

Michael Backes, Catalin Hriţcu, and Matteo Maffei. 2014. Union and intersection types for secure protocol implementations. JCS 22, 2, 301--353.

Digital Library

Google Scholar

[9]

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.

Digital Library

Google Scholar

[10]

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.

Digital Library

Google Scholar

[11]

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.

Digital Library

Google Scholar

[12]

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.

Digital Library

Google Scholar

[13]

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.

Digital Library

Google Scholar

[14]

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.

Digital Library

Google Scholar

[15]

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.

Digital Library

Google Scholar

[16]

Bruno Blanchet. 2001. An efficient cryptographic protocol verifier based on prolog rules. In 14th IEEE Computer Security Foundations Workshop (CSFW’01). IEEE, 82--96.

Digital Library

Google Scholar

[17]

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

[18]

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.

Digital Library

Google Scholar

[19]

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

[20]

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.

Digital Library

Google Scholar

[21]

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.

Digital Library

Google Scholar

[22]

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.

Crossref

Google Scholar

[23]

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.

Digital Library

Google Scholar

[24]

Michele Bugliesi, Riccardo Focardi, and Matteo Maffei. 2007. Dynamic types for authentication. JCS 15, 6, 563--617.

Digital Library

Google Scholar

[25]

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.

Digital Library

Google Scholar

[26]

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.

Digital Library

Google Scholar

[27]

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.

Crossref

Google Scholar

[28]

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.

Digital Library

Google Scholar

[29]

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

[30]

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.

Digital Library

Google Scholar

[31]

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.

Digital Library

Google Scholar

[32]

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.

Digital Library

Google Scholar

[33]

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.

Digital Library

Google Scholar

[34]

Andrew D. Gordon and Alan Jeffrey. 2003. Authenticity by typing for security protocols. JCS 11, 4, 451--519.

Digital Library

Google Scholar

[35]

Andrew D. Gordon and Alan Jeffrey. 2004. Types and effects for asymmetric cryptographic protocols. JCS 12, 3, 435--484.

Digital Library

Google Scholar

[36]

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

[37]

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.

Digital Library

Google Scholar

[38]

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.

Digital Library

Google Scholar

[39]

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.

Digital Library

Google Scholar

[40]

Robin Milner. 1992. Functions as processes. MSCS 2, 2, 119--141.

Google Scholar

[41]

James H. Morris. 1973. Protection in programming languages. CACM 16, 1, 15--21.

Digital Library

Google Scholar

[42]

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.

Digital Library

Google Scholar

[43]

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

[44]

Eijiro Sumii and Benjamin C. Pierce. 2007. A bisimulation for dynamic sealing. TCS 375, 1--3, 169--192.

Digital Library

Google Scholar

[45]

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.

Digital Library

Google Scholar

[46]

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.

Digital Library

Google Scholar

[47]

Alwen Tiu and Alberto Momigliano. 2012. Cut elimination for a logic with induction and co-induction. Journal of Applied Logic 10, 4, 330--367.

Crossref

Google Scholar

[48]

Naoyuki Tomura. 1995. llprover - A Linear Logic Prover. Retrieved June 2, 2015 from http://bach.istc.kobe-u.ac.jp/llprover/.

Google Scholar

[49]

Jesse Tov and Riccardo Pucella. 2010. Stateful contracts for affine types. In 19th European Symposium on Programming 2010 (ESOP’10). Springer, 550--569.

Digital Library

Google Scholar

[50]

Anne S. Troelstra. 1992. Lectures on Linear Logic. Center for the Study of Language and Information, Stanford, CA, LNS, vol. 29.

Google Scholar

Cited By

View all

Liao KHammer MMiller AMcKinley KFisher K(2019)ILC: a calculus for composable, computational cryptographyProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314607(640-654)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314607
Cortier VGrimm NLallemand JMaffei M(2018)Equivalence Properties by Typing in Cryptographic Branching ProtocolsPrinciples of Security and Trust10.1007/978-3-319-89722-6_7(160-187)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89722-6_7
Cortier VGrimm NLallemand JMaffei MThuraisingham BEvans DMalkin TXu D(2017)A Type System for Privacy PropertiesProceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security10.1145/3133956.3133998(409-423)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.1145/3133956.3133998
Show More Cited By

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 Security

We 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 '11

Alms 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 '09

We 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

Reviewer: 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 37, Issue 4

August 2015

204 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/2807424

Editor:
Jens Palsberg
University of California, Los Angeles, USA

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 August 2015

Accepted: 01 March 2015

Revised: 01 December 2014

Received: 01 March 2014

Published in TOPLAS Volume 37, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
363
Total Downloads

Downloads (Last 12 months)67
Downloads (Last 6 weeks)11

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Liao KHammer MMiller AMcKinley KFisher K(2019)ILC: a calculus for composable, computational cryptographyProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314607(640-654)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314607
Cortier VGrimm NLallemand JMaffei M(2018)Equivalence Properties by Typing in Cryptographic Branching ProtocolsPrinciples of Security and Trust10.1007/978-3-319-89722-6_7(160-187)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89722-6_7
Cortier VGrimm NLallemand JMaffei MThuraisingham BEvans DMalkin TXu D(2017)A Type System for Privacy PropertiesProceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security10.1145/3133956.3133998(409-423)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.1145/3133956.3133998
Balabonski TPottier FProtzenko J(2016)The Design and Formalization of Mezzo, a Permission-Based Programming LanguageACM Transactions on Programming Languages and Systems10.1145/283702238:4(1-94)Online publication date: 2-Aug-2016
https://doi.org/10.1145/2837022

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations

Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations

Practical affine types

Modeling abstract types in modules with open existential types

Reviews

Access critical reviews of Computing literature here

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations