Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2018.4
URN: urn:nbn:de:0030-drops-95425
URL: https://drops.dagstuhl.de/opus/volltexte/2018/9542/
Polyakov, Andy ; Tsai, Ming-Hsien ; Wang, Bow-Yaw ; Yang, Bo-Yin
Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk)
| pdf-format: |
|
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.
BibTeX - Entry
@InProceedings{polyakov_et_al:LIPIcs:2018:9542,
author = {Andy Polyakov and Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang},
title = {{Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk)}},
booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)},
pages = {4:1--4:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-087-3},
ISSN = {1868-8969},
year = {2018},
volume = {118},
editor = {Sven Schewe and Lijun Zhang},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/9542},
URN = {urn:nbn:de:0030-drops-95425},
doi = {10.4230/LIPIcs.CONCUR.2018.4},
annote = {Keywords: Formal verification, Cryptography, Assembly Programs}
}
| Keywords: | Formal verification, Cryptography, Assembly Programs | |
| Seminar: | 29th International Conference on Concurrency Theory (CONCUR 2018) | |
| Issue date: | 2018 | |
| Date of publication: | 31.08.2018 |
