Software
The following are selected software projects that I am, or have previously been, involved with developing.
Language Design and Analysis
-
Formulog
Formulog ties together the logic programming language Datalog and off-the-shelf SMT solvers. It is designed for writing SMT-based static analyses in a way that is both close to their formal specifications, and amenable to high-level optimizations and efficient evaluation. Available on GitHub and also see our OOPSLA 2020 publication. -
Flamio
Flamio is a programming language (a domain-specific languages embedded in Haskell) that instantiates the Flow-Limited Authorization Model (FLAM) with coarse-grained information-flow control. (See the publication for a link to download the code.) -
Whip
Whip is a contract system for modern services. Whip (i) provides programmers with a higher-order contract language tailored to the needs of modern services; and (ii) monitors services at run time to detect services that do not live up to their advertised interfaces. Contract monitoring is local to a service. Services are treated as black boxes, allowing heterogeneous implementation languages without modification to services' code. Thus, Whip does not disturb the loosely coupled nature of modern services. See the Whip website for more details and links to code. -
Pidgin
Pidgin is a program analysis and understanding tool that enables the specification and enforcement of precise application-specific information security guarantees. 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. You can download Pidgin from the Accrue project page. -
Shill
Shill is a shell scripting language designed to make it easy to follow the Principle of Least Privilege. Shill uses capabilities to control what access scripts have to your system. Every Shill script comes with a contract that describes what it can do, so users can run third-party scripts with confidence. Using capability-based sandboxes, Shill's security guarantees extend even to native executables launched by scripts. See the Shill web page for more information. -
Accrue
The Accrue Interprocedural Java Analysis Framework (Accrue) is a framework for interprocedural analysis of Java programs. It is built using the Polyglot extensible compiler framework, and is also suitable for interprocedural analysis of programs written in Java language extensions implemented with Polyglot. We developed Accrue to enable inference and discovery of strong information security guarantees in Java programs. See the Accrue project page for more information. Polyglot
Polyglot is an extensible Java source-to-source compiler. Polyglot facilitates extension of the Java programming language with new language features. See the Polyglot home page for more information.Jif
Jif is a security-typed programming language that extends Java with support for information flow control and access control, enforced at both compile time and run time. See the Jif home page for more information.JifE
JifE extends the Jif programming language with support for declassification and erasure information security policies. JifE has been used to implement Civitas, a remote voting system. Please contact me if you are interested in obtaining a copy of the JifE compiler and run-time system.
Miscellaneous
Alewife and Cassiopea
The PRINCESS project at Harvard focused on program synthesis of machine-dependent portions on an operating system. Alewife is a language/tool to write specifications of machine-depenent portions of an operating system in a machine-indepdent way; Cassiopea is a language/tool to express machine semantics and to synthesis assembly code to meet an Alewife specification. The tools are available at https://github.com/Harvard-PRINCESS/Cassiopea-Release.AbcDatalog
AbcDatalog is an open-source Datalog engine implemented in Java. It provides ready-to-use implementations of common Datalog evaluation algorithms, including efficient multi-threaded versions of bottom-up and magic set transformation techniques. See the AbcDatalog web page for more details.Civitas
Civitas is a secure voting system that allows voters to vote remotely, while provably providing universal verifiability, voter verifiability, anonymity, and coercion resistance. See the Civitas project page for more information.OS X LaTeX input mode
OS X allows user-defined input modes. The file LaTeX.inputplugin provides LaTeX-like mappings for common Unicode symbols. Place the file in the directory ~/Library/Input Methods/, and restart your machine. Under System Preferences → Language & Text → Input Sources, you can enable the newly added LaTeX input mode. Once the LaTeX input mode is selected (I bind “Select next input source” to ⌘-\ to make it easy to select the LaTeX input mode), try typing LaTeX macros for symbols, e.g. \alpha, \rightarrow, etc.