Chun-Ming Chiu
National Taiwan University, Taipei, Taiwan

Jiaxiang Liu
Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

Ming-Hsien Tsai
National Taiwan University of Science and Technology, Taipei, Taiwan

Xiaomu Shi
Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

Bow-Yaw Wang
Academia Sinica, Taipei, Taiwan

Bo-Yin Yang
Academia Sinica, Taipei, Taiwan

Keywords: Integer Set Library, CryptoLine, Formal Verification, Assembly Code

Abstract

The topic of verifying postquantum cryptographic software has never been more pressing than today between the new NIST postquantum cryptosystem standards being finalized and various countries issuing directives to switch to postquantum or at least hybrid cryptography in a decade. One critical issue in verifying lattice-based cryptographic software is range-checking in the finite-field arithmetic assembly code which occurs frequently in highly optimized cryptographic software. For the most part these have been handled by Satisfiability Modulo Theory (SMT) but so far they mostly are restricted to Montgomery arithmetic and 16-bit precision. We add semi-automatic range-check reasoning capability to the CryptoLine toolkit via the Integer Set Library (wrapped via the python package islpy) which makes it easier and faster to verify more arithmetic crypto code, including Barrett and Plantard finite-field arithmetic, and show experimentally that this is viable on production code.