Symbolic execution in a nutshell

In this chapter, we are going to learn how to configure the BINSEC symbolic execution engine to explore the different behaviors of small binary programs.

Previously on Fibonacci

Last chapter was introducing the basic reverse-engineering information we can read from the tiny ELF executable fibonacci . As a reminder, the following gives you an overview of the file content as read by BINSEC.

00000000000000100000002000000030000000400000005000000060000000700000008000000090000000a0000000b0000000c0000000d0000000e0000000f000000100000001100000012000000130000001400000015000000160000001700000018000000190000001a0000001b0000001c0000001d0000001e0000001f000000200000002100000022000000230000002400000025000000260000002700000028000000290000002a0000002b0000002c0000002d0000002e0000002f0000003000000031000000320000003300000034000000350000003600000037000000380

7f45 4c46 0201 0100 0000 0000 0000 0000 0200 3e00 0100 0000 e800 4000 0000 0000 4000 0000 0000 0000 1002 0000 0000 0000 0000 0000 4000 3800 0100 4000 0600 0500 0100 0000 0500 0000 7800 0000 0000 0000 7800 4000 0000 0000 7800 4000 0000 0000 c400 0000 0000 0000 c400 0000 0000 0000 0400 0000 0000 0000 31c0 4885 ff74 0fba 0100 0000 4892 4801 d048 ffcf 75f6 c390 31ff 0fb6 0685 c074 1c83 e830 0f88 8200 0000 3c09 777e 48ff c648 8d3c bf48 01ff 4801 c7eb ddc3 6690 6668 000a 4889 e666 5abb 0a00 0000 48ff ce31 d248 f7f3 80c2 3088 1648 85c0 75ee bf01 0000 0048 89e2 4829 f289 f80f 05c3 5f66 83ff 0275 1f48 89e7 488b 7708 e895 ffff ffe8 78ff ffff e8b3 ffff ff31 ffb8 3c00 0000 0f05 bf01 0000 0048 8d34 2529 0140 00ba 1300 0000 89f8 0f05 40b7 ffeb de55 7361 6765 3a20 6669 626f 6e61 6363 6920 4e0a 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0100 0000 0200 0100 9000 4000 0000 0000 2600 0000 0000 0000 0e00 0000 0200 0100 b800 4000 0000 0000 3000 0000 0000 0000 1a00 0000 1000 0100 e800 4000 0000 0000 0000 0000 0000 0000 2100 0000 1200 0100 7800 4000 0000 0000 1700 0000 0000 0000 0070 6172 7365 5f75 696e 7436 3400 6563 686f 5f75 696e 7436 3400 5f73 7461 7274 0066 6962 6f6e 6163 6369 0000 2e73 796d 7461 6200 2e73 7472 7461 6200 2e73 6873 7472 7461 6200 2e74 6578 7400 2e72 6f64 6174 6100 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 1b00 0000 0100 0000 0600 0000 0000 0000 7800 4000 0000 0000 7800 0000 0000 0000 b100 0000 0000 0000 0000 0000 0000 0000 0400 0000 0000 0000 0000 0000 0000 0000 2100 0000 0100 0000 0200 0000 0000 0000 2901 4000 0000 0000 2901 0000 0000 0000 1300 0000 0000 0000 0000 0000 0000 0000 0100 0000 0000 0000 0000 0000 0000 0000 0100 0000 0200 0000 0000 0000 0000 0000 0000 0000 0000 0000 4001 0000 0000 0000 7800 0000 0000 0000 0400 0000 0300 0000 0800 0000 0000 0000 1800 0000 0000 0000 0900 0000 0300 0000 0000 0000 0000 0000 0000 0000 0000 0000 b801 0000 0000 0000 2b00 0000 0000 0000 0000 0000 0000 0000 0100 0000 0000 0000 0000 0000 0000 0000 1100 0000 0300 0000 0000 0000 0000 0000 0000 0000 0000 0000 e301 0000 0000 0000 2900 0000 0000 0000 0000 0000 0000 0000 0100 0000 0000 0000 0000 0000 0000 0000

Legend
Headers Magic
Code Instructions
Read-Only Data Strings
Data Other Sections

Headers

ELF Header:
Class:               ELF64                        
Data:                2's complement, little endian
Type:                EXEC                         
Machine:             x86                        
Entry point address: 0x4000e8                     

Section Headers:
[Nr] Name      Type     Addr             Off    Size   ES Flg Lk Inf Al
[ 0]           NULL     0000000000000000 000000 000000 00      0   0  0
[ 1] .text     PROGBITS 0000000000400078 000078 0000b1 00  AX  0   0  4
[ 2] .rodata   PROGBITS 0000000000400129 000129 000013 00   A  0   0  1
[ 3] .symtab   SYMTAB   0000000000000000 000140 000078 18      4   3  8
[ 4] .strtab   STRTAB   0000000000000000 0001b8 00002b 00      0   0  1
[ 5] .shstrtab STRTAB   0000000000000000 0001e3 000029 00      0   0  1
Key to Flags:
W (write), A (alloc), X (execute), M (merge), S (strings), I (info),
L (link order), G (group), T (TLS), O (extra OS processing required)

