Article

Cryptographic protocol analysis on real c code

Authors:

Jean Goubault-Larrecq,

Fabrice ParrennesAuthors Info & Claims

VMCAI'05: Proceedings of the 6th international conference on Verification, Model Checking, and Abstract Interpretation

Pages 363 - 379

https://doi.org/10.1007/978-3-540-30579-8_24

Published: 17 January 2005 Publication History

Abstract

Implementations of cryptographic protocols, such as OpenSSL for example, contain bugs affecting security, which cannot be detected by just analyzing abstract protocols (e.g., SSL or TLS). We describe how cryptographic protocol verification techniques based on solving clause sets can be applied to detect vulnerabilities of C programs in the Dolev-Yao model, statically. This involves integrating fairly simple pointer analysis techniques with an analysis of which messages an external intruder may collect and forge. This also involves relating concrete run-time data with abstract, logical terms representing messages. To this end, we make use of so-called trust assertions. The output of the analysis is a set of clauses in the decidable class $\mathcal{H}_1$, which can then be solved independently. This can be used to establish secrecy properties, and to detect some other bugs.

References

[1]

R. M. Amadio and W. Charatonik. On name generation and set-based analysis in the Dolev-Yao model. In 13th International Conference on Concurrency Theory CONCUR'02, volume 2421 of Lecture Notes in Computer Science, pages 499-514. Springer-Verlag, 2002.

Digital Library

[2]

L. O. Andersen. Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen, 1994. (DIKU report 94/19).

[3]

B. Blanchet. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 82-96, Cape Breton, Nova Scotia, Canada, June 2001. IEEE Computer Society.

Digital Library

[4]

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L.Mauborgne, A.Miné, D. Monniaux, and X. Rival. Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software, invited chapter. In T. Mogensen, D. A. Schmidt, and I. H. Sudborough, editors, The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, volume 2566 of Lecture Notes on Computer Science, pages 85-108. Springer Verlag, Dec. 2002.

Digital Library

[5]

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A Static Analyzer for Large Safety-Critical Software. In ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI'03), pages 196- 207, San Diego, California, June 2003. ACM.

Digital Library

[6]

P. Boury and N. Elkhadi. Static Analysis of Java Cryptographic Applets. In ECOOP'2001 Workshop on Formal Techniques for Java Programs. Fern Universität Hagen, 2001.

[7]

