1

#  Macaw: A Machine Code Toolbox for the Busy Binary Analyst

Ryan G. Scott  Galois, Inc.United States<EMAIL_ADDRESS>,  Brett Boston  ,
Benjamin Davis  Galois, Inc.United States<EMAIL_ADDRESS>,  Iavor Diatchki
Galois, Inc.United States<EMAIL_ADDRESS>,  Mike Dodds  Galois,
Inc.United States<EMAIL_ADDRESS>,  Joe Hendrix  ,  Daniel Matichuk  Galois,
Inc.United States<EMAIL_ADDRESS>,  Kevin Quick  Galois, Inc.United
States<EMAIL_ADDRESS>,  Tristan Ravitch  ,  Valentin Robert  Galois,
Inc.United States<EMAIL_ADDRESS>,  Benjamin Selfridge  Galois, Inc.United
States<EMAIL_ADDRESS>,  Andrei Ștefănescu<EMAIL_ADDRESS>,
Daniel Wagner  Galois, Inc.United States<EMAIL_ADDRESS>and  Simon Winwood
<EMAIL_ADDRESS>
###### 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 instruction set
architectures.

We present Macaw, a modular framework that makes it possible to rapidly build
reliable binary analysis tools across a range of use cases. 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 itself, but also a suite of tools that are
built on top of the framework. We describe Macaw in depth and describe the
different static and dynamic analyses that it performs, many of which are
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.

††journal: PACMPL††journalvolume: 1††journalnumber: Conference††article:
1††journalyear: 2024††publicationmonth: 9††copyright: none

##  1\. Introduction

_Binary analysis_ refers to not one class of tool, but many. Starting with an
unknown binary, there are many tasks that an engineer may want to accomplish.
These may include _discovering_ the structure of the binary, _transforming_
the binary to achieve some goal, _analyzing_ the binary to identify particular
properties or vulnerabilities, and/or _formally verifying_ that the binary
matches some specification. These broad tasks can be combined and specialized
into many domains, objectives, tool types, and instruction sets. The result is
that there is as yet no optimal binary analysis tool, but rather a large space
of potentially useful designs.

We present Macaw, a binary analysis toolkit which we have built to help us
explore this design space of tools. Macaw exists in a similar niche as
frameworks such as Angr (Shoshitaishvili et al., 2016) and, to a lesser
extent, reverse-engineering suites such as Ghidra (Rohleder, 2019) and Binary
Ninja (Vector35, 2023a). What sets Macaw apart are the intended use cases.
Macaw is not a standalone tool, but it is instead a Haskell library that can
be used to rapidly construct and evaluate binary analysis tools. The main
Macaw library is also accompanied by a suite of libraries for disassembly,
representing architecture semantics, and symbolically executing machine code,
which we collectively refer to as the _Macaw ecosystem_. Macaw is designed to
help us build quickly, maximize reuse of existing components, and avoid costly
errors during prototyping. This imposes a particular set of design constraints
on the Macaw ecosystem, which we explain in this paper.

Macaw was built to support an industry research team developing novel binary
analysis tools. This team executed on multiple research projects over a
decade, with a significant amount of personnel change over this time. In this
environment, Macaw has served as a key library that helped us develop
successful tool prototypes. In this paper, we discuss the most interesting and
mature tool designs, which are:

  * •

Reopt, a binary lifter which converts x86-64 binaries to LLVM code and
performs reoptimizations on the lifted code. _This was the original Macaw use-
case._

  * •

SAW, a formal verification platform that supports mixed C and machine code.
See (Chudnov et al., 2018; Boston et al., 2021; Dodds, 2020) for industry use-
cases of SAW.

  * •

Renovate, a static binary rewriter that allows users to add or remove code
without executing the binary.

  * •

MCTrace, a binary instrumentation tool to insert probes to dynamically collect
telemetry with low-overhead tracing, including in environments without an
operating system.

  * •

Ambient-Verifier, a static verifier that can prove the presence of weird
machines (Dullien, 2020) in binaries (or lack thereof).

  * •

PATE, a relational verifier that proves that two binaries have the same
observable behaviors.

  * •

Cerridwen, a tool for ranking how similar a binary is to a known corpus of
binaries.

  * •

Surveyor, an interactive debugger that, among other features, can step through
machine code and inspect symbolic values.

To illustrate in more depth how Macaw works, we discuss two of these tools in
detail, Reopt and SAW. We focus on these two because they support very
different tasks and, as such, require combining Macaw’s components in very
different and illustrative ways.

A key component of Macaw’s design is its deep integration with Crucible
(Christiansen et al., 2019), an SMT-backed symbolic execution engine. Although
Crucible was originally developed for simulating higher-level imperative
programming languages such as C, the same technology proves valuable for
simulating the behavior of machine code as well. Many tools built on top of
Macaw—including SAW, Renovate, Ambient-Verifier, PATE, and Surveyor—leverage
Crucible to peform different analyses, including static program analysis and
formal verification. Because Crucible also supports higher-level languages
such as C, this makes it easier to simultaneously analyze codebases that mix
these languages with machine code. This is something that SAW takes advantage
of, as it leverages Macaw and Crucible to verify mixed C and machine code.

Macaw provides a specific point in the design space of binary analysis
frameworks which has proved useful for us in developing a wide range of
capabilities. In Section 2, we discuss the core design of the Macaw IR and
supporting ecosystem, and we discuss how this design aligns with goals. In
Section 3, we explore the tools that we have built on top of Macaw in more
detail. We use this to explain how Macaw helps us to effectively build tools
in a variety of domains. In Section 4, we compare Macaw to existing frameworks
such as Angr, and we also compare Macaw-based tools to similar efforts. Many
of the differences come down to tradeoffs; we describe both the upsides and
downsides of the choices that led to Macaw’s design. Section 5 concludes and
discusses our future design ambitions for Macaw.

##  2\. Design of the Macaw Ecosystem

Macaw-BaseCrucibleMacaw-SymbolicMacaw-RefinementMacaw backendsMacaw-
AArch32Macaw-PPCMacaw-RISCVMacaw-x86ISA-specific libraries Figure 1. The Macaw
library ecosystem. An arrow A $\rightarrow$ B indicates that library A depends
on library B.

The Macaw ecosystem consists of a set of Haskell libraries, whose
relationships are depicted in Figure 1. At the heart of the ecosystem is
Macaw-Base, which only contains functionality that is independent of any
particular architecture. This includes the core Macaw intermediate
representation (IR), code discovery, optimization passes, and an ELF loader
for ingesting binaries.

Any architecture-specific functionality is encapsulated in a Macaw backend
library. Macaw was originally designed with x86-64 support in mind, which gave
rise to the first backend, Macaw-x86. Later, Macaw-AArch32, Macaw-PPC, and
Macaw-RISCVwere added. Each of these backends are built on top of other
libraries that integrate Macaw with disassemblers for specific instruction set
architectures (ISAs), and they also encode the semantics of each
architecture’s instructions into a form that can be reasoned about. For
instance, Macaw-RISCV is built on top of the GRIFT library, which provides a
formal specification of the RISC-V ISA in Haskell (Selfridge, 2019).

