Use claripy ops from claripy instead of solver

examples/asisctffinals2015_fake/solve.py

@@ -1,11 +1,13 @@
-import angr
 import binascii
 
+import angr
+import claripy
+
 def main():
     p = angr.Project("fake", auto_load_libs=False)
 
     state = p.factory.blank_state(addr=0x4004AC)
-    inp = state.solver.BVS('inp', 8*8)
+    inp = claripy.BVS('inp', 8*8)
     state.regs.rax = inp
 
     simgr= p.factory.simulation_manager(state)
@@ -23,9 +25,9 @@ def main():
         cond_1 = flag.get_byte(i) <= ord('9')
         cond_2 = flag.get_byte(i) >= ord('a')
         cond_3 = flag.get_byte(i) <= ord('f')
-        cond_4 = found.solver.And(cond_0, cond_1)
-        cond_5 = found.solver.And(cond_2, cond_3)
-        found.add_constraints(found.solver.Or(cond_4, cond_5))
+        cond_4 = claripy.And(cond_0, cond_1)
+        cond_5 = claripy.And(cond_2, cond_3)
+        found.add_constraints(claripy.Or(cond_4, cond_5))
 
     # And it ends with a '}'
     found.add_constraints(flag.get_byte(32+5) == ord('}'))

examples/asisctffinals2015_license/solve.py

@@ -20,12 +20,12 @@ def main():
     for i in range(5):
         line = [ ]
         for j in range(6):
-            line.append(state.solver.BVS('license_file_byte_%d_%d' % (i, j), 8))
+            line.append(claripy.BVS('license_file_byte_%d_%d' % (i, j), 8))
             state.add_constraints(line[-1] != b'\n')
         if bytestring is None:
             bytestring = claripy.Concat(*line)
         else:
-            bytestring = bytestring.concat(state.solver.BVV(b'\n'), *line)
+            bytestring = bytestring.concat(claripy.BVV(b'\n'), *line)
 
     license_file = angr.storage.file.SimFile(license_name, bytestring)
     state.fs.insert(license_name, license_file)

examples/cmu_binary_bomb/solve.py

@@ -11,7 +11,7 @@ def run(self):
 
 class strtol_hook(angr.SimProcedure):
     def run(self, str, end, base):
-        return self.state.solver.BVS("flag", 64, explicit_name=True)
+        return claripy.BVS("flag", 64, explicit_name=True)
 
 def solve_flag_1():
 
@@ -32,7 +32,7 @@ def solve_flag_1():
     state = proj.factory.blank_state(addr=start)
 
     # a symbolic input string with a length up to 128 bytes
-    arg = state.solver.BVS("input_string", 8 * 128)
+    arg = claripy.BVS("input_string", 8 * 128)
 
     # read_line() reads a line from stdin and stores it a this address
     bind_addr = 0x603780
@@ -65,7 +65,7 @@ def solve_flag_2():
     # Sscanf is looking for '%d %d %d %d %d %d' which ends up dropping 6 ints onto the stack
     # We will create 6 symbolic values onto the stack to mimic this
     for i in range(6):
-        state.stack_push(state.solver.BVS('int{}'.format(i), 4*8))
+        state.stack_push(claripy.BVS('int{}'.format(i), 4*8))
 
     # Attempt to find a path to the end of the phase_2 function while avoiding the bomb_explode
     ex = proj.factory.simulation_manager(state)
@@ -147,8 +147,8 @@ def solve_flag_4():
     state = proj.factory.blank_state(addr=start)
 
     # insert variables by ourselves
-    var1 = state.solver.BVS('var1', 8*4)
-    var2 = state.solver.BVS('var2', 8*4)
+    var1 = claripy.BVS('var1', 8*4)
+    var2 = claripy.BVS('var2', 8*4)
     state.memory.store(state.regs.rsp+0x18-0x10, var1, endness='Iend_BE')
     state.memory.store(state.regs.rsp+0x18-0xc, var2, endness='Iend_BE')
 
@@ -165,11 +165,11 @@ def solve_flag_5():
     def is_alnum(state, c):
         # set some constraints on the char, let it
         # be a null char or alphanumeric
-        is_num = state.solver.And(c >= ord("0"), c <= ord("9"))
-        is_alpha_lower = state.solver.And(c >= ord("a"), c <= ord("z"))
-        is_alpha_upper = state.solver.And(c >= ord("A"), c <= ord("Z"))
+        is_num = claripy.And(c >= ord("0"), c <= ord("9"))
+        is_alpha_lower = claripy.And(c >= ord("a"), c <= ord("z"))
+        is_alpha_upper = claripy.And(c >= ord("A"), c <= ord("Z"))
         is_zero = (c == ord('\x00'))
-        isalphanum = state.solver.Or(
+        isalphanum = claripy.Or(
             is_num, is_alpha_lower, is_alpha_upper, is_zero)
         return isalphanum
 
@@ -211,7 +211,7 @@ class read_6_ints(angr.SimProcedure):
     def run(self, s1_addr, int_addr):
         self.int_addrs.append(int_addr)
         for i in range(6):
-            bvs = self.state.solver.BVS("phase6_int_%d" % i, 32)
+            bvs = claripy.BVS("phase6_int_%d" % i, 32)
             self.answer_ints.append(bvs)
             self.state.mem[int_addr].int.array(6)[i] = bvs
 
@@ -264,7 +264,7 @@ def solve_secret():
     sm.explore(find=find, avoid=avoid)
     ### flag found
     found = sm.found[0]
-    flag = found.solver.BVS("flag", 64, explicit_name="True")
+    flag = claripy.BVS("flag", 64, explicit_name="True")
     return str(found.solver.eval(flag))
 
 def main():

examples/csgames2018/solve.py

@@ -51,10 +51,10 @@ def wrong(state):
     # At this point, we've actually found "correct" flags, but they contain symbols that probably aren't on all keyboards. Ideally we only want to find alphanumeric keys.
 
     def is_alphanumeric(state, byte):
-        is_num = state.solver.And(byte >= b"0", byte <= b"9")
-        is_alpha_lower = state.solver.And(byte >= b"a", byte <= b"z")
-        is_alpha_upper = state.solver.And(byte >= b"A", byte <= b"Z")
-        return state.solver.Or(is_num, is_alpha_lower, is_alpha_upper)
+        is_num = claripy.And(byte >= b"0", byte <= b"9")
+        is_alpha_lower = claripy.And(byte >= b"a", byte <= b"z")
+        is_alpha_upper = claripy.And(byte >= b"A", byte <= b"Z")
+        return claripy.Or(is_num, is_alpha_lower, is_alpha_upper)
 
     # XXXX-XX-XXX-XXXX
     for i in list(range(0, 4)) + list(range(5, 7)) + list(range(8, 11)) + list(range(12, 16)):

examples/defcon2017quals_crackme2000/enlightenment/solve_chicken.py

@@ -1,9 +1,9 @@
-
 import logging
 import sys
 
 import angr
 import capstone
+import claripy
 import r2pipe
 
 l = logging.getLogger('angr.manager').setLevel(logging.WARNING)
@@ -92,11 +92,11 @@ def solve(s):
 
         state = p.factory.blank_state(addr=check_func.addr, add_options={angr.options.LAZY_SOLVES, angr.options.NO_SYMBOLIC_JUMP_RESOLUTION})
 
-        char = state.solver.BVS("chr", 64)
+        char = claripy.BVS("chr", 64)
 
         # rsi is a2
-        state.regs.rsi = state.solver.BVV(0xd000000, 64)
-        state.memory.store(0xd000000 + 16, state.solver.BVV(0xd000040, 64), endness='Iend_LE')
+        state.regs.rsi = claripy.BVV(0xd000000, 64)
+        state.memory.store(0xd000000 + 16, claripy.BVV(0xd000040, 64), endness='Iend_LE')
         state.memory.store(0xd000040 + 8, char, endness='Iend_LE')
 
         sm = p.factory.simulation_manager(state)

examples/defcon2017quals_crackme2000/occult.py

@@ -3,6 +3,7 @@
 
 import angr
 import capstone
+import claripy
 import r2pipe
 
 l = logging.getLogger('angr.manager').setLevel(logging.WARNING)
@@ -100,12 +101,12 @@ def solve(s):
 
         state = p.factory.blank_state(addr=check_func.addr, add_options={angr.options.LAZY_SOLVES, angr.options.NO_SYMBOLIC_JUMP_RESOLUTION})
 
-        char = state.solver.BVS("chr", 64)
+        char = claripy.BVS("chr", 64)
 
         # rsi is a2
-        state.regs.rsi = state.solver.BVV(0xd000000, 64)
-        state.memory.store(0xd000000, state.solver.BVV(0xd000010, 64), endness='Iend_LE')
-        state.memory.store(0xd000010 + 16, state.solver.BVV(0xd000040, 64), endness='Iend_LE')
+        state.regs.rsi = claripy.BVV(0xd000000, 64)
+        state.memory.store(0xd000000, claripy.BVV(0xd000010, 64), endness='Iend_LE')
+        state.memory.store(0xd000010 + 16, claripy.BVV(0xd000040, 64), endness='Iend_LE')
         state.memory.store(0xd000040 + 8, char, endness='Iend_LE')
 
         sm = p.factory.simulation_manager(state)

examples/defcon2017quals_crackme2000/witchcraft.py

@@ -1,10 +1,10 @@
-
 import logging
 import sys
 
-l = logging.getLogger('angr.manager').setLevel(logging.DEBUG)
-
 import angr
+import claripy
+
+l = logging.getLogger('angr.manager').setLevel(logging.DEBUG)
 
 pos = 0xd000000
 
@@ -21,7 +21,7 @@ def recvuntil(sock, s):
 
 class Alloca(angr.SimProcedure):
     def run(self):
-        return self.state.solver.BVV(pos, 64)
+        return claripy.BVV(pos, 64)
 
 def solve(s):
     p = angr.Project("witchcraft_dist/%s" % s,

examples/ekopartyctf2015_rev100/solve.py

@@ -1,29 +1,30 @@
-
 # This challenge is super big, and it's impossible to solve with IDA alone.
-# However, we are sure that most of the code is just garbage - you can't have 
-# a 100-point challenge with that much non-garbage code. Therefore the idea is 
-# to use GDB along with hardware breakpoints to find out where each byte is 
-# verified, and then run that single part of code inside angr to solve the 
+# However, we are sure that most of the code is just garbage - you can't have
+# a 100-point challenge with that much non-garbage code. Therefore the idea is
+# to use GDB along with hardware breakpoints to find out where each byte is
+# verified, and then run that single part of code inside angr to solve the
 # password.
 
-from angr.procedures.stubs.UserHook import UserHook
 import angr
+import claripy
+from angr.procedures.stubs.UserHook import UserHook
+
 
 def prepare_state(state, known_passwords):
     state = state.copy()
     password = [ ]
     for i in range(0, len(known_passwords) + 1):
-        password.append(state.solver.BVS('password_%d' % i, 8))
+        password.append(claripy.BVS('password_%d' % i, 8))
         state.memory.store(0xd0000000 + i, password[-1])
 
     for i, char in enumerate(known_passwords):
         state.add_constraints(password[i] == ord(char))
-    state.memory.store(0x6a3b7c, state.solver.BVV(0, 32))
-    state.memory.store(0x6a3b80, state.solver.BVV(0, 32))
+    state.memory.store(0x6a3b7c, claripy.BVV(0, 32))
+    state.memory.store(0x6a3b80, claripy.BVV(0, 32))
 
     state.regs.rbp = 0xffffffff00000000
-    state.memory.store(state.regs.rbp-0x148, state.solver.BVV(0xd0000100, 64), endness=state.arch.memory_endness)
-    state.memory.store(state.regs.rbp-0x140, state.solver.BVV(0xd0000100, 64), endness=state.arch.memory_endness)
+    state.memory.store(state.regs.rbp-0x148, claripy.BVV(0xd0000100, 64), endness=state.arch.memory_endness)
+    state.memory.store(state.regs.rbp-0x140, claripy.BVV(0xd0000100, 64), endness=state.arch.memory_endness)
 
     return state, password
 

examples/ekopartyctf2016_rev250/solve.py

@@ -27,7 +27,7 @@
 
 def char(state, c):
     '''returns constraints s.t. c is printable'''
-    return state.solver.And(c <= '~', c >= ' ')
+    return claripy.And(c <= '~', c >= ' ')
 
 def main():
     p = angr.Project('FUck_binary', auto_load_libs=False)

examples/ekopartyctf2016_sokohashv2/solve.py

@@ -1,8 +1,9 @@
-import angr
-import sys
 import struct
 from itertools import combinations, product
 
+import angr
+import claripy
+
 # http://immunityservices.blogspot.com.ar/2016/11/solving-sokohashv20-full-of-angr-on.html
 
 WIN_HASH = bytes.fromhex("C03922D0206DC3A33016010D6C66936E953ABAB9000010AE805CE8463CBE9A2D")
@@ -126,7 +127,7 @@ def main():
         conds = []
         for p in coords:
             conds.append(p == var)
-        init.add_constraints(init.solver.Or(*conds))
+        init.add_constraints(claripy.Or(*conds))
 
     # each coordinate must be distinct
     for v1,v2 in combinations(variables, 2):
@@ -150,7 +151,7 @@ def main():
         expected.append((hex(addr), hex(value)))
     print("Expected is '%s'\n\n" % expected)
 
-    found.add_constraints(init.solver.And(*conds))
+    found.add_constraints(claripy.And(*conds))
 
     result = []
     hash_map = get_hash_map(hash_addr)

examples/flareon2015_2/solve.py

@@ -1,5 +1,6 @@
 #!/usr/bin/env python
 import angr
+import claripy
 
 def main():
     b = angr.Project("very_success", load_options={"auto_load_libs":False})
@@ -8,12 +9,12 @@ def main():
     # remove lazy solves since we don't want to explore unsatisfiable paths
     s = b.factory.blank_state(addr=0x401084)
     # set up the arguments on the stack
-    s.memory.store(s.regs.esp+12, s.solver.BVV(40, s.arch.bits))
+    s.memory.store(s.regs.esp+12, claripy.BVV(40, s.arch.bits))
     s.mem[s.regs.esp+8:].dword = 0x402159
     s.mem[s.regs.esp+4:].dword = 0x4010e4
     s.mem[s.regs.esp:].dword = 0x401064
     # store a symbolic string for the input
-    s.memory.store(0x402159, s.solver.BVS("ans", 8*40))
+    s.memory.store(0x402159, claripy.BVS("ans", 8*40))
     # explore for success state, avoiding failure
     sm = b.factory.simulation_manager(s)
     sm.explore(find=0x40106b, avoid=0x401072)

examples/flareon2015_5/solve.py

@@ -3,6 +3,7 @@
 http://0x0atang.github.io/reversing/2015/09/18/flareon5-concolic.html
 """
 import angr
+import claripy
 
 
 # Globals
@@ -41,7 +42,7 @@ def main():
     # Setup stack to simulate the state after which the "key.txt" is read
     state.regs.esi = LEN_PW
     for i in range(LEN_PW):
-        state.mem[ADDR_PW_ORI+i:].byte = state.solver.BVS('pw', 8)
+        state.mem[ADDR_PW_ORI+i:].byte = claripy.BVS('pw', 8)
 
     # Hook instructions to use a separate buffer for the XOR-ing function
     p.hook(0x401259, hook_duplicate_pw_buf, length=0)

examples/google2016_unbreakable_1/solve.py

@@ -16,6 +16,7 @@
 """
 
 import angr
+import claripy
 
 
 START_ADDR = 0x4005bd # first part of program that does computation
@@ -31,8 +32,8 @@ def extract_memory(state):
 
 def char(state, n):
     """Returns a symbolic BitVector and contrains it to printable chars for a given state."""
-    vec = state.solver.BVS('c{}'.format(n), 8, explicit_name=True)
-    return vec, state.solver.And(vec >= ord(' '), vec <= ord('~'))
+    vec = claripy.BVS('c{}'.format(n), 8, explicit_name=True)
+    return vec, claripy.And(vec >= ord(' '), vec <= ord('~'))
 
 def main():
     p = angr.Project('unbreakable', auto_load_libs=False)

examples/insomnihack_aeg/solve.py

@@ -1,9 +1,10 @@
+import logging
 import os
 import sys
-import angr
 import subprocess
-import logging
 
+import angr
+import claripy
 from angr import sim_options as so
 
 l = logging.getLogger("insomnihack.simple_aeg")
@@ -88,7 +89,7 @@ def main(binary):
     for buf_addr in find_symbolic_buffer(ep, len(shellcode)):
         l.info("found symbolic buffer at %#x", buf_addr)
         memory = ep.memory.load(buf_addr, len(shellcode))
-        sc_bvv = ep.solver.BVV(shellcode)
+        sc_bvv = claripy.BVV(shellcode)
 
         # check satisfiability of placing shellcode into the address
         if ep.satisfiable(extra_constraints=(memory == sc_bvv,ep.regs.pc == buf_addr)):

examples/java_simple3/solve.py

@@ -1,7 +1,8 @@
-
+import logging
 import os
+
 import angr
-import logging
+import claripy
 
 
 self_dir = os.path.dirname(os.path.realpath(__file__))
@@ -17,7 +18,7 @@ def test_java_simple3():
     state = simgr.deadended[0]
     # simple3.jar return the character after the inserted one
     # we constrain stdout to "c" and we expected stdin to be "b"
-    state.add_constraints(state.posix.stdout.content[0][0] == state.solver.BVV(ord(b"c"), 8))
+    state.add_constraints(state.posix.stdout.content[0][0] == claripy.BVV(ord(b"c"), 8))
     assert state.posix.stdin.concretize() == [b"b"]