首页    期刊浏览 2024年12月02日 星期一
登录注册

文章基本信息

  • 标题:Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk)
  • 本地全文:下载
  • 作者:Andy Polyakov ; Ming-Hsien Tsai ; Bow-Yaw Wang
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2018
  • 卷号:118
  • 页码:1-16
  • DOI:10.4230/LIPIcs.CONCUR.2018.4
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要: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.
  • 关键词:Formal verification; Cryptography; Assembly Programs
国家哲学社会科学文献中心版权所有