Static analysis for detecting security vulnerabilities

Internet applications have relied for years on the SSL/TLS libraries for secure communications, but a growing body of literature points to systemic lapses in security procedure implementation and use that can render our communications insecure. At the heart of these problems is the inability for clients to reliably authenticate the server when presented with its public-key certificate. Certificate validation has been shown to be incorrect at all layers of the SSL stack, from improper certificate handling in libraries, to misuse of SSL APIs, to applications that are broken by design so that they are easier to use.

High-profile compromises [1, 2, 3] of prominent Certificate Authorities (CAs) undermine the SSL trust model. Any one of these lapses gives rise to the threat of a Man-in-the-Middle (MitM) attack, in which an attacker is able to intercept and read supposedly-secure SSL traffic in transit to or from a target website. Waiting on development teams to discover and patch these bugs is an inadequate solution. Studies of Android SSL usage have found that up to 76% of vulnerabilities persist for over a year. Another study found that 73% of developers took no action after being notified of confirmed vulnerabilities in their applications. The situation is even more grim on general computing platforms such as Windows and Linux.

In this project we consider static source code analysis and transformation as an alternate approach to securing SSL client code on full-featured operating systems. We develop tools that can automatedly detect and patch certificate validation vulnerabilities in code that makes use of the OpenSSL, GnuTLS, and LibCurl libraries.