###  2.1. Integrating ISAs into Macaw

While Macaw-Base provides the basic substrate for performing binary analysis,
it is not very useful without a mechanism for representing ISA-specific
details within Macaw. To this end, there are a suite of libraries supporting
each architecture backend. Each Macaw-supported architecture comes with its
own disassembler for parsing machine code into a form that Macaw can ingest,
and it also comes with a library for representing the semantics of each
instruction in a precise way. Having codified semantics enables both formal
verification, which Macaw richly supports (see Section 3.2), and machine-code
synthesis (Srinivasan and Reps, 2015), for which Macaw has experimental
support.

Incorporating a new ISA into Macaw can be a substantial amount of work.
Throughout the years, we have experimented with a number of different
approaches for implementing Macaw disassemblers and semantics, and we have
made pragmatic choices over time. For some architecture backends, such as
Macaw-RISCV, we implement disassemblers and semantics by hand. For other
backends, we generate implementations automatically from ISA specifications.
For instance, Macaw-AArch32’s disassembler is derived from the official ARM
XML specification (Reid, 2016), which we use to compute parse tables for each
instruction. In addition, the XML spec encodes the semantics of each
instruction in ARM’s Architecture Specification Language (ASL). We generate
Macaw-AArch32’s semantics by symbolically executing ASL expressions using
Crucible (see Section 2.6).

Each approach has its tradeoffs. Manually implementing disassemblers and
semantics makes it easier to understand the code in isolation, but it requires
more careful auditing for mistakes. Machine-generated code is generally
quicker to develop and less error-prone, but at the expense of obfuscating the
code. As a general principle, we prefer hand-written implementations for
smaller ISAs (e.g., RISC-V) and machine-generated implementations for larger
ISAs (e.g., AArch32).

###  2.2. Typed Address Representations

Macaw represents a machine address with the MemWord w type, which consists of
a machine word of size w bits. Note that w is a _type-level_ number, which
means that this convention is checked at compile-time, not runtime. This makes
critical use of GHC’s DataKinds extension, which allows certain forms of
values to be promoted to the type level (Yorgey et al., 2012).

The w type parameter is one example of a key design choice made throughout
Macaw’s code: where possible, use GHC language extensions to encode invariants
about machine code at the type level. This tradition was inspired by the
Crucible symbolic execution library (Christiansen et al., 2019), with which
Macaw integrates (see Section 2.6). For example, (Christiansen et al., 2019,
Section 3) defines a CrucibleType data type that classifies the shape of
Crucible expressions. Following suit, Macaw defines its own MacawType to
classify the shape of machine code values—we give some selected definitions in
Appendix A, Figure A.1.

An example of this strong typing discipline being put to use is encoding the
bit widths of AArch32 instructions. AArch32 processors have two instruction
sets: ARM mode, where each instruction is 32 bits, and Thumb mode, where each
instruction is 16 bits. Macaw encodes these bit widths at the type level, and
as a result, attempting to mix the two instructions sets without an explicit
mode switch will result in a type error. This has caught many potential errors
when developing Macaw-based tools, as ARM and Thumb instructions can often
occur within the same binary.

###  2.3. From Addresses to Architectures

Just as Macaw’s address types are indexed by the number of bits w, many Macaw
abstract syntax types are parameterized by an arch type parameter, which
represents the processor architecture being used. Doing so ensures that
operations from separate architectures are not mixed up. For example,
Macaw-x86 instantiates arch with an X86_64 type, Macaw-AArch32 instantiates
arch with an AArch32 type, and so on. We refer to types like X86_64 and
AArch32 as _architecture extension points_. One example of an arch-indexed
type is ArchReg, which is displayed in more detail in Appendix A, Figure A.2.
ArchReg uses GHC’s TypeFamilies extension (Schrijvers et al., 2008) to map an
architecture extension point to a register data type.

Sometimes, arch-indexed data types must interact with w-indexed data types. A
Macaw architecure uniquely determines the number of bits in a machine address,
so Macaw defines a RegAddrWidth type family to bridge the gap between the
former and the latter. This is such a commonly used type family that Macaw
also provides a variety of type synonyms defined on top of RegAddrWidth for
convenience, which are depicted in Appendix A, Figure A.2.

###  2.4. The Macaw Intermediate Language

Macaw uses a three address code–based intermediate language (Aho et al., 1986)
that is centered around basic blocks (Block). Each basic block consists of a
list of statements (Stmt) followed by a special terminator statement
(TermStmt). These data types are given in Appendix A, Figure A.3. For example,
the Block type is defined as follows:

⬇

data Block arch ids = Block

{ blockStmts :: [Stmt arch ids]

, blockTerm :: TermStmt arch ids }

Each data type is parameterized by two type parameters: arch, which encodes
the architecture, and ids, which denotes the set of identifiers used in
assignment instructions. The ids type parameter is unique to each decoded
function, which ensures that instructions from different functions cannot be
mixed without an explicit renaming step. The ids type parameter functions
similarly to the s type parameter in Haskell’s ST s type (Launchbury and
Peyton Jones, 1995).

The control flow in Macaw is oriented around basic blocks, and each basic
block has an address corresponding to the address of the first instruction. A
disassembled machine instruction can correspond to multiple Stmts, depending
on the complexity of the instruction. Note that the Stmts in two blocks are
allowed to overlap. For example, this is necessary to support AArch32
binaries, where instructions can be in both ARM or Thumb mode depending on how
they are reached.

The core Macaw IR is compact and covers common operations present in multiple
ISAs, which are used to represent the behavior of many instructions. These
operations primarily involve integer arithmetic (e.g., add and sub in x86-64),
and Macaw encodes these operations using bitvectors in a way that can be
easily translated to SMT. More complicated operations (i.e., ones that do not
map directly to SMT) are put into syntactically separate parts of the Stmt
language. For example, memory accesses are their own category, as they must be
decomposed into SMT-friendly operations via symbolic execution (see Section
2.6). There is also a separate category for architecture-specific extensions
(e.g., data cache hints in PowerPC), for which each ISA has a small number of
instructions.

This separation between common operations and more complicated ones reflects a
key Macaw design decision: the Macaw IR does not attempt to be generic enough
to encode every possible instruction directly. One benefit for this decision
is that it keeps the Macaw IR relatively readable. Although Macaw _could_
expand every instruction directly to core operations, this could easily cause
the number of Stmts to balloon in size. For example, x86-64’s AES-NI
instructions would likely need hundreds of bitvector operations to encode
directly. Another benefit is that some instructions perform effects that not
all Macaw clients need to model, so putting them into architecture-specific
extensions means that clients only “pay” for extensions that they reason
about. This gives Macaw users a high degree of control when mixing different
components.

###  2.5. Code Discovery

Entry pointaddressesExploration frontierClassifyDisassemble blockRewrite
(simplify)DiscoveredfunctionsBranchCallReturn Figure 2. Macaw’s core code
discovery algorithm.

