一句话：libLISA 无需人工编写反汇编器，即可自动发现并分析 x86-64 指令，生成 CPU 特定的形式化模型。
x86-64 指令集虽被广泛研究，但仍缺乏完整的形式化模型。本文提出 libLISA，一个自动发现并分析 CPU 指令集架构的工具。它尽量减少人工规约，不依赖人工编写的（反）汇编器来决定哪些指令可执行及其输入输出；生成 CPU 特定模型，并能为当前机器综合“未定义”行为。作者为五台 x86-64 机器生成模型，相互比较，发现未文档化指令，并生成 CPU 特定指令序列。实验表明，libLISA 几乎枚举了范围内的全部指令，其指令语义与已有工作一致，并通过暴露人工模型中的错误改进了现有工作。最终模型包含超过 118,000 个指令组，是迄今最广泛的 x86-64 形式化模型。
Even though heavily researched, a full formal model of the x86-64 instruction set is still not available. We present libLISA , a tool for automated discovery and analysis of the ISA of a CPU. This produces the most extensive formal x86-64 model to date, with over 118 000 different instruction groups. The process requires as little human specification as possible: specifically, we do not rely on a human-written (dis)assembler to dictate which instructions are executable on a given CPU, or what their in- and outputs are. The generated model is CPU-specific: behavior that is “undefined” is synthesized for the current machine. Producing models for five different x86-64 machines, we mutually compare them, discover undocumented instructions, and generate instruction sequences that are CPU-specific. Experimental evaluation shows that we enumerate virtually all instructions within scope, that the instructions’ semantics are correct w.r.t. existing work, and that we improve existing work by exposing bugs in their handwritten models.
@article{CraaijoVR24,
title = {libLISA: Instruction Discovery and Analysis on x86-64},
author = {Jos Craaijo and Freek Verbeek and Binoy Ravindran},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689723}
}