Search Results

Documents authored by Yang, Bo-Yin


Document
Invited Talk
Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk)

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

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)


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.

Cite as

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)


Copy BibTex To Clipboard

@InProceedings{polyakov_et_al:LIPIcs.CONCUR.2018.4,
  author =	{Polyakov, Andy and Tsai, Ming-Hsien and Wang, Bow-Yaw and Yang, Bo-Yin},
  title =	{{Verifying Arithmetic Assembly Programs in Cryptographic Primitives}},
  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 =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.4},
  URN =		{urn:nbn:de:0030-drops-95425},
  doi =		{10.4230/LIPIcs.CONCUR.2018.4},
  annote =	{Keywords: Formal verification, Cryptography, Assembly Programs}
}
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