One of the most important passes in Macaw-Base is code discovery, which aims
to identify all of the functions in a binary that are reachable from a set of
entry point addresses. The core algorithm that powers code discovery is
illustrated in Figure 2. The algorithm discovers one function at a time by
taking candidate function addresses from the _exploration frontier_ , which is
seeded with an initial set of entry points. Usually, these entry points are
taken from the entry point address of an ELF binary, the dynamic entry points
of a shared library, the addresses of static symbols (when available), as well
as function addresses derivable from metadata, such as DWARF unwinding tables.
Macaw also supports specifying custom entry points, which can be useful for
binaries that lack symbol information (e.g., stripped binaries).

The main part of the algorithm is the block decoding loop, which discovers
functions by decoding their individual blocks. First, Macaw decodes an
instruction using a low-level disassembly function for the specific
architecure. Next, Macaw lifts the instruction into a semantic representation
as a sequence of Stmts. If the instruction changes control flow (e.g.,
x86-64’s call), Macaw will terminate the block with a TermStmt; otherwise, it
will restart the loop and continue decoding the block.

Next, Macaw performs rewriting, which simplifies terms in the block to improve
readability and simplify later analyses. Afterwards, Macaw analyzes the block
to determine what kind of control-flow transfer terminates the block, be it a
jump, function call, or otherwise. To this end, Macaw tracks abstract domains
for each machine register, using techniques inspired by value-set analysis
(Balakrishnan and Reps, 2004) to update the domains as new blocks are
discovered. At the end of analysis, Macaw consults the abstract return
address, as well as the addresses and bounds of jump tables, to _classify_ how
the block terminates. Targets of function calls are added to the exploration
frontier as they are classified, which is used in subsequent iterations of the
algorithm.

###  2.6. Symbolic Execution via Crucible

A key component of the Macaw ecosystem is Macaw-Symbolic, which defines
functionality for simulating Macaw IR programs with Crucible, a symbolic
execution library targeting imperative code (Christiansen et al., 2019). Using
Macaw-Symbolic, one can simulate a binary with symbolic data, such as symbolic
register states or stack contents. During simulation, Crucible will generate
verification conditions that are discharged to an SMT solver.

Besides machine code, Crucible also includes backends targeting other
imperative programming languages, including C, Java, and Rust. Crucible’s LLVM
backend (which enables reasoning about C code) has been battle-tested on a
large number of verification problems from the SV-COMP verification
competition (Scott et al., 2021). Moreover, Crucible can reason about code
that mixes languages, such as C programs that use inline assembly (see Section
3.2).

####  2.6.1. Symbolic Code Discovery

The Macaw ecosystem also includes an additional, optional method of code
discovery provided by the Macaw-Refinement library. This library utilizes
symbolic execution to discover code targets, which can supplement the simpler,
pattern-based heuristics that Macaw-Base uses.

As an example, consider a switch statement whose expression is an integer i
whose range of possible values was previously constrained by an if statement.
When the various case targets of the switch statement are small and regularly
sized, the compiler may encode the switch statement as a jump to i * s, where
s is the size of the largest case block. Macaw-Base’s pattern-based heuristics
will not be aware the constraints from the if statement, and thus they cannot
limit the scope of possible jump targets to the specific set of valid
addresses. Using Macaw-Refinement, on the other hand, allows an SMT solver to
indicate the constrained set of possible jump targets to add those to the
discovery frontier.

##  3\. Case Studies

###  3.1. Reopt

Initial entrypointsIncrementalblock discoveryBlock
recoveryMacawReoptConstraintgenerationConstraintsolvingFunc recoveryLLVM
genNew entry pointsidentified Figure 3. Reopt’s function recovery loop.

Reopt (Hendrix et al., 2019) is an optimization tool that lifts functions in a
compiled binary into LLVM bitcode, optimizes the intermediate bitcode, and
then recompiles it into a new executable. Reopt currently supports x86-64
binaries compiled in the ELF format for Linux. The Macaw library began its
life as an internal component of the Reopt tool, and much of Macaw’s design
reflects considerations that were important at the time of Reopt’s
development.

The primary challenge in designing a tool like Reopt is going from Macaw’s IR,
which only has very minimal type information associated with each basic block,
to the LLVM IR, which has a comparatively richer type system. At the Macaw
level, most values in general-purpose registers look like integers, but when
Reopt outputs LLVM bitcode, it is helpful to distinguish between integers,
structs, pointers, and function pointers.

To this end, Reopt includes a type-based function recovery pass, which is
depicted in Figure 3. Starting from a list of initial entry point functions
(which are either inferred from the binary or user-specified), the tool calls
Macaw to discover the closure of basic blocks reachable from the currently
known blocks. Once the basic blocks have been recovered (c.f. Section 2.5),
Reopt performs a demand analysis, allowing it to compute the x86-64 arguments
and return registers on a per-block basis, aggregating them into register
“demand sets” for entire functions, which are then synthesized into
appropriate argument and return values for the whole function.

At this point, we only know the size of registers, but not whether they
contain integers, floating-point values, or, for those registers whose size
matches that of virtual addresses for the architecture, data or code pointers.
However, there is information in the instruction flow that can help
distinguish between all these cases, sometimes uniquely identifying what high-
level type a register should have. In order to produce better LLVM code, Reopt
will gather constraints for all intermediate registers, function arguments,
and return values. For instance, a register flowing into the memory operand of
a memory operation ought to be some pointer, while a value coming out of a
division operation must be numeric. Reopt will solve these constraints to
determine a candidate type for every function. Reopt also has some
experimental support for row types, allowing it to recover structural types,
including recursive ones such as linked lists.

During this process, Reopt may uncover calls to other functions, in which case
Macaw’s code discovery will need to be invoked once more. For instance, if a
function’s argument is determined to hold function pointers, all concrete
values flowing into this argument position can be safely added to the
candidate entry points pool. Thanks to Macaw’s incremental design, Reopt is
able to resume block discovery with those new entry points without incurring
duplicate work. Once all of the constraints are solved, the final output is an
LLVM program consisting of all the function definitions that have been
recovered, which now have much richer types.

####  3.1.1. Reopt Type Constraints

Reopt’s approach to reverse engineering types for assembly functions is
loosely based on the TIE system described in Lee et al. (2011). The type
system presented in that work is slightly more sophisticated than what Reopt
needs. For instance, Reopt generates LLVM, which does not distguish between
the types of signed and unsigned integers, so Reopt does not bother to track
this information. Likewise, where TIE relies on value-set analysis to get more
precise offset information in structured types, Reopt relies on Macaw’s
symbolic offsets, which may either be concrete offsets or opaque to its
analysis.

Ultimately, Reopt is concerned with distinguishing pointers from non-pointer
values. Without the type inference pass, Reopt would lift all pointer
arithmetic to integer arithmetic and would have to introduce an LLVM inttoptr
cast every time such a value would be in address position in a memory load or
store instruction. This is important because treating pointers as integers up
to the last second inhibits LLVM optimizations and obfuscates pointer
manipulation for both human and tool consumers of the lifted IR. Instead,
pointer arithmetic can be lifted to pointer-manipulating instructions,
describing them using types with richer structure, benefiting the readability
of the lifted code, and enabling more complex code analyses and
transformations. Knowing these types, Reopt can produce the more appropriate
getelementptr LLVM instruction, operating over typed pointers. We give an
instance of such an output change in Appendix B, Figure B.1.

