2026-08-19T09:47:23Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9542 2024-03-06T10:44:41Z ddc:004 open_access

Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk) Polyakov, Andy Tsai, Ming-Hsien Wang, Bow-Yaw Yang, Bo-Yin Formal verification Cryptography Assembly Programs 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andy Polyakov and Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang 2018 Is Part Of LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2018.4 urn:nbn:de:0030-drops-95425 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.4 eng https://creativecommons.org/licenses/by/3.0/legalcode