More Web Proxy on the site http://driver.im/

research-article

Extracting and verifying cryptographic models from C protocol code by symbolic execution

Authors:

Mihhail Aizatulin,

Andrew D. Gordon,

Jan JürjensAuthors Info & Claims

CCS '11: Proceedings of the 18th ACM conference on Computer and communications security

Pages 331 - 340

https://doi.org/10.1145/2046707.2046745

Published: 17 October 2011 Publication History

Abstract

Consider the problem of verifying security properties of a cryptographic protocol coded in C. We propose an automatic solution that needs neither a pre-existing protocol description nor manual annotation of source code. First, symbolically execute the C program to obtain symbolic descriptions for the network messages sent by the protocol. Second, apply algebraic rewriting to obtain a process calculus description. Third, run an existing protocol analyser (ProVerif) to prove security properties or find attacks. We formalise our algorithm and appeal to existing results for ProVerif to establish computational soundness under suitable circumstances. We analyse only a single execution path, so our results are limited to protocols with no significant branching. The results in this paper provide the first computationally sound verification of weak secrecy and authentication for (single execution paths of) C code.

References

[1]

M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In ACM POPL, pages 104--115, 2001.

Digital Library

[2]

M. Aizatulin, A. D. Gordon, and J. Jürjens. Extracting and verifying cryptographic models from C protocol code by symbolic execution (long version). Available at http://arxiv.org/abs/1107.1017, 2011.

[3]

J. B. Almeida, M. Barbosa, J. S. Pinto, and B. Vieira. Deductive verification of cryptographic software. In NASA Formal Methods Symposium 2009, 2009.

[4]

A. Armando, D. A. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuéllar, P. H. Drielsma, P.-C. Héam, O. Kouchnarenko, J. Mantovani, S. Mödersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganò, and L. Vigneron. The AVISPA tool for the automated validation of internet security protocols and applications. In CAV, volume 3576 of Lecture Notes in Computer Science, pages 281--285. Springer, 2005.

Digital Library

[5]

M. Backes, D. Hofheinz, and D. Unruh. CoSP: A general framework for computational soundness proofs. In ACM CCS 2009, pages 66--78, November 2009. Preprint on IACR ePrint 2009/080.

Digital Library

[6]

J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. Refinement types for secure implementations. In CSF '08: Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, pages 17--32. IEEE Computer Society, 2008.

Digital Library

[7]

B. Blanchet. A computationally sound mechanized prover for security protocols. In IEEE Symposium on Security and Privacy, pages 140--154. IEEE Computer Society, 2006.

Digital Library

[8]

B. Blanchet. Automatic verification of correspondences for security protocols. Journal of Computer Security, 17(4):363--434, 2009.

[9]

B. Blanchet, M. Abadi, and C. Fournet. Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming, 75(1):3--51, Feb.--Mar. 2008.

[10]

M. Blum and S. Micali. How to generate cryptographically strong sequences of pseudo-random bits. SIAM J. Comput., 13(4):850--864, 1984.

Digital Library

[11]

J. Burnim and K. Sen. Heuristics for scalable dynamic test generation. In ASE '08: Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, pages 443--446. IEEE Computer Society, 2008.

Digital Library

[12]

C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008), San Diego, CA, Dec. 2008.

Digital Library

[13]

S. Chaki and A. Datta. ASPIER: An automated framework for verifying security protocol implementations. In Computer Security Foundations Workshop, pages 172--185, 2009.

Digital Library

[14]

R. Corin and F. A. Manzano. Efficient symbolic execution for analysing cryptographic protocol implementations. In International Symposium on Engineering Secure Software and Systems (ESSOS'11), LNCS. Springer, 2011.

Digital Library

[15]

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238--252, Los Angeles, California, 1977. ACM Press, New York, NY.

Digital Library

[16]

D. Dolev and A. Yao. On the Security of Public-Key Protocols. IEEE Transactions on Information Theory, 29(2):198--208, 1983.

Digital Library

[17]

B. Dutertre and L. D. Moura. The Yices SMT Solver. Technical report, 2006.

[18]

P. Godefroid, M. Y. Levin, and D. A. Molnar. Automated whitebox fuzz testing. In Proceedings of the Network and Distributed System Security Symposium, NDSS 2008. The Internet Society, 2008.

[19]

S. Goldwasser and S. Micali. Probabilistic encryption. Journal of Computer and System Sciences, 28:270--299, 1984.

[20]

J. Goubault-Larrecq and F. Parrennes. Cryptographic protocol analysis on real C code. In Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), volume 3385 of Lecture Notes in Computer Science, pages 363--379. Springer, 2005.

Digital Library

[21]

J. C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385--394, 1976.

Digital Library

[22]

R. Küsters and T. Truderung. Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation. In Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF 2009), pages 157--171. IEEE Computer Society, 2009.

Digital Library

[23]

R. Küsters and T. Truderung. Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach. Journal of Automated Reasoning, 46(3):325--352, 2011.

Digital Library

[24]

G. Lowe. An attack on the Needham-Schroeder public-key authentication protocol. Inf. Process. Lett., 56:131--133, November 1995.

Digital Library

[25]

G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In Proceedings of the 11th International Conference on Compiler Construction, CC '02, pages 213--228, London, UK, 2002. Springer-Verlag.

Digital Library

[26]

Project EVA. Security protocols open repository, 2007. http://www.lsv.ens-cachan.fr/spore/.

[27]

A. Rial and G. Danezis. Privacy-friendly smart metering. Technical Report MSR--TR--2010--150, 2010.

