Macaw: A Machine Code Toolbox for the Busy Binary Analyst

TL;DR

Macaw presents a modular, statically typed binary-analysis toolkit implemented as a Haskell library, designed to support rapid prototyping of diverse tools for machine-code analysis. Its core is the Macaw-Base IR with architecture-specific dialects, enabling safe composition of analyses and transformations through strong type-level guarantees and integration with Crucible for symbolic execution. The paper details several mature case studies, notably Reopt for lifting x86-64 to LLVM and SAW for formal verification of mixed C/x86-64 code, illustrating the framework’s versatility across static and dynamic analyses as well as formal verification. The authors discuss automation strategies across dialects, highlight the benefits and costs of automated semantics generation, and outline future directions such as improving code discovery with Macaw-Refinement to balance precision and performance in practice.

Abstract

When attempting to understand the behavior of an executable, a binary analyst can make use of many different techniques. These include program slicing, dynamic instrumentation, binary-level rewriting, symbolic execution, and formal verification, all of which can uncover insights into how a piece of machine code behaves. As a result, there is no one-size-fits-all binary analysis tool, so a binary analysis researcher will often combine several different tools. Sometimes, a researcher will even need to design new tools to study problems that existing frameworks are not well equipped to handle. Designing such tools from complete scratch is rarely time- or cost-effective, however, given the scale and complexity of modern ISAs. We present Macaw, a modular framework that makes it possible to rapidly build reliable binary analysis tools across a range of use cases. Statically typed functional programming techniques are used pervasively throughout Macaw -- these range from using functional optimization passes to encoding tricky architectural invariants at the type level to statically check correctness properties. The level of assurance that functional programming ideas afford us allow us to iterate rapidly on Macaw while still having confidence that the underlying semantics are correct. Over a decade of development, we have used Macaw to support an industrial research team in building tools for machine code-related tasks. As such, the name 'Macaw' refers not just to the framework, but also a suite of tools that are built on top of it. We describe Macaw in depth and describe the different static and dynamic analyses that it performs, many powered by an SMT-based symbolic execution engine. We put a particular focus on interoperability between machine code and higher-level languages, including binary lifting from x86 to LLVM, as well verifying the correctness of mixed C and assembly code.

Figures (12)

• Figure 1: The Macaw library ecosystem. An arrow A $\rightarrow$ B indicates that library A depends on library B.
• Figure 2: The definition of in Macaw, which describes the shape of machine-code values at the type level. This type is witnessed at the value level by , which can be thought of as the singleton type singletons for .
• Figure 3: Type families and synonyms related to architecture extension points.
• Figure 4: Core data types used in Macaw's intermediate language.
• Figure 5: Macaw's core code discovery algorithm.