Click on one of the buttons above to see my publications on that topic.
In the first setting, this dissertation identifies that although modern services expose interfaces that are higher-order in spirit, the simplicity of the network protocols used forces services to rely on brittle encodings. To bridge the semantic gap, this dissertation presents Whip, a higher-order contract system that allows programmers to detect when services do not live up to their advertised higher-order interfaces. As more services use Whip, it becomes easier to identify errant services in the system.
In the second setting, this dissertation identifies that in the Disjunction Category label model, capability-like privileges are used to downgrade information, which when used inappropriately can compromise security. To ensure privileges are used as intended, this dissertation presents restricted privileges, an enhancement to privileges to control downgrading based on a specification of security conditions for when they can be legitimately used. As more privileges are restricted, information in the system becomes more protected from the accidental or malicious exercise of privileges to downgrade more information than intended.
In the third setting, this dissertation identifies that information-flow control (IFC) programs often need to interact with a key-value store that can also be accessed by non-IFC programs. These non-IFC programs may inadvertently (or maliciously) fail to respect the policies enforced by the IFC programs. In order to ensure the information protected by the IFC programs is not exfiltrated or corrupted by non-IFC programs through the key-value store, this dissertation presents Clio, an extension to a popular IFC language that transparently incorporates cryptography for data on the untrustworthy key-value store. As more IFC programs use Clio, the more information is protected from non-IFC programs in the system.
Pidgin combines program-dependence graphs (PDGs), which precisely capture the information flows in a whole application, with a custom PDG query language. Queries express properties about the paths in the PDG; because paths in the PDG correspond to information flows in the application, queries can be used to specify global security policies.
Pidgin is scalable. Generating a PDG for a 335k line Java application takes under 90 seconds, and checking each of our policies on that PDG takes under 14 seconds. The query language is expressive, supporting a large class of precise, application-specific security guarantees. Policies are separate from the code and do not interfere with testing or development, and can be used for security regression testing.
We describe the design and implementation of Pidgin and report on using it: (1) to explore information security guarantees in legacy programs; (2) to develop and modify security policies concurrently with application development; and (3) to develop policies based on known vulnerabilities.
Take a look at my National Parks Checklist to see the extent to which I've enjoyed "America's best idea."