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.
Partially supported by the ACI jeunes chercheurs “Sécurité informatique, protocoles cryptographiques et détection d’intrusions” and the ACI cryptologie “Psi-Robuste”. Work done while the second author was at LSV.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Amadio, R.M., Charatonik, W.: On name generation and set-based analysis in the Dolev- Yao model. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 499–514. Springer, Heidelberg (2002)
Andersen, L.O.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen (DIKU report 94/19) (1994)
Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14), Cape Breton, Nova Scotia, Canada, June, pp. 82–96. IEEE Computer Society Press, Los Alamitos (2001)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Design and Implementation of a Special-Purpose Static Program Analyzer for Safety- Critical Real-Time Embedded Software. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85–108. Springer, Heidelberg (2002)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A Static Analyzer for Large Safety-Critical Software. In: ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLD 2003), San Diego, California, June, pp. 196–207. ACM Press, New York (2003)
Boury, P., Elkhadi, N.: Static Analysis of Java Cryptographic Applets. In: ECOOP 2001 Workshop on Formal Techniques for Java Programs. Fern Universität Hagen (2001)
Comon-Lundh, H., Cortier, V.: Security properties: Two agents are sufficient. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 99–113. Springer, Heidelberg (2003)
Dolev, D., Yao, A.C.: On security of public key protocols. IEEE trans. on Information Theory, IT 30, 198–208 (1983)
Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of bounded security protocols. In: Heintze, N., Clarke, E. (eds.) Proceedings of the Workshop on Formal Methods and Security Protocols – FMSP, Trento, Italy (July 1999)
Freier, A., Karlton, P., Kocher, P.: The SSL protocol. Version 3.0 (1996), http://home.netscape.com/eng/ssl3/
Gay, O.: 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
Goubault-Larrecq, J. (ed.): Special Issue on Models and Methods for Cryptographic Protocol Verification, Warsaw, Poland, December. Instytut Łącsności (Institute of Telecommunications), vol. 4 (2002)
Goubault-Larrecq, J.: 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 2004), Sainte-Marie-de-Ré France, Janvier (2004) INRIA
Heintze, N., Tardieu, O.: Ultra-fast aliasing analysis using cla: a million lines of c code in a second. In: Proc. of the ACM SIGPLAN 2001 conference on Programming language design and implementation, pp. 254–263. ACM Press, New York (2001)
Hind, M.: 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, pp. 54–61. ACM Press, New York (2001)
Kadhi, N.E.: Automatic verification of confidentiality properties of cryptographic programs. Networking and Information Systems 3(6) (2001)
Lowe, G.: An attack on the needham-schroeder public-key authentication protocol. Information Processing Letters 56(3), 131–133 (1995)
Milner, R.: Communication and concurrency. Prentice Hall International (UK) Ltd., Englewood Cliffs (1995)
Needham, R., Schroeder, M.: Using encryption for authentification in large networks of computers. Communications of the ACM 21(12) (December 1978)
Nielson, F., Riis Nielson, H., Seidl, H.: Normalizable horn clauses, strongly recognizable relations, and spi. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 20–35. Springer, Heidelberg (2002)
Parrennes, F.: The CSur project (2004), http://www.lsv.ens-cachan.fr/csur/
Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Prog. Lang. Sys. 24(3), 217–298 (2002)
Selinger, P.: Models for an adversary-centric protocol logic. Electronic Notes in Theoretical Computer Science 55(1), 73–87 (2001): Goubault-Larrecq, J. (ed.) Proceedings of the 1st Workshop on Logical Aspects of Cryptographic Protocol Verification, LACPV 2001 (2001)
Simon, A., King, A.: Analyzing string buffers in C. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 365–379. Springer, Heidelberg (2002)
Wagner, D., Foster, J.S., Brewer, E.A., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: Network and Distributed System Security Symposium, San Diego, CA, February, pp. 3–17 (2000)
Weidenbach, C.: Towards an automatic analysis of security protocols. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 314–328. Springer, Heidelberg (1999)
Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topic, D.: SPASS version 2.0. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 275–279. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goubault-Larrecq, J., Parrennes, F. (2005). Cryptographic Protocol Analysis on Real C Code. In: Cousot, R. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2005. Lecture Notes in Computer Science, vol 3385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30579-8_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-30579-8_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24297-0
Online ISBN: 978-3-540-30579-8
eBook Packages: Computer ScienceComputer Science (R0)