BAP Lifter Accuracy Verification Tool

This tool uses trace files from pintrace or qemu to verify the lifters accuracy. For each instruction, the tracing tool records in the trace file all side effects, such as memory accesses, register updates, and so on. We call these effects the trace events. The bap-veri tool reads the events from the trace file then disassembles and lifts each instruction (which is also stored in the trace file) and emulates them using a BIL interpreter that collects all side-effects in the form of a set of trace events. Ideally, the stored set and the emulated sets should coincide. In reality, the tracing tools have their own abstractions and could be less precise or more precise than BAP. For example, qemu doesn't really track changes in the status registers and instead generates a flag change event even if it wasn't changed. To address this, bap-veri uses policy files that contain simple rules describing which events shall be ignored and which events are crucial.

Each instruction is compared independently starting from a clean state. Since BAP doesn't have access to the full image and execution enviroment, like the state of the heap or registers, we peek the values from the trace, e.g., if in the trace we see event like RAX => 0x2A we know that RAX contained 0x2A.

Installing

To install the tool use opam, e.g.,

opam install bap-veri

If you need the latest master version, do

opam pin add --dev-repo bap-veri

Running

First of all, you will need to obtain a trace file. For that you need to build either of our tracing tools, [pin-trace] or qemu. Both tracing tools store their information using the bap-frames file format, so you need to build and install the bap-frames codec as well. If you installed bap from opam, e.g., with opam install bap, then you can just do

opam install bap-frames

Alternatively, you can build it from sources, see the coreponding instructions.

Once you have everything ready, you can run bap veri as

bap veri --show-errors --show-stat <trace-file>

Notice that there's no need for the original binary or libraries, all the necessary information is stored in the binary. Before running bap veri you can use bap --trace-dump <trace-file> to print the contents of the trace file in a human-readable format.

You can also specify a policy file using --rules <policy-file>. If you don't know what it is, read the next section.

Policy

The policy file contains a list of rules, somewhat similar to the firewall rules. The rules are executed in order, the first that matches is applied. A rule contains four fields: ACTION INSN TRACER_EVENT LIFTER_EVENT:

1. The ACTION field is either SKIP or DENY. DENY means that we found an unacceptable inconsistency that should be reported as a problem. The SKIP action means that we can ignore this inconsistency.
2. The INSN field could contain an instruction name like MOV64rr or regular expression, like MOV.*, the rule will be applied only to instructions that match the INSN field.
3. The TRACER_EVENT field denotes a tracing event generated by the tracing tool. It could be a string or a regular expression, or '' that denotes a lack of event. The rule will be applied the tracer generated a matching event.
4. The LIFTER_EVENT field denotes a tracing event generated during the emulation of a lifted instruction. It has the same format as the TRACER_EVENT.

When bap-veri detects that the set of tracer events is not equal to the set of lifter events it will use the specified policy file to figure out what to do next. For each event in either set complements it will try to find the matching rule. Matching is performed on the textual representation of events (you can always use bap --trace-dump <trace-file> to see how they look). Rules are written in a text file in which every line is either a rule, a comment, or an empty line. A comment line starts with # and is ignored. The rule must have exactly four fields separated with whitespaces. If the field contains a space it should be delimited with with single or double quotes, e.g., "RAX => .*". If a field is empty (i.e., matches with an empty string or an absence of event), then use '' or "".

Examples

Let's imagine that a tracer, unlike BAP, ignores accesses to the ZF register. To skip this inconsistency, we write the following rule

SKIP .* '' 'ZF -> .*'

It literally means, for any instruction, if there is an umatched read from ZF then skip it.

The next two rules specify that tracer and lifter event sets must be equal. And this is the default policy, when no policy is specified.

DENY .* .* ''
DENY .* '' .*

The rules match with every instruction and trigger whenever there is a TRACER_EVENT that doesn't has a matching LIFTER_EVENT (the first rule) or there is a LIFTER_EVENT that doesn't have a matching `LIFTER_EVENT.

Backreferences

It is also possible to use back references in regular expressions. A group is denoted with simple parentheses, e.g., and could be referenced by number (counting from 1) using \<n> syntax, e.g.,

DENY .* '(.F) <= .*' '\1 <= .*'

This rule captures any writes to a flag register, e.g., ZF, PF, etc, that write different values, e.g., it will match with, ZF <= 0 vs. ZF <= 1. Keep in mind that rules are only applied to unmatched event, so if the events were already matching then they will not be even checked by the policy checker.

Developing

If you want to modify the tool, then make sure that bap is installed. Note, that installing bap prebuilt binaries will not work. You need libraries and the toolchain. Also, make sure that you have installed other dependencies. You can look them in the opam file, or ask opam to do the work for you using opam pin, e.g.,

opam pin add bap-veri --dev-repo
opam install bap-veri --deps-only
opam pin remove bap-veri

Now, when all the prerequisites are met, we can build and install bap-veri,

oasis setup
make
make install

Now you can change the code and repeat the last two steps.