Downloads

This page contains miscellaneous software I've written and chosen to make freely available.

ConFIRM: CFI Compatibility Testing & Microbenchmarking

confirm ConFIRM (CONtrol-Flow Integrity Relevance Metrics) is a suite of C/C++/Assembly code programs that my lab developed for standardized compatibility testing of CFI (Control-Flow Integrity) solutions. The tests are designed to exhibit troublesome control-flow and control-data patterns gleaned from hundreds of person-hours debugging large, commercial software products and their incompatibilities with various CFI protection algorithms. Many of the tests also double as microbenchmarks that isolate runtime overheads associated with the protection of the various problematic operations. For more information, please see our publication in USENIX 2019:

Tips for Technical Writers

Here are slides from a lecture I gave on "Technical Writing: Tips for CS Students".

Artificial Software Diversity

We implemented a small CPU emulator relationally using miniKanren, and demonstrated how this can be leveraged to synthesize diverse variants of binary code (published in the 2019 miniKanren workshop):

Download code: [ zip | tar.gz ]

The following sample code accompanies our publication at the 2016 New Security Paradigms Workshop (NSPW):

The SPoX In-lined Reference Monitoring System

SPoX (Security Policy XML) is a purely declarative policy specification language designed to be implemented by In-lined Reference Monitors (IRM's). Rather than performing security checks at an operating system level as is done with traditional Reference Monitors, an IRM modifies untrusted binaries directly so that they become self-monitoring. This allows policies to be enforced on untrusted code without modifying the operating system.

Our Java implementation of SPoX is still preliminary (early beta) but the in-development product can be downloaded below. We are currently in the process of creating useful literature such as a user manual, as well as a larger suite of sample policies to aid the non-expert user.

Downloads

Publications

LaTeX Style Files

Derivation Trees

If you write papers about type systems in LaTeX, you may have noticed that it's unpleasantly difficult to typeset nice-looking typing derivations in LaTeX documents. The macros built into LaTeX or available in the amsmath package are designed for typesetting fractions, not derivation trees. One day I finally got tired of trying to make those work and wrote the following LaTeX package for typesetting derivation trees as they really should look.

Line-art Diagrams with Metapost

Metapost is an excellent tool for creating scientific pictures, just like LaTeX is an excellent tool for creating scientific documents. I wrote the following metapost package to make easy line-art pictures for importation into LaTeX documents.

Symbol Lists

While writing my thesis, I wanted to create good list of symbols, similar to LaTeX's built-in macros for creating lists of figures and lists of tables. I wrote the following package for the task:

  • symlist.sty is the LaTeX style file.
  • View symlist.pdf for documentation.
  • The source code for both of the above is available as symlist.dtx and symlist.ins.
  • If you want to make a symbol list that is consistent with the Cornell Thesis Guidelines, place the following LaTeX code wherever you want your symbol list to be: 
    \singlespacing
\renewcommand\listofsymbolname{LIST OF SYMBOLS}
\listofsymbols
\normalspacing
\clearpage

Song Books

I originally taught myself the internals of LaTeX by writing a massive LaTeX package devoted to the creation of song books. The software I developed can function either as a stand-alone LaTeX package, or as a suite of utilities built atop the MiKTeX and Vim free software packages. The song books I created are currently being used by the Cornell Graduate Christian Fellowship and the Cornell International Christian Fellowship.