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

Sazzadur Rahaman, Haipeng Cai, Omar Haider Chowdhury, Danfeng Daphne 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. 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.

Original languageEnglish (US)
JournalIEEE Transactions on Dependable and Secure Computing
DOIs
StateAccepted/In press - 2021
Externally publishedYes

Keywords

  • Cryptographic code
  • Cryptography
  • Graphics
  • Indexes
  • information flow analysis
  • Libraries
  • security vulnerability
  • Software
  • Static analysis
  • static tainting
  • Tools

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