2 Overview

The input-output relations of libLISA are depicted in Figure 1. It uses a CPU observer, and produces a set of encodings, as well as semantics for each encoding.

2.1 CPU Observers

A CPU executes instructions: bitstrings of $8𝑛$ bits. Examples are the bitstrings 00000000 11011000 and 01000000 00000000 11011000, which correspond to the human description ADD AL, BL.

A CPU instruction operates on a CPU state. CPU state consists of all stored data a CPU can access: registers, flags, memory, and internal microarchitectural state like caches. We only need a small part of the CPU state for our analysis. A CPU state is represented as a bitstring. That bitstring contains the contents of in-scope registers, flags and memory. We only store memory areas when we have determined that this memory is accessed, as it would be infeasible to store all $2^{\left\{64\right\}}$ bytes of memory a 64-bit CPU could access. A CPU observer is a function that takes as input an instruction and a CPU state, and produces as output a new CPU state.

Our CPU state representation for x86-64 contains 769 bytes (excluding memory). It includes general-purpose registers (RAX..R15), RFLAGS, FS and GS. It also includes state from processor state components 0 (x87), 1 (SSE) and 2 (AVX): the 16 YMM registers (including the exception flags and DAZ from the MXCSR register), and the ST/MMX registers (including FSW and FTW).

The x86-64 CPU state representation does not contain unused segment registers (CS, DS, SS, ES) or state from other processor state components not mentioned above (e.g., virtualization registers, MPX, or AVX-512).

Anything not listed above is not part of the CPU state. It is therefore not observable. This does not mean that instructions using this state cannot be analyzed. Instead, the resulting semantics describe the instruction as if the parts of the CPU state that are not in our CPU state representation do not exist. For example, the semantics for a CLFLUSH (cache flush) instruction will look like an instruction that does nothing.

2.2 Encodings and Semantics

We introduce the concept of an encoding: a group of instructions that differ only by operands. The operands must remain of the same type, i.e., registers, flags, immediates or memory. In order to obtain an encoding, it must have been established what the operands are, and thus what the in- and outputs of the group of instructions are. An encoding consists of a bitpattern (for grouping instructions), as well as dataflows (for operand identification).

To formalize these notions, we introduce various concepts, summarized in Table 1. Immediate values and registers (and flags) are straightforward. An address computation of type $𝐴$ is a function over registers and immediate values (e.g, $\text{RAX}+4\ast \text{ECX}$). A memory access of type $𝑀$ is a tuple with an address computation and a size.

Bitpatterns. The bitpattern identifies parts of the bitstring, as well as the constituents these parts are mapped to, given concrete instantiations. We name the parts using underlined letters. Formally, a part can be modeled as a list of indices within the bitstring. A bitpattern, then, is a mapping from parts and bitstrings to constituents: either immediate values, registers or address computations. Reconsidering Example, we formally have the parts $\left[0,1\right]$ and $\left[3,4\right]$ and the bitpattern:

However, we use notation aa as in Example when possible.

Dataflows. A dataflow identifies a list of sources that are used as inputs to a computation that produces a value stored in a destination. Destinations are represented by parts, registers, or memory accesses. Sources can be immediate values as well. A dataflow can thus be instantiated using the part mapping of the bitpattern. Note that it does not define the computation that actually occurs. In Example, these computations thus have been denoted with undefined boxes.

The generated semantics consist of encodings together with defined computations for all dataflows. These computations describe how new values for destinations are computed using a set of sources. Effectively, the boxes in Example are replaced with actual functions.

Normally, instructions increment RIP by the instruction length to advance to the next instruction. Branch instructions are considered as normal instructions that update RIP by (conditionally) incrementing RIP with the jump offset. Repeating instructions, such as REPNZ STOSB, perform one iteration of the repetition at a time, but do not increment RIP as long as the repeat condition holds.

2.2.1 Scope

We restrict the enumeration scope to keep the runtime feasible. We exclude instructions with the following prefixes from being analyzed: REPNZ (F2), REPZ (F3), segment overrides (26, 2E, 36, 3E, 64, 65), and data overrides and address size overrides (66, 67). We enforce an ordering on instruction prefixes: a lock prefix (F0) must always appear before REX (40-4F) prefixes.

The primary reason for the restrictions on prefixes is running time. These prefixes can appear in front of any (non-VEX prefixed) instruction. Even when excluding invalid sequences of prefixes, including these prefixes would increase runtime by at least a factor of $84\times$. Segmentation, looping instructions, and data and address size overrides are excluded because these are the least commonly used prefixes. Four out of six segment registers are hard-coded to 0, while the other two have limited uses. The looping prefixes can only be applied to a handful of instructions, and are ignored for all other instructions. The data size overrides are used for legacy encodings of SSE operations and 16-bit arithmetic. The address size overrides are only relevant when using 32-bit pointers. As shown in Table 5 in Section 5, the scope still covers $97.36\%$ of instructions found in Linux binaries.

Furthermore, instructions are deemed out of enumeration scope in the following cases: they

1. perform a variable number of memory accesses,
2. do not perform the memory accesses in a fixed order,
3. always fault (e.g., with the undefined instruction exception UD),
4. access registers not included in the CPU state representation described in Section 2.1 (e.g., MXCSR),
5. perform operations involving segment selectors (e.g., LAR, LSS),
6. require privileges (i.e., they do not run in CPU ring 3)
7. save or load CPU state (e.g., XSAVE or FRSTOR)

The rationale behind this scope is a trade-off between the additional implementation complexity and additional running time that adding support for a larger scope would entail, versus the yield. For example, implementing support for a variable number of memory accesses is very hard and will likely impact the running time, but to the best of our knowledge there is only a single instruction in the x86-64 architecture that exhibits such behavior.

We would like to stress that, even if instructions are out of enumeration scope, they can still be analyzed on-the-fly. For example, if one wants to analyze a binary and encounters an instruction that is outside the enumeration scope, semantics for this instruction can still be generated on-the-fly, as long as it is within synthesis scope. We demonstrate this in Section 5.4.

We do not synthesize semantics for instructions that perform floating-point arithmetic. We exclude these, because floating point operations can be approximate. We found two approaches in related work. The first consists of using uninterpreted functions and leaving the exact semantics up to the user [1]. This is not suitable for libLISA, as it is impossible to synthesize uninterpreted functions. The second is to define floating-point semantics in terms of the semantics of floating-point instructions [2]. We considered this unsuitable for libLISA, as this means the same semantics might produce different results on different CPUs.

For all other enumerated encodings, i.e., all encodings not using floating-point operations, we expect synthesis to produce semantics. However, this may fail, e.g., due to a time-out (we have a bound of 2 tries of at most 7.5 minutes per encoding).