From Theory to Code: Identifying Logical Flaws in Cryptographic Implementations in C/C++

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. To instantiate the abstract paradigm of CPA, we develop a specification language based on deterministic finite automaton (DFA) and show that most of the meta-level properties can be expressed in terms of our language. We then 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 open-source C/C++ cryptographic libraries (e.g., OpenSSL) and observe that TaintCrypt could have helped to avoid several high-profile flaws. We also evaluated TaintCrypt on 5 popular applications and libraries, which generated new security insights. The experimental evaluation on large-scale projects indicates the scalability of our approach.