1

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 rand_addr,
        unsigned __int64 const1,
        unsigned __int64 const2)
{
  unsigned __int64 v4; 

  v4 = 0LL;
  while ( rand_addr )
  {
    if ( (rand_addr & 1) != 0 )
      v4 = (const1 + v4) % const2;
    rand_addr >>= 1;
    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!

1 Answer 1

1

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
s.add(v4 == 12345)
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.

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

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.