This page lists the main projects I am currently working on, usually pointing to source code that we hope others will find useful. The publications corresponding to these projects may be found on the publications page.
The Haskell Automatic Information Labeling System (HAILS) is a generic security architecture especially suited for building web frameworks, part of the DARPA CRASH project. The goal of HAILS is to automate, at least partially, the labeling of information in information flow system (IFC). To this end, we've been developing an information flow library, Labeled IO (LIO), and a new label format, Disjunction Category Labels (DC Labels), to allow for implementing complex dynamic systems, such as a web server, securely. To demonstrate the flexibility of HAILS, we've been working on building λbook, a facebook-like web provider, that allows for the execution of untrusted third party applications.
LIO is a Haskell library that enforces IFC dynamically without the need of Arrows of Parametrized-Monads, as used by other works. Like other IFC systems, our approach is formalized as a lambda calculus for which we prove non-interference. Unlike, similar works we also prove several confinement properties---LIO allows for the enforcement of discretionary access control and mitigation of covert channels.
Concurrent LIO extends LIO with support for (labeled) threads and synchronization/communication primitives, labeled MVars. As one of the main difficulties with adding concurrency to IFC systems is the introduction and amplification of covert channels, we prove that Concurrent LIO closes the termination and internal-timing covert channels (at the language level).You may browse the source code documentation here.
The TYPED project is a language-based approach to programing on encrypted data, part of the DARPA PROCEED project. The goal of TYPED is to provide a language that allows a programmer to use standard, familiar, constructs that operate on encrypted data. Compared to existing languages and systems, we have been working on a language that can target different execution platforms. Specifically, a programmer writes a single program which can then be executed in "the cloud" by leveraging (fully) homomorphic encryption, or secure multi-party computation. We've been working on an embedded domain specific language within the context of Haskell, but are in the process of using a more standard approach, similar to (static) IFC systems, that will require the use of Template Haskell for translation. The current code will be available upon request, we will be making the new design and code available in the future.