Advanced Language-based Techniques for Correct, Secure Networked Systems

Abstract

Developing correct and secure software is an important task that impacts many areas including finance, transportation, 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).

Finally, we verify the correctness of distributed applications based on conflict-free replicated data types (CRDTs). In order to do so, we add an extension to Liquid Haskell that facilitates stating and semi-automatically proving properties of typeclasses. Our work allows refinement types to be attached to typeclass method declarations, and ensures that instance implementations respect these types. The engineering of this extension is a modular interaction between GHC, the Glasgow Haskell Compiler, and Liquid Haskell’s core proof infrastructure. To verify CRDTs, we define them as a typeclass with refinement types that capture the mathematical properties CRDTs must satisfy, prove that these properties are sufficient to ensure that replicas’ states converge despite out-of-order delivery, implement (and prove correct) several instances of our CRDT typeclass, and use them to build two realistic applications, a multi-user calendar event planner and a collaborative text editor. In addition, we demonstrate the utility of our typeclass extension by using Liquid Haskell to modularly verify that 34 instances satisfy the laws of five standard typeclasses.