Symbol table '.symtab' contains 5 entries:
Num:            Value Size Type   Bind   Section Name        
  0: 0000000000000000    0 NOTYPE LOCAL  UND                 
  1: 0000000000400090   38 FUNC   LOCAL  .text   parse_uint64
  2: 00000000004000b8   48 FUNC   LOCAL  .text   echo_uint64
  3: 00000000004000e8    0 NOTYPE GLOBAL .text   _start    
  4: 0000000000400078   23 FUNC   GLOBAL .text   fibonacci

Disassembly

Disassembly of section .text:
00400078 <fibonacci>:
  400078:
31 c0 
xor %eax,%eax
0: %%0<1> := undef;
1: rax<64> := 0<64>;
2: of<1> := 0<1>;
3: sf<1> := 0<1>;
4: zf<1> := -1<1>;
5: af<1> := %%0<1>;
6: pf<1> := -1<1>;
7: cf<1> := 0<1>;
8: goto (0x40007a, 0) 
  40007a:
48 85 ff 
test %rdi,%rdi
0: %%0<1> :=
 !
 ((((rdi<64>{0} ^ rdi<64>{4}) ^ (rdi<64>{2} ^ rdi<64>{6})) ^
   ((rdi<64>{1} ^ rdi<64>{5}) ^ (rdi<64>{3} ^ rdi<64>{7}))));
1: %%1<1> := undef;
2: %%2<1> := (0<64> = rdi<64>);
3: %%3<1> := (rdi<64> <s 0<64>);
4: of<1> := 0<1>;
5: sf<1> := %%3<1>;
6: zf<1> := %%2<1>;
7: af<1> := %%1<1>;
8: pf<1> := %%0<1>;
9: cf<1> := 0<1>;
10: goto (0x40007d, 0) 
  40007d:
74 0f 
je 0x40008e
0: if zf<1> goto 2 else goto 1
1: goto (0x40007f, 0) 
2: goto (0x40008e, 0) 
  40007f:
ba 01 00 00 00 
mov $0x1,%edx
0: rdx<64> := 1<64>;
1: goto (0x400084, 0) 
  400084:
48 92 
xchg %rax,%rdx
0: %%0<64> := rdx<64>;
1: %%1<64> := rax<64>;
2: rdx<64> := %%1<64>;
3: rax<64> := %%0<64>;
4: goto (0x400086, 0) 
  400086:
48 01 d0 
add %rdx,%rax
0: %%0<64> := (rax<64> & rdx<64>);
1: %%1<64> := (rax<64> + rdx<64>);
2: %%2<64> := ! (%%1<64>);
3: %%3<1> :=
 (0x8000000000000000 =
  (0x8000000000000000 &
   (((rax<64> | rdx<64>) & %%2<64>) | (%%0<64> & %%1<64>))));
4: %%4<1> :=
 !
 ((((%%1<64>{0} ^ %%1<64>{4}) ^ (%%1<64>{2} ^ %%1<64>{6})) ^
   ((%%1<64>{1} ^ %%1<64>{5}) ^ (%%1<64>{3} ^ %%1<64>{7}))));
5: %%5<1> := undef;
6: %%6<1> := (0<64> = %%1<64>);
7: %%7<1> := (%%1<64> <s 0<64>);
8: %%8<1> :=
 (0x8000000000000000 =
  (0x8000000000000000 &
   ((%%0<64> & %%2<64>) | ((! (rax<64>) & ! (rdx<64>)) & %%1<64>))));
9: rax<64> := %%1<64>;
10: of<1> := %%8<1>;
11: sf<1> := %%7<1>;
12: zf<1> := %%6<1>;
13: af<1> := %%5<1>;
14: pf<1> := %%4<1>;
15: cf<1> := %%3<1>;
16: goto (0x400089, 0) 
  400089:
48 ff cf 
dec %rdi
0: %%0<64> := (rdi<64> - 1<64>);
1: %%1<1> :=
 !
 ((((%%0<64>{0} ^ %%0<64>{4}) ^ (%%0<64>{2} ^ %%0<64>{6})) ^
   ((%%0<64>{1} ^ %%0<64>{5}) ^ (%%0<64>{3} ^ %%0<64>{7}))));
2: %%2<1> := undef;
3: %%3<1> := (0<64> = %%0<64>);
4: %%4<1> := (%%0<64> <s 0<64>);
5: %%5<1> :=
 (0x8000000000000000 = (0x8000000000000000 & (rdi<64> & ! (%%0<64>))));
6: rdi<64> := %%0<64>;
7: of<1> := %%5<1>;
8: sf<1> := %%4<1>;
9: zf<1> := %%3<1>;
10: af<1> := %%2<1>;
11: pf<1> := %%1<1>;
12: goto (0x40008c, 0) 
  40008c:
75 f6 
jne 0x400084
0: if ! (zf<1>) goto 2 else goto 1
1: goto (0x40008e, 0) 
2: goto (0x400084, 0) 
  40008e:
c3 
ret
0: %%0<64> := (rsp<64> + 8<64>);
1: %%1<64> := @[rsp<64>,<-,8];
2: rsp<64> := %%0<64>;
3: goto %%1<64> #return
  40008f:
90 
nop
0: goto (0x400090, 0) 
00400090 <parse_uint64>:
  400090:
31 ff 
xor %edi,%edi
0: %%0<1> := undef;
1: rdi<64> := 0<64>;
2: of<1> := 0<1>;
3: sf<1> := 0<1>;
4: zf<1> := -1<1>;
5: af<1> := %%0<1>;
6: pf<1> := -1<1>;
7: cf<1> := 0<1>;
8: goto (0x400092, 0) 
  400092:
0f b6 06 
movzbl (%rsi),%eax
0: %%0<64> := (uext64 @[rsi<64>,<-,1]);
1: rax<64> := %%0<64>;
2: goto (0x400095, 0) 
  400095:
85 c0 
test %eax,%eax
0: %%0<32> := rax<64>{31..0};
1: %%1<1> :=
 !
 ((((rax<64>{0} ^ rax<64>{4}) ^ (rax<64>{2} ^ rax<64>{6})) ^
   ((rax<64>{1} ^ rax<64>{5}) ^ (rax<64>{3} ^ rax<64>{7}))));
2: %%2<1> := undef;
3: %%3<1> := (0<32> = %%0<32>);
4: %%4<1> := (%%0<32> <s 0<32>);
5: of<1> := 0<1>;
6: sf<1> := %%4<1>;
7: zf<1> := %%3<1>;
8: af<1> := %%2<1>;
9: pf<1> := %%1<1>;
10: cf<1> := 0<1>;
11: goto (0x400097, 0) 
  400097:
74 1c 
je 0x4000b5
0: if zf<1> goto 2 else goto 1
1: goto (0x400099, 0) 
2: goto (0x4000b5, 0) 
  400099:
83 e8 30 
sub $0x30,%eax
0: %%0<32> := rax<64>{31..0};
1: %%1<32> := (%%0<32> - 48<32>);
2: %%2<1> := (0x80000000 = (0x80000000 & (! (%%0<32>) & %%1<32>)));
3: %%3<1> :=
 !
 ((((%%1<32>{0} ^ %%1<32>{4}) ^ (%%1<32>{2} ^ %%1<32>{6})) ^
   ((%%1<32>{1} ^ %%1<32>{5}) ^ (%%1<32>{3} ^ %%1<32>{7}))));
4: %%4<1> := undef;
5: %%5<1> := (0<32> = %%1<32>);
6: %%6<1> := (%%1<32> <s 0<32>);
7: %%7<1> := (0x80000000 = (0x80000000 & (%%0<32> & ! (%%1<32>))));
8: %%8<64> := (uext64 %%1<32>);
9: rax<64> := %%8<64>;
10: of<1> := %%7<1>;
11: sf<1> := %%6<1>;
12: zf<1> := %%5<1>;
13: af<1> := %%4<1>;
14: pf<1> := %%3<1>;
15: cf<1> := %%2<1>;
16: goto (0x40009c, 0) 
  40009c:
0f 88 82 00 00 00 
js 0x400124
0: if sf<1> goto 2 else goto 1
1: goto (0x4000a2, 0) 
2: goto (0x400124, 0) 
  4000a2:
3c 09 
cmp $0x9,%al
0: %%0<8> := rax<64>{7..0};
1: %%1<8> := (%%0<8> - 9<8>);
2: %%2<1> := (-128<8> = (-128<8> & (! (%%0<8>) & %%1<8>)));
3: %%3<1> :=
 !
 ((((%%1<8>{0} ^ %%1<8>{4}) ^ (%%1<8>{2} ^ %%1<8>{6})) ^
   ((%%1<8>{1} ^ %%1<8>{5}) ^ (%%1<8>{3} ^ %%1<8>{7}))));
4: %%4<1> := undef;
5: %%5<1> := (0<8> = %%1<8>);
6: %%6<1> := (%%1<8> <s 0<8>);
7: %%7<1> := (-128<8> = (-128<8> & (%%0<8> & ! (%%1<8>))));
8: of<1> := %%7<1>;
9: sf<1> := %%6<1>;
10: zf<1> := %%5<1>;
11: af<1> := %%4<1>;
12: pf<1> := %%3<1>;
13: cf<1> := %%2<1>;
14: goto (0x4000a4, 0) 
  4000a4:
77 7e 
ja 0x400124
0: if ! ((cf<1> | zf<1>)) goto 2 else goto 1
1: goto (0x4000a6, 0) 
2: goto (0x400124, 0) 
  4000a6:
48 ff c6 
inc %rsi
0: %%0<64> := (rsi<64> + 1<64>);
1: %%1<1> :=
 !
 ((((%%0<64>{0} ^ %%0<64>{4}) ^ (%%0<64>{2} ^ %%0<64>{6})) ^
   ((%%0<64>{1} ^ %%0<64>{5}) ^ (%%0<64>{3} ^ %%0<64>{7}))));
