[angr] Using Claripy to find constraints on symbolic values

Cheng, Eric echeng at mitre.org
Fri Sep 23 11:26:10 PDT 2016


Hello,

I am trying to obtain the constraints and possible values of a symbolic variable using the min(), max(), and eval() methods from the Claripy Solver Engine.

I am using the source code shown below with a simple conditional branch where 'x' will be represented by a BVS. I can step through the code one instruction at a time. When taking one of the branches and then calling the three methods mentioned above on the symbolic value, the values are not what I am expecting. For example, if take the branch (x < 3), calling max() returns '4294967295' though I would expect it should return '2'. The result when calling eval() returns a set of very large numbers (4193278L, 4294967284L, 67092491L, 8190L, 4294967292L), when I would expect it to return (0, 1, 2). I am not sure if I am using Claripy correctly in this scenario.

Additionally, if I were to call the solver engine method "state.se.any_int(state.regs.r3)" on the branch where (x < 3), it returns '0', which is a correct value. The method seems to always return the smallest possible value for the specific branch. Is there a way to use this method to print out the bounds of the possible values?

Source Code compiled for ARM:

int main(int x) {
    if(x < 3) {
        return x;
    } else if (x < 5) {
        return x;
    }
}

Disassembly from Radare2:

/ (fcn) sym.main 76
|           0x00008d0c      04b02de5       str fp, [sp, -4]!
|           0x00008d10      00b08de2       add fp, sp, 0
|           0x00008d14      0cd04de2       sub sp, sp, 0xc
|           0x00008d18      08000be5       str r0, [fp - arg_8h]
|           0x00008d1c      08301be5       ldr r3, [fp - arg_8h]
|           0x00008d20      020053e3       cmp r3, 2
|       ,=< 0x00008d24      010000ca       bgt 0x8d30
|       |   0x00008d28      08301be5       ldr r3, [fp - arg_8h]
|      ,==< 0x00008d2c      050000ea       b 0x8d48
|      |`-> 0x00008d30      08301be5       ldr r3, [fp - arg_8h]
|      |    0x00008d34      040053e3       cmp r3, 4
|      |,=< 0x00008d38      010000ca       bgt 0x8d44
|      ||   0x00008d3c      08301be5       ldr r3, [fp - arg_8h]
|     ,===< 0x00008d40      000000ea       b 0x8d48
|    ,==`-> 0x00008d44      ffffffea       b 0x8d48
|    |||    ; JMP XREF from 0x00008d44 (sym.main)
|    |||    ; JMP XREF from 0x00008d40 (sym.main)
|    |||    ; JMP XREF from 0x00008d2c (sym.main)
|    ```--> 0x00008d48      0300a0e1       mov r0, r3
|           0x00008d4c      00d08be2       add sp, fp, 0
|           0x00008d50      0008bde8       ldm sp!, {fp}
\           0x00008d54      1eff2fe1       bx lr


Python Script:

import angr, claripy

proj = angr.Project('bvtestarm')
main = proj.loader.main_bin.get_symbol("main")
state = proj.factory.entry_state(addr=main.addr) # start at address of main
path = proj.factory.path(state)
pg = proj.factory.path_group(path)
s = claripy.Solver()
state.regs.r0 = claripy.BVS("symbolic", 32) # set x as a symbolic variable

for i in range(12):
     pg.step(num_inst=1) # step one instruction at a time
     pgList = [] # get list of active paths
     for i in range(len(pg.active)):
           pgList.append(pg.active[i].state)
     for state in pgList: # print out information for each active path
           print"-----------------------------------------------------"
           print "State address:", state.regs.pc
           print "Value in r3:", state.regs.r3
           print "Maximum possible value in r3:", s.max(state.regs.r3)
           print "Minimum possible value in r3:", s.min(state.regs.r3)
           print "Possible values in r3:", s.eval(state.regs.r3, 5)
           print "Solver engine for r3:", state.se.any_int(state.regs.r3)

Final Step Output:

-----------------------------------------------------
State address: <BV32 0x8d4c>
Value in r3: <BV32 symbolic_0_32>
Maximum possible value in r3: 4294967295
Minimum possible value in r3: 0
Possible values in r3: (4294950912L, 4160749568L, 536854529L, 134201345L, 268419073L)
Solver engine for r3: 1073741824
-----------------------------------------------------
State address: <BV32 0x8d48>
Value in r3: <BV32 symbolic_0_32>
Maximum possible value in r3: 4294967295
Minimum possible value in r3: 0
Possible values in r3: (4294950912L, 4160749568L, 536854529L, 134201345L, 268419073L)
Solver engine for r3: 4
-----------------------------------------------------
State address: <BV32 0x8d54>
Value in r3: <BV32 symbolic_0_32>
Maximum possible value in r3: 4294967295
Minimum possible value in r3: 0
Possible values in r3: (4294950912L, 4160749568L, 536854529L, 134201345L, 268419073L)
Solver engine for r3: 0
-----------------------------------------------------

Thanks in advance!

Eric
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cs.ucsb.edu/pipermail/angr/attachments/20160923/776374cd/attachment.html>


More information about the angr mailing list