It's spelled .solver

examples/0ctf_trace/solve.py

@@ -56,7 +56,7 @@ def main():
     })
 
     state = project.factory.blank_state(addr=MAIN_START)
-    state.memory.store(FLAG_LOCATION, state.se.BVS("flag", 8*32))
+    state.memory.store(FLAG_LOCATION, state.solver.BVS("flag", 8*32))
     state.memory.store(FLAG_PTR_LOCATION, struct.pack("<I", FLAG_LOCATION))
 
     sm = project.factory.simulation_manager(state)
@@ -89,7 +89,7 @@ def main():
 
     print("Running solver...")
 
-    solution = state.se.eval(state.memory.load(FLAG_LOCATION, 32), cast_to=str).rstrip(b'\0').decode('ascii')
+    solution = state.solver.eval(state.memory.load(FLAG_LOCATION, 32), cast_to=str).rstrip(b'\0').decode('ascii')
     print("The flag is", solution)
 
     return solution

examples/9447_nobranch/solve.py

@@ -45,22 +45,22 @@ def main():
             val = state.registers.load(reg_name)                                               # after each step, if the symbolic AST for that value has become larger than
             if val.symbolic and val.depth > 3:                                                      # three nodes deep, stub it out by replacing it with a single symbolic value
                 newval = claripy.BVS('replacement', len(val))                                       # constrained to be equal to the original value. This makes the constraints much
-                state.se.add(newval == val)                                                    # easier for z3 to bite into in smaller chunks. It might also indicate that there
+                state.solver.add(newval == val)                                                    # easier for z3 to bite into in smaller chunks. It might also indicate that there
                 state.registers.store(reg_name, newval)                                        # some issues with angr's current usage of z3 :-)
 
         for mem_addr in range(outaddr, outaddr + 0x1f) + [state.regs.rsp - x for x in xrange(0x40)]:
             val = state.memory.load(mem_addr, 1)
             if val.symbolic and val.depth > 3:
                 newval = claripy.BVS('replacement', len(val))
-                state.se.add(newval == val)
+                state.solver.add(newval == val)
                 state.memory.store(mem_addr, newval)
 
     fstate = state.copy()
-    fstate.se._solver.timeout = 0xfffffff                                                           # turn off z3's timeout for solving :^)
+    fstate.solver._solver.timeout = 0xfffffff                                                           # turn off z3's timeout for solving :^)
     for i, c in enumerate(shouldbe):
-        fstate.se.add(fstate.memory.load(0x616050 + i, 1) == ord(c))                                # constrain the output to what we were told it should be
+        fstate.solver.add(fstate.memory.load(0x616050 + i, 1) == ord(c))                                # constrain the output to what we were told it should be
 
-    cflag = hex(fstate.se.eval(flag))[2:-1].decode('hex')                                        # solve for the flag!
+    cflag = hex(fstate.solver.eval(flag))[2:-1].decode('hex')                                        # solve for the flag!
     return cflag
 
 def test():

examples/ais3_crackme/solve.py

@@ -26,7 +26,7 @@ def main():
 
     found = sm.found[0]
     #ask to the symbolic solver to get the value of argv1 in the reached state as a string
-    solution = found.se.eval(argv1, cast_to=str)
+    solution = found.solver.eval(argv1, cast_to=str)
 
     print repr(solution)
     solution = solution[:solution.find("\x00")]

examples/android_arm_license_validation/solve.py

@@ -36,8 +36,8 @@ def main():
     # Get the solution string from *(R11 - 0x24).
 
     addr = found.memory.load(found.regs.r11 - 0x24, endness='Iend_LE')
-    concrete_addr = found.se.eval(addr)
-    solution = found.se.eval(found.memory.load(concrete_addr,10), cast_to=str)
+    concrete_addr = found.solver.eval(addr)
+    solution = found.solver.eval(found.memory.load(concrete_addr,10), cast_to=str)
 
     return base64.b32encode(solution)
 

examples/asisctffinals2015_fake/solve.py

@@ -5,7 +5,7 @@
 def strtol(state):
     # We return an unconstrained number here
     global unconstrained_number
-    unconstrained_number = state.se.BVS('strtol', 64)
+    unconstrained_number = state.solver.BVS('strtol', 64)
     # Store it to rax
     state.regs.rax = unconstrained_number
 