2: %%2<1> := undef;
3: %%3<1> := (0<64> = %%0<64>);
4: %%4<1> := (%%0<64> <s 0<64>);
5: %%5<1> :=
 (0x8000000000000000 = (0x8000000000000000 & (! (rsi<64>) & %%0<64>)));
6: rsi<64> := %%0<64>;
7: of<1> := %%5<1>;
8: sf<1> := %%4<1>;
9: zf<1> := %%3<1>;
10: af<1> := %%2<1>;
11: pf<1> := %%1<1>;
12: goto (0x4000a9, 0) 
  4000a9:
48 8d 3c bf 
lea (%rdi,%rdi,4),%rdi
0: %%0<64> := (rdi<64> + (rdi<64> lsl 2<64>));
1: rdi<64> := %%0<64>;
2: goto (0x4000ad, 0) 
  4000ad:
48 01 ff 
add %rdi,%rdi
0: %%0<64> := (rdi<64> + rdi<64>);
1: %%1<64> := (rdi<64> & ! (%%0<64>));
2: %%2<1> :=
 (0x8000000000000000 =
  (0x8000000000000000 & (%%1<64> | (rdi<64> & %%0<64>))));
3: %%3<1> :=
 !
 ((((%%0<64>{0} ^ %%0<64>{4}) ^ (%%0<64>{2} ^ %%0<64>{6})) ^
   ((%%0<64>{1} ^ %%0<64>{5}) ^ (%%0<64>{3} ^ %%0<64>{7}))));
4: %%4<1> := undef;
5: %%5<1> := (0<64> = %%0<64>);
6: %%6<1> := (%%0<64> <s 0<64>);
7: %%7<1> :=
 (0x8000000000000000 =
  (0x8000000000000000 & (%%1<64> | (! (rdi<64>) & %%0<64>))));
8: rdi<64> := %%0<64>;
9: of<1> := %%7<1>;
10: sf<1> := %%6<1>;
11: zf<1> := %%5<1>;
12: af<1> := %%4<1>;
13: pf<1> := %%3<1>;
14: cf<1> := %%2<1>;
15: goto (0x4000b0, 0) 
  4000b0:
48 01 c7 
add %rax,%rdi
0: %%0<64> := (rdi<64> & rax<64>);
1: %%1<64> := (rdi<64> + rax<64>);
2: %%2<64> := ! (%%1<64>);
3: %%3<1> :=
 (0x8000000000000000 =
  (0x8000000000000000 &
   (((rdi<64> | rax<64>) & %%2<64>) | (%%0<64> & %%1<64>))));
4: %%4<1> :=
 !
 ((((%%1<64>{0} ^ %%1<64>{4}) ^ (%%1<64>{2} ^ %%1<64>{6})) ^
   ((%%1<64>{1} ^ %%1<64>{5}) ^ (%%1<64>{3} ^ %%1<64>{7}))));
5: %%5<1> := undef;
6: %%6<1> := (0<64> = %%1<64>);
7: %%7<1> := (%%1<64> <s 0<64>);
8: %%8<1> :=
 (0x8000000000000000 =
  (0x8000000000000000 &
   ((%%0<64> & %%2<64>) | ((! (rdi<64>) & ! (rax<64>)) & %%1<64>))));
9: rdi<64> := %%1<64>;
10: of<1> := %%8<1>;
11: sf<1> := %%7<1>;
12: zf<1> := %%6<1>;
13: af<1> := %%5<1>;
14: pf<1> := %%4<1>;
15: cf<1> := %%3<1>;
16: goto (0x4000b3, 0) 
  4000b3:
eb dd 
jmp 0x400092
0: goto (0x400092, 0) 
  4000b5:
c3 
ret
0: %%0<64> := (rsp<64> + 8<64>);
1: %%1<64> := @[rsp<64>,<-,8];
2: rsp<64> := %%0<64>;
3: goto %%1<64> #return
  4000b6:
66 90 
nop
0: goto (0x4000b8, 0) 
004000b8 <echo_uint64>:
  4000b8:
66 68 00 0a 
pushw $0xa00
0: %%0<64> := (rsp<64> - 2<64>);
1: @[%%0<64>,<-,2] := 2560<16>;
2: rsp<64> := %%0<64>;
3: goto (0x4000bc, 0) 
  4000bc:
48 89 e6 
mov %rsp,%rsi
0: %%0<64> := rsp<64>;
1: rsi<64> := %%0<64>;
2: goto (0x4000bf, 0) 
  4000bf:
66 5a 
pop %dx
0: %%0<16> := @[rsp<64>,<-,2];
1: %%1<64> := (rsp<64> + 2<64>);
2: rsp<64> := %%1<64>;
3: rdx<64>{0, 15} := %%0<16>;
4: goto (0x4000c1, 0) 
  4000c1:
bb 0a 00 00 00 
mov $0xa,%ebx
0: rbx<64> := 10<64>;
1: goto (0x4000c6, 0) 
  4000c6:
48 ff ce 
dec %rsi
0: %%0<64> := (rsi<64> - 1<64>);
1: %%1<1> :=
 !
 ((((%%0<64>{0} ^ %%0<64>{4}) ^ (%%0<64>{2} ^ %%0<64>{6})) ^
   ((%%0<64>{1} ^ %%0<64>{5}) ^ (%%0<64>{3} ^ %%0<64>{7}))));
2: %%2<1> := undef;
3: %%3<1> := (0<64> = %%0<64>);
4: %%4<1> := (%%0<64> <s 0<64>);
5: %%5<1> :=
 (0x8000000000000000 = (0x8000000000000000 & (rsi<64> & ! (%%0<64>))));
6: rsi<64> := %%0<64>;
7: of<1> := %%5<1>;
8: sf<1> := %%4<1>;
9: zf<1> := %%3<1>;
10: af<1> := %%2<1>;
11: pf<1> := %%1<1>;
12: goto (0x4000c9, 0) 
  4000c9:
31 d2 
xor %edx,%edx
0: %%0<1> := undef;
1: rdx<64> := 0<64>;
2: of<1> := 0<1>;
3: sf<1> := 0<1>;
4: zf<1> := -1<1>;
5: af<1> := %%0<1>;
6: pf<1> := -1<1>;
7: cf<1> := 0<1>;
8: goto (0x4000cb, 0) 
  4000cb:
48 f7 f3 
div %rbx
0: %%0<128> := (uext128 rbx<64>);
1: %%1<1> := (0<64> = rbx<64>);
2: %%2<128> := (rdx<64> :: rax<64>);
3: %%3<64> := %%1<1> ? rax<64> : (%%2<128> /u %%0<128>){63..0};
4: %%4<64> := %%1<1> ? rdx<64> : (%%2<128> %u %%0<128>){63..0};
5: if %%1<1> goto 6 else goto 7
6: @assert (0<1>);
7: rdx<64> := %%4<64>;
8: rax<64> := %%3<64>;
9: goto (0x4000ce, 0) 
  4000ce:
80 c2 30 
add $0x30,%dl
0: %%0<8> := rdx<64>{7..0};
1: %%1<8> := (%%0<8> + 48<8>);
2: %%2<1> := (-128<8> = (-128<8> & (%%0<8> & ! (%%1<8>))));
3: %%3<1> :=
 !
 ((((%%1<8>{0} ^ %%1<8>{4}) ^ (%%1<8>{2} ^ %%1<8>{6})) ^
   ((%%1<8>{1} ^ %%1<8>{5}) ^ (%%1<8>{3} ^ %%1<8>{7}))));
4: %%4<1> := undef;
5: %%5<1> := (0<8> = %%1<8>);
6: %%6<1> := (%%1<8> <s 0<8>);
7: %%7<1> := (-128<8> = (-128<8> & (! (%%0<8>) & %%1<8>)));
8: rdx<64>{0, 7} := %%1<8>;
9: of<1> := %%7<1>;
10: sf<1> := %%6<1>;
11: zf<1> := %%5<1>;
12: af<1> := %%4<1>;
13: pf<1> := %%3<1>;
14: cf<1> := %%2<1>;
15: goto (0x4000d1, 0) 
  4000d1:
88 16 
mov %dl,(%rsi)
0: %%0<8> := rdx<64>{7..0};
1: %%1<64> := rsi<64>;
2: @[%%1<64>,<-,1] := %%0<8>;
3: goto (0x4000d3, 0) 
  4000d3:
48 85 c0 
test %rax,%rax
0: %%0<1> :=
 !
 ((((rax<64>{0} ^ rax<64>{4}) ^ (rax<64>{2} ^ rax<64>{6})) ^
   ((rax<64>{1} ^ rax<64>{5}) ^ (rax<64>{3} ^ rax<64>{7}))));
1: %%1<1> := undef;
2: %%2<1> := (0<64> = rax<64>);
3: %%3<1> := (rax<64> <s 0<64>);
4: of<1> := 0<1>;
5: sf<1> := %%3<1>;
6: zf<1> := %%2<1>;
7: af<1> := %%1<1>;
8: pf<1> := %%0<1>;
9: cf<1> := 0<1>;
10: goto (0x4000d6, 0) 
  4000d6:
75 ee 
jne 0x4000c6
0: if ! (zf<1>) goto 2 else goto 1
1: goto (0x4000d8, 0) 
2: goto (0x4000c6, 0) 
  4000d8:
bf 01 00 00 00 
mov $0x1,%edi
0: rdi<64> := 1<64>;
1: goto (0x4000dd, 0) 
  4000dd:
48 89 e2 
mov %rsp,%rdx
0: %%0<64> := rsp<64>;
1: rdx<64> := %%0<64>;
2: goto (0x4000e0, 0) 
  4000e0:
48 29 f2 
sub %rsi,%rdx
0: %%0<64> := ! (rdx<64>);
1: %%1<64> := (rdx<64> - rsi<64>);
2: %%2<64> := ! (%%1<64>);
3: %%3<64> := (%%0<64> & rsi<64>);
4: %%4<1> :=
 (0x8000000000000000 =
  (0x8000000000000000 &
   (((%%0<64> | rsi<64>) & %%1<64>) | (%%3<64> & %%2<64>))));
5: %%5<1> :=
 !
 ((((%%1<64>{0} ^ %%1<64>{4}) ^ (%%1<64>{2} ^ %%1<64>{6})) ^
   ((%%1<64>{1} ^ %%1<64>{5}) ^ (%%1<64>{3} ^ %%1<64>{7}))));
6: %%6<1> := undef;
7: %%7<1> := (0<64> = %%1<64>);
8: %%8<1> := (%%1<64> <s 0<64>);
9: %%9<1> :=
 (0x8000000000000000 =
  (0x8000000000000000 &
   (((rdx<64> & ! (rsi<64>)) & %%2<64>) | (%%3<64> & %%1<64>))));
10: rdx<64> := %%1<64>;
11: of<1> := %%9<1>;
12: sf<1> := %%8<1>;
13: zf<1> := %%7<1>;
14: af<1> := %%6<1>;
15: pf<1> := %%5<1>;
16: cf<1> := %%4<1>;
17: goto (0x4000e3, 0) 
  4000e3:
89 f8 
mov %edi,%eax
0: %%0<64> := (0x00000000ffffffff & rdi<64>);
1: rax<64> := %%0<64>;
2: goto (0x4000e5, 0) 
  4000e5:
0f 05 
syscall
0: #unsupported syscall
  4000e7:
c3 
ret
0: %%0<64> := (rsp<64> + 8<64>);
1: %%1<64> := @[rsp<64>,<-,8];
2: rsp<64> := %%0<64>;
3: goto %%1<64> #return
004000e8 <_start>:
  4000e8:
5f 
pop %rdi
0: %%0<64> := (rsp<64> + 8<64>);
1: %%1<64> := @[rsp<64>,<-,8];
2: rdi<64> := %%1<64>;
3: rsp<64> := %%0<64>;
4: goto (0x4000e9, 0) 
  4000e9:
66 83 ff 02 
cmp $0x2,%di
0: %%0<16> := rdi<64>{15..0};
1: %%1<16> := (%%0<16> - 2<16>);
2: %%2<1> := (0x8000 = (0x8000 & (! (%%0<16>) & %%1<16>)));
3: %%3<1> :=
 !
 ((((%%1<16>{0} ^ %%1<16>{4}) ^ (%%1<16>{2} ^ %%1<16>{6})) ^
   ((%%1<16>{1} ^ %%1<16>{5}) ^ (%%1<16>{3} ^ %%1<16>{7}))));
4: %%4<1> := undef;
5: %%5<1> := (0<16> = %%1<16>);
6: %%6<1> := (%%1<16> <s 0<16>);
7: %%7<1> := (0x8000 = (0x8000 & (%%0<16> & ! (%%1<16>))));
8: of<1> := %%7<1>;
9: sf<1> := %%6<1>;
10: zf<1> := %%5<1>;
11: af<1> := %%4<1>;
12: pf<1> := %%3<1>;
13: cf<1> := %%2<1>;
14: goto (0x4000ed, 0) 
  4000ed:
75 1f 
jne 0x40010e
0: if ! (zf<1>) goto 2 else goto 1
1: goto (0x4000ef, 0) 
2: goto (0x40010e, 0) 
  4000ef:
48 89 e7 
mov %rsp,%rdi
0: %%0<64> := rsp<64>;
1: rdi<64> := %%0<64>;
2: goto (0x4000f2, 0) 
  4000f2:
48 8b 77 08 
mov 0x8(%rdi),%rsi
0: %%0<64> := @[(rdi<64> + 8<64>),<-,8];
1: rsi<64> := %%0<64>;
2: goto (0x4000f6, 0) 
  4000f6:
e8 95 ff ff ff 
call 0x400090
0: %%0<64> := (rsp<64> - 8<64>);
1: @[%%0<64>,<-,8] := 0x00000000004000fb;
2: rsp<64> := %%0<64>;
3: goto (0x400090, 0) #call with return address @ (0x4000fb, 0)
  4000fb:
e8 78 ff ff ff 
call 0x400078
0: %%0<64> := (rsp<64> - 8<64>);
1: @[%%0<64>,<-,8] := 0x0000000000400100;
2: rsp<64> := %%0<64>;
3: goto (0x400078, 0) #call with return address @ (0x400100, 0)
  400100:
e8 b3 ff ff ff 
call 0x4000b8
0: %%0<64> := (rsp<64> - 8<64>);
1: @[%%0<64>,<-,8] := 0x0000000000400105;
2: rsp<64> := %%0<64>;
3: goto (0x4000b8, 0) #call with return address @ (0x400105, 0)
  400105:
31 ff 
xor %edi,%edi
0: %%0<1> := undef;
1: rdi<64> := 0<64>;
2: of<1> := 0<1>;
3: sf<1> := 0<1>;
4: zf<1> := -1<1>;
5: af<1> := %%0<1>;
6: pf<1> := -1<1>;
7: cf<1> := 0<1>;
8: goto (0x400107, 0) 
  400107:
b8 3c 00 00 00 
mov $0x3c,%eax
0: rax<64> := 60<64>;
1: goto (0x40010c, 0) 
  40010c:
0f 05 
syscall
0: #unsupported syscall
  40010e:
bf 01 00 00 00 
mov $0x1,%edi
0: rdi<64> := 1<64>;
1: goto (0x400113, 0) 
  400113:
48 8d 34 25 29 01 40 00 
lea 0x400129,%rsi
0: rsi<64> := 0x0000000000400129;
1: goto (0x40011b, 0) 
  40011b:
ba 13 00 00 00 
mov $0x13,%edx
0: rdx<64> := 19<64>;
1: goto (0x400120, 0) 
  400120:
89 f8 
mov %edi,%eax
0: %%0<64> := (0x00000000ffffffff & rdi<64>);
1: rax<64> := %%0<64>;
2: goto (0x400122, 0) 
  400122:
0f 05 
syscall
0: #unsupported syscall
  400124:
40 b7 ff 
mov $0xff,%dil
0: rdi<64>{0, 7} := -1<8>;
1: goto (0x400127, 0) 
  400127:
eb de 
jmp 0x400107
0: goto (0x400107, 0) 

Concrete emulation

Putting aside the Symbolic in Symbolic execution ends up with straight (concrete) execution: not the fastest nor the most robust, but enough to play with small machine code, even if it does not match the processor of your computer.

Here, we can evaluate the computation of the Fibonacci sequence of the eponymous function.

int fibonacci(int);

info

