How do I populate memory address using angr with array of integers (?) and add a constraint so each int will be positive & less than 17 ?
I hope it's clear I need to find out the in_array combination
chall.c
// gcc -m32 chall.c -o chall
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
int p = 0;
int c = 1;
char d[45] = {0, 0, 0, 0, 1, 0, 0, 1, 0, 1, 1, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 0, 0, 0, 1, 0, 0, 0, 0, 1, 1, 1, 1, 1, 0, 1, 0};
char in_array[16] = {0};
int M(char *a1, int a2);
void BAD();
void GOOD();
int main(int argc, char *argv[])
{
if (M(in_array, 16))
GOOD();
}
int M(char *a1, int a2)
{
char *v2; // r11
unsigned int v3; // r10
signed int v4; // r9
int v5; // r6
int v6; // r3
int v7; // r4
int v8; // r5
signed int v9; // r8
unsigned int v10; // r2
unsigned int v11; // r1
char v12; // r1
int v14; // [sp+14h] [bp-34h]
char v15[16]; // [sp+18h] [bp-30h]
int v16; // [sp+28h] [bp-20h]
v2 = a1;
v3 = a2;
if ( a2 >= 2 )
{
v4 = (unsigned int)a2 >> 1;
M(a1, (unsigned int)a2 >> 1);
if ( c )
{
v5 = (int) &v2[v3 >> 1];
M(&v2[v3 >> 1], v3 - (v3 >> 1));
if ( c )
{
v6 = v3 - (v3 >> 1);
v14 = v3 - (v3 >> 1);
if ( (signed int)(v3 - (v3 >> 1)) >= 1 )
{
v7 = 0;
v8 = 0;
v9 = 0;
while ( 1 )
{
v10 = *(char *)(v5 + v8);
v11 = v2[v9];
if ( v11 >= v10 )
{
if ( v11 <= v10 || d[p] )
{
LABEL_21:
c = 0;
BAD();
// return 0;
}
++p;
v12 = *(char *)(v5 + v8++);
}
else
{
if ( d[p] != 1 )
goto LABEL_21;
v6 = v14;
++p;
v12 = v2[v9++];
}
v15[v7++] = v12;
if ( v9 >= v4 || v8 >= v6 )
goto LABEL_16;
}
}
v9 = 0;
v8 = 0;
v7 = 0;
LABEL_16:
if ( v4 > v9 )
{
memcpy(&v15[v7], &v2[v9], v4 - v9);
v6 = v14;
v7 = v7 + v4 - v9;
}
if ( v8 < v6 )
memcpy(&v15[v7], &v2[v8 + v4], v3 - v8 - v4);
memcpy(v2, v15, v3);
}
}
}
return 1;
}
void BAD()
{
printf("BAD\n");
exit(2);
}
void GOOD()
{
printf("GOOD\n");
for (int j = 0; j < 16; j++)
printf("%d ", in_array[j]);
printf("\n");
}
$ readelf -s chall | grep -E "in_array|GOOD|BAD|main" | grep -v libc
44: 0000063d 46 FUNC GLOBAL DEFAULT 14 BAD
72: 000006d9 69 FUNC GLOBAL DEFAULT 14 main
78: 00002078 16 OBJECT GLOBAL DEFAULT 24 in_array
79: 0000066b 110 FUNC GLOBAL DEFAULT 14 GOOD
solve.py
import angr
import claripy
base = 0x400000
main, good, bad = base + 0x6d9, base + 0x66b, base + 0x63d
pointer_size = 4
in_array_addr, in_array_size = base + 0x2078, 16 * pointer_size
p = angr.Project('./chall')
state = p.factory.blank_state(addr=main)
arr = claripy.BVS('in_array', in_array_size)
for i in arr.chop(pointer_size):
state.add_constraints(i >= 0)
state.add_constraints(i < 17)
state.memory.store(in_array_addr, arr)
sm = p.factory.simulation_manager(state)
sm.explore(find=good, avoid=bad)
print('found ?', len(sm.found))
flag_state = sm.found[0]
flag_data = flag_state.memory.load(in_array, in_array_size)
print(flag_state.solver.eval(flag_data, cast_to=bytes).strip(b'\0\n'))
angr log
WARNING | cle.loader | The main binary is a position-independent executable. It is being loaded with a base address of 0x400000.
WARNING | angr.state_plugins.symbolic_memory | The program is accessing memory or registers with an unspecified value. This could indicate unwanted behavior.
WARNING | angr.state_plugins.symbolic_memory | angr will cope with this by generating an unconstrained symbolic variable and continuing. You can resolve this by:
WARNING | angr.state_plugins.symbolic_memory | 1) setting a value to the initial state
WARNING | angr.state_plugins.symbolic_memory | 2) adding the state option ZERO_FILL_UNCONSTRAINED_{MEMORY,REGISTERS}, to make unknown regions hold null
WARNING | angr.state_plugins.symbolic_memory | 3) adding the state option SYMBOL_FILL_UNCONSTRAINED_{MEMORY_REGISTERS}, to suppress these messages.
WARNING | angr.state_plugins.symbolic_memory | Filling memory at 0x7fff0000 with 4 unconstrained bytes referenced from 0x4006e0 (main+0x7 in chall (0x6e0))
WARNING | angr.state_plugins.symbolic_memory | Filling register ebp with 4 unconstrained bytes referenced from 0x4006e3 (main+0xa in chall (0x6e3))
WARNING | angr.state_plugins.symbolic_memory | Filling register esi with 4 unconstrained bytes referenced from 0x400721 (M+0x3 in chall (0x721))
WARNING | angr.state_plugins.symbolic_memory | Filling register ebx with 4 unconstrained bytes referenced from 0x400722 (M+0x4 in chall (0x722))
found ? 0
state.solver.add. Examples here