@@ -35,9 +35,9 @@ def main():
         cond_2 = found.memory.load(flag_addr + 5 + i, 1) >= ord('a')
         cond_3 = found.memory.load(flag_addr + 5 + i, 1) <= ord('f')
         found.add_constraints(
-            found.se.Or(
-                found.se.And(cond_0, cond_1),
-                found.se.And(cond_2, cond_3)
+            found.solver.Or(
+                found.solver.And(cond_0, cond_1),
+                found.solver.And(cond_2, cond_3)
             )
         )
 
@@ -50,10 +50,10 @@ def main():
     # if there are less constraints. I added all constraints just to stay on the 
     # safe side.
 
-    flag = found.se.eval(found.memory.load(flag_addr, 8 * 5))
+    flag = found.solver.eval(found.memory.load(flag_addr, 8 * 5))
     return hex(flag)[2:-1].decode("hex").strip('\0')
 
-    #print "The number to input: ", found.se.eval(unconstrained_number)
+    #print "The number to input: ", found.solver.eval(unconstrained_number)
     #print "Flag:", flag
 
     # The number to input:  25313971399

examples/asisctffinals2015_license/solve.py

@@ -20,12 +20,12 @@ def main():
     for i in xrange(5):
         line = [ ]
         for j in xrange(6):
-            line.append(state.se.BVS('license_file_byte_%d_%d' % (i, j), 8))
+            line.append(state.solver.BVS('license_file_byte_%d_%d' % (i, j), 8))
             state.add_constraints(line[-1] != 0x0a)
         if bytes is None:
-            bytes = state.se.Concat(*line)
+            bytes = state.solver.Concat(*line)
         else:
-            bytes = state.se.Concat(bytes, state.se.BVV(0x0a, 8), *line)
+            bytes = state.solver.Concat(bytes, state.solver.BVV(0x0a, 8), *line)
     content = angr.state_plugins.SimSymbolicMemory(memory_id="file_%s" % license_name)
     content.set_state(state)
     content.store(0, bytes)
@@ -60,9 +60,9 @@ def main():
         )
     flag_length = strlen(found, arguments=[flag_addr]).ret_expr
     # In case it's not null-terminated, we get the least number as the length
-    flag_length_int = min(found.se.eval_upto(flag_length, 3))
+    flag_length_int = min(found.solver.eval_upto(flag_length, 3))
     # Read out the flag!
-    flag_int = found.se.eval(found.memory.load(flag_addr, flag_length_int))
+    flag_int = found.solver.eval(found.memory.load(flag_addr, flag_length_int))
     flag = hex(flag_int)[2:-1].decode("hex")
     return flag
 

examples/cmu_binary_bomb/solve.py

@@ -12,7 +12,7 @@ def run(self):
 
 class strtol_hook(angr.SimProcedure):
     def run(self, str, end, base):
-        return self.state.se.BVS("flag", 64, explicit_name=True)
+        return self.state.solver.BVS("flag", 64, explicit_name=True)
 
 def solve_flag_1():
 
@@ -29,7 +29,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.se.BVS("input_string", 8 * 128)
+    arg = state.solver.BVS("input_string", 8 * 128)
 
     # read_line() reads a line from stdin and stores it a this address
     bind_addr = 0x603780
@@ -48,7 +48,7 @@ def solve_flag_1():
 
     if ex.found:
         found = ex.found[0]
-        return found.se.eval(arg, cast_to=str).rstrip(chr(0)) # remove ending \0
+        return found.solver.eval(arg, cast_to=str).rstrip(chr(0)) # remove ending \0
 
     pass
 
