LibLISA is a library for Learning Instruction Set Architecture semantics. It only needs to know about CPU registers, flags, memory and how to observe the execution of a single instruction. From there, libLISA can learn the semantics of x86-64 instructions that use general-purpose registers and flags.
We ran libLISA for around 300 hours and enumerated around 25,000 encodings. From that, we learned the correct semantics for around 4,000 encodings in around 40 hours. These 4000 encodings represent around 5% of the x86-64 instruction space. We provide the results in the results/
directory. The encodings-enumerated.json
file contains all encodings that we enumerated. The encodings-correct.json
file contains all encodings with correct semantics.
Results are stored by serializing the structures to JSON via the serde_json
crate. We provide a file containing all encodings that have been enumerated, as well as a file containing the encodings with correctly synthesized computations. The former are stored as a Vec<Encoding<X64Arch, BasicComputation>>
, while the latter are stored as a Vec<Encoding<X64Arch, DecisionTreeComputation>>
.
The easiest way to use the results is to load them using the serde_json
crate. This can be done as follows:
let file = File::open("results/encodings-enumerated.json")?;
let enumerated_encodings: Vec<Encoding<X64Arch, BasicComputation>> = serde_json::from_reader(file)?;
You can build all binaries by running cargo build --release
. The binaries can then be found in target/release/
. You can also run binaries directly by running cargo run --release --bin [name of binary] -- [arguments..]
. Learning the semantics of a CPU is split into three phases:
- Preparation: Create an output directory. Replace
$DIR
with your output directory in all following commands. - Phase 1: Enumeration
- (Optional) scan the instruction space by running
scan $DIR/scan-output.json
. - Create a new enumerator by running
enumerate $DIR/enumeration/ create --workers 16
. You may optionally specify the instruction scan with--scan $DIR/scan-output.json
- Run enumeration with
enumerate $DIR/enumeration run
. You can terminate this process at any time by sending^C
. This will gracefully terminate the worker threads and save state to disk. You may also check the progress of the enumeration by runningenumerate $DIR/enumeration/ status
. - Once enumeration has finished or you are satisfied with the number of instructions that were enumerated, you can run
enumerate $DIR/enumeration/ extract $DIR/encodings-enumerated.json
to extract all enumerated encodings.
- (Optional) scan the instruction space by running
- Phase 2: Synthesis
- Create an address synthesizer by running
synthesize-addrs $DIR/synthesis/addrs/ create --workers 16
. - Run address synthesis with
synthesize-addrs $DIR/synthesis/addrs/ run
. You can terminate this process at any time by sending^C
. This will gracefully terminate the worker threads and save state to disk. You may also check the progress of the synthesis by runningsynthesize-addrs $DIR/synthesis/addrs/ status
. - Once address synthesis has finished or you are satisfied with the number of synthesized addresses, you can start synthesizing dataflows. Create a dataflow synthesizer by running
synthesize-dataflows $DIR/synthesis/dataflows/ create $DIR/synthesis/addrs/ --workers 16
. - Run address synthesis with
synthesize-dataflows $DIR/synthesis/dataflows/ run
. You can terminate this process at any time by sending^C
. This will gracefully terminate the worker threads and save state to disk. You may also check the progress of the synthesis by runningsynthesize-dataflows $DIR/synthesis/dataflows/ status
. - Once dataflow synthesis has finished or you are satisfied with the number of synthesized dataflows, you can extract encodings with computations by running
synthesize-dataflows $DIR/synthesis/dataflows/ extract $DIR/encodings-synthesized.json
. You must pass the--partial
flag if dataflow synthesis has not finished synthesizing all computations.
- Create an address synthesizer by running
- Phase 3: Validation
- Create a correctness verifier by running
verify-correctness $DIR/correctness/ create $DIR/encodings-synthesized.json
. - Run correctness verification with
verify-correctness $DIR/correctness/ run
. You can terminate this process at any time by sending^C
. This will gracefully terminate the worker threads and save state to disk. You may also check the progress of the synthesis by runningverify-correctness $DIR/correctness/ status
. - Once correctness verification has has finished or you are satisfied with the time spent on validation, you can extract the correct encodings by running
verify-correctness $DIR/correctness/ extract $DIR/encodings-correct.json
.
- Create a correctness verifier by running
The project is split into six crates:
liblisa-core
contains generic definitions of CPU state, ISAs, encodings, dataflows and other core components of libLISA.liblisa-enc
contains all code for encoding analysis.liblisa-synth
contains all code for the synthesis of computations.liblisa
contains some high-level code for processing encodings as well as code to handle long-running enumeration, synthesis, or validation sessions that can be interrupted at any time.liblisa-x64
contains all code related to the x64 architecture. It defines registers, flags and CPU state. It also provides implementations for observing the execution of instructions.liblisa-x64-kmod
contains the kernel module and a wrapper library.lisacli
contains code for the command-line (CLI) binaries that can be used to invoke libLISA.
The code in this repository is licensed under the AGPLv3, except for the kernel module in liblisa-x64-kmod/module/
which is licensed under the GNU Public License v2. The results in the results/
directory are released under a Creative Commons Zero license.