5 Results

We analyzed the x86-64 CPUs listed in Table Table 4. The AMD 3900X and AMD 7700X use the Zen 2 and Zen 4 microarchitecture respectively. The Intel i9-13900 has two different kinds of cores. Performance cores (${𝐴}_2$) use Raptor Cove, while efficiency cores (${𝐴}_3$) use the Gracemont microarchitecture. The Intel Xeon 4110 Silver uses the Skylake microarchitecture, a predecessor of Raptor Lake.

Table 5 provides an overview of the results. Per architecture, it provides the number of generated encodings and the total time it took to run libLISA.

5.1 Validation

To validate our approach, we aim to answer two questions:

1. Do libLISA’s encodings cover all instructions on the CPU?
2. Is libLISA able to synthesize semantics for undefined behavior?

Each of these questions is impossible to answer definitively, without access to an oracle that provides the ground truth (e.g., a trustworthy hardware design). Such oracles do not exist for x86-64 CPUs, e.g., there is no trustworthy complete overview of the set of all valid instructions for each of the CPUs. We therefore in this section devise best-effort oracles and answer these questions relative to those oracles. In that section, we provide an evaluative comparison to related work instead of relative to a best-effort oracle.

5.1.1 Instruction Coverage

As best-effort oracle, we generate lists of instructions. The first list consists of instructions extracted from the Linux binaries ls, libxul.so, grep, gcc, ls, perl and ssh. This generally produces documented instructions, although these instructions are not always valid instructions on the CPU that is being analyzed.

From the Linux binaries we extracted 3190703 instructions. On average, these instructions covered 4975.4 distinct encodings.

Per architecture, we compute the in-scope coverage ${𝐶}_{\text{in}}$ as the percentage of instructions in enumeration scope from the oracle that are covered by an encoding.

The out-of-scope coverage ${𝐶}_{\text{out}}$ is computed as the percentage of all oracle-instructions that are covered.

Table 5 presents results. On average, libLISA achieves 99.99% in-scope coverage. Uncovered instructions consist of instructions with the EVEX prefix, which are not supported by any of the architectures we tested, and the SHA instructions, which are not supported by ${𝐴}_4$. These instructions are conditionally executed only when CPU support is detected.

The second approach is to randomly generate byte sequences. This discovers instructions that can be undocumented or not commonly used in real-world programs, but it is biased to simpler instructions. We randomly generated an average of 7719371.8 instructions per architecture, covering 8052.6 encodings on average.

Table 5 shows the coverage ${𝐶}_{\text{random},\text{in}}$, the percentage of in-scope oracle-instructions discovered by libLISA, which is 99.9% on average.

5.1.2 Undefined Behavior

We aim to determine how well our approach is able to synthesize semantics for undefined behavior. By determining the encodings which have undefined behavior using a best-effort oracle, we can compute the percentage for which libLISA has successfully synthesized semantics.

The best-effort oracle is a manual translation of the undefined behavior specified in the Intel Reference Manual to a machine-readable specification. This specification relies on the Intel XED disassembler library to map bitstrings to instruction variants listed in the Intel Reference Manual.

There is no one-to-one mapping from instruction variants produced by the Intel XED disassembler library to encodings. This makes it unfeasible to delineate exactly which parts of the instruction space covered by an encoding exhibit undefined behavior. We therefore define the term “undefined behavior” conservatively: if even one instruction covered by the encoding has at least one input for which at least one output is undefined, we consider the encoding to have “undefined behavior”.

We determine if an encoding has “undefined behavior” by randomly sampling instructions covered by the encoding. Then, we query the oracle separately for each sampled instruction. If the oracle determines that at least one of the sampled instructions exhibits undefined behavior, we consider the encoding to have undefined behavior.

The results are shown in Table 6. On average, 90% of the encodings marked as having undefined behavior by the oracle were synthesized.

5.2 Comparisons with Existing Work

In this section we aim to answer two questions:

1. Do our semantics cover the same instructions semantics provided by related work?
2. Are our semantics correct relative to semantics provided by related work?

As related work, we consider the work of Dasgupta et al. [1] (see Section Section 3 for a more in-depth discussion on related work). The work provides a mapping of instruction variants to semantics. Examples of instruction variants are ADD R8, IMM8 and XCHL R32, EAX.

