PhD Proposal: Factors and verification tools in software security

Developing secure software is an important task that impacts many areas including finance, health, and defense. In order to develop secure programs, it is critical to understand the factors that influence the introduction of vulnerable code. To investigate, we ran the Build-it, Break-it, Fix-it (BIBIFI) contest as a quasi-controlled experiment. BIBIFI aims to assess the ability to securely build software, not just break it. In BIBIFI, teams build specified software with the goal of maximizing correctness, performance, and security. The latter is tested when teams attempt to break other teams’ submissions. Winners are chosen from among the best builders and the best breakers. BIBIFI was designed to be open-ended—teams can use any language, tool, process, etc. that they like. As such, contest outcomes shed light on factors that correlate with successfully building secure software and breaking insecure software. We ran three contests involving a total of 156 teams and three different programming problems. Quantitative analysis from these contests found that the most efficient build-it submissions used C/C++, but submissions coded in a statically-typed language were less likely to have a security flaw. Break-it teams that were also successful build-it teams were significantly better at finding security bugs.To improve secure development, we created LWeb, a tool for enforcing label-based, information flow policies in database-using web applications. In a nutshell, LWeb marries the LIO Haskell IFC enforcement library with the Yesod web programming framework. The implementation has two parts. First, we extract the core of LIO into a monad transformer (LMonad) and then apply it to Yesod’s core monad. Second, we extend Yesod’s table definition DSL and query functionality to permit defining and enforcing label-based policies on tables and enforcing them during query processing. LWeb’s policy language is expressive, permitting dynamic per-table and per-row policies. We formalize the essence of LWeb in the λLWeb calculus and mechanize the proof of noninterference in Liquid Haskell. This mechanization constitutes the first metatheoretic proof carried out in Liquid Haskell. We also used LWeb to build the web site hosting BIBIFI. The site involves 40 data tables and sophisticated policies. Compared to manually checking security policies, LWeb imposes a modest runtime overhead of between 2% to 21%. It reduces the trusted code base from the whole application to just 1% of the application code, and 21% of the code overall (when counting LWeb too).In future work, I propose to extend Liquid Haskell to fully support quantifying information flow (QIF). Specifically, I will write proofs about non-linear abstract domains using equational reasoning. In addition, I will implement synthesis for Liquid Haskell, so that it can automatically generate posterior belief distributions to model adversary queries.
Examining Committee:

Chair: Dr. Michael Hicks Dept rep: Dr. David Mount Members: Dr. Michelle Mazurek Dr. Niki Vazou