Now I can't get ida pro 6.9 for linux, because it's too old. So I want to know the tools just support the version?

Hello,

While analysing a binary with the checkct plugin, several control flow leaks are reported on adcs rn, rm instructions, which does not seem to make sense?

I was not able to reproduce the issue as-is on a simple test-case, but the following binary

Disassembly of section .text:

000200e4 <_start>:
   200e4:	b580      	push	{r7, lr}
   200e6:	6802      	ldr	r2, [r0, #0]
   200e8:	680b      	ldr	r3, [r1, #0]
   200ea:	415a      	adcs	r2, r3
   200ec:	bd80      	pop	{r7, pc}
   200ee:	defe      	udf	#254	; 0xfe

leads to the following analysis result (with @[r0, 4] := secret)

[sse:info] Empty path worklist: halting ...
[sse:info] SMT queries
             Preprocessing simplifications
               total          4
               sat            0
               unsat          2
               constant enum  2
             
             Satisfiability queries
               total          1
               sat            1
               unsat          0
               unknown        0
               time           0.00
               average        0.00
             
           Exploration
             total paths                      2
             completed/cut paths              2
             pending paths                    0
             stale paths                      0
             failed assertions                0
             branching points                 3
             max path depth                   5
             visited instructions (unrolled)  6
             visited instructions (static)    5
             
           
[checkct:result] Program status is : secure (0.024)
[checkct:info] 2 visited paths covering 5 instructions
[checkct:info] 3 / 3 control flow checks pass
[checkct:info] 9 / 9 memory access checks pass

whereas the same program with adcs r2, r3 replaced by adc r2, r3 leads to

[sse:info] Empty path worklist: halting ...
[sse:info] SMT queries
             Preprocessing simplifications
               total          2
               sat            0
               unsat          1
               constant enum  1
             
             Satisfiability queries
               total          0
               sat            0
               unsat          0
               unknown        0
               time           0.00
               average        nan
             
           Exploration
             total paths                      1
             completed/cut paths              1
             pending paths                    0
             stale paths                      0
             failed assertions                0
             branching points                 1
             max path depth                   5
             visited instructions (unrolled)  5
             visited instructions (static)    5
             
           
[checkct:result] Program status is : secure (0.022)
[checkct:info] 1 visited path covering 5 instructions
[checkct:info] 1 / 1 control flow checks pass
[checkct:info] 7 / 7 memory access checks pass

which differ in the number queries and paths, which is not what I would have expected, although I may be missing something.

Hi,

I tried the example pointer_arith inside the docker image. I don't understand the result binsec gives me. As a reminder, here is the assembly code of the main function we want to analyse:

08048e24 <main>:
 8048e24:       55                      push   ebp
 8048e25:       89 e5                   mov    ebp,esp
 8048e27:       83 ec 20                sub    esp,0x20
 8048e2a:       c7 45 f0 01 00 00 00    mov    DWORD PTR [ebp-0x10],0x1
 8048e31:       c7 45 f4 02 00 00 00    mov    DWORD PTR [ebp-0xc],0x2
 8048e38:       c7 45 f8 03 00 00 00    mov    DWORD PTR [ebp-0x8],0x3
 8048e3f:       c7 45 fc 04 00 00 00    mov    DWORD PTR [ebp-0x4],0x4
 8048e46:       8d 45 f0                lea    eax,[ebp-0x10]
 8048e49:       8d 55 f8                lea    edx,[ebp-0x8]
 8048e4c:       83 c2 04                add    edx,0x4
 8048e4f:       01 c2                   add    edx,eax
 8048e51:       8d 45 f8                lea    eax,[ebp-0x8]
 8048e54:       29 c2                   sub    edx,eax
 8048e56:       89 d0                   mov    eax,edx
 8048e58:       89 45 ec                mov    DWORD PTR [ebp-0x14],eax
 8048e5b:       8b 45 ec                mov    eax,DWORD PTR [ebp-0x14]
 8048e5e:       c9                      leave  
 8048e5f:       c3                      ret 

As written in the config/default file we start at address 0x08048e24(main+0x0) and end at address 0x8048e5e (leave instruction):

[kernel]
isa = x86
entrypoint = 0x08048e24
file = exe/default

[sim2]
enabled = true
init = mem/default
goals = \
      0x8048e5e enumerate eax<32>; \
      0x08048e5e cut

We set memory as:

ebp<32> := 0x8BADF00D;
esp<32> := 0x0000003A;

According to me, at the leave instruction, eax is supposed to equal esp-0xc (the esp value we write in mem/default). As such it should return 46 but it returns 42.

Thanks

Hi,

I try to analyze the fauxware binary using Binsec from the core dump. To do so I launch the following commands:

$ path/to/make_coredump.sh fauxware.core fauxware
$ binsec -sse -sse-script binsec.config fauxware.core

Some time running these two commands works well. Some time, I get the following output:

[smt:info] Found Z3 in the path.
[sse:info] TTY: press [space] to switch between log and monitor modes.
[sse:info] SMT querieseached address 0x00400692 (0 to go)
             Preprocessing simplificationsY"
               total          305
               sat            46
               unsat          125
               constant enum  134
             
             Satisfiability queries
               total          160
               sat            95
               unsat          65
               unknown        0
               time           3.96
               average        0.02
             
           Exploration
             total paths                      84
             completed/cut paths              72
             pending paths                    12
             stale paths                      0
             failed assertions                0
             branching points                 440
             max path depth                   76
             visited instructions (unrolled)  1140
             visited instructions (static)    72
             

(the fauxware and the binsec.config files are available here )

Hi, it seems like the latest version doesn't compile.

dune build @install
      menhir src/smtlib/smtlib_parser.{ml,mli}
Warning: one state has shift/reduce conflicts.
Warning: 9 shift/reduce conflicts were arbitrarily resolved.
      menhir src/parser/dbacsl_parser.{ml,mli}
Warning: 7 states have shift/reduce conflicts.
Warning: 94 shift/reduce conflicts were arbitrarily resolved.
      menhir src/parser/parser.{ml,mli}
Warning: 4 states have shift/reduce conflicts.
Warning: 4 shift/reduce conflicts were arbitrarily resolved.
File "src/parser/parser.ml", line 1583, characters 22-24:
1583 |   | MenhirBox_dba of ('a Dba_types.program) [@@unboxed]
                             ^^
Error: The type variable 'a is unbound in this type declaration. 
make: *** [Makefile:77: binsec] Error 1

The same error happens with versions c5e8cdc, b747414 and ff550b0.

To reproduce, create a Dockerfile:

FROM archlinux:latest

RUN yes | pacman -Syuu
RUN yes | pacman -Syuu --needed git make opam dune which rsync gcc patch diffutils

RUN opam init --yes --disable-sandboxing
RUN opam install --yes ocamlgraph zarith menhir dune-site

RUN git clone https://github.com/binsec/binsec.git
RUN cd binsec && eval $(opam env) && make -j8 install

then run docker build . in the directory where you created the Dockerfile.

Hello,

I have encountered an issue where the checkct plugin reports a leak, but when examining the output of -checkct-stats-file, the secret1 and secret2 values are the exact same.

I was unfortunately not able to sufficiently reduce the test case so as to be able to share it, but the output of -checkct-stats-file looks like this:

["CT report"."Insecurity models".0x[redacted].public]
"%entropy%8" = ["0x82", "0xae", "0x63", "0x3a", "0xe4", "0x56", "0x0d", "0x0d", "0x48", "0x5c", "0x07", "0x80", "0xff", "0x8d", "0x62", "0x10", "0xae", "0x10", "0x8c", "0xad", "0x04", "0x74", "0x38", "0x51", "0xdc", "0x26", "0x3c", "0xc0", "0x1c", "0x44", "0x06", "0xf3"]
fp = ["0x0fcb746f"]
r1 = ["0x0000002b"]
r3 = ["0x2b87fd18"]
r4 = ["0x0c86df4e"]
r5 = ["0x2169ca1a"]
r6 = ["0x08020e9a"]
r7 = ["0x03ced407"]
r8 = ["0x187e8e64"]
sl = ["0x2e1ab22a"]
["CT report"."Insecurity models".0x[redacted].secret1]
"%secret%64" = ["0x0000000035e70847"]
["CT report"."Insecurity models".0x[redacted].secret2]
"%secret%64" = ["0x0000000035e70847"]

Additionally, r1 has been assume-d to be between 0x28 and 0x2c.

The infringing instruction is a bne immediately following a cmp r3, r2, and must in fact be constant-time, because the formulas for r2 and r3 at that location do not make use of any secret, which I have verified with a reach * [inst] then print formula for r2 as r2 and print formula for r3 as r3 (I am not sure, however, how to determine exactly which of those reach statements the failing insecurity query corresponds to).

Do you know what could be causing this?

Hello, I am trying to analyse the examples from the tutorial at 'doc/sse/relse.md' compiled for Arm, but I am hitting an error :

~$ arm-none-eabi-gcc -static -mthumb test_harness.c candidate_1.c -o candidate_1_arm
~$ binsec -sse -checkct -sse-script checkct.cfg candidate_1_arm -arm-supported-modes thumb
[checkct:result] Instruction 0x00008250 has control flow leak (0.070s)
[checkct:result] Instruction 0x00008224 has control flow leak (0.079s)
Fatal error: exception Not_found

Should I be doing something differently, or is this a bug ?

This is the 'test_harness.c' I am using (slightly modified from the tutorial) :

#include <stddef.h>

void exit(int res) {
	for(;;) {}
}

int memcmp(const void *s1, const void *s2, size_t n); /* function under analysis */

#define SIZE (1 << 4) /* 16B */
char s1[SIZE];   /* secret buffer */
char s2[SIZE];   /* public buffer */
size_t n = SIZE; /* public variable */

int main(int argc, char *argv[])
{
	int res = memcmp(s1, s2, n);
	
	/* ensure the result is in [-1..1] */
	res |= res >> 1;
	res |= res >> 2;
	res |= res >> 4;
	res |= res >> 8;
	res |= res >> 16;
	res = (res & 1) | (res >> 31);
	
	exit(res); /* identify halting point and prevent compiler optimizations */
}

Hi, I'm recently learning to use Binsc BB-DSE to detect opaque predicates, after setting up the relevant environment, I run the given example echo normally, but I use binsec to detect the examples of opaque predicates we created, but it doesn't seem to work when building control flow graphs, the run results are as follows：

INFO ANALYZING changes made by post scripts: /home/dqp/Desktop/demo (HeadlessAnalyzer)
INFO REPORT: Post-analysis succeeded for file: /home/dqp/Desktop/demo (HeadlessAnalyzer)
INFO REPORT: Save succeeded for file: /demo (HeadlessAnalyzer)
[ghidra:result] Fatal error: exception Not_found

We can run BINSEC BBSSE with default option. The following error occurs.

Done: 93% (1326/1416, 90 left) (jobs: 0)[bbsse:fatal] Can not find a conditional jump at 0x004003ee.
Fatal error: exception Failure("abort")

I think the reason for the failure is due to a flaw in the construction of the control flow diagram.I am not very good at using Ghidra, so I hope to get your help!

Here is the source code of a simple C program that we built via gcc. We tried several C programs and all had similar problems with the control flow graph.

#include <stdio.h>
#include <stdlib.h>

// Calculates the nth fibonacci number
int fib(int n) {
	int i, c, d;
	int a = 1;
	int b = 1;

	for (i = 0; i < n; ++i) {
		if (7*b*b - 1 != a*a) { // Opaquely true
			c = a;
			a = a + b;
			b = c;
		} else {
			b = a - c; // BOGUS
			c = i + a;
			a = b;
		}
	}

	return a;
}

// Calculates n!
int fac(int n) {
	int res = 1;
	int i;

	if (n < 0) {
		return 0;
	}

	for (; n > 1; --n) {
		if (7*res*res - 1 != n*n) { // Opaquely true
			res *= n;
		} else {
			n *= res; // BOGUS
		}
	}

	return res;
}

int main(int argc, char *argv[]) {
	int input = atoi(argv[1]);
	int choice = atoi(argv[2]);
	int res;

	if (choice == 1)
		res = fib(input);
	else
		res = fac(input);

	printf("res: %d\n", res);
}

As shown in the title.

Hello,

I encountered the following error while using the checkct plugin to analyse an arm (thumb) binary

binsec -sse -checkct -sse-script checkct.cfg -arm-supported-modes thumb target
[...]
[sse:error] Cut path 3 (uninterpreted "smlabb\tr1, r1, r4, r2") @ 0x00023f60
[...]

I suppose this is a limitation of unisim_archisec, but perhaps you know if and how support for this instruction could be added/enabled?

Hi, I'm very intersted in BB-DSE and binary deobfuscation, so trying to run BINSEC in a stand-alone backward analyzer mode for opaque predicate detection. However, I'm not an ocaml expert, it is not trivial to me, so asking for a help. (* This issue is not related to any contribution; if not approapriate, I will delete this issue right away. *)

(1) Although x86 disasm option with a little HelloWorld example works quite well in my computer, "-bw -bw-opaque" option makes it stop in the middle, always. (From the code, I'd like to guess the control flow graph is not built well, but I'm not sure.) Should I try with different command-line options?

(2) It might be very fundamental question but, is there any method to debug or trace the analysis process? (I tried to attach additional Loggers or to opt out expressions, but it made me tired and confused, mostly due to the complicated behaviors of channels the loggers use. I guess there exist more efficient ways.) Any references would be appreciated.

(3) Beside src/backward/*, I found another opaque predicate related code exists on src/dynamic/dse/examples/. Could you please let me know the differences? (Is the latter the one I'm looking for?, that is, a stand alone opaque predicate detector?)

Thank you so much in advance,

-fcmonoid-

The https://hub.docker.com/u/binsec images are not up-to-date (according to GitHub, the latest release is 0.4.1).

Hello,
I'm trying to use the Abstract Interpretation module of binsec however, it fails to run in the Docker provided.

Steps to reproduce

1. docker pull binsec/binsec-0.3:v1
2. docker run -it --rm binsec/binsec-0.3:v1 /bin/bash

binsec@ee0992dd8dd3:~$ binsec -file examples/memcpy/exe/default -ai
Fatal error: exception Failure("Parse error /usr/local/share/binsec/arch/x86.dba (line 2, column 8) at w: word_size")

Thanks a lot for your help

Hello,

I am using the checkct plugin to analyse an arm binary, that contains the following snippets:

[...]
   317b0: 0d f5 13 7d   add.w   sp, sp, #588
   317b4: bd e8 00 0f   pop.w   {r8, r9, r10, r11}
   317b8: f0 bd         pop     {r4, r5, r6, r7, pc}
[...]
   369da: 41 77         strb    r1, [r0, #29]
   369dc: 03 b0         add     sp, #12
   369de: bd e8 00 0f   pop.w   {r8, r9, r10, r11}
   369e2: f0 bd         pop     {r4, r5, r6, r7, pc}
[...]

Now when using the following script:

load sections .text from file
starting from <fn_to_analyze>
with concrete stack pointer
lr := 0x8badf00d ^ 1
reach 0x369e2 then print @[sp + 16,4]
reach * 0x317b0
reach * 0x317b1
reach * 0x317b4
halt at 0x8badf00d ^ 1
explore all

the analysis returns

[sse:info] Load section .text (0x00030b00, 0x4225a)
[sse:result] Path 238 reached address 0x000369e2 (0 to go)
[sse:result] Value @[(sp<32> + 16<32>),4] : 0x000317b1

and then keeps running without printing anything else, until it gets killed by the kernel.
So it seems that address 0x317b0/1 is never reached, which is weird.

What's more if I interrupt the process before it gets killed, the output is always exactly the same (apart from the time, that is):

^C[sse:info] SMT queries
             Preprocessing simplifications
               total          747958
               sat            550
               unsat          743046
               constant enum  4362
             
             Satisfiability queries
               total          506
               sat            237
               unsat          269
               unknown        0
               time           25.51
               average        0.05
             
           Exploration
             total paths                      238
             completed/cut paths              0
             pending paths                    238
             stale paths                      0
             failed assertions                0
             branching points                 5699
             max path depth                   1489483
             visited instructions (unrolled)  1489483
             visited instructions (static)    3526
             
           
[checkct:result] Program status is : unknown (30.945)
[checkct:info] 0 visited path covering 3526 instructions
[checkct:info] 5699 / 5699 control flow checks pass
[checkct:info] 737702 / 737702 memory access checks pass
[checkct:warning] Exploration is incomplete:
                  - timeout has left (at least) 238 pending paths (-sse-timeout)

Do you have an idea as to what could be happening?

Hi,

Would you consider porting the source code from OCaml to F#?

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?

Hello, I am hitting an error while trying to analyse an arm32 function with the checkct plugin.

Here's a reduced test case binary

Disassembly of section .text:

000200e4 <_start>:
   200e4: 80 ea 00 00   eor.w   r0, r0, r0
   200e8: 03 fa 0c fc   lsl.w   r12, r3, r12
   200ec: 83 ea 03 03   eor.w   r3, r3, r3
   200f0: fe de         trap

which, when analysed with the following script

starting from <_start>
with concrete stack pointer
lr := 0x8badf00d ^ 1
halt at 0x8badf00d ^ 1
explore all

yields

binsec -sse -checkct -sse-script checkct.cfg -arm-supported-modes thumb target
[sse:info] TTY: press [space] to switch between log and monitor modes.
[sse:error] Cut path 1 (uninterpreted "lsl.w\tip, r3, ip") @ 0x000200e8
[sse:info] Empty path worklist: halting ...
[sse:info] SMT queries
[...]
[checkct:result] Program status is : unknown (0.023)
[checkct:info] 0 visited path covering 2 instructions
[checkct:info] 0 / 0 control flow checks pass
[checkct:info] 0 / 0 memory access checks pass
[checkct:warning] Exploration is incomplete:

I am guessing this is an issue in unisim_archisec?

Hello, I have a large object file with several functions that I am setting up constant-time verification for, using the relse engine.

I would like to avoid re-disassembling the same binary for every function that I analyse.

I am using one script per function, but perhaps there is a way to run multiple analyses in a single script, or somehow cache the disassembly result ?

Hello developers I am using binsec to Automatically find opaque predicates but I get the following error

dqp@ubuntu:~/binsec$ binsec -ghidra-cache ghidra.log -bbsse-process-all-jumps echo
[smt:fatal] No SMT solver found.
Fatal error: exception Failure("abort")

But I checked to see if ocaml-bitwuzla was already installed

dqp@ubuntu:~/binsec$ opam list

Packages matching: installed

Name # Installed # Synopsis

astring 0.8.5 Alternative String module for OCaml
base v0.14.3 Full standard library replacement for OCaml
base-bigarray base
base-bytes base Bytes library distributed with the OCaml compiler
base-threads base
base-unix base
bitwuzla 1.0.3 SMT solver for AUFBVFP
bitwuzla-c 1.0.3 SMT solver for AUFBVFP (C API)
camlp-streams 5.0.1 The Stream and Genlex libraries for use with Camlp4 and Camlp5
cmdliner 1.1.1 Declarative definition of command line interfaces for OCaml
conf-emacs 1 Virtual package to install the Emacs editor
conf-g++ 1.0 Virtual package relying on the g++ compiler (for C++)
conf-gcc 1.0 Virtual package relying on the gcc compiler (for C)
conf-git 1.1 Virtual package relying on git
conf-gmp 4 Virtual package relying on a GMP lib system installation
conf-ncurses 1 Virtual package relying on ncurses
conf-pkg-config 2 Check if pkg-config is installed and create an opam switch local pkgconfig folder
cppo 1.6.9 Code preprocessor like cpp for OCaml
csexp 1.5.1 Parsing and printing of S-expressions in Canonical form
curses 1.0.10 Bindings to ncurses
dot-merlin-reader 4.5 Reads config files for merlin
dune 3.5.0 Fast, portable, and opinionated build system
dune-build-info 3.5.0 Embed build informations inside executable
dune-configurator 3.5.0 Helper library for gathering system configuration
dune-private-libs 3.5.0 Private libraries of Dune
dune-site 3.5.0 Embed locations informations inside executable and libraries
dyn 3.5.0 Dynamic type
either 1.0.0 Compatibility Either module
fix 20220121 Algorithmic building blocks for memoization, recursion, and more
fmt 0.9.0 OCaml Format pretty-printer combinators
fpath 0.7.3 File system paths for OCaml
ISO8601 0.2.6 ISO 8601 and RFC 3999 date parsing for OCaml
menhir 20211128 An LR(1) parser generator
menhirLib 20211128 Runtime support library for parsers generated by Menhir
menhirSdk 20211128 Compile-time library for auxiliary tools related to Menhir
merlin 3.8.0 Editor helper, provides completion, typing and source browsing in Vim and Emacs
ocaml 4.09.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.1 Official release 4.09.1
ocaml-config 1 OCaml Switch Configuration
ocaml-version 3.5.0 Manipulate, parse and generate OCaml compiler version strings
ocamlbuild 0.14.2 OCamlbuild is a build system with builtin rules to easily build most OCaml projects
ocamlfind 1.9.5 A library manager for OCaml
ocamlformat 0.23.0 Auto-formatter for OCaml code
ocamlgraph 2.0.0 A generic graph library for OCaml
ocp-indent 1.8.1 A simple tool to indent OCaml programs
odoc 2.1.1 OCaml documentation generator
odoc-parser 1.0.1 Parser for ocaml documentation comments
ordering 3.5.0 Element ordering
ounit2 2.2.6 OUnit testing framework
pp 1.1.2 Pretty-printing library
qcheck 0.20 Compatibility package for qcheck
qcheck-core 0.20 Core qcheck library
qcheck-ounit 0.20 OUnit backend for qcheck
re 1.10.4 RE is a regular expression library for OCaml
result 1.5 Compatibility Result module
seq base Compatibility package for OCaml's standard iterator type starting from 4.07.
sexplib0 v0.14.0 Library containing the definition of S-expressions and some base converters
stdio v0.14.0 Standard IO library for OCaml
stdlib-shims 0.3.0 Backport some of the new stdlib features to older compiler
stdune 3.5.0 Dune's unstable standard library
toml 7.0.0 Library for TOML with a parser, a serializer and a printer
topkg 1.0.6 The transitory OCaml software packager
tuareg 3.0.1 OCaml mode for GNU Emacs
tyxml 4.5.0 A library for building correct HTML and SVG documents
unisim_archisec 0.0.3 UNISIM-VP DBA decoder
user-setup 0.7 Helper for the configuration of editors for the use of OCaml tools
uucp 15.0.0 Unicode character properties for OCaml
uuseg 15.0.0 Unicode text segmentation for OCaml
uutf 1.0.3 Non-blocking streaming Unicode codec for OCaml
yojson 2.0.2 Yojson is an optimized parsing and printing library for the JSON format
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers

I don't know what the problem is, I hope I can get your help！！

Hi,
Much appreciated to your awesome project. Is binsec_v0.2 compatibale with IDASEC ? More simple guide will be greatly helpfull.

Hi, I try to test binsec with example in tutorial 4 https://github.com/binsec/binsec/blob/master/doc/sse/relse.md.
I run the command followed by the tutorial:
gcc -g -m32 -static test_harness.c candidate_1.c -o candidate_1
binsec -sse -checkct -sse-script checkct.cfg candidate_1
The result is

[smt:info] Found Bitwuzla in the path.
[sse:info] Empty path worklist: halting ...
Fatal error: exception Libsse.Exec.Halt

The binsec can correctly print the command line information with command binsec --help
I try to build binsec in my computer several time (as well as binsec/rel), could this be the source of the problem?

By the way, is binsec able to run the -checkct with 64 bit programs?

I noticed you have a plugin for IDA, but it is not the only one tool available.
Radare2 is a highly-portable cross-platform reverse engineering framework and a toolkit without dependencies. It has support for analyzing binaries, disassembling code, debugging programs, attaching to remote GDB/LLDB, WinDbg servers, rich plugin system (see r2pm), and integration with various decompilers. For example, ghidra decompiler plugin - r2ghidra-dec. It is actively developed and can be easily integrated in various open source and commercial products. I believe, it will be highly beneficial to support these and provide a package for install from r2pm, see the package repository here: https://github.com/radareorg/radare2-pm

In case if you need to get the information from radare2 into the OCaml you can use the so called r2pipe mechanism that returns JSON-formed output for the radare2 commands. We maintain a r2pipe opam package. Feel free to reach me if you have the question or suggestions for this r2pipe interface (or radare2 in general).

For documentation on writing plugins for radare2 see Scripting and Plugins Radare2 Book chapters.

Cutter is a crossplatform Qt/C++ GUI frontend to radare2:

For documentation on writing plugins for Cutter see the official tutorial and the curated list of various popular plugins.

As the titile.
And is their other limited option need to be set as infinited If I want to get the example be proved constant time?

Hi,

I wrote a simple code to test sim2 module based on the examples given in the docker. Unlike when using sse, sim2 doesn't accept function name as entrypoint.

$ unzip testSim.zip
$ cd testSim
$ binsec -config ./config/default.ini 
Fatal error: exception Failure("Bitvector.of_string : should start with [+-]?0[xb]")

Here is the zip file: testSim.zip

If I replace foo by its address 0x560 it works well.

Thanks

I complie a example with a compiler compcert and verified it with checkct.
The result is that it is secure but is much more faster than the gcc compiled version.
I find that it might becasue the cut path show in the result.
What does cut path mean?

[sse:warning] Cut path 3 (non executable) @ 0x00000000
[sse:warning] Cut path 2 (non executable) @ 0xffffffffffffffff
[sse:warning] Cut path 1 (non executable) @ 0xfffffffffffffffe
[sse:info] Empty path worklist: halting ...
[sse:info] SMT queries
             Preprocessing simplifications
               total          68
               sat            31
               unsat          36
               constant enum  1

             Satisfiability queries
               total          2
               sat            2
               unsat          0
               unknown        0
               time           0.00
               average        0.00

           Exploration
             total paths                      3
             completed/cut paths              0
             pending paths                    0
             stale paths                      3
             failed assertions                0
             branching points                 33
             max path depth                   737
             visited instructions (unrolled)  737
             visited instructions (static)    520


[checkct:result] Program status is : secure (0.132)
[checkct:info] 0 visited path covering 520 instructions
[checkct:info] 33 / 33 control flow checks pass
[checkct:info] 283 / 283 memory access checks pass

@rbonichon @strongcourage

i have already installed ocamlfind but its giving me error please provide me the steps to install

arun@arun:/binsec-master$ opam install ocamlfind
[NOTE] Package ocamlfind is already installed (current version is 1.8.0).
arun@arun:/binsec-master$ ./configure
checking for make... make
checking GNU make version... Good! (4.1)
checking for ocamlfind... no
configure: error: Could not find ocamlfind

Hello, I am hitting an error while trying to analyse a function that contains a 'udiv' instruction (in arm).

Here's the reduced test case

Disassembly of section .text:

000200e4 <_start>:
   200e4:       b580            push    {r7, lr}
   200e6:       466f            mov     r7, sp
   200e8:       f04f 0008       mov.w   r0, #8
   200ec:       f04f 0310       mov.w   r3, #16
   200f0:       fbb3 f0f0       udiv    r0, r3, r0
   200f4:       bd80            pop     {r7, pc}
   200f6:       defe            udf     #254    ; 0xfe

which, when analysed with the following script

load sections .text from file

starting from <_start>
with concrete stack pointer
lr := 0x8badf00d

halt at 0x8badf00d
explore all

yields

[sse:info] Load section .text (0x000200e4, 0x14)
[sse:error] Cut path 1 (uninterpreted "KO") @ 0x000200f0
[sse:info] Empty path worklist: halting ...
[sse:info] SMT queries
             [...]
[checkct:result] Program status is : unknown (0.033)
[checkct:info] 0 visited path covering 5 instructions
[checkct:info] 0 / 0 control flow checks pass
[checkct:info] 2 / 2 memory access checks pass
[checkct:warning] Exploration is incomplete:

How could I go about solving this ?

binsec >= 0.7 seems to fail when processing a trivial Aarch64 hello world:

0000000000000714 <main>:
     714: 52800020      mov     w0, #1
     718: d65f03c0      ret

Disassembly of section .fini:

The binary was compiled using this C source: int main() { return 1; }
(I am not attaching a binary program, any program seems to reproduce the issue)

Script repro.ini:

sp := 0x100000000

starting from 0x714

reach 0x2000

Command:

binsec -sse -sse-debug-level 1 -sse-script repro.ini -isa aarch64 -aarch64-debug-level 1 hello

Output:

[smt:info] Found Z3 in the path.
[sse:debug] Running SSE on hello
[sse:debug] Reading script from repro.ini
[aarch64:debug] Parsing (address . 0x0000000000000714)
(opcode . 0x52800020)
(size . 4)
(mnemonic . "mov        w0, #0x1")
(0x0000000000000714,0) x0<64> := 0x0000000000000001; goto 1
(0x0000000000000714,1) goto (0x0000000000000718,0)

[aarch64:debug] Parsing (address . 0x0000000000000718)
(opcode . 0x52800020)
(size . 4)
(mnemonic . "mov        w0, #0x1")
(0x0000000000000718,0) x0<64> := 0x0000000000000001; goto 1
(0x0000000000000718,1) goto (0x000000000000071c,0)

[aarch64:debug] Parsing (address . 0x000000000000071c)
(opcode . 0x52800020)
(size . 4)
(mnemonic . "mov        w0, #0x1")
(0x000000000000071c,0) x0<64> := 0x0000000000000001; goto 1
(0x000000000000071c,1) goto (0x0000000000000720,0)

<repeating endlessly the same instruction>

[aarch64:debug] Parsing (address . 0x0000000000001ffc)
(opcode . 0x52800020)
(size . 4)
(mnemonic . "mov        w0, #0x1")
(0x0000000000001ffc,0) x0<64> := 0x0000000000000001; goto 1
(0x0000000000001ffc,1) goto (0x0000000000002000,0)

[sse:warning] Cut path 0 (max depth) @ 0x00000714
[sse:info] Empty path worklist: halting ...
[sse:info] SMT queries
             Preprocessing simplifications
               total          0
               sat            0
               unsat          0
               constant enum  0
             
             Satisfiability queries
               total          0
               sat            0
               unsat          0
               unknown        0
               time           0.00
               average        -nan
             
           Exploration
             total paths                      1
             completed/cut paths              0
             pending paths                    1
             stale paths                      0
             failed assertions                0
             branching points                 0
             max path depth                   1595
             visited instructions (unrolled)  1595
             visited instructions (static)    1595

The version of unisim_archisec in the OPAM environment is 0.0.5

The problem happens with tags 0.7.1, 0.7.2, 0.7.3

With version 0.6.3 parsing is correct:

[aarch64:debug] Parsing (address . 0x0000000000000714)
(opcode . 0x52800020)
(size . 4)
(mnemonic . "mov        w0, #0x1")
(0x0000000000000714,0) x0<64> := 0x0000000000000001; goto 1
(0x0000000000000714,1) goto (0x0000000000000718,0)

[aarch64:debug] Parsing (address . 0x0000000000000718)
(opcode . 0xd65f03c0)
(size . 4)
(mnemonic . "ret")
(0x0000000000000718,0) %%0<64> := x30<64>; goto 1
(0x0000000000000718,1) goto (%%0<64>)

[sse:debug] Selecting path #2 (among 3)
[sse:warning] Jump (0x00000718, 1) : goto %%0<64> 
              could have led to invalid address 0x00000000; skipping
[sse:debug] Selecting path #1 (among 2)
[sse:warning] Jump (0x00000718, 1) : goto %%0<64> 
              could have led to invalid address 0x00000001; skipping
[sse:debug] Selecting path #0 (among 1)
[sse:warning] Jump (0x00000718, 1) : goto %%0<64> 
              could have led to invalid address 0x00000003; skipping
[sse:info] Empty path worklist: halting ...
...
             visited instructions (unrolled)  2
             visited instructions (static)    2

The which command used in the Makefile (https://github.com/binsec/binsec/blob/master/Makefile#L24) is not available by default on all distributions. When it isn't available, the Makefile crashes with the message "Please install opam.", even if opam is installed.

Please see https://unix.stackexchange.com/questions/85249/why-not-use-which-what-to-use-then.