Program Analysis of Cryptographic Implementations for Security

Cryptographic implementation errors in popular open source libraries (e.g., OpenSSL, GnuTLS, BotanTLS, etc.) and the misuses of cryptographic primitives (e.g., as in Juniper Network) have been the major source of vulnerabilities in the wild. These serious problems prompt the need for new compile-time security checking. Such security enforcements demand the study of various cryptographic properties and their mapping into enforceable program analysis rules. We refer to this new security approach as cryptographic program analysis (CPA). In this paper, we show how cryptographic program analysis can be performed effectively andits security applications. Specifically, we systematically investigate different threat categories on various cryptographicimplementations and their usages. Then, we derive varioussecurity rules, which are enforceable by program analysistools during code compilation. We also demonstrate the capabilities of static taint analysis to enforce most of these security rules and provide a prototype implementation. We point out promising future research and development directions in this new area of cryptographic program analysis.