The following are selected software projects that I am, or have previously been, involved with developing.
Language Design and Analysis
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 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.
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 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 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 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.
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 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.