2

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
1
2
+50

Making a few changes to the code you've posted, angr is able to find a solution.

The addresses of the symbol are resolved dynamically using proj.loader.find_symbol. This avoids hard coding the address which may each change each-time the source is recompiled.

Instead of declaring a big BitVector covering the entire array, I've declared 16 8-bit BitVectors, one each for every element of the array. This way it's easier to apply the constraints.

import angr

proj = angr.Project('./chall')

# Addresses of symbols
main = proj.loader.find_symbol('main').rebased_addr
good = proj.loader.find_symbol('GOOD').rebased_addr 
bad = proj.loader.find_symbol('BAD').rebased_addr 

in_array_addr = proj.loader.find_symbol('in_array').rebased_addr  

# in_array is a char array with 16 elements and sizeof(char)=1
in_array_size = 16 * 1

initial_state = proj.factory.entry_state(addr=main)

for i in range(in_array_size):
    # Each char of the array is a 8 bit BitVector
    ch = initial_state.solver.BVS('ch{}'.format(i), 8)

    # Add constraints
    initial_state.solver.add(ch >= 0)    
    initial_state.solver.add(ch < 17)

    # Store BV to memory
    initial_state.memory.store(in_array_addr+i, ch)


# Create a Simulation manager from the current state
sm = proj.factory.simulation_manager(initial_state)

# Find a path to good while avoiding bad
sm.explore(find=good, avoid=bad)

print("No. of solutions found:", len(sm.found))

if len(sm.found) > 0:        
    # Considering the first goal state
    goal_state = sm.found[0]

    # Load contents of memory at the said address
    flag_data = goal_state.memory.load(in_array_addr, in_array_size)

    # Convert flag_data from BitVector to bytes
    answer = goal_state.solver.eval(flag_data, cast_to=bytes)
    print (list(answer))

Output

user@70a6c29adea0 $ python solve.py
WARNING | 2019-07-04 21:09:04,764 | angr.state_plugins.symbolic_memory | The program is accessing memory or registers with an unspecified value. This could indicate unwa
nted behavior.
WARNING | 2019-07-04 21:09:04,764 | angr.state_plugins.symbolic_memory | angr will cope with this by generating an unconstrained symbolic variable and continuing. You ca
n resolve this by:
WARNING | 2019-07-04 21:09:04,764 | angr.state_plugins.symbolic_memory | 1) setting a value to the initial state
WARNING | 2019-07-04 21:09:04,764 | angr.state_plugins.symbolic_memory | 2) adding the state option ZERO_FILL_UNCONSTRAINED_{MEMORY,REGISTERS}, to make unknown regions h
old null
WARNING | 2019-07-04 21:09:04,764 | angr.state_plugins.symbolic_memory | 3) adding the state option SYMBOL_FILL_UNCONSTRAINED_{MEMORY_REGISTERS}, to suppress these messa
ges.
WARNING | 2019-07-04 21:09:04,765 | angr.state_plugins.symbolic_memory | Filling register edi with 4 unconstrained bytes referenced from 0x8048861 (__libc_csu_init+0x1 i
n chall (0x8048861))
WARNING | 2019-07-04 21:09:04,770 | angr.state_plugins.symbolic_memory | Filling register ebx with 4 unconstrained bytes referenced from 0x8048863 (__libc_csu_init+0x3 i
n chall (0x8048863))
No. of solutions found: 1
[0, 1, 2, 3, 4, 5, 6, 7, 8, 10, 11, 12, 13, 14, 15, 16]

UPDATE

After OP mentioned that its a challenge from Google CTF Quals 2019, I decided to look at the original binary instead.

Apparently the previous answer from angr doesn't satisfy the C code OP posted. There were a couple of reasons for this.

The first and glaring mistake was using the goal_state to load flag_data. This is wrong as in goal_state the flag_data will get changed.

The second mistake was the bytes of in_array should be in between 0 and 16 (not 0 and 17).

This can be inferred from the Ghidra decompiler screenshot.

enter image description here

The last line

return uVar2 & (uint)((byte)local_24[15] < 16);

checks whether the final element of the array is < 16.

