Verifying Curve25519 Software

被引：28

作者：

Chen, Yu-Fang ^{[1
]}

Hsu, Chang-Hong ^{[2
]}

Lin, Hsin-Hung ^{[3
]}

Schwabe, Peter ^{[4
]}

Tsai, Ming-Hsien ^{[1
]}

Wang, Bow-Yaw ^{[1
]}

Yang, Bo-Yin ^{[1
]}

Yang, Shang-Yi ^{[1
]}

机构：

[1] Acad Sinica, Inst Informat Sci, Taipei, Taiwan

[2] Univ Michigan, Ann Arbor, MI 48109 USA

[3] Kyushu Univ, Fac Informat Sci & Elect Engn, Fukuoka, Fukuoka, Japan

[4] Radboud Univ Nijmegen, Inst Comp & Informat Sci, Nijmegen, Netherlands

来源：

CCS'14: PROCEEDINGS OF THE 21ST ACM CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY | 2014年

关键词：

Elliptic-curve cryptography; optimized assembly; Hoare logic; SMT solver; Boolector; Coq;

D O I：

10.1145/2660267.2660370

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper presents results on formal verification of high-speed cryptographic software. We consider speed-record-setting hand-optimized assembly software for Curve25519 elliptic-curve key exchange presented by Bernstein et al. at CHES 2011. Two versions for different microarchitectures are available. We successfully verify the core part of the computation, and reproduce detection of a bug in a previously published edition. An SMT solver supporting array and bit-vector theories is used to establish almost all properties. Remaining properties are verified in a proof assistant with simple rewrite tactics. We also exploit the compositionality of Hoare logic to address the scalability issue. Essential differences between both versions of the software are discussed from a formal-verification perspective.

引用

页码：299 / 309

页数：11

共 37 条

[1]

Affeldt R, 2007, LECT NOTES COMPUT SC, V4435, P346

[2] On construction of a library of formally verified low-level arithmetic functions [J].

Affeldt, Reynald .

INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2013, 9 (02) :59-77

[3] Certifying assembly with formal security proofs: The case of BBS [J].

Affeldt, Reynald ;

Nowak, David ;

Yamada, Kiyoshi .

SCIENCE OF COMPUTER PROGRAMMING, 2012, 77 (10-11) :1058-1074

[4]

Almeida J.B., 2013, P 2013 ACM SIGSAC C, P1217

[5]

Alpern B., 1988, Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, P1, DOI 10.1145/73560.73561

[6]

[Anonymous], ebacs: Ecrypt benchmarking of cryptographic systems

[7]

Avanzi R., 2006, Handbook of elliptic and hyperelliptic curve cryptography

[8]

Bartzia E.-I., 2011, THESIS

[9]

Bayrak AG, 2013, LECT NOTES COMPUT SC, V8086, P293, DOI 10.1007/978-3-642-40349-1_17

[10]

Bernstein Daniel J., 2012, Progress in Cryptology - LATINCRYPT 2012. Proceedings of the 2nd International Conference on Cryptology and Information Security in Latin America, P159, DOI 10.1007/978-3-642-33481-8_9

← 1 2 3 4 →