Instruction variants do not easily translate to encodings, or the other way around. An instruction variant is not a subset of an encoding, nor is an encoding a subset of an instruction variant. It is also not possible to query all bitstrings that are described by a certain instruction variant. This makes it impossible to compare instruction variants and encodings directly.

5.2.1 Approach

To map encodings to variants, we randomly pick instantiations (i.e., concrete bitstrings). For each encoding, we generate 10000 instantiations and filter them such that there are at most three instantiations with the same mnemonic, operand types and operand equality, according to objdump (also used by Dasgupta et al.). Then, we find the right instruction variant in the related work (if it exists) and instantiate it. We export both semantics to the SMTLib format [16], and check for equivalence using Z3 [26].

It is difficult to export Dasgupta et al.‘s semantics, which are specified in the K framework [27], to SMTLib format. Dasgupta et al. have implemented a conversion to the SMTLib format by constructing a program containing a single instruction followed by RETQ, then recompiling the semantics, executing the K prover on the program, extracting the last K state from the output log, converting this K state to Z3 by parsing the state, generating a Python program that uses the Z3 library to reconstruct the expressions, and then running the Python program. This process is too slow for 118000 encodings.

To be able to extract semantics quickly, we have written a minimal parser and rewrite engine that can process the original K semantics. There are 62 variants which we were unable to process. Four variants contain incorrect rules (LOOPNE, [V]PCMPISTR[I/M]). We exclude the CLD, STD variants because these variants use the direction flag, which libLISA does not synthesize. The rest of the 62 variants require functionality that we did not implement, e.g., late-evaluation of RSP in memory addresses.

It is not always clear which variant should be picked. Dasgupta et al.‘s semantics do not specify immediate value sizes. They attempt to fix this during compilation by always deleting the imm8 variants of instructions that also have imm32 variants, forcing the imm32 variant to be used. However, their list of instructions is incomplete (for example, sbb_r32_imm8 is missing) We instead inspect variable names to determine the intended size of immediate values. The semantics also contain overlapping variants (e.g., shl_r32_one and shl_r32_imm8), we use a heuristic to score variants and select the most applicable variant.

Some of Dasgupta et al.‘s instruction variants are aliases of other variants. We copy the comparison results from the variant returned by the disassembler to other aliases.

5.2.2 Comparison Results

Table 7 provides the results. A variant agrees with libLISA when for all concrete bitstrings generated from the encodings, Z3 is able to prove equivalence between libLISA and Dasgupta et al.‘s semantics. A variant disagrees with libLISA when this is not the case. We discuss the differences between libLISA and Dasgupta et al. in more detail in the rest of this section.

Disagreements (Dasgupta et al. incorrect). We identify errors in 28 variants of the semantics of Dasgupta et al.:

1. The overflow flag (OF) of RCLB/RCRB is undefined when the masked rotate count is not 0 or 1. However, Dasgupta et al. specifies the OF as undefined when the masked rotate count modulo the operand size + 1 is not 0 or 1. (10 variants)
2. In vmpsadbw_xmm_xmm_m128_imm8, the result is written to the source operand (R3) instead of the destination operand (R4). (1 variant)
3. In all bit test variants (BT/BTS/BTR/BTC) on memory with a register bit offset, the bit offset is computed incorrectly. The bit offset is converted to a byte offset by shifting right by 3, then zero-extending the result to 64 bits. It should be sign-extended, to preserve the sign bits of negative offsets. (8 variants)
4. The CMPS variants perform a comparison by setting flags according to ${𝑚}_2-{𝑚}_1$, but they should be set according to ${𝑚}_1-{𝑚}_2$. (6 variants)
5. The instruction XCHGL EAX, EAX can be encoded as both 87C0 and 90. The second encoding has the semantics of NOP (do nothing), while the first has the semantics of XCHGL (set the upper 32 bits of RAX to zero). The disassembler used by Dasgupta et al. incorrectly disassembles 90 with a REX prefix as XCHGL instead of NOP. (1 variant)
6. The MULX instructions write a result to two destination operands. The destination operands can be equal. Dasgupta et al.‘s semantics have not taken this possibility into account, causing the K prover to crash when MULX with equal destination operands is executed. (2 variants)

