Dispel the magic

In this session, your mission will be to solve the small reverse-engineering challenge called magic .

The function magic to analyze has the following prototype.

int magic (int);

Hexdump

As usual, here is the summary of the basic reverse-engineering information.

info

The x86-32 calling convention states that arguments are passed in the stack. The stack pointer is esp. The memory layout at the callee entry is as follow.

esp offset	Size	Value	BINSEC syntax
+0	4 bytes	Return address	@[esp, 4]
+4	4 bytes	First argument	@[esp + 4, 4]
+8	4 bytes	Second argument	@[esp + 8, 4]
...
+(4*i+4)	4 bytes	ith argument	@[esp + 4 * (i + 1), 4]

The return value is put in eax.

00000000000000100000002000000030000000400000005000000060000000700000008000000090000000a0000000b0000000c0000000d0000000e0000000f000000100000001100000012000000130000001400000015000000160000001700000018000000190000001a0000001b0000001c0000001d0000001e0000001f000000200000002100000022000000230000002400000025000000260000002700000028000000290

7f45 4c46 0101 0100 0000 0000 0000 0000 0200 0300 0100 0000 e080 0408 3400 0000 d001 0000 0000 0000 3400 2000 0100 2800 0500 0400 0100 0000 5400 0000 5480 0408 5480 0408 0a01 0000 0a01 0000 0500 0000 0100 0000 8b54 2404 31c0 89d1 0fc9 84c9 790f d1ea f5d1 d071 f905 07f6 f66a 0f94 c0c3 0001 0203 0405 0607 0809 ffff ffff ffff ff0a 0b0c 0d0e 0fff ffff ffff ffff ffff ffff ffff ffff ffff ffff ffff ffff ffff ff0a 0b0c 0d0e 0fff ffff ffff ffff ffff ffff ffff ffff ffff ffff ffff ffff ffff 4645 4544 4330 4445 0a00 4445 4144 4645 4544 0a00 3842 4144 4630 3044 0a00 b9c2 8004 08e8 6200 0000 ba08 0000 0089 e1bb 0200 0000 b803 0000 00cd 8031 c089 4424 080f b614 2444 84d2 7419 7834 83ea 3078 2f0f b692 7280 0408 84d2 7824 c1e0 0409 d0eb de50 e829 ffff ff84 c074 13b9 cc80 0408 e813 0000 0031 dbb8 0100 0000 cd80 b9d6 8004 0868 3b81 0408 ba09 0000 00bb 0100 0000 b804 0000 00cd 80c3 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 0000 5480 0408 0000 0000 0300 0100 0100 0000 e080 0408 0000 0000 1000 0100 0800 0000 5480 0408 1e00 0000 1200 0100 005f 7374 6172 7400 6d61 6769 6300 002e 7379 6d74 6162 002e 7374 7274 6162 002e 7368 7374 7274 6162 002e 7465 7874 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 5480 0408 5400 0000 0a01 0000 0000 0000 0000 0000 0100 0000 0000 0000 0100 0000 0200 0000 0000 0000 0000 0000 6001 0000 4000 0000 0300 0000 0200 0000 0400 0000 1000 0000 0900 0000 0300 0000 0000 0000 0000 0000 a001 0000 0e00 0000 0000 0000 0000 0000 0100 0000 0000 0000 1100 0000 0300 0000 0000 0000 0000 0000 ae01 0000 2100 0000 0000 0000 0000 0000 0100 0000 0000 0000 0000

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

Headers

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

Section Headers:
  [Nr] Name      Type     Addr     Off    Size   ES Flg Lk Inf Al
  [ 0]           NULL     00000000 000000 000000 00      0   0  0
  [ 1] .text     PROGBITS 08048054 000054 00010a 00  AX  0   0  1
  [ 2] .symtab   SYMTAB   00000000 000160 000040 10      3   2  4
  [ 3] .strtab   STRTAB   00000000 0001a0 00000e 00      0   0  1
  [ 4] .shstrtab STRTAB   00000000 0001ae 000021 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 4 entries:
  Num:    Value Size Type    Bind   Section Name  
    0: 00000000    0 NOTYPE  LOCAL  UND           
    1: 08048054    0 SECTION LOCAL  .text         
    2: 080480e0    0 NOTYPE  GLOBAL .text   _start
    3: 08048054   30 FUNC    GLOBAL .text   magic

