| about | publications | projects | blog | github | gitstar |

Projects

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.

hails

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.

Labeled IO IFC Library:

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.
Disjunction Category Labels:
DC Labels are a new label format that allows for the expression of security policies in a very simple manner. Specifically, a DC label expresses confidentiality and integrity restrictions on the flow of information, which is enforced using logical implication (⇒). We express the DC Label model as a first order logic, which allows for using DC labels to enforce IFC not only dynamically, but statically, without modifying the type system (at least for a type system that has product and sum types). We implemented DC labels as two Haskell modules: a dynamic library in which labels are compose using strings that correspond to principals (sources of authority, such as a user), and a static library that uses the Haskell type system to enforce IFC. For the former module, we define the corresponding LIO interface, i.e., allow for LIO+DCLabels; for the latter, we provide a automatic theorem prover that finds proofs (a la Curry Howard isomorphism) which directly correspond to IFC relations. You may browse the source code documentation here.

typed

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.



Last modified: 13:46:21 22-Mar-2013