# Using Angr's Claripy to bruteforce a number

I'm trying to bruteforce an address as part of a CTF challenge using Angr's Claripy. The function is the following:

``````unsigned __int64 __fastcall sub_555555555310(
unsigned __int64 const1,
unsigned __int64 const2)
{
unsigned __int64 v4;

v4 = 0LL;
while ( rand_addr )
{
if ( (rand_addr & 1) != 0 )
v4 = (const1 + v4) % const2;
const1 = 2 * const1 % const2;
}
return v4;
}
``````

where rand_addr is the address I'm trying to reverse. To be precise, I only need the lower half of the address (32 lower bits). I have v4, const1 and const2 values. This is what I've done so far with Claripy:

``````def do_op(rand, const1, const2):
v4 = claripy.BVV(0, 64)
b = claripy.BVV(0, 2)
#while(claripy.UGE(rand, 1)):
for i in range(64):
b = claripy.If(rand & 1 != 0, claripy.BVV(1,1), claripy.BVV(0,1))
v4 = claripy.If(b == 1, (const1 + v4) % const2, v4)
rand = claripy.If(b == 0, claripy.RotateRight(rand, 1), rand)
const1 = claripy.If(b == 0, 2 * const1 % const2, const1)
s.add(v4[31:0] == claripy.BVV(<some_value>, 32))
``````

Angr claims that this solver is unsat and I was wondering what am I doing wrong.

Thank you!

There are some problems with the way you write constraints in claripy. Here's a simple correction

``````import claripy
s = claripy.Solver()
const1 = claripy.BVS('const1', 64)
const2 = claripy.BVS('const2', 64)
rand = claripy.BVS('rand', 64)
v4 = claripy.BVS('v4', 64)
for i in range(64):
v4 = claripy.If(rand & 1 != 0, (const1 + v4) % const2, v4)
rand = rand >> 1
const1 = 2 * const1 % const2
print("check")
print(s.check_satisfiability())
``````

You don't need to check the `If` for every statement. In the original code it was used only to change v4. For `BVV`

Creates a bit-vector value (i.e., a concrete value).

For `BVS`

Creates a bit-vector symbol (i.e., a variable).

The C code shows right shift, not `RotateRight` so just use the `>>` operator since its been implemented with `__rshift__` in claripy.

Another thing to work on is to search for the constants used in `const1` and `const2` - you might get a standard function.

• Thank you so much! and sorry for the late reply. Jun 7 at 6:32