The x86-64 calling convention states that the first (integer'like) arguments are given, in order, via the registers rdi, rsi, rdx, rcx, r8 and r9. The result is returned in the register rax.

We can feed BINSEC with the following script.

starting from <fibonacci>
rdi := 5
reach <fibonacci> return then print dec rax

Browser

Output

Command-line

Download or copy the content of the script in the file fibonacci_script_1.ini, then run the following command.

binsec -sse -sse-script fibonacci_script_1.ini fibonacci

Output

[sse:result] Path 1 reached address 0x0040008e (<fibonacci> return) (0 to go)
[sse:result] Value rax<64> : 5
[sse:info] SMT queries
         Preprocessing simplifications
           total          8
           true           5
           false          2
           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              0
         pending paths                    1
         stale paths                      0
         failed assertions                0
         branching points                 6
         max path depth                   24
         visited instructions (unrolled)  24
         visited instructions (static)    9

Here, the script is close to the natural language:

• the first line moves the initial instruction pointer to the value of the symbol <fibonacci> (i.e. 0x400078);
• the second line initialize the register rdi, i.e. the function argument according to the calling convention ();
• the last line add the address of the function return (i.e. 0x4000b5) to the goal of the analysis. If the address is reach, the engine will print the value of the register rax (return value).

tip

You can adjust the value of the argument by using the slider.

Input-Output inversion

Let us reintroduce the symbolic in the equation! Instead of choosing a concrete input value for rdi, we will give some freedom to the symbolic engine. Symbolic execution is able to provide an input witness, called "model", for each program path it covers, i.e. an assignment for the symbolic variables we can feed to the program to follow the given path. Thus, it means we can query the tool to find a set of inputs that triggers a special condition.

Here, we can use the following script to find the input number which produces a given Fibonacci sequence value.

starting from <fibonacci>
rdi := nondet as n
reach <fibonacci> return such that rax = 5 then print dec n
cut at <fibonacci> return

Browser

Output

Command-line

Download or copy the content of the script in the file fibonacci_script_2.ini, then run the following command.

binsec -sse -sse-script fibonacci_script_2.ini fibonacci

Output

[sse:result] Path 7 reached address 0x0040008e (<fibonacci> return) (0 to go)
[sse:result] Value n<64> : 5
[sse:info] SMT queries
         Preprocessing simplifications
           total          6
           true           1
           false          4
           constant enum  1
         
         Satisfiability queries
           total          6
           sat            6
           unsat          0
           unknown        0
           time           0.00
           average        0.00
         
       Exploration
         total paths                      7
         completed/cut paths              4
         pending paths                    3
         stale paths                      0
         failed assertions                0
         branching points                 6
         max path depth                   24
         visited instructions (unrolled)  24
         visited instructions (static)    9

warning

A reach does not prevent the execution to go past its address. To avoid the exploration to go outside the fibonacci code, we add the cut instruction, so the execution will stop at the fibonacci return address even if the condition is not met.

note

Any non-initialized location (registers and memory) is implicitly treated as symbolic by BINSEC. Yet, you can not reliably use or constraint them in the script without a name. Thus, it is recommended to always explicitly initialize the program variables either with concrete values or symbolic declarations.

Path enumeration

Up to now, we were looking for a precise, single goal. But, we can also use the symbolic execution to just explore and report all the way to reach a given address.

Here, we will use the reach* goal which stands for reach all.

starting from <fibonacci>
rdi := nondet as n
assume 0 <= n <= 10
reach* <fibonacci> return then print dec rax
cut at <fibonacci> return

Browser

Output

Command-line

Download or copy the content of the script in the file fibonacci_script_3.ini, then run the following command.

binsec -sse -sse-script fibonacci_script_3.ini -sse-heuristics bfs fibonacci

Output

[sse:result] Path 1 reached address 0x0040008e (<fibonacci> return) (* to go)
[sse:result] Value rax<64> : 0
[sse:result] Path 3 reached address 0x0040008e (<fibonacci> return) (* to go)
[sse:result] Value rax<64> : 1
[sse:result] Path 4 reached address 0x0040008e (<fibonacci> return) (* to go)
[sse:result] Value rax<64> : 1
[sse:result] Path 5 reached address 0x0040008e (<fibonacci> return) (* to go)
[sse:result] Value rax<64> : 2
[sse:result] Path 6 reached address 0x0040008e (<fibonacci> return) (* to go)
[sse:result] Value rax<64> : 3
[sse:result] Path 7 reached address 0x0040008e (<fibonacci> return) (* to go)
[sse:result] Value rax<64> : 5
[sse:result] Path 8 reached address 0x0040008e (<fibonacci> return) (* to go)
[sse:result] Value rax<64> : 8
[sse:result] Path 9 reached address 0x0040008e (<fibonacci> return) (* to go)
[sse:result] Value rax<64> : 13
[sse:result] Path 10 reached address 0x0040008e (<fibonacci> return) (* to go)
[sse:result] Value rax<64> : 21
[sse:result] Path 11 reached address 0x0040008e (<fibonacci> return) (* to go)
[sse:result] Value rax<64> : 34
[sse:result] Path 2 reached address 0x0040008e (<fibonacci> return) (* to go)
[sse:result] Value rax<64> : 55
[sse:info] Empty path worklist: halting ...
[sse:info] SMT queries
         Preprocessing simplifications
           total          22
           true           11
           false          0
           constant enum  11
         
         Satisfiability queries
           total          12
           sat            11
           unsat          1
           unknown        0
           time           0.00
           average        0.00
         
       Exploration
         total paths                      11
         completed/cut paths              11
         pending paths                    0
         stale paths                      0
         failed assertions                0
         branching points                 11
         max path depth                   44
         visited instructions (unrolled)  44
         visited instructions (static)    9

note

BINSEC symbolic execution runs until either all the goals are fulfilled or there is no other valid successor state to execute. As consequences:

• a single goal script will stop as soon as it reach its target;
• a script without any goal will stop immediately;
• an infeasible or infinite goal prevents the exploration to stop before its worklist exhaustion.

tip

Here, we use an assumption to reduce the valid range of value for n . It should be the preferred way to limit the search space of the analysis.

Bounded verification

Last but not least, if we are able to exhaustively explore all the paths of a program up to a given bound, we can all along verify that nothing wrong will happen under this scope.

For instance, we may wonder what is the upper limit of n for which our fibonacci computation is correct. Indeed, the fibonacci sequence grows exponentially while the implementation use fixed 64-bit values.

info

Beside the actual result, the x86 arithmetic instructions also update the condition flags, including the carry flag cf and the overflow flag of. The addition instruction add sets these flags when the, respectively unsigned and signed results do not fit in the destination operand.

starting from <fibonacci>
rdi := nondet as n
assume 0 <= n <= 10
at 0x400089 assert !of
cut at <fibonacci> return
explore all

Browser

Output

Command-line

Download or copy the content of the script in the file fibonacci_script_4.ini, then run the following command.

binsec -sse -sse-script fibonacci_script_4.ini -sse-heuristics bfs fibonacci

Output

[sse:info] Empty path worklist: halting ...
[sse:info] SMT queries
         Preprocessing simplifications
           total          10
           true           10
           false          0
           constant enum  0
         
         Satisfiability queries
           total          12
           sat            11
           unsat          1
           unknown        0
           time           0.00
           average        0.00
         
       Exploration
         total paths                      11
         completed/cut paths              11
         pending paths                    0
         stale paths                      0
         failed assertions                0
         branching points                 11
         max path depth                   44
         visited instructions (unrolled)  44
         visited instructions (static)    9

Here, we put an assertion to test the overflow flag of just after the execution of the add instruction. If BINSEC terminates its exploration without raising an alarm, we have the guaranty the no overflow will happen up to the chosen limit. Yet, starting from 93, the assertion fails, meaning the program output is no longer reliable.

tip

The explore all command ensure the exhaustive enumeration of the program paths. It makes clear the goal of the script and will never been optimized out in the future.

In this chapter, you have learned how to setup the entrypoint and the goal of the analysis, how to initialize or symbolize program variables and how to make use of assumption and assertions. It is time to put what you have just learned into practice.