Output

The CSV output of the analyzer is just a “flattened” version of the Transmission object, which can be found in analyzer/shared/transmission.py.

Warning

Our CSV outputs all use ; as a separator

Some useful terminology when inspecting the tool’s output:

  • Components: base, secret_address, secret_val and transmitted_secret are referred to as the “components” of a transmission. Refer to the paper for a formal definition of what these components are.

  • Requirements: For each gadget and for each component, we provide a list of registers and memory locations that the attacker needs to control in order to exploit it. This means that we can initially consider all registers controlled, and later refine the search by looking at each gadget’s requirements.

  • TFPs: short for “Tainted Function Pointers”, referred to as “dispatch gadgets” in the paper

  • Aliases: During symbolic execution, our memory model creates a new symbolic variable for each symbolic load. If two symbolic loads are bound to alias in memory (e.g. LOAD64[rax] and LOAD32[rax+1]) we create alias constrain for the loaded values.

  • Constraints: During symbolic execution, we record two types of constraints:

    • “hard” constraints (or simply constraints), generated by CMOVEs and Sign-Extensions. In these cases, we split the state in two and we attach a hard constraint to the child state. These constraints cannot be bypassed.

    • “soft” constraints (or branches), generated by branch instructions. These constraints can be bypassed with speculation.

You can find some example queries in the queries/ folder.

Column List

TODO: Generate a complete description of the columns somewhere.