H. Comon-Lundh and V. Cortier. Security properties: Two agents are sufficient. In Proc. 12th European Symposium on Programming (ESOP'2003), pages 99-113, Warsaw, Poland, Apr. 2003. Springer-Verlag LNCS 2618.

Digital Library

[8]

D. Dolev and A. C. Yao. On security of public key protocols. IEEE trans. on Information Theory, IT-30:198-208, 1983.

[9]

N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In N. Heintze and E. Clarke, editors, Proceedings of the Workshop on Formal Methods and Security Protocols - FMSP, Trento, Italy, July 1999.

[10]

A. Freier, P. Karlton, and P. Kocher. The SSL protocol. Version 3.0., 1996. http://home. netscape.com/eng/ssl3/.

[11]

O. Gay. Exploitation avancée de buffer overflows. Technical report, LASEC, Ecole Polytechnique Fédérale de Lausanne, June 2002. http://diwww.epfl.ch/~ogay/advbof/ advbof.pdf.

[12]

J. Goubault-Larrecq, editor. Special Issue on Models and Methods for Cryptographic Protocol Verification, volume 4. Instytut Lacsności (Institute of Telecommunications), Warsaw, Poland, Dec. 2002.

[13]

J. Goubault-Larrecq. Une fois qu'on n'a pas trouvé de preuve, comment le faire comprendre à un assistant de preuve ? In Actes 15èmes journées francophones sur les langages applicatifs (JFLA'04), Sainte-Marie-de-Ré France, Janvier 2004. INRIA.

[14]

N. Heintze and O. Tardieu. Ultra-fast aliasing analysis using cla: a million lines of c code in a second. In Proc. of the ACM SIGPLAN'01 conference on Programming language design and implementation, pages 254-263. ACM Press, 2001.

Digital Library

[15]

M. Hind. Pointer analysis: haven't we solved this problem yet? In Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, pages 54-61. ACM Press, 2001.

Digital Library

[16]

N. E. Kadhi. Automatic verification of confidentiality properties of cryptographic programs. Networking and Information Systems, 3(6), 2001.

[17]

G. Lowe. An attack on the needham-schroeder public-key authentication protocol. Information Processing Letters, 56(3):131-133, 1995.

Digital Library

[18]

R. Milner. Communication and concurrency. Prentice Hall International (UK) Ltd., 1995.

Digital Library

[19]

R. Needham and M. Schroeder. Using encryption for authentification in large networks of computers. Communications of the ACM, 21(12), December 1978.

Digital Library

[20]

F. Nielson, H. R. Nielson, and H. Seidl. Normalizable horn clauses, strongly recognizable relations, and spi. In Proceedings of the 9th International Symposium on Static Analysis, volume 2477, pages 20-35. Springer-Verlag, 2002.

Digital Library

[21]

F. Parrennes. The CSur project. http://www.lsv.ens-cachan.fr/csur/, 2004.

[22]

S. Sagiv, T. W. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Trans. Prog. Lang. Sys., 24(3):217-298, may 2002.

Digital Library

[23]

P. Selinger. Models for an adversary-centric protocol logic. Electronic Notes in Theoretical Computer Science, 55(1):73-87, July 2001. Proceedings of the 1st Workshop on Logical Aspects of Cryptographic Protocol Verification (LACPV'01), J. Goubault-Larrecq, ed.

[24]

A. Simon and A. King. Analyzing string buffers in C. In Intl. Conf. on Algebraic Methods and Software Methodology (AMAST'2002), pages 365-379, 2002.

Digital Library

[25]

D.Wagner, J. S. Foster, E. A. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In Network and Distributed System Security Symposium, pages 3-17, San Diego, CA, February 2000.

[26]

C.Weidenbach. Towards an automatic analysis of security protocols. In H. Ganzinger, editor, 16th International Conference on Automated Deduction CADE-16, volume 1632, pages 378- 382. Springer, 1999.

Digital Library

[27]

C. Weidenbach, U. Brahm, T. Hillenbrand, E. Keen, C. Theobald, and D. Topic. SPASS version 2.0. In Proc. 18th Conference on Automated Deduction (CADE 2002), pages 275-279. Springer-Verlag LNCS 2392, 2002.

Digital Library

Cited By

Zhang XZhang CLi XDu ZMao BLi YZheng YLi YPan LLiu YDeng R(2024)A Survey of Protocol FuzzingACM Computing Surveys10.1145/369678857:2(1-36)Online publication date: 10-Oct-2024
https://dl.acm.org/doi/10.1145/3696788
Wu FLiu JLi YNi M(2024)LπCETIET Information Security10.1049/2024/26347442024Online publication date: 1-Jan-2024
https://dl.acm.org/doi/10.1049/2024/2634744
Yao JXu CLi DLin SCao X(2022)Formal Verification of Security Protocols: ProVerif and ExtensionsArtificial Intelligence and Security10.1007/978-3-031-06788-4_42(500-512)Online publication date: 15-Jul-2022
https://dl.acm.org/doi/10.1007/978-3-031-06788-4_42
Show More Cited By

Cryptographic protocol analysis on real c code

Recommendations

Parallel Maude-NPA for Cryptographic Protocol Analysis
Rewriting Logic and Its Applications
Abstract
Maude-NPA is a symbolic model checker for analyzing cryptographic protocols in the Dolev-Yao strand space model modulo an equational theory defining the cryptographic operations, which starts from an attack state to find counterexamples by ...
A Cryptographic Analysis of the TLS 1.3 Handshake Protocol Candidates
CCS '15: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security

The Internet Engineering Task Force (IETF) is currently developing the next version of the Transport Layer Security (TLS) protocol, version 1.3. The transparency of this standardization process allows comprehensive cryptographic analysis of the ...
Verifpal: Cryptographic Protocol Analysis for the Real World
Progress in Cryptology – INDOCRYPT 2020
Abstract
Verifpal is a new automated modeling framework and verifier for cryptographic protocols, optimized with heuristics for common-case protocol specifications, that aims to work better for real-world practitioners, students and engineers without ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

VMCAI'05: Proceedings of the 6th international conference on Verification, Model Checking, and Abstract Interpretation

January 2005

481 pages

ISBN:354024297X

Editor:
Radhia Cousot
CNRS, Paris, France

Sponsors

ACM: Association for Computing Machinery
EAPLS: European Association for Programming Languages and Systems

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 17 January 2005

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

41
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Zhang XZhang CLi XDu ZMao BLi YZheng YLi YPan LLiu YDeng R(2024)A Survey of Protocol FuzzingACM Computing Surveys10.1145/369678857:2(1-36)Online publication date: 10-Oct-2024
https://dl.acm.org/doi/10.1145/3696788
Wu FLiu JLi YNi M(2024)LπCETIET Information Security10.1049/2024/26347442024Online publication date: 1-Jan-2024
https://dl.acm.org/doi/10.1049/2024/2634744
Yao JXu CLi DLin SCao X(2022)Formal Verification of Security Protocols: ProVerif and ExtensionsArtificial Intelligence and Security10.1007/978-3-031-06788-4_42(500-512)Online publication date: 15-Jul-2022
https://dl.acm.org/doi/10.1007/978-3-031-06788-4_42
Vanhoef MPiessens FRossow CYounan Y(2018)Symbolic execution of security protocol implementationsProceedings of the 12th USENIX Conference on Offensive Technologies10.5555/3307423.3307436(13-13)Online publication date: 13-Aug-2018
https://dl.acm.org/doi/10.5555/3307423.3307436
Wu FZhang HWang WJia JYuan S(2017)A New Method to Analyze the Security of Protocol Implementations Based on Ideal TraceSecurity and Communication Networks10.1155/2017/70428352017Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1155/2017/7042835
Diaz JArroyo DRodriguez F(2014)A formal methodology for integral security design and verification of network protocolsJournal of Systems and Software10.5555/2747476.274752989:C(87-98)Online publication date: 1-Mar-2014
https://dl.acm.org/doi/10.5555/2747476.2747529
Backes MHriţcu CMaffei M(2014)Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementationsJournal of Computer Security10.5555/2595841.259584522:2(301-353)Online publication date: 1-Mar-2014
https://dl.acm.org/doi/10.5555/2595841.2595845
Cortier VKremer S(2014)Formal Models and Techniques for Analyzing Security ProtocolsFoundations and Trends in Programming Languages10.1561/25000000011:3(151-267)Online publication date: 13-Nov-2014
https://dl.acm.org/doi/10.1561/2500000001
Sun CWang ZWang G(2014)A property-based testing framework for encryption programsFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-014-3040-y8:3(478-489)Online publication date: 1-Jun-2014
https://dl.acm.org/doi/10.1007/s11704-014-3040-y
Aizatulin MGordon AJürjens JYu TDanezis GGligor V(2012)Computational verification of C protocol implementations by symbolic executionProceedings of the 2012 ACM conference on Computer and communications security10.1145/2382196.2382271(712-723)Online publication date: 16-Oct-2012
https://dl.acm.org/doi/10.1145/2382196.2382271
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents