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

Sazzadur Rahaman, Haipeng Cai, Omar Chowdhury, Danfeng Yao

Research output: Contribution to journalArticlepeer-review

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. 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.

Original languageEnglish (US)
Pages (from-to)3790-3803
Number of pages14
JournalIEEE Transactions on Dependable and Secure Computing
Volume19
Issue number6
DOIs
StatePublished - 2022
Externally publishedYes

Keywords

  • Cryptographic code
  • information flow analysis
  • security vulnerability
  • static tainting

ASJC Scopus subject areas

  • Computer Science(all)
  • Electrical and Electronic Engineering

Fingerprint

Dive into the research topics of 'From Theory to Code: Identifying Logical Flaws in Cryptographic Implementations in C/C++'. Together they form a unique fingerprint.

Cite this