Refinement Types for Secure Implementations

Jesper Bengtson; Karthikeyan Bhargavan; Cédric Fournet; Andrew D. Gordon; Sergio Maffeis

doi:10.1109/CSF.2008.27

Refinement Types for Secure Implementations

Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a λ-calculus equipped with reﬁnement types for expressing pre- and post-conditions within ﬁrst-order logic. We derive formal cryptographic primitives and represent active adversaries within the type theory. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. The implementation amounts to an enhanced typechecker for the general purpose functional language F#; typechecking generates veriﬁcation conditions that are passed to an SMT solver. We describe a series of checked examples. This is the ﬁrst tool to verify authentication properties of cryptographic protocols by typechecking their source code.

Original language	English
Title of host publication	Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, 23-25 June 2008
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Pages	17-32
Number of pages	16
ISBN (Print)	978-0-7695-3182-3
DOIs	https://doi.org/10.1109/CSF.2008.27
Publication status	Published - Jun 2008

Access to Document

10.1109/CSF.2008.27

http://doi.ieeecomputersociety.org/10.1109/CSF.2008.27

Cite this

@inproceedings{2f380b8ab1e945a1955b0f6f7f5f404a,

title = "Refinement Types for Secure Implementations",

abstract = "We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a λ-calculus equipped with reﬁnement types for expressing pre- and post-conditions within ﬁrst-order logic. We derive formal cryptographic primitives and represent active adversaries within the type theory. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. The implementation amounts to an enhanced typechecker for the general purpose functional language F#; typechecking generates veriﬁcation conditions that are passed to an SMT solver. We describe a series of checked examples. This is the ﬁrst tool to verify authentication properties of cryptographic protocols by typechecking their source code.",

author = "Jesper Bengtson and Karthikeyan Bhargavan and C{\'e}dric Fournet and Gordon, {Andrew D.} and Sergio Maffeis",

year = "2008",

month = jun,

doi = "10.1109/CSF.2008.27",

language = "English",

isbn = "978-0-7695-3182-3",

pages = "17--32",

booktitle = "Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, 23-25 June 2008",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

address = "United States",

}

Refinement Types for Secure Implementations. / Bengtson, Jesper; Bhargavan, Karthikeyan; Fournet, Cédric et al.

Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, 23-25 June 2008. Institute of Electrical and Electronics Engineers (IEEE), 2008. p. 17-32.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Refinement Types for Secure Implementations

AU - Bengtson, Jesper

AU - Bhargavan, Karthikeyan

AU - Fournet, Cédric

AU - Gordon, Andrew D.

AU - Maffeis, Sergio

PY - 2008/6

Y1 - 2008/6

N2 - We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a λ-calculus equipped with reﬁnement types for expressing pre- and post-conditions within ﬁrst-order logic. We derive formal cryptographic primitives and represent active adversaries within the type theory. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. The implementation amounts to an enhanced typechecker for the general purpose functional language F#; typechecking generates veriﬁcation conditions that are passed to an SMT solver. We describe a series of checked examples. This is the ﬁrst tool to verify authentication properties of cryptographic protocols by typechecking their source code.

AB - We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a λ-calculus equipped with reﬁnement types for expressing pre- and post-conditions within ﬁrst-order logic. We derive formal cryptographic primitives and represent active adversaries within the type theory. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. The implementation amounts to an enhanced typechecker for the general purpose functional language F#; typechecking generates veriﬁcation conditions that are passed to an SMT solver. We describe a series of checked examples. This is the ﬁrst tool to verify authentication properties of cryptographic protocols by typechecking their source code.

U2 - 10.1109/CSF.2008.27

DO - 10.1109/CSF.2008.27

M3 - Conference contribution

SN - 978-0-7695-3182-3

SP - 17

EP - 32

BT - Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, 23-25 June 2008

PB - Institute of Electrical and Electronics Engineers (IEEE)

ER -

Refinement Types for Secure Implementations

Abstract

Access to Document

Fingerprint

Cite this