Article

Verifying cryptographic code in c: some experience and the csec challenge

Authors:

Mihhail Aizatulin,

François Dupressoir,

Andrew D. Gordon,

Jan JürjensAuthors Info & Claims

FAST'11: Proceedings of the 8th international conference on Formal Aspects of Security and Trust

Pages 1 - 20

https://doi.org/10.1007/978-3-642-29420-4_1

Published: 12 September 2011 Publication History

Abstract

The security of much critical infrastructure depends in part on cryptographic software coded in C, and yet vulnerabilities continue to be discovered in such software. We describe recent progress on checking the security of C code implementing cryptographic software. In particular, we describe projects that combine verification-condition generation and symbolic execution techniques for C, with methods for stating and verifying security properties of abstract models of cryptographic protocols. We illustrate these techniques on C code for a simple two-message protocol.

References

[1]

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

Digital Library

[2]

Aizatulin, M., Dupressoir, F., Gordon, A., Jürjens, J.: Verifying cryptographic code in C: Some experience and the Csec challenge. Technical Report MSRTR- 2011-118, Microsoft Research (November 2011a)

[3]

Aizatulin, M., Gordon, A., Jürjens, J.: Extracting and verifying cryptographic models from C protocol code by symbolic execution. In: 18th ACM Conference on Computer and Communications Security, CCS 2011 (2011), http://arxiv.org/abs/1107.1017

Digital Library

[4]

Backes, M., Hofheinz, D., Unruh, D.: CoSP: A general framework for computational soundness proofs. In: ACM CCS 2009, pp. 66-78 (November 2009); preprint on IACR ePrint 2009/080

Digital Library

[5]

Barbosa, M., Pinto, J., Filliâtre, J., Vieira, B.: A deductive verification platform for cryptographic software. In: Proceedings of the Fourth International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010). Electronic Communications of the EASST, vol. 33. EASST (2010)

[6]

Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A. D., Maffeis, S.: Refinement types for secure implementations. In: 21st IEEE Computer Security Foundations Symposium (CSF 2008), pp. 17-32 (2008)

Digital Library

[7]

Bhargavan, K., Fournet, C., Gordon, A. D.: Modular verification of security protocol code by typing. In: ACM Symposium on Principles of Programming Languages (POPL 2010), pp. 445-456 (2010)

Digital Library

[8]

Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: IEEE Computer Security Foundations Workshop (CSFW 2001), pp. 82-96 (2001)

Digital Library

[9]

Cadar, C., Dunbar, D., Engler, D.: 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 (December 2008)

Digital Library

[10]

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

Digital Library

[11]

Cohen, E., Dahlweid, M., Hillebrand, M. A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A Practical System for Verifying Concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23-42. Springer, Heidelberg (2009)

Digital Library

[12]

Corin, R., Manzano, F. A.: Efficient Symbolic Execution for Analysing Cryptographic Protocol Implementations. In: Erlingsson, Ú., Wieringa, R., Zannone, N. (eds.) ESSoS 2011. LNCS, vol. 6542, pp. 58-72. Springer, Heidelberg (2011)

Digital Library

[13]

Dupressoir, F., Gordon, A., Jürjens, J., Naumann, D.: Guiding a general-purpose C verifier to prove cryptographic protocols. In: 24th IEEE Computer Security Foundations Symposium, pp. 3-17 (2011)

Digital Library

[14]

Dutertre, B., de Moura, L.: The Yices SMT Solver. Technical report (2006)

[15]

Erkök, L., Carlsson, M., Wick, A.: Hardware/software co-verification of cryptographic algorithms using Cryptol. In: FMCAD (2009)

[16]

Fournet, C., Bhargavan, K., Gordon, A. D.: Cryptographic Verification by Typing for a Sample Protocol Implementation. In: Aldini, A., Gorrieri, R. (eds.) FOSAD 2011. LNCS, vol. 6858, pp. 66-100. Springer, Heidelberg (2011)

Digital Library

[17]