####  3.1.2. Reopt Limitations

Reopt’s function recovery, as sophisticated as it is, may still not be enough
to infer a precise type for a function. One reason is that Macaw’s code
discovery is not perfect, and when it cannot process all of the instructions
in a basic block, it will conservatively bail out and possibly omit some
instructions that are crucial for inferring the types of the block’s inputs
and outputs. To help alleviate this problem, Reopt includes an option to
supply header files, as well as debug information files, which contain
function type signatures that Reopt should assume when it encounters known
functions. This is particularly useful for external function calls (e.g., from
libc), where Reopt either does not have the entire function definition
available, or the full definition is sufficiently low-level that analyzing it
proves costly.

Recent work has also been aimed at addressing limitations when working with
stripped binaries with no debug sections. Such binaries have historically
proven challenging for Reopt, as the only entry point initially known for such
binaries is the one listed as entry point of the executable. Typically, this
will be the address of a symbol that would have been named _start before
stripping, and whose code does _not_ contain an explicit call to the address
of the main symbol.

⬇

void _start() {

// Some scaffolding code, ending with:

__libc_start_main(&main); // ‘main‘ called back when C runtime ready

}

Instead, the start routine will call the C run-time scaffolding symbol,
__libc_start_main, passing the address of the main symbol as an argument to
it. As such, the binary does not contain any explicit call to main, and Macaw
will subsequently miss the main function and stop exploring right away. This
is where the type-driven analysis of Reopt can help. In this case, Reopt knows
that __libc_start_main expects a function pointer thanks to the libc debug
information. Upon noticing the address of main flowing into a call to
__libc_start_main, Reopt will instruct Macaw to resume block discovery with
this new address as a function entry point.

There are three reasons why we designed Reopt to use a type-based approach.
First, Reopt favors this approach over heuristical ones, as this not only
applies to discovering the main symbol in a stripped binary, but also any
function address passed to a higher-order function, be it in an external
library or locally within the binary being lifted. Second, Reopt prefers a
discovery-guided approach, where we only inspect bytes of the code section
when we witness an explicit flow of control to it, over a greedy inspection of
the entire code section, as it still allows us to avoid false positives such
as dead code, nop paddings, or misaligned decodings. Finally, Reopt favors a
type-aware approach to a greedy inspection of all pointer-sized values that
could look like they could point to code, as some floating-point values may
also look like pointers to the code segment, and this would also yield false
positives. In all the above cases, not only does Reopt find known-to-be-
reachable addresses, it also discovers them in a context where it knows the
type of their arguments and return value, which allows Reopt to properly lift
these basic blocks into well-typed LLVM functions.

###  3.2. SAW

The Software Analysis Workbench (SAW) (Dockins et al., 2016) is a verification
tool that can reason about the behavior of imperative programs by proving them
equivalent to functional specifications. SAW supports a variety of different
source languages, including code written in C, Java, Rust, and most relevantly
for this work, x86-64. SAW has been successfully used to verify a variety of
industrial-strength cryptographic libraries written in a mixture of C and
x86-64, including the s2n Transport Layer Security (TLS) stack (Chudnov et
al., 2018), the AWS LibCrypto library (Boston et al., 2021), and the BLST
library (Dodds, 2020).

SAW ingests x86-64 machine code by leveraging Macaw to lift assembly
instructions into a Crucible control-flow graph. Separately from the machine
code itself, SAW also takes as input a list of specifications that describe
the intended behavior of each assembly function. These specifications consist
of Hoare-style pre- and post-conditions that describe the shape of memory and
the behavior of the function itself. SAW checks each function against its
specification by symbolically executing the function’s CFG and ensuring that
the conditions described in the function are respected along the way,
discharging any non-trivial proof goals to an SMT solver.

Aside from checking functional correctness, SAW also checks that a function is
memory safe. In the context of a language like C, this is a well understood
problem, as the C standard dictates what it means for a C program to interact
with memory in a valid way. The notion of memory safety becomes blurrier with
assembly code, however, as there are almost no universally accepted rules on
what constitutes safe reads and writes. The only guidelines that one can
typically rely on are the conventions used within a particular program, as
well as the Application Binary Interface (ABI) for calling external functions.

SAW specifically targets programs with mixed C and x86-64 code where the C
code controls the program’s memory, and all x86-64 functions only ever access
the C code’s memory. In this setting, SAW can leverage Crucible’s LLVM-based
memory model for modeling both types of code. This means that SAW is able to
prove all memory reads and writes in the x86-64 code are correct with respect
to the host language’s memory model. As a small example of how SAW’s x86-64
support works, we will verify the behavior of a tiny increment assembly
function that takes a single pointer argument and increments the value it
points to by one.

⬇ increment: mov rax, [rdi] add rax, 1 mov [rdi], rax ret |  ⬇ // Equivalent C code: void increment(uint64_t* i) { *i += 1; }
---|---

We can write a SAW specification increment_spec that captures the intended
behavior:

⬇ let increment_spec = do { ptr <- llvm_alloc (llvm_int 64); val <-
llvm_fresh_var "val" (llvm_int 64); llvm_points_to ptr (llvm_term val);
llvm_execute_func [ptr]; llvm_points_to ptr (llvm_term {{ val + 1 }}); };
---

This specification declares a series of statements, where each statement
before the llvm_execute_func is a pre-condition and each statement after is a
post-condition. The pre-conditions state that the function accepts a single
pointer argument that points to an arbitrary 64-bit LLVM integer value. The
post-condition states that after the function is invoked, the pointer argument
will then point to the initial integer value plus one. Again, we are
leveraging LLVM to describe the shape of memory, and all of the commands used
here could apply to C functions just as much as x86-64 ones.

The increment function can be checked against increment_spec by running:

⬇ llvm_verify_x86 "./increment_bin" "increment" increment_spec z3;
---

Here, increment_bin is the ELF binary that defines increment, and z3 is the
SMT solver to discharge proof goals to during symbolic execution. This is the
only command that is machine code–specific, as this is where Macaw is used to
lift the assembly code in increment to a CFG and pass it on to SAW’s symbolic
execution engine. Although the llvm_verify_x86 command is specific to the
x86-64 ISA, it could very easily be extended to handle other architectures as
well 111For example, an llvm_verify_aarch32 command is planned: _anonymized
for review_ .

###  3.3. Other Case Studies

##### Ambient-Verifier

