I enjoy building secure and correct systems. I have built a number of static analysis and automated verification tools, with a recent focus on analysis of binaries.
Data structures that may be generally useful
- haggle [39 ⭐ 📖]: An efficient graph library for Haskell
- persistent-vector [27 ⭐ 📖]: Persistent vectors for Haskell based on array mapped tries
- robbed [4 ⭐]: A pure Haskell implementation of Reduced Ordered Binary Decision Diagrams (BDDs)
- ql-grep [3 ⭐]: A code search tool that implements CodeQL on the tree-sitter infrastructure
- build-bom [45 ⭐]: Dynamically discover the commands used to create a piece of software
- whole-program-llvm [678 ⭐]: A wrapper script to build whole-program LLVM bitcode files; note that I consider this to be obsoleted by
build-bom
, which takes a more robust approach to the same problem - itanium-abi [12 ⭐ 📖]: An implementation of C++ name mangling for the Itanium ABI
- what4-serialize [0 ⭐]: Serialization/deserialization for What4 expressions
- crepitans [2 ⭐]: A tool for scriptable exploration of binaries
- dismantle [24 ⭐]: A library of assemblers and disassemblers derived from LLVM TableGen data
- portable-executable [3 ⭐]: Tools for working with the Windows Portable Executable (PE) file format
- semmc [35 ⭐]: Stratified synthesis for learning machine code instruction semantics
- macaw [195 ⭐]: Open source binary analysis tools.
- macaw-loader [5 ⭐]: Uniform interface to load a binary executable and get Macaw Memory and a list of entry points.
- renovate [47 ⭐]: A library for binary analysis and rewriting
- language-sleigh [5 ⭐]: A parser for the Sleigh language, which is used to represent ISA semantics in Ghidra
- mctrace [5 ⭐]: An implementation of DTrace for machine code
- ddmin [3 ⭐]: An implementation of delta debugging (ddmin) in Haskell
- surveyor [18 ⭐]: A symbolic debugger for C/C++ (via LLVM), machine code, and JVM programs
- binary-walkr [2 ⭐]: A tool for examining ELF binaries
Note that these are interesting and informative, but definitely not efficient enough to use in production
- satisfaction [2 ⭐]: A DPLL SAT solver written in Haskell
- datalog [102 ⭐]: A pure Haskell implementation of Datalog
- ifscs [4 ⭐ 📖]: An inductive form set constraint solver in Haskell
- satir [1 ⭐]: An implementation of a SAT solver in Rust
- haskell-pragma.el [3 ⭐]: An emacs hydra to enable Haskell language extensions efficiently
- haskell-interactive-import.el [0 ⭐]: A Haskell function and minor mode for interactively adding imports to modules