@@ -63,7 +63,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 xrange(6):
-        state.stack_push(state.se.BVS('int{}'.format(i), 4*8))
+        state.stack_push(state.solver.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.surveyors.Explorer(start=state, find=(0x400f3c,),
@@ -77,7 +77,7 @@ def solve_flag_2():
         answer = []
 
         for x in xrange(3):
-            curr_int = found.se.eval(found.stack_pop())
+            curr_int = found.solver.eval(found.stack_pop())
 
             # We are popping off 8 bytes at a time
             # 0x0000000200000001
@@ -127,7 +127,7 @@ def solve_flag_3():
                 found = p
                 found.stack_pop() # ignore, our args start at offset 0x8
 
-                iter_sol = found.se.eval_upto(found.stack_pop(), 10) # ask for up to 10 solutions if possible
+                iter_sol = found.solver.eval_upto(found.stack_pop(), 10) # ask for up to 10 solutions if possible
                 for sol in iter_sol:
 
                     if sol == None:
@@ -163,7 +163,7 @@ def solve_flag_4():
     # stopped on the ret account for the stack
     # that has already been moved
 
-    answer = unpack('II', found.se.eval(
+    answer = unpack('II', found.solver.eval(
         found.memory.load(found.regs.rsp - 0x18 + 0x8, 8), cast_to=str))
 
     return ' '.join(map(str, answer))
@@ -174,11 +174,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.se.And(c >= ord("0"), c <= ord("9"))
-        is_alpha_lower = state.se.And(c >= ord("a"), c <= ord("z"))
-        is_alpha_upper = state.se.And(c >= ord("A"), c <= ord("Z"))
+        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_zero = (c == ord('\x00'))
-        isalphanum = state.se.Or(
+        isalphanum = state.solver.Or(
             is_num, is_alpha_lower, is_alpha_upper, is_zero)
         return isalphanum
 
@@ -204,9 +204,9 @@ def is_alnum(state, c):
     mem = found.memory.load(string_addr, 32)
     for i in xrange(32):
         found.add_constraints(is_alnum(found, mem.get_byte(i)))
-    return found.se.eval(mem, cast_to=str).split('\x00')[0]
+    return found.solver.eval(mem, cast_to=str).split('\x00')[0]
     # more than one solution could, for example, be returned like this:
-    # return map(lambda s: s.split('\x00')[0], found.se.eval_upto(mem, 10, cast_to=str))
+    # return map(lambda s: s.split('\x00')[0], found.solver.eval_upto(mem, 10, cast_to=str))
 
 
 class read_6_ints(angr.SimProcedure):
@@ -216,7 +216,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.se.BVS("phase6_int_%d" % i, 32)
+            bvs = self.state.solver.BVS("phase6_int_%d" % i, 32)
             self.answer_ints.append(bvs)
             self.state.mem[int_addr].int.array(6)[i] = bvs
 
@@ -234,7 +234,7 @@ def solve_flag_6():
     sm.explore(find=find, avoid=avoid)
     found = sm.found[0]
 
-    answer = [found.se.eval(x) for x in read_6_ints.answer_ints]
+    answer = [found.solver.eval(x) for x in read_6_ints.answer_ints]
     return ' '.join(map(str, answer))
 
 def solve_secret():
@@ -254,8 +254,8 @@ def solve_secret():
     sm.explore(find=find, avoid=avoid)
     ### flag found
     found = sm.found[0]
-    flag = found.se.BVS("flag", 64, explicit_name="True")
-    return str(found.se.eval(flag))
+    flag = found.solver.BVS("flag", 64, explicit_name="True")
+    return str(found.solver.eval(flag))
 
 def main():
 #   print "Flag    1: " + solve_flag_1()

examples/csaw_wyvern/solve.py

@@ -19,12 +19,12 @@ def main():
     # Constrain the first 28 bytes to be non-null and non-newline:
     for _ in xrange(28):
         k = st.posix.files[0].read_from(1)
-        st.se.add(k != 0)
-        st.se.add(k != 10)
+        st.solver.add(k != 0)
+        st.solver.add(k != 10)
 
     # Constrain the last byte to be a newline
     k = st.posix.files[0].read_from(1)
-    st.se.add(k == 10)
+    st.solver.add(k == 10)
 
     # Reset the symbolic stdin's properties and set its length.
     st.posix.files[0].seek(0)

examples/defcon2016quals_baby-re_1/solve.py

@@ -25,7 +25,7 @@ def main():
 
     def patch_scanf(state):
         print(state.regs.rsi)
-        state.mem[state.regs.rsi:].char = state.se.BVS('c', 8)
+        state.mem[state.regs.rsi:].char = state.solver.BVS('c', 8)
 
     # IDA xrefs
     scanf_offsets = (0x4d, 0x85, 0xbd, 0xf5, 0x12d, 0x165, 0x19d, 0x1d5, 0x20d, 0x245, 0x27d, 0x2b5, 0x2ed)
@@ -45,7 +45,7 @@ def patch_scanf(state):
 
     print(ex)
     s = ex.found[0]
-    flag = s.se.eval(s.memory.load(flag_addr, 50), cast_to=str)
+    flag = s.solver.eval(s.memory.load(flag_addr, 50), cast_to=str)
 
     # The flag is 'Math is hard!'
     print("The flag is '{0}'".format(flag))

examples/defcon2017quals_crackme2000/enlightenment/solve_chicken.py

@@ -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.se.BVS("chr", 64)
+        char = state.solver.BVS("chr", 64)
 
         # rsi is a2
-        state.regs.rsi = state.se.BVV(0xd000000, 64)
-        state.memory.store(0xd000000 + 16, state.se.BVV(0xd000040, 64), endness='Iend_LE')
+        state.regs.rsi = state.solver.BVV(0xd000000, 64)
+        state.memory.store(0xd000000 + 16, state.solver.BVV(0xd000040, 64), endness='Iend_LE')
         state.memory.store(0xd000040 + 8, char, endness='Iend_LE')
 
         sm = p.factory.simulation_manager(state)
@@ -106,7 +106,7 @@ def solve(s):
         for state in sm.deadended:
             if not state.satisfiable():
                 continue
-            char_n = state.se.eval_upto(char, 2)
+            char_n = state.solver.eval_upto(char, 2)
             if len(char_n) == 2:
                 continue
             the_char = char_n[0]

examples/defcon2017quals_crackme2000/occult.py

@@ -101,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.se.BVS("chr", 64)
+        char = state.solver.BVS("chr", 64)
 
         # rsi is a2
-        state.regs.rsi = state.se.BVV(0xd000000, 64)
-        state.memory.store(0xd000000, state.se.BVV(0xd000010, 64), endness='Iend_LE')
-        state.memory.store(0xd000010 + 16, state.se.BVV(0xd000040, 64), endness='Iend_LE')
+        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.memory.store(0xd000040 + 8, char, endness='Iend_LE')
 
         sm = p.factory.simulation_manager(state)
@@ -116,7 +116,7 @@ def solve(s):
         for state in sm.deadended:
             if not state.satisfiable():
                 continue
-            char_n = state.se.eval_upto(char, 2)
+            char_n = state.solver.eval_upto(char, 2)
             if len(char_n) == 2:
                 continue
             the_char = char_n[0]

examples/defcon2017quals_crackme2000/witchcraft.py

@@ -21,7 +21,7 @@ def recvuntil(sock, s):
 
 class Alloca(angr.SimProcedure):
     def run(self):
-        return self.state.se.BVV(pos, 64)
+        return self.state.solver.BVV(pos, 64)
 
 def solve(s):
     p = angr.Project("witchcraft_dist/%s" % s,
@@ -63,7 +63,7 @@ def solve(s):
 
     state = sm.deadended[-1]
     mem = state.memory.load(pos + 0x20, 60)
-    mem_str = state.se.eval(mem, cast_to=str).replace("\x00", "")
+    mem_str = state.solver.eval(mem, cast_to=str).replace("\x00", "")
     return mem_str
 
 def main():

examples/ekopartyctf2015_rev100/solve.py

@@ -13,17 +13,17 @@ def prepare_state(state, known_passwords):
     state = state.copy()
     password = [ ]
     for i in xrange(0, len(known_passwords) + 1):
-        password.append(state.se.BVS('password_%d' % i, 8))
+        password.append(state.solver.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.se.BVV(0, 32))
-    state.memory.store(0x6a3b80, state.se.BVV(0, 32))
+    state.memory.store(0x6a3b7c, state.solver.BVV(0, 32))
+    state.memory.store(0x6a3b80, state.solver.BVV(0, 32))
 
     state.regs.rbp = 0xffffffff00000000
-    state.memory.store(state.regs.rbp-0x148, state.se.BVV(0xd0000100, 64), endness=state.arch.memory_endness)
-    state.memory.store(state.regs.rbp-0x140, state.se.BVV(0xd0000100, 64), endness=state.arch.memory_endness)
+    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)
 
     return state, password
 
@@ -59,7 +59,7 @@ def calc_one_byte(p, known_passwords, hook_func, start_addr, load_addr1, load_ad
 
     s0 = sm.active[0].copy()
     s0.add_constraints(getattr(s0.regs, cmp_flag_reg) == 0x1)
-    candidates = s0.se.eval_upto(password[byte_pos], 256)
+    candidates = s0.solver.eval_upto(password[byte_pos], 256)
     # assert len(candidates) == 1
 
     return chr(candidates[0])