A verification tool built on top of Macaw that evaluates whether or not it is
possible to trigger a _weird machine_ (WM) (Dullien, 2020) in a binary, i.e.,
a code execution path that occurs outside of the intended specification of the
program. One challenging aspect of triaging the presence of WMs is determining
what environmental conditions—such as command-line arguments, environment
variables, or file system state—are strictly required to trigger the WM, and
which conditions are irrelevant to the WM. To this end, Ambient-Verifier
leverages symbolic execution to make certain parts of the environment symbolic
to explore the different execution paths, which can help users of the tool
determine which parts of the environment are most relevant to the WM at hand.

Many WMs reside in a shared library that a binary depends on, such as libc. To
this end, it is important to be able symbolically execute the code inside of
low-level shared libraries, but this can be difficult due to how often these
libraries contain low-level functions and system calls. While Crucible can
simulate this type of code, the performance is often impractically slow.

To allow the tool to execute shared libraries in an efficient manner, Ambient-
Verifier includes a mechanism for overriding the behavior of functions and
system calls. For instance, Ambient-Verifier can intercept calls to the
getppid system call and replace it with a version that returns a fresh,
symbolic integer as the process ID. While this does not faithfully emulate the
actual implementation of getppid, this can be an acceptable compromise to make
to speed up symbolic execution, especially for WMs where the behavior of
getppid is irrelevant.

#####  PATE (Patches Assured up to Trace Equivalence)

A relational verification (Barthe et al., 2011, 2013) tool that proves that a
property about a binary’s observable behavior holds before and after a patch
is applied to the binary’s code. A typical use case for PATE is verifying that
security-oriented patches fix undesirable behaviors in a binary without
adversely affecting other parts of the binary. First, PATE splits the original
and patched binaries into _conflict-free acyclic regions_ (CFARs). A CFAR is a
collection of basic blocks with control flow between them, but with no
backedges. PATE uses the original binary as the behavioral specification,
inferring frame conditions for each CFAR. PATE then symbolically executes each
CFAR in the original and patched binary, and if the patched binary fails to
satisfy the frame condition inferred from the original binary, then PATE
produces a summary of the conditions that lead to exhibiting different
behavior.

##### Cerridwen

A tool that quantifies similarities among x86-64 binaries. The algorithm for
ranking similarity largely follows the description in (David et al., 2017).
Cerridwen decomposes a binary into strands—that is, data-flow slices of basic
blocks (David et al., 2016)—which are used as units of measurement for
comparing how similar the binary is to a corpus of known binaries. The basic
blocks resulting from Macaw’s code discovery are used to compute each strand,
which consists of the operations that lead to the computation of a single
value within a basic block.

##### Renovate

A static binary rewriting library for ELF binaries. Using Renovate, one can
add, remove, or rewrite basic blocks in a statically linked binary without
needing to execute it. The core of Renovate’s rewriting machinery is
architecture-independent, and there exist x86-64, PowerPC, and AArch32
backends. One particular use case for Renovate is achieving binary diversity
(Cohen, 1993)—that is, randomizing the layout of basic blocks to make it more
resilient to attackers.

##### MCTrace

An x86-64 and PowerPC binary instrumentation tool that is heavily inspired by
DTrace (Cantrill et al., 2004; Gregg and Mauro, 2011), but does not require
any special kernel support or recompiling the program to be traced. MCTrace
reads the same tracing specifications as DTrace (written in the D language)
and leverage’s Renovate’s binary rewriting capabilities to insert probes into
binaries. The traces that these probes generate can support a variety of
different systems. For example, MCTrace-instrumented binaries have been
successfully run on bare metal using an MPC5777C PowerPC microcontroller.

##### Surveyor

A library for interactively debugging LLVM, JVM, x86-64, and PowerPC programs,
using an interface inspirted by gdb and emacs. Notably, Surveyor is a
_symbolic_ debugger: it supports setting breakpoints during Crucible’s
symbolic execution, and it can inspect the values of arguments to a basic
block, which may possibly be symbolic themselves. Surveyor also supports
stepping through a binary’s execution and recording a trace of symbolic
events, which can be replayed later.

##  4\. Related Work

##### Reverse Engineering Frameworks

The closest tools to Macaw in terms of capabilities are industrial binary
analysis frameworks such as Ghidra (Rohleder, 2019), Binary Ninja (Vector35,
2023a), Radare2 (Alvarez, 2023), and IDA Pro (Eagle, 2011). Like Macaw, these
frameworks handle a multitude of binary analysis tasks such as reverse
engineering, disassembly, decompilation, and static analysis. Each framework
also includes a native IR that abstracts some low-level architectural
details—for example, Ghidra’s P-Code (Naus et al., 2023) and others (Vector35,
2023b; Radare2 Book, 2023; Rolles, 2018).

The main difference between these tool and Macaw lies in their respective
design goals. Ghidra and similar are intended for industrial-strength reverse
engineering applications. Macaw is intended to be a research-oriented toolkit
for rapidly building novel binary analysis tools. For the user, these binary
analysis frameworks offer a polished experience which Macaw does not seek to
provide. For example, Ghidra features a full, graphical IDE that allows users
to visualize disassembled programs, label fields, rename variables, and more.
We have experimented with different UI approaches via the Surveyor tool, but
as exploratory tools, not fully-developed capabilities.

Macaw’s greatest strength is providing a platform to build new binary analysis
tools from scratch. Frameworks such as Ghidra typically support plugins via
some API, but this is usually meant for extending the existing functionality
rather than building standalone applications. In this sense, Macaw occupies a
different niche in the design space. Indeed, it is possible to build a custom
analysis tool with Macaw and integrate its capabilities into Ghidra’s IDE.

Another difference is Macaw’s intrinsically typed IR, which encodes invariants
about well-formedness at the type level. This guarantees that IR values are
valid in the context of the analyses they want to perform. To our knowledge,
none of the other IRs mentioned earlier employ a comparable approach to IR
validity. There have been efforts to give formal semantics to P-Code, but this
effort is external to the actual P-Code representation used in Ghidra (Naus et
al., 2023).

##### Binary Lifting

Reopt is one tool in the large space of binary lifters and rewriters; see
Schulte et al. (2022) for a comparison. Reopt lifts machine code to the LLVM
IR, which puts it in the same category as lifters such as McSema (Dinaburg and
Ruef, 2014), SecondWrite (Anand et al., 2013), RevGen (Chipounov and Candea,
2011), and rev.ng (Di Federico et al., 2017). It differs primarily in the
style of LLVM code that it produces. Most LLVM-based lifters map processor
registers directly to LLVM variables with an explicit stack, which results in
atypical LLVM code. Reopt unifies the machine code stack with the LLVM stack
in an effort to produce more “human-friendly” LLVM.

##### Symbolic Execution of Machine Code

Macaw leverages Crucible’s support for forward symbolic execution (King, 1976;
Schwartz et al., 2010) to analyze the behavior of programs. Other binary
analysis frameworks use symbolic execution as well, examples of which include
Angr (Shoshitaishvili et al., 2016), BAP (Brumley et al., 2011), Triton
(Saudel and Salwan, 2015), Mayhem (Cha et al., 2012), and KLEE-Native
(Vegasena and Goodman, 2019). Most of these leverage _dynamic_ symbolic
execution (also known as _concolic_ execution), while Macaw uses _static_
symbolic execution by lifting a binary to a high-level IR and analyzing it
using symbolic values.