Fournet, C., Kohlweiss, M., Strub, P.-Y.: Modular code-based cryptographic verification. In: 18th ACM Conference on Computer and Communications Security, CCS 2011 (2011) Technical report, sample code, and formal proofs available from, http://research.microsoft.com/~fournet/comp-f7/

Digital Library

[18]

Godefroid, P., Khurshid, S.: Exploring Very Large State Spaces using Genetic Algorithms. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 266-280. Springer, Heidelberg (2002)

Digital Library

[19]

Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Programming Language Design and Implementation (PLDI 2005), pp. 213- 223. ACM (2005)

Digital Library

[20]

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

[21]

Goubault-Larrecq, J., Parrennes, F.: Cryptographic Protocol Analysis on Real C Code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 363-379. Springer, Heidelberg (2005)

Digital Library

[22]

Hritçu, C.: Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis. PhD thesis, Department of Computer Science, Saarland University (2011)

[23]

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

Digital Library

[24]

McGrew, D. A., Viega, J.: Flexible and efficient message authentication in hardware and software. manuscript and software available at (2005), http://www.zork.org/gcm

[25]

Necula, G.C., McPeak, S., Rahul, S. P., Weimer, W.: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: Proceedings of the 11th International Conference on Compiler Construction, CC 2002, pp. 213-228. Springer, London (2002) ISBN 3-540-43369-4, http://portal.acm.org/citation.cfm?id=647478.727796

Digital Library

[26]

PolarSSL. PolarSSL, http://polarssl.org

[27]

Polikarpova, N., Moskal, M.: Verifying implementations of security protocols by refinement. In: Verified Software: Theories, Tools and Experiments, VSTTE 2012 (to appear, 2012)

Digital Library

[28]

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

[29]

Udrea, O., Lumezanu, C., Foster, J. S.: Rule-Based static analysis of network protocol implementations. In: Proceedings of the 15Th Usenix Security Symposium, pp. 193-208 (2006), http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.111.8168

Digital Library

Cited By

Voelter MMolotnikov ZKolb BGray JSprinkle JTolvanen JRossi M(2015)Towards improving software security using language engineering and mbeddr CProceedings of the Workshop on Domain-Specific Modeling10.1145/2846696.2846698(55-62)Online publication date: 27-Oct-2015
https://dl.acm.org/doi/10.1145/2846696.2846698
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
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

Verifying cryptographic code in c: some experience and the csec challenge

Recommendations

Verifying verified code
Abstract
A recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a follow-up case study that explores the methodology from the perspective of three research ...
Verifying Code and Its Optimizations: An Experience Report
ICSTW '11: Proceedings of the 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops

We present our experience in formally verifying the correctness of a 200-line industrial C implementation of Cyclic Redundancy Check (CRC) and its optimizations. Our experience indicates that (a) both the specification and verification of even such ...
Extracting and verifying cryptographic models from C protocol code by symbolic execution
CCS '11: Proceedings of the 18th ACM conference on Computer and communications security

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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FAST'11: Proceedings of the 8th international conference on Formal Aspects of Security and Trust

September 2011

277 pages

ISBN:9783642294198

Editors:
Gilles Barthe
IMDEA Software Institute, Universidad Politecnica de Madrid, Campus Montegancedo, Boadilla del Monte, Madrid, Spain
,
Anupam Datta
IMDEA Software Institute, Carnegie Mellon University, NASA Research Park, Bldg. 23 (MS 23-11), Moffet Field, CA, Spain
,
Sandro Etalle
Faculty of Mathematics and Computer Science, Embedded Systems Security Group, Technical University of Eindhoven, NASA Research Park, Bldg. 23 (MS 23-11), Eindhoven, CA, The Netherlands

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 12 September 2011

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Voelter MMolotnikov ZKolb BGray JSprinkle JTolvanen JRossi M(2015)Towards improving software security using language engineering and mbeddr CProceedings of the Workshop on Domain-Specific Modeling10.1145/2846696.2846698(55-62)Online publication date: 27-Oct-2015
https://dl.acm.org/doi/10.1145/2846696.2846698
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
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

View Options

View options

Figures

Tables

Media

View Table of Conten