Journal article
From Theory to Code: Identifying Logical Flaws in Cryptographic Implementations in C/C++
IEEE transactions on dependable and secure computing, Vol.19(6), pp.3790-3803
08/26/2021
DOI: 10.1109/TDSC.2021.3108031
Abstract
Cryptographic protocols are often expected to be provably secure. However, this security guarantee often falls short in practice due to various implementation flaws. We propose a new paradigm called cryptographic program analysis (CPA) which prescribes the use of program analysis to detect these implementation flaws at compile time. The principal insight of the CPA is that many of these flaws in cryptographic implementations can be mapped to the violation of meta-level properties of implementations. A program property that is necessary to realize a cryptographic property is referred to as meta-level property. We show that violations of these meta-level properties can be identified at compile-time that can serve as sufficient evidence of the encompassing flaws. We investigated existing literature on cryptographic implementation flaws and derived 25 corresponding meta-level properties. We develop a specification language based on deterministic finite automaton (DFA) and show that most of the meta-level properties can be expressed in our language. We also develop a tool called TAINTCRYPT which uses static taint analysis to identify meta-level property violations of C/C++ cryptographic implementations at compile-time. We demonstrate the efficacy of TAINTCRYPT by analyzing various open-source applications and libraries. Our experimental analysis generated new security insights and also indicates the scalability of our approach.
Details
- Title: Subtitle
- From Theory to Code: Identifying Logical Flaws in Cryptographic Implementations in C/C++
- Creators
- Sazzadur Rahaman - Computer Science, Virginia Polytechnic Institute and State University, 1757 Blacksburg, Virginia, United States, 24061-0131 (e-mail: sazzad14@vt.edu)Haipeng Cai - Washington State UniversityOmar Haider Chowdhury - Computer Science, University of Iowa, 4083 Iowa City, Iowa, United States, 52242-1002 (e-mail: omar-chowdhury@uiowa.edu)Danfeng Daphne Yao - Virginia Tech
- Resource Type
- Journal article
- Publication Details
- IEEE transactions on dependable and secure computing, Vol.19(6), pp.3790-3803
- Publisher
- IEEE
- DOI
- 10.1109/TDSC.2021.3108031
- ISSN
- 1545-5971
- eISSN
- 1941-0018
- Grant note
- DOI: 10.13039/100000006, name: Office of Naval Research, award: ONR-N00014-17-1-2498; DOI: 10.13039/501100008982, name: National Science Foundation, award: CNS 1657124
- Language
- English
- Electronic publication date
- 08/26/2021
- Academic Unit
- Computer Science
- Record Identifier
- 9984259430502771
Metrics
19 Record Views