This reflects a difference in the types of problems we have typically targeted
with Macaw. Other tools typically use symbolic execution in bug-finding (for
which dynamic symbolic execution is well-suited) while we have often used
Macaw to support exhaustive exploration or formal verification (for which
static symbolic execution is necessary).

Angr is static insofar as it lifts binaries to an IR and performs additional
analyses, but it is also provides dynamic analyses such as a symbolic-assisted
fuzzer (Stephens et al., 2016). This is similar to our Macaw-based tool
Ambient-Verifier, but Angr uses a combination of static and dynamic symbolic
execution depending on the use case. For example, Angr can directly interact
with files and the operating system, whereas Ambient-Verifier can only model
filesystem and OS interactions in an abstract way.

Another important distinction is that Angr often concretizes certain types of
symbolic values during execution, depending on the _concretization strategy_
that the user chooses. With the default concretization strategy, Angr will
concretize symbolic addresses that are written to, as well as symbolic length
values passed to the read() and write() system calls. This is done primarily
for performance reasons, as preserving all symbolic values can often lead to
VCs that are prohibitively expensive to solve for. By contrast, Ambient-
Verifier (and Macaw more generally) propagates symbolic values throughout its
analyses. This means that Ambient-Verifier will explore more paths by default,
but perhaps at the expense of additional analysis time.

##### Formal Verification of Machine Code

Our Macaw-based verification tool SAW is similar to Vale (Bosamiya et al.,
2020; Fromherz et al., 2019; Bond et al., 2017), a tool for writing verified
x86-64 assembly code. Vale integrates with Low* (Protzenko et al., 2017) to
allow verification of mixed C/x86-64 code. Vale and Low* are used in the
implementation of EverCrypt (Protzenko et al., 2020), a library of verified
C/x86-64 cryptography.

Unlike Vale and Low*, SAW is primarily used to verify _pre-existing_ C/x86-64
code, whereas Vale and Low* are primarily meant for writing code and proofs
simultaneously. Because SAW verifies x86-64 code as-is, SAW makes essential
use of Macaw’s binary lifting as part of the overall verification process.
Vale, on the other hand, generates x86-64 code from a verified domain-specific
language, so it does not rely on binary lifting.

##  5\. Conclusions and Next Steps

Macaw has been a keystone technology for us in developing binary analysis
tools over a decade. Macaw’s core IR builds in multiple features that let us
build rapidly and with confidence, while its symbolic execution capabilities
have enabled a diverse range of testing and verification tools.

Our current focus is on improving Macaw’s code discovery capabilities. A
common pain point is discovering the targets of calls through jump tables—by
default, Macaw uses simple pattern-based heuristics. We have developed Macaw-
Refinement (Section 2.6.1) as a more accurate alternative. However, its
reliance on SMT solving can increase discovery time in a way that is
unacceptable for many applications. We are currently investigating how to
limit SMT calls to only the places that the pattern-based heuristic fails. Our
eventual goal is to make Macaw-Refinement fast enough to be the default code
discovery algorithm which would bring many more target binaries within reach.