The following updated script prints out the the contents of in_array which satisfies the constraints.

import angr

proj = angr.Project('./chall')

# Addresses of symbols
main = proj.loader.find_symbol('main').rebased_addr
good = proj.loader.find_symbol('GOOD').rebased_addr 
bad = proj.loader.find_symbol('BAD').rebased_addr 

in_array_addr = proj.loader.find_symbol('in_array').rebased_addr  
in_array_size = 16

initial_state = proj.factory.blank_state(addr=main)
flag = [None] * in_array_size

for i in range(in_array_size):
    # Each char of the array is a 8 bit BitVector
    ch = initial_state.solver.BVS('ch{}'.format(i), 8)
    flag[i] = ch

    # Add constraints
    initial_state.solver.add(ch >= 0)    
    initial_state.solver.add(ch < 16)

    # Store BV to memory
    initial_state.memory.store(in_array_addr+i, ch)


# Create a Simulation manager from the current state
sm = proj.factory.simulation_manager(initial_state)

# Find a path to good while avoiding bad
sm.explore(find=good, avoid=bad)

print("No. of solutions found:", len(sm.found))

if len(sm.found) > 0:        
    # Considering the first goal state
    goal_state = sm.found[0]       

    print([goal_state.solver.eval(d) for d in flag])

Output

user@ec03a79cf15f$ python solver.py
WARNING | 2019-07-06 10:29:07,128 | angr.state_plugins.symbolic_memory | The program is accessing memory or registers with an unspecified value. This could indicate unwanted behavior.
WARNING | 2019-07-06 10:29:07,128 | angr.state_plugins.symbolic_memory | angr will cope with this by generating an unconstrained symbolic variable and continuing. You can resolve this by:
WARNING | 2019-07-06 10:29:07,129 | angr.state_plugins.symbolic_memory | 1) setting a value to the initial state
WARNING | 2019-07-06 10:29:07,129 | angr.state_plugins.symbolic_memory | 2) adding the state option ZERO_FILL_UNCONSTRAINED_{MEMORY,REGISTERS}, to make unknown regions hold null
WARNING | 2019-07-06 10:29:07,129 | angr.state_plugins.symbolic_memory | 3) adding the state option SYMBOL_FILL_UNCONSTRAINED_{MEMORY_REGISTERS}, to suppress these messages.
WARNING | 2019-07-06 10:29:07,129 | angr.state_plugins.symbolic_memory | Filling memory at 0x7fff0000 with 4 unconstrained bytes referenced from 0x8048532 (main+0x7 in chall (0x8048532))
WARNING | 2019-07-06 10:29:07,131 | angr.state_plugins.symbolic_memory | Filling register ebp with 4 unconstrained bytes referenced from 0x8048535 (main+0xa in chall (0x8048535))
WARNING | 2019-07-06 10:29:07,380 | angr.state_plugins.symbolic_memory | Filling register ebx with 4 unconstrained bytes referenced from 0x8048567 (M+0x3 in chall (0x8048567))
No. of solutions found: 1
[9, 8, 7, 2, 11, 15, 13, 10, 6, 5, 14, 4, 3, 0, 12, 1]

Using the following as the contents of in_array solves the challenge.

[9, 8, 7, 2, 11, 15, 13, 10, 6, 5, 14, 4, 3, 0, 12, 1]
5
  • 1
    @Iddo I see. But this is the solution angr came up with. Maybe some other changes need to be made. Sharing the original challenge binary would be great. – 0xec Jul 5 '19 at 6:43
  • @Iddo Check updated answer – 0xec Jul 6 '19 at 9:40
  • The 17 was on purpose >< honeyput, thanks mate, u deserve more than the +50 – i.e. Jul 6 '19 at 11:08
  • @Iddo Thanks. Angr would still find a solution with < 17 . 10, 8, 7, 2, 12, 16, 14, 11, 6, 5, 15, 4, 3, 0, 13, 1 but this is not correct as far as the original challenge is concerned. – 0xec Jul 6 '19 at 11:26
  • I have another related question hopefully you can help reverseengineering.stackexchange.com/questions/25571/… – i.e. Jul 29 '20 at 12:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.