The RSE and QRSE analysis (about Robust Symbolic Execution and its Quantitative version) are now available in a single, up-to-date package: the brand-new RSE BINSEC plugin.
What is robust reachability?
Most software analysis techniques focus on bug reachability, i.e., proving the existence of inputs triggering a bug. However, this approach does not account for how the bug can be reliably reproduced, especially when some program inputs are not under our control (regarded as randomness).
The Robust reachability property tackles this issue and lets you know when a program location is reachable regardless of the uncontrolled input. It stands for perfect reproducibility.
Yet, robust reachability is quite a strong property, i.e. either it holds or not. The Quantitative version was thus proposed to bring more nuances, in order to handle more subtle scenarios where a bug is not fully reproducible but still very likely.
A quick example
Let’s apply RSE to the magic CTF example from BINSEC.
We can (somewhat artificially) transform it into a robustness problem by considering half of the input as uncontrolled in crackme.ini:
starting from <magic> # set the entrypoint to the function symbol 'magic'
esp := 0xffffccf1 # arbitrarily concretize the stack pointer
# arbitrarily concretize and set the return address of the function
return_address<32> := 0x0804812b
@[esp, 4] := return_address
@[esp + 4, 2] := controlled as input
@[esp + 6, 2] := nondet as input2
RSE defines the controlled keyword, equivalent to nondet, for controlled inputs. nondet is considered to be uncontrolled and uniformly random.
Then, to check if the winning state is robustly reachable, we would use the following objective:
robust <win> reach return_address such that al <> 0 then print input and print input2
The analysis then tells us that it is not the case:
$ binsec -sse -sse-script crackme.ini -rse magic
[rse:result] robust<win:0>: reached
[rse:result] robust<win:0>: not robustly reachable
[sse:result] Path 4 reached address 0x0804812b (return_address) (0 to go)
[sse:result] Value input<16> : 0xdead
[sse:result] Value input2<16> : 0xc0de
To measure the quantitative robustness of the winning state, we need to add the quant keyword to the objective:
robust <win> quant reach return_address such that al <> 0 then print input and print input2
The results tell us that it is quite low:
$ binsec -sse -sse-script crackme.ini -rse magic
[rse:result] robust<win:0>[quant]: reached
[rse:result] robust<win:0>[quant]: 1.53e-05, input: 0b1101111010101101
[rse:result] ALL DONE
[sse:result] Path 4 reached address 0x0804812b (return_address) (0 to go)
[sse:result] Value input<16> : 0xdead
[sse:result] Value input2<16> : 0xc0de
However we are only considering single execution paths. To check if the winning condition is robustly reachable over multiple paths, we need to use path merging, with the merge keyword:
robust <win> merge quant reach return_address such that al <> 0 then print input and print input2
But here it is not the case:
$ binsec -sse -sse-script crackme.ini -rse magic
[rse:result] robust<win:0>[merge, quant]: reached
[rse:result] robust<win:0>[merge, quant]: 1.53e-05, input: 0b1101111010101101
[rse:result] ALL DONE
[sse:result] Path 4 reached address 0x0804812b (return_address) (0 to go)
[sse:result] Value input<16> : 0xdead
[sse:result] Value input2<16> : 0xc0de
On the other hand, if we check for any exit point of the function:
robust <win> merge reach * return_address
We see that eventually all possible paths are exhausted and we have robust reachability:
$ binsec -sse -sse-script crackme.ini -rse magic
[rse:result] robust<win:0>[merge, quant]: reached
[rse:result] robust<win:0>[merge, quant]: 0.5, input: 0bXXXXXXXXXXXXXXX0
[sse:result] Path 3 reached address 0x0804812b (return_address) (* to go)
[rse:result] robust<win:0>[merge, quant]: reached
[rse:result] robust<win:0>[merge, quant]: 0.5, input: 0bXXXXXXXXXXXXXX01
[sse:result] Path 4 reached address 0x0804812b (return_address) (* to go)
...
[rse:result] robust<win:0>[merge, quant]: reached
[rse:result] robust<win:0>[merge, quant]: 0.5, input: 0b1110000111010101
[sse:result] Path 2 reached address 0x0804812b (return_address) (* to go)
[rse:result] robust<win:0>[merge, quant]: reached
[rse:result] robust<win:0>[merge, quant]: robustly reachable
[rse:result] ALL DONE
[sse:result] Path 1 reached address 0x0804812b (return_address) (* to go)
[sse:info] Empty path worklist: halting ...
We can also set an acceptance threshold for quantitative robustness:
robust <win> merge quant threshold 0.2 reach * return_address
$ binsec -sse -sse-script crackme.ini -rse magic
[rse:result] robust<win:0>[merge, quant > 0.2]: reached
[rse:result] robust<win:0>[merge, quant > 0.2]: 0.5, input: 0bXXXXXXXXXXXXXXX0
[rse:result] robust<win:0>[merge, quant > 0.2]: OK
[rse:result] ALL DONE
Links
You can check out the plugin source on GitHub, but also take a look at the two papers it is based on (Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference and Quantitative Robustness for Vulnerability Assessment).