Disagreements (libLISA incorrect). Three to seven disagreements are errors in the semantics generated by libLISA. Our synthesis accepts semantics as correct when a hypothesis is correct w.r.t. two million consecutive random observations. In rare cases, these observations do not encompass all behavior of the instruction, which can lead to incorrect semantics. We see that the same kind of instruction is more often synthesized incorrectly across different architectures, but the exact variant differs. For example, ${𝐴}_0$ synthesized adc_rax_imm32 incorrectly, while ${𝐴}_1$ synthesized that variant correctly and synthesized adcq_r64_imm32 incorrectly instead. This indicates that these errors could be prevented by increasing the amount of random observations, or by improving the quality of the random observations. Some examples of errors are:

1. The zero flag of the SHLDQ M64, R64, 0x9 instruction is synthesized incorrectly for ${𝐴}_0$. The semantics correctly check that the part of the result from M64 is zero, but incorrectly check only the lower 8 instead of 9 bits shifted in from R64. This happened because the synthesizer did not encounter any cases where the lower 8 bits were 0, but the 9th bit was 1.
2. The overflow flag of the ADC instruction is synthesized incorrectly. The overflow flag being $1$ is relatively rare, and the synthesizer has not seen enough cases to form a good hypothesis.
3. The zero flag of the VPTEST instruction with identical operands is synthesized as always zero. The synthesizer did not encounter any cases where all 256 bits of the register were zero, and has therefore not seen any evidence that the zero flag can be non-zero.

Incorrect specifications. There are rel32 variants of the JRCXZ and JECXZ instructions, but these should only have rel8 variants. One variant of VCVTDQ2PD accepts two YMM operands, while it should accept one XMM and one YMM operand instead. Two variants, vcvtpd2ps_xmm_m256 and vcvttpd2dq_xmm_m256, have m128 variants that always match the same instructions. Instructions from both the m128 and m256 variants will incorrectly use the semantics of only one of the two variants. Finally, the vpinsrq_xmm_xmm_m64_imm8 variant is a copy of vpinsrq_xmm_m64_imm8. This is incorrect, as this variant should accept one more XMM register.

Out-of-scope. 744 variants are out of enumeration scope for libLISA, as described in Section 2.2.1. Most variants in this category are non-VEX versions of SSE/AVX instructions, which re-use the data size override prefix 66. For around 396.2 out-of-scope variants, similar variants without the data size override prefix agree with libLISA’s semantics. This means that by extending scope and doubling runtime, libLISA would be able to generate semantics where around 1900 variants would agree.

Synthesis failure. For 623 to 694 variants synthesis failed. This concerns mostly floating point operations, for which we did not implement support in our synthesis.

Not covered by Dasgupta et al. These encodings include both instructions that Dasgupta et al. considered out-of-scope, and instructions that Dasgupta et al. considered in-scope. Examples of variants outside Dasgupta et al.‘s scope are: undocumented instructions, instructions operating on the MMX registers, instructions using segment registers, and recent ISA extensions like the SHA1 and SHA256 instructions. Missing variants within Dasgupta et al.’s scope include: YMM variants for the VPSIGNB/VPSIGNW/VPSIGND/VPMINSW instructions, vcvtdq2pd_xmm_ymm and retq_imm.

5.3 Use Cases

We demonstrate the feasibility of three use cases:

• comparing CPU-implementations
• discovering and analyzing undocumented instructions
• emulating userspace binaries

5.3.1 Comparing CPU Implementations

By comparing the semantics of different CPU microarchitectures, we can find interesting differences. We describe the differences between the semantics we found in Table 8.

Most encodings are part of group 0, which have identical semantics across all 5 architectures. All other groups show differences between architectures. Architecture 0 and 1 often share the same semantics. This is likely because architecture 1 is a successor of architecture 0. Similarly, architecture 2 and 4 also often share semantics, and architecture 2 is also a successor of architecture 4.

Group 1, 3, 5, 20 and 28 consist primarily of differences between microarchitectural implementations. When manually inspecting these groups we find bit shifts, rotates, multiplication, division and bit manipulation instructions. These are common instructions that can exhibit undefined behavior.

Groups 2, 6-9 and 19 show differences in instruction support. Upon manual inspection, we found that group 2 contains the undocumented AMD-only instructions. Group 6 contains the SHA1 and SHA256 instructions, which were introduced after architecture 4 was released. Group 7, 8 and 9 contain various other instructions introduced in x86-64 ISA extensions. Group 19 contains the VMCALL virtualization instructions, which are Intel-only.

We can also use this table to construct fingerprinting programs. Such a program can identify the architecture it is running on, among all the analyzed architectures. For example, to distinguish between the five architectures we analyzed, we could use group 1 and group 7. By observing an instruction from group 1, we can distinguish between ${𝐴}_0$, ${𝐴}_1$ or ${𝐴}_2$, ${𝐴}_4$ or ${𝐴}_3$. Then, by also observing group 7, we can distinguish between ${𝐴}_0$ and ${𝐴}_1$ or ${𝐴}_2$ and ${𝐴}_4$. This would require executing at most 3 instructions and some logic to decode the result.

5.3.2 Discovery and Analysis of Undocumented Instructions

Undocumented instructions are valid instructions which have not been specified by the manufacturer in their documentation. For example, on Intel CPUs there used to be an undocumented instruction D6, which was only added to the Intel reference manual as the SALC instruction in 2017.

We use the Intel XED disassembler library as an oracle to determine whether instructions are documented. To eliminate false positives, we manually verified the undocumented instructions we found against the Intel and AMD reference manual and objdump.

The results are listed in Table 5. We identified one group of undocumented instructions on AMD CPUs. We did not identify any undocumented instructions on Intel CPUs. It is possible that our results are favoring Intel CPUs because we are using a disassembler library created by Intel. While we were able to manually confirm that all undocumented instructions are indeed undocumented, there might be undocumented instructions on Intel CPUs that XED incorrectly decodes successfully.

The semantics of the group of undocumented instructions on the AMD CPUs match the semantics of the VPERMQ instruction. The VPERMQ expects VEX.W to be 1. These undocumented instructions are bit-for-bit identical with VPERMQ variants except for VEX.W, which is 0. We suspect that the decoding logic for the VEX prefix does not check the value of VEX.W, and causes the instructions to be treated as if they were valid VPERMQ instructions.

5.4 Emulating Userspace Binaries

We implement a proof-of-concept emulator that uses libLISA’s semantics as-is to emulate x86-64 ELF binaries. The emulator uses the semantics from the 118000 encodings, and runs encoding analysis and synthesis on-the-fly for instructions that are out-of-prefix-scope. This makes it possible to fully emulate some Linux binaries that do not use floating-point instructions. Table 9 presents the binaries we have successfully emulated on an AMD 3900X.

The emulator stores the emulated CPU state in a data structure. During execution, it repeatedly modifies the emulated CPU state. To execute an instruction, it reads memory at the address stored in the emulated RIP. The semantics for the instruction are found by searching through libLISA’s semantics. If no suitable semantics are found, on-the-fly encoding analysis and synthesis is invoked.

The semantics are executed by fetching inputs, computing results, and then storing results. First, the values of all sources in the dataflows are fetched by reading the value from the data structure storing the emulated CPU state or memory. Then, the new values for all destinations are computed using the synthesized computations in the semantics. Finally, the new values are written to the destinations.

The emulator provides handwritten implementations for the SYSCALL, XGETBV and CPUID instructions. Additionally, we treat four additional instructions as NOPs: ICEBP, RDTSC, XSAVEC, and XRSTOR. For all other instructions we use semantics generated by libLISA.

We verify the emulated instructions against the real CPU behavior using the CPU observer. For each instruction we emulate, we compute the next CPU state, and then observe the real next CPU state. If these differ, we abort execution. In total, we have verified 1244385 instruction executions against the real CPU behavior.

We emulate the binary itself, the dynamic linker (/lib64/ld-linux-x86-64.so.2), and all dynamically loaded binaries (e.g., libc.so). This reduces the manual implementation effort, as we can rely on the dynamic linker to link dependencies automatically, instead of having to implement these manually. It also significantly increases the amount of instructions that are executed for simple binaries. The hello world binary consists of one call to printf, consisting of around 100 instructions, with the rest of the executed instructions being in the dynamic linker and the C standard library.