libLISA - Instruction Discovery and Analysis on x86-64
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.
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).