[28]

N. Swamy, J. Chen, C. Fournet, K. Bharagavan, and J. Yang. Security programming with refinement types and mobile proofs. Technical Report MSR--TR--2010--149, 2010.

[29]

D. Unruh. The impossibility of computationally sound XOR, July 2010. Preprint on IACR ePrint 2010/389.

[30]

A. C. Yao. Theory and application of trapdoor functions. In SFCS '82: Proceedings of the 23rd Annual Symposium on Foundations of Computer Science, pages 80--91. IEEE Computer Society, 1982.

Cited By

Morio KKünnemann RLuo BLiao XXu JKirda ELie D(2024)SpecMon: Modular Black-Box Runtime Monitoring of Security ProtocolsProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3690197(2741-2755)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3690197
Fang WYing M(2024)Symbolic Execution for Quantum Error Correction ProgramsProceedings of the ACM on Programming Languages10.1145/36564198:PLDI(1040-1065)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656419
Nasrabadi FKünnemann RNemati HMeng WJensen CCremers CKirda E(2023)CryptoBap: A Binary Analysis Platform for Cryptographic ProtocolsProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623090(1362-1376)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623090
Show More Cited By

Index Terms

Recommendations

Computational verification of C protocol implementations by symbolic execution
CCS '12: Proceedings of the 2012 ACM conference on Computer and communications security

We verify cryptographic protocols coded in C for correspondence properties with respect to the computational model of cryptography. The first step uses symbolic execution to extract a process calculus model from a C implementation of the protocol. The ...
Verifying systems rules using rule-directed symbolic execution
ASPLOS '13

Systems code must obey many rules, such as "opened files must be closed." One approach to verifying rules is static analysis, but this technique cannot infer precise runtime effects of code, often emitting many false positives. An alternative is ...
Verifying systems rules using rule-directed symbolic execution
ASPLOS '13: Proceedings of the eighteenth international conference on Architectural support for programming languages and operating systems

Systems code must obey many rules, such as "opened files must be closed." One approach to verifying rules is static analysis, but this technique cannot infer precise runtime effects of code, often emitting many false positives. An alternative is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '11: Proceedings of the 18th ACM conference on Computer and communications security

October 2011

742 pages

ISBN:9781450309486

DOI:10.1145/2046707

General Chair:
Yan Chen
Northwestern University, USA
,
Program Chairs:
George Danezis
Microsoft Research Cambridge, UK
,
Vitaly Shmatikov
University of Texas at Austin, USA

Copyright © 2011 ACM.

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 ACM 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]

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 October 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

CCS'11

Sponsor:

SIGSAC

CCS'11: the ACM Conference on Computer and Communications Security

October 17 - 21, 2011

Illinois, Chicago, USA

Acceptance Rates

CCS '11 Paper Acceptance Rate 60 of 429 submissions, 14%;

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '25

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 13 - 17, 2025

Taipei , Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

37
Total Citations
View Citations
533
Total Downloads

Downloads (Last 12 months)21
Downloads (Last 6 weeks)2

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Morio KKünnemann RLuo BLiao XXu JKirda ELie D(2024)SpecMon: Modular Black-Box Runtime Monitoring of Security ProtocolsProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3690197(2741-2755)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3690197
Fang WYing M(2024)Symbolic Execution for Quantum Error Correction ProgramsProceedings of the ACM on Programming Languages10.1145/36564198:PLDI(1040-1065)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656419
Nasrabadi FKünnemann RNemati HMeng WJensen CCremers CKirda E(2023)CryptoBap: A Binary Analysis Platform for Cryptographic ProtocolsProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623090(1362-1376)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623090
Prokopev S(2023)Cryptographic protocol conformance testing based on domain-specific state machineJournal of Computer Virology and Hacking Techniques10.1007/s11416-023-00474-120:2(249-259)Online publication date: 3-Apr-2023
https://doi.org/10.1007/s11416-023-00474-1
Pan YLin WHe YZhu Y(2022)Coverage-guided differential testing of TLS implementations based on syntax mutationPLOS ONE10.1371/journal.pone.026217617:1(e0262176)Online publication date: 24-Jan-2022
https://doi.org/10.1371/journal.pone.0262176
Ho SProtzenko JBichhawat ABhargavan K(2022)Noise: A Library of Verified High-Performance Secure Channel Protocol Implementations2022 IEEE Symposium on Security and Privacy (SP)10.1109/SP46214.2022.9833621(107-124)Online publication date: May-2022
https://doi.org/10.1109/SP46214.2022.9833621
Yu YLiu JMu D(2022)A Points-to-Sensitive Model Checker for C Programs in IoT FirmwareIEEE Internet of Things Journal10.1109/JIOT.2022.31633839:19(18998-19011)Online publication date: 1-Oct-2022
https://doi.org/10.1109/JIOT.2022.3163383
Aljaafari FMenezes RManino EShmarov FMustafa MCordeiro L(2022)Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent ProgramsIEEE Access10.1109/ACCESS.2022.322335910(121365-121384)Online publication date: 2022
https://doi.org/10.1109/ACCESS.2022.3223359
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
Mahadewa KWang KBai GShi LLiu YDong JLiang Z(2021)Scrutinizing Implementations of Smart Home IntegrationsIEEE Transactions on Software Engineering10.1109/TSE.2019.296069047:12(2667-2683)Online publication date: 1-Dec-2021
https://doi.org/10.1109/TSE.2019.2960690
Show More Cited By

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents