libLISA: Instruction Discovery and Analysis on x86-64
summary
libLISA automatically discovers and synthesizes x86-64 instruction semantics by observing execution and inferring operand encodings, producing a CPU-specific formal model of over 118,000 instruction groups. Running on five machines (two AMD, three Intel) over 7–21 weeks yields CPU differences, undocumented VPpermQ-like encodings on AMD, and instruction sequences usable for fingerprinting. The pipeline synthesizes semantics for about 90% of encodings marked undefined, and a comparison to a hand-written model finds 32 mismatches (28 errors in the manual model), with sources and artifacts published.
AI-written summary · about
chapters (18)
- 0:00Binary analysis challenges
- 1:03CPU instruction semantics
- 2:07Manual semantics limits
- 2:49Automating semantics discovery
- 3:51Encoding instruction operands
- 5:17Undefined behavior across CPUs
- 6:20Undocumented AMD encodings
- 7:23CPU implementation comparison
- 8:45Semantics validation
- 10:31Synthesis accuracy improvements
- 10:53Online semantics exploration
- 11:14Summary and open-source
- 11:34Q&A: Architectural vs microarchitectural state
- 12:40Q&A: Detecting CPU bugs
- 13:21Q&A: Hardware transactional memory limits
- 13:42Q&A: Finding NSA backdoors
- 14:04Q&A: Complex instructions
- 15:11Q&A: Inferring instruction templates
related talks
11mGetting Started with RISC-V Custom Instructions
17mLLM Inference on RISC-V Embedded CPUs
13mDemo: RISC-V as an Enabler of Heterogeneous Compute
01h 10mWhy RISC-V Through ISA Customization Demonstration
23mRunning an Open Source LLM on Open Source Hardware
20mThe RISC-V Formal Specification Technical Group: Progress Report
38mBASE ISA
21mA Comparative Analysis of RISC-V Architecture Based on the RISC-V SoC DV Experience