Disassembly

Disassembly of section .text:
08048054 <magic>:
 8048054:
8b 54 24 04 
mov edx, [esp + 0x4]
0: edx<32> := @[(esp<32> + 4<32>),<-,4];
1: goto (0x8048058, 0) 
 8048058:
31 c0 
xor eax, eax
0: res32<32> := 0<32>;
1: OF<1> := 0<1>;
2: SF<1> := (res32<32> <s 0<32>);
3: ZF<1> := (0<32> = res32<32>);
4: AF<1> := 0<1>;
5: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
6: CF<1> := 0<1>;
7: eax<32> := res32<32>;
8: goto (0x804805a, 0) 
 804805a:
89 d1 
mov ecx, edx
0: ecx<32> := edx<32>;
1: goto (0x804805c, 0) 
 804805c:
0f c9 
bswap ecx
0: temp32<32> := ecx<32>;
1: ecx<32>{0, 7} := temp32<32>{31..24};
2: ecx<32>{8, 15} := temp32<32>{23..16};
3: ecx<32>{16, 23} := temp32<32>{15..8};
4: ecx<32>{24, 31} := temp32<32>{7..0};
5: goto (0x804805e, 0) 
 804805e:
84 c9 
test cl, cl
0: res8<8> := ecx<32>{7..0};
1: OF<1> := 0<1>;
2: SF<1> := (res8<8> <s 0<8>);
3: AF<1> := undef;
4: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
5: ZF<1> := (0<8> = res8<8>);
6: CF<1> := 0<1>;
7: goto (0x8048060, 0) 
 8048060:
79 0f 
jns 0x8048071
0: if ! (SF<1>) goto (0x8048071, 0) else goto 1
1: goto (0x8048062, 0) 
 8048062:
d1 ea 
shr edx, 0x1
0: res32<32> := (edx<32> lsr 1<32>);
1: OF<1> := edx<32>{31};
2: SF<1> := (res32<32> <s 0<32>);
3: ZF<1> := (0<32> = res32<32>);
4: CF<1> := edx<32>{0};
5: AF<1> := undef;
6: edx<32> := res32<32>;
7: goto (0x8048064, 0) 
 8048064:
f5 
cmc
0: CF<1> := ! (CF<1>);
1: goto (0x8048065, 0) 
 8048065:
d1 d0 
rcl eax, 0x1
0: temp33<33> := ((CF<1> :: eax<32>) rol 1<33>);
1: CF<1> := temp33<33>{32};
2: OF<1> := (temp33<33>{31} ^ CF<1>);
3: eax<32> := temp33<33>{31..0};
4: goto (0x8048067, 0) 
 8048067:
71 f9 
jno 0x8048062
0: if ! (OF<1>) goto (0x8048062, 0) else goto 1
1: goto (0x8048069, 0) 
 8048069:
05 07 f6 f6 6a 
add eax, 0x6af6f607
0: res32<32> := (eax<32> + 0x6af6f607);
1: OF<1> := (! (eax<32>{31}) & (eax<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: ZF<1> := (0<32> = res32<32>);
4: AF<1> := ((uext5 eax<32>{3..0}) + 7<5>){4};
5: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
6: CF<1> := ((uext33 eax<32>) + 0b001101010111101101111011000000111){32};
7: eax<32> := res32<32>;
8: goto (0x804806e, 0) 
 804806e:
0f 94 c0 
setz al
0: eax<32>{0, 7} := ZF<1> ? 1<8> : 0<8>;
1: goto (0x8048071, 0) 
 8048071:
c3 
ret
0: esp<32> := (esp<32> + 4<32>);
1: goto @[(esp<32> - 4<32>),<-,4] #return
 8048072:
00 01 
add [ecx], al
0: res8<8> := (@[ecx<32>,<-,1] + eax<32>{7..0});
1: OF<1> :=
 ((@[ecx<32>,<-,1]{7} = eax<32>{7}) & (@[ecx<32>,<-,1]{7} <> res8<8>{7}));
2: SF<1> := (res8<8> <s 0<8>);
3: ZF<1> := (0<8> = res8<8>);
4: AF<1> := ((uext5 @[ecx<32>,<-,1]{3..0}) + (uext5 eax<32>{3..0})){4};
5: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
6: CF<1> := ((uext9 @[ecx<32>,<-,1]) + (uext9 eax<32>{7..0})){8};
7: @[ecx<32>,<-,1] := res8<8>;
8: goto (0x8048074, 0) 
 8048074:
02 03 
add al, [ebx]
0: res8<8> := (eax<32>{7..0} + @[ebx<32>,<-,1]);
1: OF<1> := ((eax<32>{7} = @[ebx<32>,<-,1]{7}) & (eax<32>{7} <> res8<8>{7}));
2: SF<1> := (res8<8> <s 0<8>);
3: ZF<1> := (0<8> = res8<8>);
4: AF<1> := ((uext5 eax<32>{3..0}) + (uext5 @[ebx<32>,<-,1]{3..0})){4};
5: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
6: CF<1> := ((uext9 eax<32>{7..0}) + (uext9 @[ebx<32>,<-,1])){8};
7: eax<32>{0, 7} := res8<8>;
8: goto (0x8048076, 0) 
 8048076:
04 05 
add al, 0x5
0: res8<8> := (eax<32>{7..0} + 5<8>);
1: OF<1> := (! (eax<32>{7}) & (eax<32>{7} <> res8<8>{7}));
2: SF<1> := (res8<8> <s 0<8>);
3: ZF<1> := (0<8> = res8<8>);
4: AF<1> := ((uext5 eax<32>{3..0}) + 5<5>){4};
5: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
6: CF<1> := ((uext9 eax<32>{7..0}) + 5<9>){8};
7: eax<32>{0, 7} := res8<8>;
8: goto (0x8048078, 0) 
 8048078:
06 
push es
0: @[(esp<32> - 2<32>),<-,2] := es<16>;
1: esp<32> := (esp<32> - 2<32>);
2: goto (0x8048079, 0) 
 8048079:
07 
pop es
0: es<16> := @[esp<32>,<-,2];
1: esp<32> := (esp<32> + 2<32>);
2: goto (0x804807a, 0) 
 804807a:
08 09 
or [ecx], cl
0: res8<8> := (@[ecx<32>,<-,1] | ecx<32>{7..0});
1: OF<1> := 0<1>;
2: SF<1> := (res8<8> <s 0<8>);
3: ZF<1> := (0<8> = res8<8>);
4: AF<1> := 0<1>;
5: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
6: CF<1> := 0<1>;
7: @[ecx<32>,<-,1] := res8<8>;
8: goto (0x804807c, 0) 
 804807c:
ff ff 
unknown
0: #undecoded ff ff
 804807e:
ff ff 
unknown
0: #undecoded ff ff
 8048080:
ff ff 
unknown
0: #undecoded ff ff
 8048082:
ff 0a 
dec [edx]
0: res32<32> := (@[edx<32>,<-,4] - 1<32>);
1: OF<1> :=
 (@[(edx<32> + 3<32>),<-,1]{7} &
  (@[(edx<32> + 3<32>),<-,1]{7} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := (@[edx<32>,<-,1]{3..0} <u 1<4>);
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: @[edx<32>,<-,4] := res32<32>;
7: goto (0x8048084, 0) 
 8048084:
0b 0c 0d 0e 0f ff ff 
or ecx, [ecx + 0xffff0f0e]
0: res32<32> := (ecx<32> | @[(ecx<32> + 0xffff0f0e),<-,4]);
1: OF<1> := 0<1>;
2: SF<1> := (res32<32> <s 0<32>);
3: ZF<1> := (0<32> = res32<32>);
4: AF<1> := 0<1>;
5: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
6: CF<1> := 0<1>;
7: ecx<32> := res32<32>;
8: goto (0x804808b, 0) 
 804808b:
ff ff 
unknown
0: #undecoded ff ff
 804808d:
ff ff 
unknown
0: #undecoded ff ff
 804808f:
ff ff 
unknown
0: #undecoded ff ff
 8048091:
ff ff 
unknown
0: #undecoded ff ff
 8048093:
ff ff 
unknown
0: #undecoded ff ff
 8048095:
ff ff 
unknown
0: #undecoded ff ff
 8048097:
ff ff 
unknown
0: #undecoded ff ff
 8048099:
ff ff 
unknown
0: #undecoded ff ff
 804809b:
ff ff 
unknown
0: #undecoded ff ff
 804809d:
ff ff 
unknown
0: #undecoded ff ff
 804809f:
ff ff 
unknown
0: #undecoded ff ff
 80480a1:
ff ff 
unknown
0: #undecoded ff ff
 80480a3:
0a 0b 
or cl, [ebx]
0: res8<8> := (ecx<32>{7..0} | @[ebx<32>,<-,1]);
1: OF<1> := 0<1>;
2: SF<1> := (res8<8> <s 0<8>);
3: ZF<1> := (0<8> = res8<8>);
4: AF<1> := 0<1>;
5: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
6: CF<1> := 0<1>;
7: ecx<32>{0, 7} := res8<8>;
8: goto (0x80480a5, 0) 
 80480a5:
0c 0d 
or al, 0xd
0: res8<8> := (13<8> | eax<32>{7..0});
1: OF<1> := 0<1>;
2: SF<1> := (res8<8> <s 0<8>);
3: ZF<1> := (0<8> = res8<8>);
4: AF<1> := 0<1>;
5: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
6: CF<1> := 0<1>;
7: eax<32>{0, 7} := res8<8>;
8: goto (0x80480a7, 0) 
 80480a7:
0e 
push cs
0: @[(esp<32> - 2<32>),<-,2] := cs<16>;
1: esp<32> := (esp<32> - 2<32>);
2: goto (0x80480a8, 0) 
 80480a8:
0f ff 
unknown
0: #undecoded 0f ff
 80480aa:
ff ff 
unknown
0: #undecoded ff ff
 80480ac:
ff ff 
unknown
0: #undecoded ff ff
 80480ae:
ff ff 
unknown
0: #undecoded ff ff
 80480b0:
ff ff 
unknown
0: #undecoded ff ff
 80480b2:
ff ff 
unknown
0: #undecoded ff ff
 80480b4:
ff ff 
unknown
0: #undecoded ff ff
 80480b6:
ff ff 
unknown
0: #undecoded ff ff
 80480b8:
ff ff 
unknown
0: #undecoded ff ff
 80480ba:
ff ff 
unknown
0: #undecoded ff ff
 80480bc:
ff ff 
unknown
0: #undecoded ff ff
 80480be:
ff ff 
unknown
0: #undecoded ff ff
 80480c0:
ff ff 
unknown
0: #undecoded ff ff
 80480c2:
46 
inc esi
0: res32<32> := (esi<32> + 1<32>);
1: OF<1> := (! (esi<32>{31}) & (esi<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := ((uext5 esi<32>{3..0}) + 1<5>){4};
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: esi<32> := res32<32>;
7: goto (0x80480c3, 0) 
 80480c3:
45 
inc ebp
0: res32<32> := (ebp<32> + 1<32>);
1: OF<1> := (! (ebp<32>{31}) & (ebp<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := ((uext5 ebp<32>{3..0}) + 1<5>){4};
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: ebp<32> := res32<32>;
7: goto (0x80480c4, 0) 
 80480c4:
45 
inc ebp
0: res32<32> := (ebp<32> + 1<32>);
1: OF<1> := (! (ebp<32>{31}) & (ebp<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := ((uext5 ebp<32>{3..0}) + 1<5>){4};
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: ebp<32> := res32<32>;
7: goto (0x80480c5, 0) 
 80480c5:
44 
inc esp
0: res32<32> := (esp<32> + 1<32>);
1: OF<1> := (! (esp<32>{31}) & (esp<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := ((uext5 esp<32>{3..0}) + 1<5>){4};
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: esp<32> := res32<32>;
7: goto (0x80480c6, 0) 
 80480c6:
43 
inc ebx
0: res32<32> := (ebx<32> + 1<32>);
1: OF<1> := (! (ebx<32>{31}) & (ebx<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := ((uext5 ebx<32>{3..0}) + 1<5>){4};
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: ebx<32> := res32<32>;
7: goto (0x80480c7, 0) 
 80480c7:
30 44 45 0a 
xor [eax * 2 + ebp + 0xa], al
0: res8<8> := (@[(ebp<32> + ((2<32> * eax<32>) + 10<32>)),<-,1] ^ eax<32>{7..0})
 ;
1: OF<1> := 0<1>;
2: SF<1> := (res8<8> <s 0<8>);
3: ZF<1> := (0<8> = res8<8>);
4: AF<1> := 0<1>;
5: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
6: CF<1> := 0<1>;
7: @[(ebp<32> + ((2<32> * eax<32>) + 10<32>)),<-,1] := res8<8>;
8: goto (0x80480cb, 0) 
 80480cb:
00 44 45 41 
add [eax * 2 + ebp + 0x41], al
0: res8<8> := (@[(ebp<32> + ((2<32> * eax<32>) + 65<32>)),<-,1] + eax<32>{7..0})
 ;
1: OF<1> :=
 ((@[(ebp<32> + ((2<32> * eax<32>) + 65<32>)),<-,1]{7} = eax<32>{7}) &
  (@[(ebp<32> + ((2<32> * eax<32>) + 65<32>)),<-,1]{7} <> res8<8>{7}));
2: SF<1> := (res8<8> <s 0<8>);
3: ZF<1> := (0<8> = res8<8>);
4: AF<1> :=
 ((uext5 @[(ebp<32> + ((2<32> * eax<32>) + 65<32>)),<-,1]{3..0}) +
  (uext5 eax<32>{3..0})){4};
5: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
6: CF<1> :=
 ((uext9 @[(ebp<32> + ((2<32> * eax<32>) + 65<32>)),<-,1]) +
  (uext9 eax<32>{7..0})){8};
7: @[(ebp<32> + ((2<32> * eax<32>) + 65<32>)),<-,1] := res8<8>;
8: goto (0x80480cf, 0) 
 80480cf:
44 
inc esp
0: res32<32> := (esp<32> + 1<32>);
1: OF<1> := (! (esp<32>{31}) & (esp<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := ((uext5 esp<32>{3..0}) + 1<5>){4};
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: esp<32> := res32<32>;
7: goto (0x80480d0, 0) 
 80480d0:
46 
inc esi
0: res32<32> := (esi<32> + 1<32>);
1: OF<1> := (! (esi<32>{31}) & (esi<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := ((uext5 esi<32>{3..0}) + 1<5>){4};
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: esi<32> := res32<32>;
7: goto (0x80480d1, 0) 
 80480d1:
45 
inc ebp
0: res32<32> := (ebp<32> + 1<32>);
1: OF<1> := (! (ebp<32>{31}) & (ebp<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := ((uext5 ebp<32>{3..0}) + 1<5>){4};
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: ebp<32> := res32<32>;
7: goto (0x80480d2, 0) 
 80480d2:
45 
inc ebp
0: res32<32> := (ebp<32> + 1<32>);
1: OF<1> := (! (ebp<32>{31}) & (ebp<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := ((uext5 ebp<32>{3..0}) + 1<5>){4};
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: ebp<32> := res32<32>;
7: goto (0x80480d3, 0) 
 80480d3:
44 
inc esp
0: res32<32> := (esp<32> + 1<32>);
1: OF<1> := (! (esp<32>{31}) & (esp<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := ((uext5 esp<32>{3..0}) + 1<5>){4};
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: esp<32> := res32<32>;
7: goto (0x80480d4, 0) 
 80480d4:
0a 00 
or al, [eax]
0: res8<8> := (eax<32>{7..0} | @[eax<32>,<-,1]);
1: OF<1> := 0<1>;
2: SF<1> := (res8<8> <s 0<8>);
3: ZF<1> := (0<8> = res8<8>);
4: AF<1> := 0<1>;
5: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
6: CF<1> := 0<1>;
7: eax<32>{0, 7} := res8<8>;
8: goto (0x80480d6, 0) 
 80480d6:
38 42 41 
cmp [edx + 0x41], al
0: res8<8> := (@[(edx<32> + 65<32>),<-,1] - eax<32>{7..0});
1: OF<1> :=
 ((@[(edx<32> + 65<32>),<-,1]{7} <> eax<32>{7}) &
  (@[(edx<32> + 65<32>),<-,1]{7} <> res8<8>{7}));
2: SF<1> := (res8<8> <s 0<8>);
3: ZF<1> := (0<8> = res8<8>);
4: AF<1> := (@[(edx<32> + 65<32>),<-,1]{3..0} <u eax<32>{3..0});
5: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
6: CF<1> := (@[(edx<32> + 65<32>),<-,1] <u eax<32>{7..0});
7: goto (0x80480d9, 0) 
 80480d9:
44 
inc esp
0: res32<32> := (esp<32> + 1<32>);
1: OF<1> := (! (esp<32>{31}) & (esp<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := ((uext5 esp<32>{3..0}) + 1<5>){4};
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: esp<32> := res32<32>;
7: goto (0x80480da, 0) 
 80480da:
46 
inc esi
0: res32<32> := (esi<32> + 1<32>);
1: OF<1> := (! (esi<32>{31}) & (esi<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := ((uext5 esi<32>{3..0}) + 1<5>){4};
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: esi<32> := res32<32>;
7: goto (0x80480db, 0) 
 80480db:
30 30 
xor [eax], dh
0: res8<8> := (@[eax<32>,<-,1] ^ edx<32>{15..8});
1: OF<1> := 0<1>;
2: SF<1> := (res8<8> <s 0<8>);
3: ZF<1> := (0<8> = res8<8>);
4: AF<1> := 0<1>;
5: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
6: CF<1> := 0<1>;
7: @[eax<32>,<-,1] := res8<8>;
8: goto (0x80480dd, 0) 
 80480dd:
44 
inc esp
0: res32<32> := (esp<32> + 1<32>);
1: OF<1> := (! (esp<32>{31}) & (esp<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := ((uext5 esp<32>{3..0}) + 1<5>){4};
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: esp<32> := res32<32>;
7: goto (0x80480de, 0) 
 80480de:
0a 00 
or al, [eax]
0: res8<8> := (eax<32>{7..0} | @[eax<32>,<-,1]);
1: OF<1> := 0<1>;
2: SF<1> := (res8<8> <s 0<8>);
3: ZF<1> := (0<8> = res8<8>);
4: AF<1> := 0<1>;
5: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
6: CF<1> := 0<1>;
7: eax<32>{0, 7} := res8<8>;
8: goto (0x80480e0, 0) 
080480e0 <_start>:
 80480e0:
b9 c2 80 04 08 
mov ecx, 0x80480c2
0: ecx<32> := 0x080480c2;
1: goto (0x80480e5, 0) 
 80480e5:
e8 62 00 00 00 
call 0x804814c
0: esp<32> := (esp<32> - 4<32>);
1: @[esp<32>,<-,4] := 0x080480ea;
2: goto (0x804814c, 0) #call with return address @ (0x80480ea, 0)
 80480ea:
ba 08 00 00 00 
mov edx, 0x8
0: edx<32> := 8<32>;
1: goto (0x80480ef, 0) 
 80480ef:
89 e1 
mov ecx, esp
0: ecx<32> := esp<32>;
1: goto (0x80480f1, 0) 
 80480f1:
bb 02 00 00 00 
mov ebx, 0x2
0: ebx<32> := 2<32>;
1: goto (0x80480f6, 0) 
 80480f6:
b8 03 00 00 00 
mov eax, 0x3
0: eax<32> := 3<32>;
1: goto (0x80480fb, 0) 
 80480fb:
cd 80 
unsupported int 128
0: #unsupported cd 80
 80480fd:
31 c0 
xor eax, eax
0: res32<32> := 0<32>;
1: OF<1> := 0<1>;
2: SF<1> := (res32<32> <s 0<32>);
3: ZF<1> := (0<32> = res32<32>);
4: AF<1> := 0<1>;
5: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
6: CF<1> := 0<1>;
7: eax<32> := res32<32>;
8: goto (0x80480ff, 0) 
 80480ff:
89 44 24 08 
mov [esp + 0x8], eax
0: @[(esp<32> + 8<32>),<-,4] := eax<32>;
1: goto (0x8048103, 0) 
 8048103:
0f b6 14 24 
movzx edx, [esp]
0: edx<32> := (uext32 @[esp<32>,<-,1]);
1: goto (0x8048107, 0) 
 8048107:
44 
inc esp
0: res32<32> := (esp<32> + 1<32>);
1: OF<1> := (! (esp<32>{31}) & (esp<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: AF<1> := ((uext5 esp<32>{3..0}) + 1<5>){4};
4: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
5: ZF<1> := (0<32> = res32<32>);
6: esp<32> := res32<32>;
7: goto (0x8048108, 0) 
 8048108:
84 d2 
test dl, dl
0: res8<8> := edx<32>{7..0};
1: OF<1> := 0<1>;
2: SF<1> := (res8<8> <s 0<8>);
3: AF<1> := undef;
4: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
5: ZF<1> := (0<8> = res8<8>);
6: CF<1> := 0<1>;
7: goto (0x804810a, 0) 
 804810a:
74 19 
jz 0x8048125
0: if ZF<1> goto (0x8048125, 0) else goto 1
1: goto (0x804810c, 0) 
 804810c:
78 34 
js 0x8048142
0: if SF<1> goto (0x8048142, 0) else goto 1
1: goto (0x804810e, 0) 
 804810e:
83 ea 30 
sub edx, 0x30
0: res32<32> := (edx<32> - 48<32>);
1: OF<1> := (edx<32>{31} & (edx<32>{31} <> res32<32>{31}));
2: SF<1> := (res32<32> <s 0<32>);
3: ZF<1> := (0<32> = res32<32>);
4: AF<1> := (edx<32>{3..0} <u 0<4>);
5: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
6: CF<1> := (edx<32> <u 48<32>);
7: edx<32> := res32<32>;
8: goto (0x8048111, 0) 
 8048111:
78 2f 
js 0x8048142
0: if SF<1> goto (0x8048142, 0) else goto 1
1: goto (0x8048113, 0) 
 8048113:
0f b6 92 72 80 04 08 
movzx edx, [edx + 0x8048072]
0: edx<32> := (uext32 @[(edx<32> + 0x08048072),<-,1]);
1: goto (0x804811a, 0) 
 804811a:
84 d2 
test dl, dl
0: res8<8> := edx<32>{7..0};
1: OF<1> := 0<1>;
2: SF<1> := (res8<8> <s 0<8>);
3: AF<1> := undef;
4: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
5: ZF<1> := (0<8> = res8<8>);
6: CF<1> := 0<1>;
7: goto (0x804811c, 0) 
 804811c:
78 24 
js 0x8048142
0: if SF<1> goto (0x8048142, 0) else goto 1
1: goto (0x804811e, 0) 
 804811e:
c1 e0 04 
shl eax, 0x4
0: res32<32> := (eax<32> lsl 4<32>);
1: OF<1> := undef;
2: SF<1> := (res32<32> <s 0<32>);
3: ZF<1> := (0<32> = res32<32>);
4: CF<1> := eax<32>{28};
5: AF<1> := undef;
6: eax<32> := res32<32>;
7: goto (0x8048121, 0) 
 8048121:
09 d0 
or eax, edx
0: res32<32> := (eax<32> | edx<32>);
1: OF<1> := 0<1>;
2: SF<1> := (res32<32> <s 0<32>);
3: ZF<1> := (0<32> = res32<32>);
4: AF<1> := 0<1>;
5: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
6: CF<1> := 0<1>;
7: eax<32> := res32<32>;
8: goto (0x8048123, 0) 
 8048123:
eb de 
jmp 0x8048103
0: goto (0x8048103, 0) 
 8048125:
50 
push eax
0: @[(esp<32> - 4<32>),<-,4] := eax<32>;
1: esp<32> := (esp<32> - 4<32>);
2: goto (0x8048126, 0) 
 8048126:
e8 29 ff ff ff 
call 0x8048054
0: esp<32> := (esp<32> - 4<32>);
1: @[esp<32>,<-,4] := 0x0804812b;
2: goto (0x8048054, 0) #call with return address @ (0x804812b, 0)
 804812b:
84 c0 
test al, al
0: res8<8> := eax<32>{7..0};
1: OF<1> := 0<1>;
2: SF<1> := (res8<8> <s 0<8>);
3: AF<1> := undef;
4: PF<1> :=
 !
 ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^ res8<8>{3}) ^ res8<8>{4}) ^
     res8<8>{5}) ^ res8<8>{6}) ^ res8<8>{7}));
5: ZF<1> := (0<8> = res8<8>);
6: CF<1> := 0<1>;
7: goto (0x804812d, 0) 
 804812d:
74 13 
jz 0x8048142
0: if ZF<1> goto (0x8048142, 0) else goto 1
1: goto (0x804812f, 0) 
 804812f:
b9 cc 80 04 08 
mov ecx, 0x80480cc
0: ecx<32> := 0x080480cc;
1: goto (0x8048134, 0) 
 8048134:
e8 13 00 00 00 
call 0x804814c
0: esp<32> := (esp<32> - 4<32>);
1: @[esp<32>,<-,4] := 0x08048139;
2: goto (0x804814c, 0) #call with return address @ (0x8048139, 0)
 8048139:
31 db 
xor ebx, ebx
0: res32<32> := 0<32>;
1: OF<1> := 0<1>;
2: SF<1> := (res32<32> <s 0<32>);
3: ZF<1> := (0<32> = res32<32>);
4: AF<1> := 0<1>;
5: PF<1> :=
 !
 ((((((((res32<32>{0} ^ res32<32>{1}) ^ res32<32>{2}) ^ res32<32>{3}) ^
      res32<32>{4}) ^ res32<32>{5}) ^ res32<32>{6}) ^ res32<32>{7}));
6: CF<1> := 0<1>;
7: ebx<32> := res32<32>;
8: goto (0x804813b, 0) 
 804813b:
b8 01 00 00 00 
mov eax, 0x1
0: eax<32> := 1<32>;
1: goto (0x8048140, 0) 
 8048140:
cd 80 
unsupported int 128
0: #unsupported cd 80
 8048142:
b9 d6 80 04 08 
mov ecx, 0x80480d6
0: ecx<32> := 0x080480d6;
1: goto (0x8048147, 0) 
 8048147:
68 3b 81 04 08 
push 0x804813b
0: @[(esp<32> - 4<32>),<-,4] := 0x0804813b;
1: esp<32> := (esp<32> - 4<32>);
2: goto (0x804814c, 0) 
 804814c:
ba 09 00 00 00 
mov edx, 0x9
0: edx<32> := 9<32>;
1: goto (0x8048151, 0) 
 8048151:
bb 01 00 00 00 
mov ebx, 0x1
0: ebx<32> := 1<32>;
1: goto (0x8048156, 0) 
 8048156:
b8 04 00 00 00 
mov eax, 0x4
0: eax<32> := 4<32>;
1: goto (0x804815b, 0) 
 804815b:
cd 80 
unsupported int 128
0: #unsupported cd 80
 804815d:
c3 
ret
0: esp<32> := (esp<32> + 4<32>);
1: goto @[(esp<32> - 4<32>),<-,4] #return

Your solution

# Enter your script here # starting from ... # ... # reach ... # cut at ...

# Enter your script here
# starting from ...
# ...
# reach ...
# cut at ...

Output

Proposed solution

starting from <magic>
@[esp + 4, 4] := nondet as x
reach <magic> return such that al = 1 then print x
cut at <magic> return

Browser

Output

Command-line

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

binsec -sse -sse-script magic_script_1.ini magic

Output

[sse:info] Load section .data (0x0000000000004010, 0x10)
[sse:info] Load section .rodata (0x0000000000002000, 0x64)
[sse:result] Path 9 reached address 0x00001030 (<printf@plt>) (0 to go)
[sse:result] C string stdin[0<64>, *] : "sudo0x18"
[sse:info] SMT queries
         Preprocessing simplifications
           total          9
           true           2
           false          3
           constant enum  4
         
         Satisfiability queries
           total          8
           sat            8
           unsat          0
           unknown        0
           time           0.01
           average        0.00
         
       Exploration
         total paths                      9
         completed/cut paths              0
         pending paths                    9
         stale paths                      0
         failed assertions                0
         branching points                 13
         max path depth                   74
         visited instructions (unrolled)  74
         visited instructions (static)    84

More detail at https://github.com/binsec/binsec/blob/master/doc/sse/beginners.md