Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/3611643.3613096acmconferencesArticle/Chapter ViewAbstractPublication PagesfseConference Proceedingsconference-collections
research-article
Open access

llvm2CryptoLine: Verifying Arithmetic in Cryptographic C Programs

Published: 30 November 2023 Publication History

Abstract

Correct implementations of cryptographic primitives are essential for modern security. These implementations often contain arithmetic operations involving non-linear computations that are infamously hard to verify. We present llvm2CryptoLine, an automated formal verification tool for arithmetic operations in cryptographic C programs. llvm2CryptoLine successfully verifies 51 arithmetic C programs from industrial cryptographic libraries OpenSSL, wolfSSL and NaCl. Most of the programs are verified fully automatically and efficiently. A screencast that showcases llvm2CryptoLine can be found at https://youtu.be/QXuSmja45VA. Source code is available at https://github.com/fmlab-iis/llvm2cryptoline.

References

[1]
Daniel J. Bernstein. 2006. Curve25519: New Diffie-Hellman Speed Records. In Public Key Cryptography - PKC 2006, 9th International Conference on Theory and Practice of Public-Key Cryptography, New York, NY, USA, April 24-26, 2006, Proceedings, Moti Yung, Yevgeniy Dodis, Aggelos Kiayias, and Tal Malkin (Eds.) (Lecture Notes in Computer Science, Vol. 3958). Springer, 207–228. https://doi.org/10.1007/11745853_14
[2]
Dirk Beyer and M. Erkan Keremoglu. 2011. CPAchecker: A Tool for Configurable Software Verification. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.) (Lecture Notes in Computer Science, Vol. 6806). Springer, 184–190. https://doi.org/10.1007/978-3-642-22110-1_16
[3]
Marek Chalupa, Vincent Mihalkovic, Anna Rechtácková, Lukás Zaoral, and Jan Strejcek. 2022. Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding - (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II, Dana Fisman and Grigore Rosu (Eds.) (Lecture Notes in Computer Science, Vol. 13244). Springer, 462–467. https://doi.org/10.1007/978-3-030-99527-0_32
[4]
The NaCl Developers. 2011. NaCl: Networking and Cryptography library. https://nacl.cr.yp.to/
[5]
The wolfSSL Developers. 2023. The wolfSSL Library. https://github.com/wolfSSL/wolfssl
[6]
Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Frank Schüssele, and Andreas Podelski. 2023. Ultimate Taipan and Race Detection in Ultimate - (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, Sriram Sankaranarayanan and Natasha Sharygina (Eds.) (Lecture Notes in Computer Science, Vol. 13994). Springer, 582–587. https://doi.org/10.1007/978-3-031-30820-8_40
[7]
Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. 2019. Signed Cryptographic Program Verification with Typed CryptoLine. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019, Lorenzo Cavallaro, Johannes Kinder, XiaoFeng Wang, and Jonathan Katz (Eds.). ACM, 1591–1606. https://doi.org/10.1145/3319535.3354199
[8]
Mikhail Y. R. Gadelha, Felipe R. Monteiro, Lucas C. Cordeiro, and Denis A. Nicole. 2019. ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference - (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen (Eds.) (Lecture Notes in Computer Science, Vol. 11429). Springer, 209–213. https://doi.org/10.1007/978-3-030-17502-3_15
[9]
Matthias Heizmann, Max Barth, Daniel Dietsch, Leonard Fichtner, Jochen Hoenicke, Dominik Klumpp, Mehdi Naouar, Tanja Schindler, Frank Schüssele, and Andreas Podelski. 2023. Ultimate Automizer and the CommuHash Normal Form - (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, Sriram Sankaranarayanan and Natasha Sharygina (Eds.) (Lecture Notes in Computer Science, Vol. 13994). Springer, 577–581. https://doi.org/10.1007/978-3-031-30820-8_39
[10]
C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM, 12, 10 (1969), 576–580. https://doi.org/10.1145/363235.363259
[11]
James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM, 19, 7 (1976), 385–394. https://doi.org/10.1145/360248.360252
[12]
Neal Koblitz. 1987. Elliptic curve cryptosystems. Mathematics of computation, 48, 177 (1987), 203–209.
[13]
Daniel Kroening and Michael Tautschnig. 2014. CBMC - C Bounded Model Checker - (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, Erika Ábrahám and Klaus Havelund (Eds.) (Lecture Notes in Computer Science, Vol. 8413). Springer, 389–391. https://doi.org/10.1007/978-3-642-54862-8_26
[14]
Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. 2019. Verifying Arithmetic in Cryptographic C Programs. In 34th IEEE/ACM International Conference on Automated Software Engineering, ASE 2019, San Diego, CA, USA, November 11-15, 2019. IEEE, 552–564. https://doi.org/10.1109/ASE.2019.00058
[15]
Victor S. Miller. 1985. Use of Elliptic Curves in Cryptography. In Advances in Cryptology - CRYPTO ’85, Santa Barbara, California, USA, August 18-22, 1985, Proceedings, Hugh C. Williams (Ed.) (Lecture Notes in Computer Science, Vol. 218). Springer, 417–426. https://doi.org/10.1007/3-540-39799-X_31
[16]
David Molnar, Matt Piotrowski, David Schultz, and David A. Wagner. 2005. The Program Counter Security Model: Automatic Detection and Removal of Control-Flow Side Channel Attacks. In Information Security and Cryptology - ICISC 2005, 8th International Conference, Seoul, Korea, December 1-2, 2005, Revised Selected Papers, Dongho Won and Seungjoo Kim (Eds.) (Lecture Notes in Computer Science, Vol. 3935). Springer, 156–168. https://doi.org/10.1007/11734727_14
[17]
Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. 2018. Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). In 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, Sven Schewe and Lijun Zhang (Eds.) (LIPIcs, Vol. 118). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 4:1–4:16. https://doi.org/10.4230/LIPIcs.CONCUR.2018.4
[18]
The OpenSSL Project. 2023. The OpenSSL Library. https://github.com/openssl/openssl
[19]
Zvonimir Rakamaric and Michael Emmi. 2014. SMACK: Decoupling Source Language Details from Verifier Implementations. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, Armin Biere and Roderick Bloem (Eds.) (Lecture Notes in Computer Science, Vol. 8559). Springer, 106–113. https://doi.org/10.1007/978-3-319-08867-9_7
[20]
Cedric Richter and Heike Wehrheim. 2019. PeSCo: Predicting Sequential Combinations of Verifiers - (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen (Eds.) (Lecture Notes in Computer Science, Vol. 11429). Springer, 229–233. https://doi.org/10.1007/978-3-030-17502-3_19
[21]
Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, and Bo-Yin Yang. 2023. Certified Verification for Algebraic Abstraction. In Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, Constantin Enea and Akash Lal (Eds.) (Lecture Notes in Computer Science, Vol. 13966). Springer, 329–349. https://doi.org/10.1007/978-3-031-37709-9_16

Cited By

View all
  • (2024)Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence CheckingComputer Security – ESORICS 202410.1007/978-3-031-70903-6_19(377-395)Online publication date: 16-Sep-2024

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
ESEC/FSE 2023: Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering
November 2023
2215 pages
ISBN:9798400703270
DOI:10.1145/3611643
This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 30 November 2023

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. cryptographic programs
  2. formal verification
  3. functional correctness

Qualifiers

  • Research-article

Funding Sources

Conference

ESEC/FSE '23
Sponsor:

Acceptance Rates

Overall Acceptance Rate 112 of 543 submissions, 21%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)215
  • Downloads (Last 6 weeks)18
Reflects downloads up to 19 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2024)Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence CheckingComputer Security – ESORICS 202410.1007/978-3-031-70903-6_19(377-395)Online publication date: 16-Sep-2024

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media