Make Crypto Safe Again ! Detecting Bugs in API Usage Using Bounded Model Checking

The codebases of many popular cryptographic libraries are the result of decades of development and incremental changes. OpenSSL for example, arguably the most important crypto library available today, has been around since 1998 [6]. As a result, the libraries’ application programming interfaces (APIs) have been continuously adapted and changed, often increasing their complexity and making them harder to use correctly. Correct API usage is especially important in the context of information security, because neglecting even minor details can lead to a complete break of the security the protocol is intended to provide (cf. [2]). With OpenSSL, mistakes such as ignoring a single return statement have been observed to be able to lead to a complete breach in confidentiality [3]. A recent line of academic work has applied model checking techniques to discover API misuse (cf. [3, 8]). In this context, the goal of this project is to evaluate the feasibility of using Bounded Model Checking techniques (in particular, the Bounded Model Checker CBMC [1]) to validate correct API usage. For this, we will develop property monitors that allow to check that programs follow a correct sequence of API calls. The remainder of this report is structured as follows. Section 2 presents the necessary background on the validation of SSL certificates. Section 3 explains how we can use property monitors in combination with a Bounded Model Checker such as CBMC to validate correct API usage, and Section 4 shows the concrete validation we perform for OpenSSL. Section 5 presents some examples of applying our property models and discusses the limitations of this approach. Finally, Section 6 concludes the report.