As software becomes increasingly embedded in our daily lives, it becomes more and more critical to find the vulnerabilities in this software. Worse, since the amount and variety of this software is rapidly proliferating, manual analysis by rare, talented hackers cannot scale to keep this software safe.

My first foray into what became my dissertation work tried to address a specific class of this general problem: backdoors inserted (either due to malice or for later support and maintenance convenience) into internet-connected embedded devices, such as smart power-meters. To address the requirement of having to reason about logical bugs and to analyze enormous amounts of binary code, I created a novel combination of static and dynamic-symbolic analysis techniques. Combining this with an insight into a new way to define a backdoor, I was able to build a system that analyzed firmware of real-world devices to identify such vulnerabilities in them.

This first foray led into my main contribution: the generalization of this analysis composition in the form of a principled binary analysis framework built to enable the seamless combination of diverse program analysis techniques. This framework, angr, provides a powerful base future research from myself, my lab-mates, and researchers around the world (as the framework is fully open source). One of the early applications of the system was the identification of authentication bypass vulnerabilities in binary firmware using a combination of static analysis and dynamic symbolic execution.

Using angr, we built an autonomous program analysis system that was able to analyze, exploit, and protect binary code without any human intervention. This system, the Mechanical Phish, won third place in the Cyber Grand Challenge, a competition created by DARPA to bootstrap the development of autonomous Cyber Reasoning Systems. While the system did well, its performance in the Cyber Grand Challenge provided an insight that shaped the conclusion of my dissertation: even with the current program analysis techniques combined into a coherent Cyber Reasoning System, serious limitations still exist. In the final work of my graduate studies, I explored the careful reintegration of human assistance into our analysis automation, in a way that addresses its limitations without compromising its scalability advantage over manual analysis.

Web-based single sign-on describes a class of protocols where a user signs into a web site with the authentication provided as a service by a third party. In exchange for the increased complexity of the authentication procedure, SSO makes it convenient for users to authenticate themselves to many different web sites (relying parties), using just a single account at an identity provider such as Facebook or Google.

Single sign-on (SSO) protocols, however, are not immune to vulnerabilities. Recent research introduced several attacks against existing SSO protocols, and further work showed that these problems are prevalent: 6.5% of the investigated relying parties were vulnerable to impersonation attacks, which can lead to account compromises and privacy breaches. Prior work used formal verification methods to identify vulnerabilities in SSO protocols or leveraged invariances of SSO interaction traces to identify logic flaws. No prior work, however, systematically studied the actual root cause of impersonation attacks against the relying party.

In this paper, we systematically examine existing SSO protocols and determine the root cause of the aforementioned vulnerabilities: the design of the communication channel between the relying party and the identity provider, which, depending on the protocol and implementation, suffers from being a one-way communication protocol, or from a lack of authentication. We (a) systematically study the weakness responsible for the vulnerabilities in existing protocols that allow impersonation attacks against the relying party, (b) introduce a dedicated, authenticated, bi-directional, secure channel that does not suffer from those shortcomings, (c) formally verify the authentication property of this channel using a well-known cryptographic protocol verifier (ProVerif), and (d) evaluate the practicality of a prototype implementation of our protocol.

Ultimately, to support a smooth and painless transition from existing SSO protocols, we introduce a proxy setup in which our channel can be used to secure existing SSO protocols from impersonation attacks. Furthermore, to demonstrate the flexibility of our approach, we design two different SSO protocols: an OAuth-like and an OpenID-like protocol.

Security competitions have become a popular way to foster security education by creating a competitive environment in which participants go beyond the effort usually required in traditional security courses. Live security competitions (also called “Capture The Flag,” or CTF competitions) are particularly well-suited to support hands-on experience, as they usually have both an attack and a defense component. Unfortunately, because these competitions put several (possibly many) teams against one another, they are difficult to design, implement, and run. This paper presents a framework that is based on the lessons learned in running, for more than 10 years, the largest educational CTF in the world, called iCTF. The framework’s goal is to provide educational institutions and other organizations with the ability to run customizable CTF competitions. The framework is open and leverages the security community for the creation of a corpus of educational security challenges.