NJPLS at the University of Pennsylvania, November 15, 2012

This instance of NJPLS will take place in UPenn's Towne Hall, room 337. Breakfast and lunch will be served just outside the classroom.

Agenda

Abstracts

All Your IFCException Are Belong To Us

(Joint work with Michael Greenberg, Ben Karel, Benjamin Pierce, Greg Morrisett, and more)

I'll talk about how we do exception handling in Breeze, a new programming language that combines fine-grained, dynamic information flow control with discretionary access control and dynamically checked contracts. Existing designs for fine-grained, dynamic information-flow control assume that it's acceptable to terminate the entire system when an incorrect flow is detected -- i.e, they give up availability for the sake of confidentiality and integrity. This is an unrealistic limitation for systems such as long-running servers.

We identify public labels and delayed exceptions as crucial ingredients for making information-flow errors recoverable while retaining the fundamental soundness property of non-interference, and we propose two new error-handling mechanisms that make all errors recoverable. The first mechanism builds directly on these basic ingredients, using not-a-values (NaVs) and data flow to propagate errors. The second mechanism adapts the standard exception model to satisfy the extra constraints arising from information flow control, converting thrown exceptions to delayed ones at certain points. We have proved formally that both mechanisms are sound, and we believe that they have equivalent expressive power. We have implemented NaVs in Breeze and report on our (limited) practical experience using them.

Slides for this talk are available from my website.

Compiling Dynamic Information Flow Control

Information flow control systems have been around for some time, but (sound) dynamic approaches have only recently arrived. Naive implementations have 100% memory overhead to track information flow labels. How should we compile programs that dynamically control the flow of sensitive information, and how should we evaluate the effectiveness of such a compiler?

Test-Driven Development of an Information-Flow ISA: A QuickCheck Adventure

A Relational Program Logic for Data Abstraction and Security

(Joint work with Anindya Banerjee)

A relational property says that two programs, run from related initial states, reach related outcomes. Examples include noninterference and other information flow properties of a single program, simulations between data representations, and context-dependent equivalences for refactoring, for optimizing compilation, and for enabling further analyses. Specific relational properties have been checked by specialized static analyses or by semantic reasoning such as representation independence theorems formalized in interactive theorem provers. For scalable automation, techniques are needed to leverage first order provers for modular relational reasoning. We introduce biprograms, which encode interleavings shown in prior work to be needed for automated relational verification. Our relational logic of biprograms features local reasoning with first order assertions and relations, building directly on region logic, and a second order frame rule from which we derive representation independence results.

Mechanized Metatheory for Authorization Logic

(Joint work with Michael Clarkson)

Authorization logics are concerned with determining which principals in a system are securely permitted to take what actions. This talk presents ongoing work on verifying the metatheory of an authorization logic (Nexus Authorization Logic, derived from CDD and DCC) in Coq, including a natural-deduction proof system, a Kripke-style semantics, and a proof of soundness. The verification process exposed subtle issues with the semantics. The talk also presents some experience and lessons learned from using Coq to express complex semantic models.

Picat: A Scalable Logic-based Language

(Joint work with Jonathan Fruhman)

Picat is general-purpose language that incorporates features from logic programming, functional programming, and scripting languages. The letters in the name summarize the main features of Picat: (1) 'P' stands for predicates. A predicate defines a relation, and can have zero, one, or multiple answers. A function is a special kind of a predicate that always succeeds with one answer. Picat is a rule-based language. Predicates and functions are defined with pattern-matching rules. (2) 'I' stands for Imperative. Picat incorporates features of imperative programming languages, which tell the computer how to perform operations. Picat provides assignment and loop statements for programming everyday things. (3) 'C' stands for constraints. Picat supports constraint programming. Given a set of variables, each of which has a domain of possible values, and a set of constraints that limit the acceptable set of assignments of values to variables, the goal is to find an assignment of values to the variables that satisfies all the constraints. (4) 'A' stands for actors. Actors are event-driven calls. Picat provides action rules for describing event-driven behaviors of actors. Events are posted through channels. An actor can be attached to a channel in order to watch and process its events. Picat treats threads as channels and allows use of action rules to program concurrent threads. (5) 'T' stands for tabling. Tabling can be used to store the results of certain calculations in memory, allowing the program to do a quick table lookup instead of repeatedly calculating a value. As computer memory grows, tabling is becoming increasingly important for offering dynamic programming solutions for many problems. The resulting system is aimed for a variety of application areas including optimization, NLP, and scripting tasks for Web services.

An overview of the language is available online.

Linear Dependent Types For Differential Privacy

Differential privacy offers a way to answer queries about sensitive information while offering strong, provable privacy guarantees. Several tools have been developed for certifying that a given query is differentially private. In one approach, Reed and Pierce[31] proposed a functional programming language, Fuzz, for writing differentially private queries. Fuzz uses linear types to track sensitivity, as well as a probability monad to express randomized computation; it guarantees that any program that has a certain type is differentially private. Fuzz can successfully verify many useful queries. However, it fails when the analysis depends on values that are not known statically.

We present DFuzz, an extension of Fuzz with a combination of linear indexed types and lightweight dependent types. This combination allows a richer sensitivity analysis that is able to analyze a larger class of queries, including queries whose sensitivity depends on runtime information. As in Fuzz, the differential privacy guarantees follows directly from the soundness theorem for the type system. We demonstrate the enhanced expressivity of DFuzz by certifying differential privacy a broad class of iterative algorithms that could not be typed previously.

BioScape: A Modeling and Simulation Language for Bacteria-Materials Interactions

(Joint work with Adriana Compagnoni, Yifei Bao, Svetlana Sukhishvilli, Mathew Libera, Philippe Bidinger, Livio Bioglio and Eduardo Bonelli)

We design BioScape, a concurrent language for the stochastic simulation of biological and bio-materials processes in a reactive environment in 3D space. BioScape is based on the Stochastic Pi-Calculus, and it is motivated by the need for individual-based, continuous motion, and continuous space simulation in modeling complex bacteria-materials interactions. Our driving example is a bio-triggered drug delivery system for infection-resistant medical implants. Our models in BioScape will help in identifying biological targets and materials strategies to treat biomaterials associated bacterial infections.

The novel aspects of BioScape include syntactic primitives to declare the scope in space where species can move, diffusion rate, shape, and reaction distance, and an operational semantics that deals with the species of 3D locations, verifying reaction distance, and featuring random movement. We define a translation from BioScape to 3pi and prove its soundness with respect to the operational semantics.

Designing a Language for Secure Multi-Party Communication

(Joint work with Mike Hicks and Matt Hammer)

Secure two-party computation allows two parties to jointly evaluate a function on their respective secret inputs in a way that the computation reveals nothing but the final output. Yao proposed a garbled circuit protocol that can be used to securely compute an arbitrary function from its boolean combinational circuit model. Recent research has focused on optimizing the protocol by generating optimal circuit representations, parallelizing circuit garbling with evaluation, etc. However, secure computation in general has not yet benefitted from the programming languages research.

In this project, we aim to use program analysis to optimize secure computation by identifying code fragments that can be computed locally without incurring the secure computation overhead, and more importantly without revealing anything more than what can already be inferred by a party from the knowledge of its own inputs and the output. One possible approach is to use invariants generation algorithms to infer variables that are "known". Taking this a step further, we plan to investigate whether the language of secure computation can be enriched with loops, conditionals, dynamic memory, among other features that lack from current frameworks.

In this talk, we present an outline of our approach with some preliminary results.