Blogs (1) >>
ASE 2019
Sun 10 - Fri 15 November 2019 San Diego, California, United States
Wed 13 Nov 2019 14:00 - 14:20 at Cortez 1 - Verification and Bug Detection Chair(s): Raghavan Komondoor

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 Nov
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

13:40 - 15:20: Papers - Verification and Bug Detection at Cortez 1
Chair(s): Raghavan KomondoorIndian Institute of Science, Bangalore
ase-2019-papers13:40 - 14:00
Ahmet CelikThe University of Texas at Austin, Karl PalmskogUniversity of Texas at Austin, Marinela ParovicThe University of Texas at Austin, Emilio Jesús Gallego AriasMINES ParisTech, Milos GligoricThe University of Texas at Austin
ase-2019-papers14:00 - 14:20
Jiaxiang LiuShenzhen University, Xiaomu ShiShenzhen University, Ming-Hsien TsaiAcademia Sinica, Taiwan, Bow-Yaw WangAcademia Sinica, Bo-Yin YangAcademia Sinica
ase-2019-papers14:20 - 14:40
Dongwoo KimKyungpook National University, Yunja ChoiKyungpook National University
ase-2019-papers14:40 - 15:00
Frédéric RecoulesCEA LIST, Sebastien BardinCEA LIST, Richard BonichonCEA LIST, Laurent MounierUniversité Grenoble Alpes, Marie-Laure PotetUniversité Grenoble Alpes
DOI Pre-print
ase-2019-Demonstrations15:00 - 15:10
Mohammad AfzalTata Cosultancy Services, A AsiaTata Cosultancy Services, Avriti ChauhanTata Cosultancy Services, Bharti ChimdyalwarTata Consultancy Services, Priyanka DarkeTata Consultancy Services, Advaita DatarTata Consultancy Services Ltd, Shrawan KumarTata Cosultancy Services, R VenkateshTata Research Development and Design Centre
ase-2019-Demonstrations15:10 - 15:20
Da LiState Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University, Nanjing, China, Huiyan WangState Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University, Nanjing, China, Chang XuNanjing University, Ruiqing ZhangSearch Tech. Center Asia, Microsoft, Suzhou, China, Shing-Chi CheungDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Xiaoxing MaState Key Lab. for Novel Software Tech. and Dept. of Comp. Sci. and Tech., Nanjing University