License: 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: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9542/
Go to the corresponding LIPIcs Volume Portal

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

Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk)

pdf-format:
LIPIcs-CONCUR-2018-4.pdf (0.5 MB)

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
Collection: 29th International Conference on Concurrency Theory (CONCUR 2018)
Issue Date: 2018
Date of publication: 31.08.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI