Document Open Access Logo

Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk)

Authors Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.4.pdf
  • Filesize: 0.49 MB
  • 16 pages

Document Identifiers

Author Details

Andy Polyakov
  • The OpenSSL project
Ming-Hsien Tsai
  • Academia Sinica, Taiwan
Bow-Yaw Wang
  • Academia Sinica, Taiwan
Bo-Yin Yang
  • Academia Sinica, Taiwan

Funding

  • Tsai, Ming-Hsien: partially supported by the Academia Sinica Project AS-106-TP-A06
  • Wang, Bow-Yaw: partially supported by the Academia Sinica Project AS-106-TP-A06
  • Yang, Bo-Yin: partially supported by the MOST Project 105-2221-E-001-014-MY3

Cite As Get BibTex

Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.4

Abstract

Arithmetic over large finite fields is indispensable in modern cryptography. For efficienty, these operations are often implemented in manually optimized assembly programs. Since these arithmetic assembly programs necessarily perform lots of non-linear computation, checking their correctness is a challenging verification problem. We develop techniques to verify such programs automatically in this paper. Using our techniques, we have successfully verified a number of assembly programs in OpenSSL. Moreover, our tool verifies the boringSSL Montgomery Ladderstep (about 1400 assembly instructions) in 1 hour. This is by far the fastest verification technique for such programs.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
Keywords
  • Formal verification
  • Cryptography
  • Assembly Programs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Reynald Affeldt. On construction of a library of formally verified low-level arithmetic functions. Innovations in Systems and Software Engineering, 9(2):59-77, 2013. Google Scholar
  2. Reynald Affeldt and Nicolas Marti. An approach to formal verification of arithmetic functions in assembly. In Mitsu Okada and Ichiro Satoh, editors, Advances in Computer Science, volume 4435 of LNCS, pages 346-360. Springer, 2007. Google Scholar
  3. Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying assembly with formal security proofs: The case of BBS. Science of Computer Programming, 77(10-11):1058-1074, 2012. Google Scholar
  4. Andrew W. Appel. Verification of a cryptographic primitive: SHA-256. ACM Transactions on Programming Languages and Systems, 37(2):7:1-7:31, 2015. URL: http://dx.doi.org/10.1145/2701415.
  5. Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. Verified correctness and security of openssl HMAC. In USENIX Security Symposium 2015, pages 207-221. USENIX Association, 2015. Google Scholar
  6. Daniel J. Bernstein and Peter Schwabe. gfverif: Fast and easy verification of finite-field arithmetic, 2016. URL: http://gfverif.cryptojedi.org.
  7. B. Bond, C. Hawblitzel, M. Kapritsos, K. R. M. Leino, J. R. Lorch, B. Parno, A. Rane, S. Setty, and L. Thompson. Vale: Verifying high-performance cryptographic assembly code. In USENIX Security Symposium 2017, pages 917-934. USENIX Association, 2017. Google Scholar
  8. Yu-Fang Chen, Chang-Hong Hsu, Hsin-Hung Lin, Peter Schwabe, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, and Shang-Yi Yang. Verifying curve25519 software. In Gail-Joon Ahn, Moti Yung, and Ninghui Li, editors, CCS, pages 299-309. ACM, 2014. Google Scholar
  9. Fiat-crypto. https://github.com/mit-plv/fiat-crypto, 2015. Accessed: 2017-05-19.
  10. Michael R. Garey and David S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman and company, 1979. Google Scholar
  11. John Harrison. Automating elementary number-theoretic proofs using Gröbner bases. In Frank Pfenning, editor, CADE, volume 4603 of LNCS, pages 51-66. Springer, 2007. Google Scholar
  12. D. Kroening and O. Strichman. Decision Procedures - an algorithmic point of view. EATCS. Springer, 2008. Google Scholar
  13. Magnus O. Myreen and Gregorio Curello. Proof pearl: A verified bignum implementation in x86-64 machine code. In Certified Programs and Proofs, volume 8307 of LNCS, pages 66-81. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-319-03545-1_5.
  14. Magnus O. Myreen and Michael J. C. Gordon. Hoare logic for realistically modelled machine code. In Orna Grumberg and Michael Huth, editors, TACAS, volume 4424 of LNCS, pages 568-582. Springer, 2007. Google Scholar
  15. Aaron Tomb. Automated verification of real-world cryptographic implementations. IEEE Security & Privacy, 14(6):26-33, 2016. URL: http://dx.doi.org/10.1109/MSP.2016.125.
  16. Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. Certified verification of algebraic properties on low-level mathematical constructs in cryptographic programs. In David Evans, Tal Malkin, and Dongyan Xu, editors, CCS. ACM, 2017. Google Scholar
  17. Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, and Andrew W. Appel. Verified correctness and security of mbedtls HMAC-DRBG. In CCS, pages 2007-2020. ACM, 2017. URL: http://dx.doi.org/10.1145/3133956.3133974.
  18. Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. HACL*: A verified modern cryptographic library. In CCS, pages 1789-1806. ACM, 2017. URL: http://dx.doi.org/10.1145/3133956.3134043.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact