Hello, I try to run elational symbolic execution of constant time check with binsec. I hope to get the same or similiar result with binsec/rel at the benchmark set https://github.com/binsec/rel_bench.
First I install binsec/rel and run the tests in rel_bench, it works well. (By the way, binsec works well with the examples in toturial) For example, I run test the benchmark donna (https://github.com/binsec/rel_bench/tree/main/src/donna) with the command line option:
binsec -relse -fml-solver-timeout 0 -relse-timeout 3600 -relse-debug-level 0 -sse-depth 0 -sse-memory src/donna/memory.txt -relse-paths 0 -sse-load-ro-sections -sse-load-sections .got.plt,.data,.plt -relse-stat-prefix donna_O0 -relse-stat-file ./__results__/donna_2023-10-07.csv -fml-solver boolector -relse-store-type rel -relse-memory-type row-map -relse-property ct -relse-dedup 1 -relse-fp block -relse-leak-info instr -relse-print-model ./src/donna/donna_O0
To test the binary donna_O0
and it takes about15 minutes and get the result that it is secure.
I fail to get the similar result with binsec.
I verify the same binary file donna_O0
with the command line
binsec -sse -checkct donna_O0 -sse-script checkct3.cfg -fml-solver-timeout 0 -sse-timeout 3600 -sse-depth 4611686018427387903 -checkct-stats-file ./2.csv -smt-solver boolector -checkct-leak-info instr
and the cfg file checkct3.cfg
is:
starting from <main>
# Setting memset function to __memset_ia32
@[0x080EF034, 4] := 0x08060EF0
ebp<32>:=0xffffcc28
esp<32>:=0xffffcbc0
load sections .text, .rodata, .data, .got.plt, .plt from file
explore all
It won't stop in 1 hours and get no results.
I try to add secret and public input information in the above .cfg file with
secret secret
public basepoint, mypublic
however it reports
Fatal error: exception Parse error at word `secret
' (line 13, column 7 in checkct3.cfg)
"secret secret"
So I modify the donna_wrapper.c file, which only changing input variables from local to global.
#include "../../__libsym__/sym.h"
#include "donna.c"
u8 mypublic[32]; // declassified in output
u8 secret[32]; // secret
u8 basepoint[32]; // public
int main() {
// u8 mypublic[32]; // declassified in output
// u8 secret[32]; // secret
// u8 basepoint[32]; // public
high_input_32(mypublic);
high_input_32(secret);
low_input_32(basepoint);
return curve25519_donna(mypublic,secret,basepoint);
}
I complie and get the new binary file donna_global
(use the same compile command with donna_O0). Test it with the command
binsec -sse -checkct donna_global -sse-script checkct5.cfg -fml-solver-timeout 0 -sse-timeout 3600 -sse-depth 4611686018427387903 -checkct-stats-file ./2.csv -smt-solver boolector -checkct-leak-info instr
and the cfg file checkct5.cfg
starting from <main>
# Setting memset function to __memset_ia32
@[0x080EF034, 4] := 0x08060EF0
secret global secret
public global basepoint, mypublic
ebp<32>:=0xffffcc28
esp<32>:=0xffffcbc0
load sections .text, .rodata, .data, .got.plt, .plt from file
explore all
This time it will report find several leakage:
[sse:info] Load section .plt (0x08049030, 0xe0)
[sse:info] Load section .got.plt (0x080ec000, 0x44)
[sse:info] Load section .data (0x080ec060, 0xec0)
[sse:info] Load section .rodata (0x080ba000, 0x1b3ac)
[sse:info] Load section .text (0x08049110, 0x6f7b1)
[checkct:result] Instruction 0x0807437d has control flow leak (0.162s)
[checkct:result] Instruction 0x08074384 has control flow leak (0.435s)
[sse:warning] Cut path 4 (non executable) @ 0x00000000
[sse:warning] Cut path 3 (non executable) @ 0xffffffff
[sse:warning] Cut path 2 (non executable) @ 0xfeffffff
[checkct:result] Instruction 0x08095e27 has control flow leak (1.082s)
[checkct:result] Instruction 0x08095e2d has memory access leak (1.733s)
[checkct:result] Instruction 0x08095e41 has control flow leak (3.378s)
[checkct:result] Instruction 0x08095e46 has control flow leak (4.845s)
[checkct:result] Instruction 0x080743bc has control flow leak (6.911s)
[sse:warning] Cut path 12 (non executable) @ 0x00000000
[sse:warning] Cut path 11 (non executable) @ 0x80808080
[sse:warning] Cut path 10 (non executable) @ 0xffffffff
[sse:warning] Cut path 9 (non executable) @ 0x0a0743ad
[sse:warning] Cut path 14 (non executable) @ 0x00000000
[sse:warning] Cut path 13 (non executable) @ 0x00000001
[sse:warning] Cut path 8 (non executable) @ 0x00000101
[checkct:result] Instruction 0x08095e65 has memory access leak (10.176s)
[sse:warning] Cut path 7 (non executable) @ 0x00000000
[sse:warning] Cut path 16 (non executable) @ 0x00000000
[sse:warning] Cut path 15 (non executable) @ 0xffffffff
[sse:warning] Cut path 6 (non executable) @ 0xfeffffff
[sse:warning] Cut path 21 (non executable) @ 0x00000000
[sse:warning] Cut path 20 (non executable) @ 0xffffffff
[sse:warning] Cut path 19 (non executable) @ 0xfeffffff
[sse:warning] Cut path 18 (non executable) @ 0x0a0743ad
[sse:warning] Cut path 23 (non executable) @ 0x00000000
[sse:warning] Cut path 22 (non executable) @ 0x00000001
[sse:warning] Cut path 17 (non executable) @ 0x00000101
[sse:warning] Cut path 5 (non executable) @ 0x00000000
[sse:warning] Cut path 25 (non executable) @ 0x00000000
[sse:warning] Cut path 24 (non executable) @ 0xffffffff
[sse:warning] Cut path 1 (non executable) @ 0xfeffffff
[sse:info] Empty path worklist: halting ...
[sse:info] SMT queries
Preprocessing simplifications
total 52
sat 1
unsat 37
constant enum 14
Satisfiability queries
total 34
sat 32
unsat 2
unknown 0
time 15.21
average 0.45
Exploration
total paths 25
completed/cut paths 0
pending paths 0
stale paths 25
failed assertions 0
branching points 24
max path depth 88
visited instructions (unrolled) 143
visited instructions (static) 84
[checkct:result] Program status is : insecure (15.266)
[checkct:info] 0 visited path covering 84 instructions
[checkct:info] 6 / 12 control flow checks pass
[checkct:info] 73 / 75 memory access checks pass
I am uncertain that:
Do I use the binsec correctly? (i.e., with the correct command line options)
I read from toturial that it does not matter what the exact value of the esp (also ebp) is. But I find that the donna_O3's address of __memset_ia32 is different from donna_O0, but binsec/rel test it with the same memory.txt which means the same setting
# Setting memset function to __memset_ia32
@[0x080EF034, 4] := 0x08060EF0;
Does it means what the exact value of the __memset_ia32
is trivial, too?
How to set the public and secret input in the cfg file if the public and secret variables are not global?