## References

  * (1)
  * Aho et al. (1986) Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. 1986\.  _Compilers: principles, techniques, and tools_.  Addison-Wesley Longman Publishing Co., Inc., USA.
  * Alvarez (2023) Sergi Alvarez. 2023\.  Libre and Portable Reverse Engineering Framework.  https://www.radare.org/n/
  * Anand et al. (2013) Kapil Anand, Matthew Smithson, Khaled Elwazeer, Aparna Kotha, Jim Gruen, Nathan Giles, and Rajeev Barua. 2013.  A Compiler-Level Intermediate Representation Based Binary Analysis and Rewriting System. In _Proceedings of the 8th ACM European Conference on Computer Systems_ (Prague, Czech Republic) _(EuroSys ’13)_. Association for Computing Machinery, New York, NY, USA, 295–308.  https://doi.org/10.1145/2465351.2465380
  * Balakrishnan and Reps (2004) Gogul Balakrishnan and Thomas Reps. 2004.  Analyzing Memory Accesses in x86 Executables. In _Compiler Construction_ , Evelyn Duesterwald (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 5–23.
  * Barthe et al. (2011) Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2011\.  Relational Verification Using Product Programs. In _FM 2011: Formal Methods_ , Michael Butler and Wolfram Schulte (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 200–214.  https://doi.org/10.1007/978-3-642-21437-0_17
  * Barthe et al. (2013) Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2013\.  Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification. In _Logical Foundations of Computer Science_ , Sergei Artemov and Anil Nerode (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 29–43.  https://doi.org/10.1007/978-3-642-35722-0_3
  * Bond et al. (2017) Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. 2017.  Vale: Verifying High-Performance Cryptographic Assembly Code. In _Proceedings of the 26th USENIX Conference on Security Symposium_ (Vancouver, BC, Canada) _(SEC’17)_. USENIX Association, USA, 917–934.
  * Bosamiya et al. (2020) Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, and Chris Hawblitzel. 2020.  Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language. In _Software Verification: 12th International Conference, VSTTE 2020, and 13th International Workshop, NSV 2020, Los Angeles, CA, USA, July 20–21, 2020, Revised Selected Papers_ (Los Angeles, CA, USA). Springer-Verlag, Berlin, Heidelberg, 106–123.  https://doi.org/10.1007/978-3-030-63618-0_7
  * Boston et al. (2021) Brett Boston, Samuel Breese, Joey Dodds, Mike Dodds, Brian Huffman, Adam Petcher, and Andrei Stefanescu. 2021.  Verified cryptographic code for everybody. In _CAV 2021_.  https://doi.org/10.1007/978-3-030-81685-8_31
  * Brumley et al. (2011) David Brumley, Ivan Jager, Thanassis Avgerinos, and Edward J. Schwartz. 2011.  BAP: A Binary Analysis Platform. In _Computer Aided Verification_ , Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 463–469.  https://doi.org/10.1007/978-3-642-22110-1_37
  * Cantrill et al. (2004) Bryan M. Cantrill, Michael W. Shapiro, and Adam H. Leventhal. 2004.  Dynamic Instrumentation of Production Systems. In _Proceedings of the Annual Conference on USENIX Annual Technical Conference_ (Boston, MA) _(ATEC ’04)_. USENIX Association, USA, 2\.  https://doi.org/10.5555/1247415.1247417
  * Cha et al. (2012) Sang Kil Cha, Thanassis Avgerinos, Alexandre Rebert, and David Brumley. 2012.  Unleashing Mayhem on Binary Code. In _2012 IEEE Symposium on Security and Privacy_. 380–394.  https://doi.org/10.1109/SP.2012.31
  * Chipounov and Candea (2011) Vitaly Chipounov and George Candea. 2011.  Enabling Sophisticated Analyses of ×86 Binaries with RevGen. In _Proceedings of the 2011 IEEE/IFIP 41st International Conference on Dependable Systems and Networks Workshops_ _(DSNW ’11)_. IEEE Computer Society, USA, 211–216.  https://doi.org/10.1109/DSNW.2011.5958815
  * Christiansen et al. (2019) David Thrane Christiansen, Iavor S. Diatchki, Robert Dockins, Joe Hendrix, and Tristan Ravitch. 2019\.  Dependently Typed Haskell in Industry (Experience Report).  _Proc. ACM Program. Lang._ 3, ICFP, Article 100 (July 2019), 16 pages.  https://doi.org/10.1145/3341704
  * Chudnov et al. (2018) Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCárthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb, and Eddy Westbrook. 2018\.  Continuous Formal Verification of Amazon s2n. In _Computer Aided Verification_ , Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing, Cham, 430–446.  https://doi.org/10.1007/978-3-319-96142-2_26
  * Cohen (1993) Frederick B. Cohen. 1993\.  Operating System Protection through Program Evolution.  _Comput. Secur._ 12, 6 (oct 1993), 565–584.  https://doi.org/10.1016/0167-4048(93)90054-9
  * David et al. (2016) Yaniv David, Nimrod Partush, and Eran Yahav. 2016\.  Statistical Similarity of Binaries.  _SIGPLAN Not._ 51, 6 (jun 2016), 266–280.  https://doi.org/10.1145/2980983.2908126
  * David et al. (2017) Yaniv David, Nimrod Partush, and Eran Yahav. 2017\.  Similarity of Binaries through Re-Optimization. In _Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Barcelona, Spain) _(PLDI 2017)_. Association for Computing Machinery, New York, NY, USA, 79–94.  https://doi.org/10.1145/3062341.3062387
  * Di Federico et al. (2017) Alessandro Di Federico, Mathias Payer, and Giovanni Agosta. 2017\.  rev.ng: a unified binary analysis framework to recover CFGs and function boundaries. In _Proceedings of the 26th International Conference on Compiler Construction_ (Austin, TX, USA) _(CC 2017)_. Association for Computing Machinery, New York, NY, USA, 131–141.  https://doi.org/10.1145/3033019.3033028
  * Dinaburg and Ruef (2014) Artem Dinaburg and Andrew Ruef. 2014.  McSema: Static Translation of X86 Instructions to LLVM. In _ReCon 2014 Conference, Montreal, Canada_.  https://recon.cx/2014/slides/McSema.pdf
  * Dockins et al. (2016) Robert Dockins, Adam Foltzer, Joe Hendrix, Brian Huffman, Dylan McNamee, and Aaron Tomb. 2016\.  Constructing Semantic Models of Programs with the Software Analysis Workbench. In _Verified Software. Theories, Tools, and Experiments_ , Sandrine Blazy and Marsha Chechik (Eds.). Springer International Publishing, Cham, 56–72.  https://doi.org/10.1007/978-3-319-48869-1_5
  * Dodds (2020) Joey Dodds. 2020\.  Announcing the ‘blst’ BLS Verification Project.  https://galois.com/blog/2020/09/announcing-the-blst-bls-verification-project/
  * Dullien (2020) Thomas Dullien. 2020\.  Weird Machines, Exploitability, and Provable Unexploitability.  _IEEE Transactions on Emerging Topics in Computing_ 8, 2 (2020), 391–403.  https://doi.org/10.1109/TETC.2017.2785299
  * Eagle (2011) Chris Eagle. 2011\.  _The IDA Pro Book: The Unofficial Guide to the World’s Most Popular Disassembler_.  No Starch Press, USA.
  * Eisenberg and Weirich (2012) Richard A. Eisenberg and Stephanie Weirich. 2012.  Dependently Typed Programming with Singletons.  _SIGPLAN Not._ 47, 12 (sep 2012), 117–130.  https://doi.org/10.1145/2430532.2364522
  * Fromherz et al. (2019) Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy. 2019.  A Verified, Efficient Embedding of a Verifiable Assembly Language.  _Proc. ACM Program. Lang._ 3, POPL, Article 63 (jan 2019), 30 pages.  https://doi.org/10.1145/3290376
  * Gregg and Mauro (2011) Brendan Gregg and Jim Mauro. 2011.  _DTrace: Dynamic Tracing in Oracle Solaris, Mac OS X and FreeBSD_ (1st ed.).  Prentice Hall Press, USA.  https://doi.org/10.5555/1971960
  * Hendrix et al. (2019) Joe Hendrix, Guannan Wei, and Simon Winwood. 2019.  Towards verified binary raising. In _Workshop on Instruction Set Architecture Specification (co-located with ITP 2019)_ , Vol. 6.
  * King (1976) James C. King. 1976\.  Symbolic execution and program testing.  _Commun. ACM_ 19, 7 (jul 1976), 385–394.  https://doi.org/10.1145/360248.360252
  * Launchbury and Peyton Jones (1995) John Launchbury and Simon L. Peyton Jones. 1995.  State in Haskell.  _Lisp Symb. Comput._ 8, 4 (dec 1995), 293–341.  https://doi.org/10.1007/BF01018827
  * Lee et al. (2011) JongHyup Lee, Thanassis Avgerinos, and David Brumley. 2011\.  TIE: Principled Reverse Engineering of Types in Binary Programs.  (2 2011).  https://doi.org/10.1184/R1/6469466.v1
  * Naus et al. (2023) Nico Naus, Freek Verbeek, Dale Walker, and Binoy Ravindran. 2023\.  A Formal Semantics For P-Code. In _Verified Software. Theories, Tools and Experiments.: 14th International Conference, VSTTE 2022, Trento, Italy, October 17–18, 2022, Revised Selected Papers_ (Trento, Italy). Springer-Verlag, Berlin, Heidelberg, 111–128.  https://doi.org/10.1007/978-3-031-25803-9_7
  * Protzenko et al. (2020) Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, and Santiago Zanella-Beguelin. 2020\.  EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. In _2020 IEEE Symposium on Security and Privacy (SP)_. 983–1002.  https://doi.org/10.1109/SP40000.2020.00114
  * Protzenko et al. (2017) Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. 2017\.  Verified Low-Level Programming Embedded in F*.  _Proc. ACM Program. Lang._ 1, ICFP, Article 17 (aug 2017), 29 pages.  https://doi.org/10.1145/3110261
  * Radare2 Book (2023) Radare2 Book. 2023\.  ESIL.  https://book.rada.re/disassembling/esil.html
  * Reid (2016) Alastair Reid. 2016\.  Trustworthy specifications of ARM® v8-A and v8-M system level architecture. In _2016 Formal Methods in Computer-Aided Design (FMCAD)_. 161–168.  https://doi.org/10.1109/FMCAD.2016.7886675
  * Rohleder (2019) Roman Rohleder. 2019\.  Hands-On Ghidra - A Tutorial about the Software Reverse Engineering Framework. In _Proceedings of the 3rd ACM Workshop on Software Protection_ (London, United Kingdom) _(SPRO’19)_. Association for Computing Machinery, New York, NY, USA, 77–78.  https://doi.org/10.1145/3338503.3357725
  * Rolles (2018) Rolf Rolles. 2018\.  Hex-Rays Microcode API vs. Obfuscating Compiler.  https://hex-rays.com/blog/hex-rays-microcode-api-vs-obfuscating-compiler/
  * Saudel and Salwan (2015) Florent Saudel and Jonathan Salwan. 2015.  Triton: Concolic execution framework. In _Symposium sur la sécurité des technologies de l’information et des communications (SSTIC)_.
  * Schrijvers et al. (2008) Tom Schrijvers, Simon Peyton Jones, Manuel Chakravarty, and Martin Sulzmann. 2008.  Type Checking with Open Type Functions. In _Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming_ (Victoria, BC, Canada) _(ICFP ’08)_. Association for Computing Machinery, New York, NY, USA, 51–62.  https://doi.org/10.1145/1411204.1411215
  * Schulte et al. (2022) Eric Schulte, Michael D. Brown, and Vlad Folts. 2022.  A Broad Comparative Evaluation of X86-64 Binary Rewriters. In _Proceedings of the 15th Workshop on Cyber Security Experimentation and Test_ (Virtual, CA, USA) _(CSET ’22)_. Association for Computing Machinery, New York, NY, USA, 129–144.  https://doi.org/10.1145/3546096.3546112
  * Schwartz et al. (2010) Edward J. Schwartz, Thanassis Avgerinos, and David Brumley. 2010.  All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask). In _Proceedings of the 2010 IEEE Symposium on Security and Privacy_ _(SP ’10)_. IEEE Computer Society, USA, 317–331.  https://doi.org/10.1109/SP.2010.26
  * Scott et al. (2021) Ryan Scott, Robert Dockins, Tristan Ravitch, and Aaron Tomb. 2021.  Crux: Symbolic Execution Meets SMT-based Verification (Competition Contribution).  https://doi.org/10.5281/zenodo.6147218
  * Selfridge (2019) Benjamin Selfridge. 2019\.  GRIFT: A richly-typed, deeply-embedded RISC-V semantics written in Haskell. In _Proc. SpISA 2019: Workshop Instr. Set Architect. Specification_.
  * Shoshitaishvili et al. (2016) Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Audrey Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, and Giovanni Vigna. 2016.  SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis. In _IEEE Symposium on Security and Privacy_.
  * Srinivasan and Reps (2015) Venkatesh Srinivasan and Thomas Reps. 2015.  Synthesis of machine code from semantics. In _Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation_. 596–607.
  * Stephens et al. (2016) Nick Stephens, John Grosen, Christopher Salls, Andrew Dutcher, Ruoyu Wang, Jacopo Corbetta, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna. 2016.  Driller: Augmenting fuzzing through selective symbolic execution.. In _NDSS_ , Vol. 16. 1–16.
  * Vector35 (2023a) Vector35. 2023a.  Binary Ninja.  https://binary.ninja/
  * Vector35 (2023b) Vector35. 2023b.  Binary Ninja Intermediate Language: Overview.  https://docs.binary.ninja/dev/bnil-overview.html
  * Vegasena and Goodman (2019) Sai Vegasena and Peter Goodman. 2019.  Binary symbolic execution with KLEE-Native.  https://blog.trailofbits.com/2019/08/30/binary-symbolic-execution-with-klee-native/
  * Yorgey et al. (2012) Brent A. Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and José Pedro Magalhães. 2012\.  Giving Haskell a Promotion. In _Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation_ (Philadelphia, Pennsylvania, USA) _(TLDI ’12)_. Association for Computing Machinery, New York, NY, USA, 53–66.  https://doi.org/10.1145/2103786.2103795

##  Appendix A Macaw Design (Additional Details)

⬇ data MemRepr (tp :: MacawType) where BVMemRepr :: (1 <= w) => NatRepr w ->
Endianness -> MemRepr (BVType (8*w)) FloatMemRepr :: FloatInfoRepr f ->
Endianness -> MemRepr (FloatType f) PackedVecMemRepr :: NatRepr n -> MemRepr
tp -> MemRepr (VecType n tp) data FloatInfoRepr (fi :: FloatInfo) where
SingleFloatRepr :: FloatInfoRepr SingleFloat DoubleFloatRepr :: FloatInfoRepr
DoubleFloat ...
---
Figure A.1. The definition of MacawType in Macaw, which describes the shape of
machine-code values at the type level. This type is witnessed at the value
level by MemRepr, which can be thought of as the singleton type (Eisenberg and
Weirich, 2012) for MacawType.

⬇

type family ArchReg arch :: MacawType -> Type

type instance ArchReg X86_64 = X86Reg

type instance ArchReg AArch32 = ARMReg

...

type family ArchStmt arch :: MacawType -> Type

type family ArchTermStmt arch :: MacawType -> Type

type family RegAddrWidth (r :: MacawType -> Type) :: Nat

type instance RegAddrWidth X86Reg = 64

type instance RegAddrWidth ARMReg = 32

...

type ArchAddrWidth arch = RegAddrWidth (ArchReg arch)

type ArchAddrWord arch = MemWord (ArchAddrWidth arch)

type ArchMemAddr arch = MemAddr (ArchAddrWidth arch)

type ArchSegmentOff arch = MemSegmentOff (ArchAddrWidth arch)

Figure A.2. Type families and synonyms related to architecture extension
points. ⬇ data Stmt arch ids where AssignStmt :: Assignment arch ids tp ->
Stmt arch ids WriteMem :: ArchAddrValue arch ids -> MemRepr tp -> Value arch
ids tp -> Stmt arch ids ExecArchStmt :: ArchStmt arch (Value arch ids) -> Stmt
arch ids ArchState :: ArchMemAddr arch) -> RegState (ArchReg arch) (Value arch
ids) -> Stmt arch ids InstructionStart :: ArchAddrWord arch -> Text -> Stmt
arch ids Comment :: Text -> Stmt arch ids
---
Figure A.3. Data types used in Macaw’s intermediate language.

##  Appendix B Reopt Case Study (Additional Details)

⬇ ;; Original x86-64 instruction cmpb $0x30,0x3(%rax) ; in AT&T syntax cmp
BYTE PTR [rax+0x3],0x30 ; in Intel syntax ;; Translation without type
inference ;; %t0 corresponds to %rax and is given type i64 %t1 = add i64 %t0,
0x3 %t2 = load i8, i8* inttoptr (i64 %t1 to i8*) %t3 = icmp eq i8 %t2, 0x30 ;;
Translation with type inference ;; %t0 corresponds to %rax and is given type
{{i8,i8,i8},{i8,i8}}* %t1 = getelementptr {{i8,i8,i8},{i8,i8}},
{{i8,i8,i8},{i8,i8}}* %t0, i32 0, i32 1 %t2 = getelementptr {i8,i8}, {i8,i8}*
%t1, i32 0, i32 0 %t3 = load i8, i8* %t2 %t4 = icmp eq i8 %t3, 0x30
---
Figure B.1. Example of the impact of Reopt ’s type inference on LLVM output.
getelementptr instructions only help LLVM’s type system and have no
performance impact.