Cryptographic primitives are ubiquitous for modern security. The correctness of their implementations is crucial to resist malicious attacks. Typical arithmetic computation of these C programs contains large numbers of non-linear operations, hence is challenging existing automatic C verification tools. We present an automated approach to verify cryptographic C programs. Our approach successfully verifies C implementations of various arithmetic operations used in NIST P-224, P-256, P-521 and Curve25519 in OpenSSL. During verification, we expose a bug and a few anomalies that have been existing for a long time. They have been reported to and confirmed by the OpenSSL community. Our results establish the functional correctness of these C implementations for the first time.
Wed 13 NovDisplayed time zone: Tijuana, Baja California change
13:40 - 15:20 | Verification and Bug DetectionDemonstrations / Research Papers at Cortez 1 Chair(s): Raghavan Komondoor Indian Institute of Science, Bangalore | ||
13:40 20mTalk | Mutation Analysis for Coq Research Papers Ahmet Celik The University of Texas at Austin, Karl Palmskog University of Texas at Austin, Marinela Parovic The University of Texas at Austin, Emilio Jesús Gallego Arias MINES ParisTech, Milos Gligoric The University of Texas at Austin | ||
14:00 20mTalk | Verifying Arithmetic in Cryptographic C Programs Research Papers Jiaxiang Liu Shenzhen University, Xiaomu Shi Shenzhen University, Ming-Hsien Tsai Academia Sinica, Taiwan, Bow-Yaw Wang Academia Sinica, Bo-Yin Yang Academia Sinica Pre-print | ||
14:20 20mTalk | Model checking embedded control software using OS-in-the-loop CEGAR Research Papers Pre-print | ||
14:40 20mTalk | Get rid of inline assembly through verification-oriented lifting Research Papers Frédéric Recoules CEA LIST, Sébastien Bardin CEA LIST, Richard Bonichon CEA LIST, Laurent Mounier Université Grenoble Alpes, Marie-Laure Potet Université Grenoble Alpes DOI Pre-print | ||
15:00 10mDemonstration | VeriAbs : Verification by Abstraction and Test Generation Demonstrations Mohammad Afzal Tata Cosultancy Services, A Asia Tata Cosultancy Services, Avriti Chauhan Tata Cosultancy Services, Bharti Chimdyalwar Tata Consultancy Services, Priyanka Darke Tata Consultancy Services, Advaita Datar Tata Consultancy Services Ltd, Shrawan Kumar Tata Cosultancy Services, R Venkatesh Tata Research Development and Design Centre | ||
15:10 10mDemonstration | SGUARD: A Feature-based Clustering Tool for Effective Spreadsheet Defect Detection Demonstrations Da Li State Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University, Nanjing, China, Huiyan Wang State Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University, Nanjing, China, Chang Xu Nanjing University, Ruiqing Zhang Search Tech. Center Asia, Microsoft, Suzhou, China, Shing-Chi Cheung Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiaoxing Ma State Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University | ||