Joe Hendrix

I am a Principal Computer Scientist at SRI International. I am interested using computation to make the world more trustworthy and fair, and primarily do that through work on automated reasoning, program verification and decompilation.

Projects

Reopt Github

Reopt is a general purpose decompilation and recompilation tool for repurposing application logic. It does this by analyzing machine code to recover a more flexible program representation -- specifically the LLVM assembly language. Once in this format, one can then apply optimization tools to optimize the LLVM, recompile the application into optimized or security hardened object code, and use Reopt to merge the recompiled code back into the original executable.

Grackle

https://grackle.galois.com

Grackle is a symbolic execution tool designed for symbolically executing MATLAB and LLVM code, and evaluating those expressions using SAT and SMT solvers such as ABC and Yices. Grackle is intended to enable engineers to reason symbolically about numerical programs. It can be used to, for example, find inputs that may crash a system or exceeds physical tolerances, model compression and decompression routines, or integrate numerical and symbolic solvers.

Galois Program Analysis Libraries

While at Galois, I lead initial development of many of the core libraries used for program analysis and verification. This includes:

Crucible Github

Crucible is a symbolic simulation framework that lets one construct formal mathematical expressions that precisely capturing the semantics of code. It uses the what4 library to send these expressions to automated provers such as SAT and SMT solvers so that you can verify programs correct or find bugs. Crucible supports symbolic execution of many languages including C/C++, Java, and Matlab.

Macaw Github

Macaw is a library that analyzes machine code binaries to understand their structure and the semantics of the code. It uses program analysis to identify functions in a binary, understand the organization of code within each function, and then generates control flow graphs describing the semantics.

What4 Github

What4 is a Haskell library developed at Galois that presents a generic interface to SMT solvers (Z3, Yices, etc.) as well as some specialized solvers such as abc and blt. It makes it easy to generate problems for the solvers, run satisfiability checks and obtain results including counterexamples.

Parameterized-utils Github

Parameterized-utils is a collection of typeclasses and data structures for working with parameterized types, that is types that are polymorphic over a parameter. One example would be a map of type Map k v that for each type tp, maps a key of type k tp to a value of type v tp. This generalizes the normal key-value map in the Haskell containers package to

Microsoft Attack Surface Analyzer 1.0

The Microsoft Attack Surface Analyzer helps software developers, Independent Software Vendors (ISVs) and IT Professionals better understand changes in Windows systems’ attack surface resulting from the installation of new applications.

The Maude Inductive Theorem Prover

The Maude Inductive Theorem Prover is an proof assistant for proving properties about Maude specifications. It supports structural and coverset induction schemes, rewriting-based simplification and an arithmetic decision procedure.

The Maude Sufficient Completness Checker

The Maude Sufficient Completeness Checker is a pair tool designed to check that one has completely defined operations in Maude specifications. The tool currently comes in two different versions, each with different features: (1) a narrowing-based tool integrated with the Maude Inductive Theorem Prover for checking the sufficient completeness of specifications with conditions; (2) a tree automata-based tool for checking the sufficient completeness of specifications with rewriting modulo associativity, commutativity, and identity.

Combining Equational Tree Automata (CETA)

Ceta is a library for reasoning about combinations of equational tree languages. It supports emptiness testing of tree languages definable by a Boolean combination of regular tree automaton over an equational theory containing operators that are associative and/or commutative with identity symbols.

Presentations

  • Verified Binary Lifting (slides)
    High Confidence Software and Systems Conference (HCSS) 2021
  • Towards Verified Decompilation using Lean 4 Youtube
    Lean Together 2021
  • High-Assurance Blockchains: Applications and Verification.
    HCSS 2018
  • Mobile Connected Devices: Security Challenges and Opportunities.
    SOCC 2016
  • Verification of Elliptic Curve Cryptography.
    HCSS 2012
  • Cryptol Tutorial.
    with Levent Erkök and Sean Weaver
    HCSS 2011

Publications

PhD Dissertation

Decision Procedures for Equationally Based Reasoning (2008)
University of Illinois at Urbana-Champaign

Conferences and Workshops