libLISA is a tool that can fully automatically scan instruction space, discover instructions and synthesize their semantics. It produces machine-readable, CPU-specific x86-64 instruction semantics. It relies on as little human specification as possible: specifically, it does not rely on a handwritten (dis)assembler to dictate which instructions are executable on a given CPU, or what their operands are.
We will present libLISA at OOPSLA'24.
Read the paper
Explore the data
View source code
Motivation
Even though heavily researched, a full formal model of the x86-64 instruction set is still not available. This is caused by the sheer complexity of the x86-64 architecture: the informal specification found in Intel manuals is roughly 4700 pages, and even these are known to be not trustworthy.
Specifications of CPU architectures often rely heavily on manual work, which is error-prone and labor-intensive. The current state-of-the-art formal semantics for x86-64 took 8 man-months to write, and even that specification still contains 34 errors (see Section 5.2 of our paper).
This situation becomes even more dire when taking into account that different x86-64 machines will behave differently: not only can they have different instruction sets, but behavior is also allowed to be undefined, in which case the same instruction has different behavior on different machines.
libLISA aims to solve this problem by using a CPU as the ground truth, and deriving semantics by observing instruction execution.
x86-64 Instruction Semantics
We analyzed five different architectures: AMD 3900X, AMD 7700X, Intel i9-13900 (p), Intel i9-13900 (e) and Intel Xeon Silver 4110. For each architecture, we generated around 120k encodings.
The semantics can be accessed in the following two ways:
- Use explore.liblisa.nl to browse the semantics manually.
- Use the liblisa-semantics-tool or the liblisa Rust crate to use the semantics programmatically.
The generated x86-64 semantics are CPU-specific. Around 90% of all encodings is identical on all 5 CPU architectures that we analyzed. The remaining 10% differs between architectures. We can broadly classify these differences into two categories: instruction set extensions and undefined behavior. Some x86-64 instruction set extensions, such as the SHA1 instructions, are not implemented on all CPUs. There are also many differences in how undefined behavior is implemented across different x86-64 CPU architectures.
An example of undefined behavior is the IMUL instruction. The reference manual states: "The SF, ZF, AF, and PF flags are undefined." This means that the values of these flags can differ between CPU architectures, even if the instruction is provided with the same inputs. As can be seen in libLISA's semantics explorer, The AMD 3900X and AMD 7700X do not modify these flags. The Intel i9-13900 (p) and Intel Xeon Silver 4110 compute the SF and PF correctly, and set the AF and ZF to 0. The Intel i9-13900 (e) additionally also computes the ZF flag correctly, and sets only the AF to 0.
The AMD 3900X and AMD 7700X often share the same instruction semantics. This is likely because the AMD 7700X is a successor of the AMD 3900X. Similarly, the Intel i9-13900 (p) and Intel Xeon Silver 4110 often also share semantics, likely because the Intel i9-13900 (p) is also a successor of the Intel Xeon Silver 4110.
Acknowledgements
This work is supported by the Defense Advanced Research Projects Agency (DARPA) and Naval Information Warfare Center Pacific (NIWC Pacific) under Contract No. N66001-21-C-4028.