Solve an angr function with string parameters

Question

Look at this C code:

#include <stdio.h>
#include <string.h>

int my_function(char *s);

int my_function(char *s)
{
    for (int i=0;i<strlen(s);i++)
    {
       s[i]++;
    }
    if (strncmp(s,"b{fsuz",6)==0)
    {
       return 1; 
    }
    return 0;
}


int main(int argc , char *argv[])
{
    // Lot of stuff, including UI
    if (my_function(argv[1])==1)
    {
        printf("Good\n");
    }
    else
    {
        printf("Wrong !\n");
    }
    return 0;
}

What i want to do is to make a symbolic analysis on my_function (and only this function) with angr.

Here is the function disassembly:

|           ; var int local_28h @ rbp-0x28
|           ; var int local_14h @ rbp-0x14
|           ; CALL XREF from 0x000011e7 (main)
|           0x00001155      55             push rbp
|           0x00001156      4889e5         mov rbp, rsp
|           0x00001159      53             push rbx
|           0x0000115a      4883ec28       sub rsp, 0x28               ; '('
|           0x0000115e      48897dd8       mov qword [local_28h], rdi
|           0x00001162      c745ec000000.  mov dword [local_14h], 0
|       ,=< 0x00001169      eb19           jmp 0x1184
|      .--> 0x0000116b      8b45ec         mov eax, dword [local_14h]
|      :|   0x0000116e      4863d0         movsxd rdx, eax
|      :|   0x00001171      488b45d8       mov rax, qword [local_28h]
|      :|   0x00001175      4801d0         add rax, rdx                ; '('
|      :|   0x00001178      0fb610         movzx edx, byte [rax]
|      :|   0x0000117b      83c201         add edx, 1
|      :|   0x0000117e      8810           mov byte [rax], dl
|      :|   0x00001180      8345ec01       add dword [local_14h], 1
|      :|   ; JMP XREF from 0x00001169 (sym.my_function)
|      :`-> 0x00001184      8b45ec         mov eax, dword [local_14h]
|      :    0x00001187      4863d8         movsxd rbx, eax
|      :    0x0000118a      488b45d8       mov rax, qword [local_28h]
|      :    0x0000118e      4889c7         mov rdi, rax
|      :    0x00001191      e8bafeffff     call sym.imp.strlen         ; size_t strlen(const char *s)
|      :    0x00001196      4839c3         cmp rbx, rax
|      `==< 0x00001199      72d0           jb 0x116b
|           0x0000119b      488b45d8       mov rax, qword [local_28h]
|           0x0000119f      ba06000000     mov edx, 6
|           0x000011a4      488d35590e00.  lea rsi, str.b_fsuz         ; 0x2004 ; "b{fsuz"
|           0x000011ab      4889c7         mov rdi, rax
|           0x000011ae      e87dfeffff     call sym.imp.strncmp        ; int strncmp(const char *s1, const char *s2, size_t n)
|           0x000011b3      85c0           test eax, eax
|       ,=< 0x000011b5      7507           jne 0x11be
|       |   0x000011b7      b801000000     mov eax, 1
|      ,==< 0x000011bc      eb05           jmp 0x11c3
|      |`-> 0x000011be      b800000000     mov eax, 0
|      |    ; JMP XREF from 0x000011bc (sym.my_function)
|      `--> 0x000011c3      4883c428       add rsp, 0x28               ; '('
|           0x000011c7      5b             pop rbx
|           0x000011c8      5d             pop rbp
\           0x000011c9      c3             ret

What i want is to ask angr: Which string should i pass in parameter to my_function in order to get a return of 1.

Here is what i've done:

import angr

base = 0x400000
function_start = base + 0x00001155 # 0x0000115e
function_target = base + 0x000011b7
function_end = base + 0x000011be

p = angr.Project("./a.out")
state = p.factory.blank_state(addr=function_start)
a = state.solver.BVS('a', 8*7)
# state.memory.store(state.regs.rbp-0x28,a)
state.memory.store(state.regs.rdi,a)

sm = p.factory.simulation_manager(state)
sm.explore(find=function_target, avoid=function_end)

found_path = sm.found[0]
print(found_path.state.se.any_str(a))

It displays "a{fsuz" but the good answer is "azerty".

What is wrong ?

Second question: why does angr not found anything if i put 0x00001156 address as function start ?

Thanks

Answer 1

I think you might have a couple of errors there.

First, and this one shouldn't be too critical, is that your start address is not the function's entry (at 0x00001155). That may have been your intention when you were writing the BVS to the stack, but it is unnecessary now.

The second and more critical issue is that the BVS a is 6 bytes long, while it should be 7 bytes long to include the null terminator value that is required for strings of 6 non-null characters for angr's strlen implementation to function properly.

Answer 2

There is a problem in how you declare that string to angr. I started with your example code and checked if it works when I assign some address for the argument witch is checked. My best guess is that

state.memory.store(state.regs.rdi,a)

Does not do what you expect it to do. Here is the full solution (addresses may differ):

# coding: utf8
import angr

function_start = 0x400590
function_target = 0x400603
function_end = 0x400616
dummy_addr = 0x300000

p = angr.Project("./a.out")
state = p.factory.blank_state(addr=function_start)
a = state.solver.BVS('a', 8 * 7)
state.memory.store(dummy_addr, a)
state.regs.rdi = dummy_addr

sm = p.factory.simulation_manager(state)
sm.explore(find=function_target, avoid=function_end)

found_path = sm.found[0]
print found_path.state.se.eval(a, cast_to=bytes)

edit

stack solution as requested

Please note my variables are located at a different offset (clang/gcc)

# coding: utf8
import angr

function_start = 0x40059c
function_target = 0x400603
function_end = 0x400616
dummy_addr = 0x300000

p = angr.Project("./a.out")
state = p.factory.blank_state(addr=function_start)
a = state.solver.BVS('a', 8 * 7)
state.memory.store(dummy_addr, a)
state.mem[state.regs.rbp-0x10].uint64_t = dummy_addr

sm = p.factory.simulation_manager(state)
sm.explore(find=function_target, avoid=function_end)

found_path = sm.found[0]
print found_path.state.se.eval(a, cast_to=bytes)