RSE

An updated version of Guillaume Girol's Robust Symbolic Execution (RSE) and Quantitative Robust Symbolic Execution (QRSE) as a single Binsec plugin.

How to build and install

Nix

You can run either:

• nix-build, which will create a symlink to the nix store (result).
• nix-shell, which will open a shell with binsec and all necessary runtime dependencies (i.e., Popcon).

Getting dune plugins to work with Nix is tricky, nix/dunePlugins.nix implements a solution (can be used for other / multiple plugins too).

Locally

First, you will need to install Binsec and Popcon.

Then, run:

dune build && dune install

Usage

Controlled inputs

RSE defines a controlled keyword, equivalent to nondet, for marking inputs as controlled.

Examples:

input<32> := controlled
@[esp + 4, 4] := controlled
@[esp + 8, 4] := controlled as input

Objectives

RSE extends the regular reachability objectives syntax.

robust [<name>] [merge] [quant [threshold t]] reach ...

• <name> attaches the name "name" to the objective
• merge enables the merging of states reaching the objective (only for checking quantitative robustness)
• quant enables quantitative robustness
• threshold t sets an acceptance threshold for quantitative robustness objectives (float between 0 and 1)

Examples:

robust reach * address
robust quant reach * address
robust <single> quant threshold 0.2 reach address such that ... then ...
robust <merged> merge quant threshold 0.2 reach address such that ... then ...

Command line options

• -rse: enable RSE
• -rse-term: terminate analysis when all RSE objectives are fulfilled
• -rse-qr-portfolio: set up the quantitative robustness solver portfolio (see description from binsec --help)
• -rse-no-qr-rr-precheck: disables robust reachability checking before quantitative robustness queries

Example:

binsec -sse -sse-script test/crackme.ini -rse test/magic

Publications

• Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference (CAV 2021)
• Quantitative Robustness for Vulnerability Assessment (PLDI 2024)