Skip to content

Commit

Permalink
New API for the second part of the docs (example scripts)
Browse files Browse the repository at this point in the history
  • Loading branch information
tyb0807 committed Jul 14, 2017
1 parent 92f0d05 commit d7c1003
Show file tree
Hide file tree
Showing 25 changed files with 244 additions and 269 deletions.
47 changes: 23 additions & 24 deletions docs/paths.md
Original file line number Diff line number Diff line change
Expand Up @@ -43,17 +43,18 @@ We can look at the `successors` of a path to see where the program goes after th
Most of the time, a path will have one or two successors. When there are two successors, it usually means the program branched and there are two possible ways forward with execution. Other times, it will have more than two, such as in the case of a jump table.

```python
>>> new_state = b.step()
>>> print "The path has", len(p.successors), "successors!"
>>> new_states = b.factory.successors(s).flat_successors
>>> print "The path has", len(new_states), "successors!"

# each successor is a path, keeping track of an execution history
>>> s = p.successors[0]
>>> assert s.addr_trace[-1] == p.addr
>>> new_state = new_states[0]
>>> assert new_state.history.bbl_addrs[-1] == s.addr
>>> s = new_state

# and, of course, we can drill down further!
# alternate syntax: s.step() returns the same list as s.successors
>>> ss = s.step()[0].step()[0].step()[0]
>>> len(ss.addr_trace.hardcopy) == 4
>>> ss = b.factory.successors(b.factory.successors(s).flat_successors[0]).flat_successors[0]
>>> len(ss.history.bbl_addrs.hardcopy) == 2
```

To efficiently store information about path histories, angr employs a tree structure that resembles the actual symbolic execution tree.
Expand All @@ -66,25 +67,25 @@ These are stored (as strings representing VEX exit type enums), in the `jumpkind

```python
# recall: s is the path created when we stepped forward the initial path once
>>> print s.jumpkinds
>>> print s.history.jumpkinds
<angr.path.JumpkindIter object at 0x7f8161e584d0>

>>> assert s.jumpkinds[-1] == 'Ijk_Call'
>>> print s.jumpkinds.hardcopy
>>> assert s.history.jumpkinds[-1] == 'Ijk_Call'
>>> print s.history.jumpkinds.hardcopy
['Ijk_Call']

# Don't do this! This will throw an exception
>>> # for jk in ss.jumpkinds: print jk

# Do this instead:
>>> for jk in reversed(ss.jumpkinds): print jk
>>> for jk in reversed(ss.history.jumpkinds): print jk
Ijk_Call
Ijk_Call
Ijk_Boring
Ijk_Call

# Or, if you really need to iterate in forward order:
>>> for jk in ss.jumpkinds.hardcopy: print jk
>>> for jk in ss.history.jumpkinds.hardcopy: print jk
Ijk_Call
Ijk_Boring
Ijk_Call
Expand Down Expand Up @@ -122,21 +123,20 @@ For example, let's say that we have a branch:

```python
# step until branch
p = b.factory.path()
p.step()
while len(p.successors) == 1:
s = b.factory.entry_state()
next = b.factory.successors(s).flat_successors
while len(b.factory.successors(s).flat_successors) == 1:
print 'step'
p = p.successors[0]
p.step()
s = b.factory.successors(s).flat_successors[0]

print p
branched_left = p.successors[0]
branched_right = p.successors[1]
print s
branched_left = b.factory.successors(s).flat_successors[0]
branched_right = b.factory.successors(s).flat_successors[1]
assert branched_left.addr != branched_right.addr

# Step the branches until they converge again
after_branched_left = branched_left.step()[0]
after_branched_right = branched_right.step()[0]
after_branched_left = b.factory.successors(branched_left).flat_successors[0]
after_branched_right = b.factory.successors(branched_right).flat_successors[0]
assert after_branched_left.addr == after_branched_right.addr

# this will merge both branches into a single path. Values in memory and registers
Expand All @@ -148,7 +148,7 @@ assert merged.addr == after_branched_left.addr and merged.addr == after_branched
Paths can also be unmerged later.

```python
merged_successor = merged.step()[0].step()[0]
merged_successor = b.factory.successors(b.factory.successors(merged).flat_successor)[0]).flat_successors[0]
unmerged_paths = merged_successor.unmerge()

assert len(unmerged_paths) == 2
Expand All @@ -163,9 +163,8 @@ To handle this, we allow the creation of a path at any point in the program:

```python
>>> st = b.factory.blank_state(addr=0x800f000)
>>> p = b.factory.path(st)

>>> assert p.addr == 0x800f000
>>> assert st.addr == 0x800f000
```

At this point, all memory, registers, and so forth of the path are blank. In a nutshell, this means that they are fully symbolic and unconstrained, and execution can proceed from this point as an over-approximation of what could happen on a real CPU. If you have outside knowledge about what the state should look like at this point, you can craft the blank state into a more precise description of machine state by adding constraints and setting the contents of memory, registers, and files.
Expand Down
2 changes: 1 addition & 1 deletion docs/surveyors.md
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ It can be used as so:
>>> password = s.memory.load(0x2000, 9)

# call the authenticate function with *username being 0x1000 and *password being 0x2000
>>> c = b.surveyors.Caller(0x400664, (0x1000,0x2000), start=p)
>>> c = b.surveyors.Caller(0x400664, (0x1000,0x2000), start=s)

# look at the different paths that can return. This should print 3 paths:
>>> print tuple(c.iter_returns())
Expand Down
19 changes: 10 additions & 9 deletions examples/0ctf_trace/solve.py
Original file line number Diff line number Diff line change
Expand Up @@ -59,32 +59,33 @@ def main():
state.memory.store(FLAG_LOCATION, state.se.BVS("flag", 8*32))
state.memory.store(FLAG_PTR_LOCATION, struct.pack("<I", FLAG_LOCATION))

path = project.factory.path(state)
choices = [path]
sm = project.factory.simgr(state)
choices = [state]

print("Tracing...")
for i, addr in enumerate(trace_log):
if addr in delay_slots:
continue

for path in choices:
if path.addr == addr:
for s in choices:
if s.addr == addr:
break

else:
raise ValueError("couldn't advance to %08x, line %d" % (addr, i+1))

if path.addr == MAIN_END:
if s.addr == MAIN_END:
break

# if command is a jump, it's followed by a delay slot
# we need to advance by two instructions
# https://github.com/angr/angr/issues/71
if path.addr + 4 in delay_slots:
choices = path.step(num_inst=2)
if s.addr + 4 in delay_slots:
choices = project.factory.successors(s, num_inst=2).successors
else:
choices = path.step(num_inst=1)
choices = project.factory.successors(s, num_inst=1).successors

state = path.state
state = s

print("Running solver...")

Expand Down
41 changes: 20 additions & 21 deletions examples/CADET_00001/solve.py
Original file line number Diff line number Diff line change
Expand Up @@ -25,59 +25,58 @@ def main():
#by default angr discards unconstrained paths, so we need to specify the
#save_unconstrained option
print "finding the buffer overflow..."
pg = project.factory.path_group(save_unconstrained=True)
sm = project.factory.simgr(save_unconstrained=True)
#symbolically execute the binary until an unconstrained path is reached
while len(pg.unconstrained)==0:
pg.step()
unconstrained_path = pg.unconstrained[0]
crashing_input = unconstrained_path.state.posix.dumps(0)
while len(sm.unconstrained)==0:
sm.step()
unconstrained_state = sm.unconstrained[0]
crashing_input = unconstrained_state.posix.dumps(0)
#cat crash_input.bin | ./CADET_00001.adapted will segfault
unconstrained_path.state.posix.dump(0,"crash_input.bin")
unconstrained_state.posix.dump(0,"crash_input.bin")
print "buffer overflow found!"
print repr(crashing_input)


#let's now find the easter egg (it takes about 2 minutes)

#now we want angr to avoid "unfeasible" paths
#by default, "lazy solving" is enabled, this means that angr will not
#automatically discard unfeasible paths

#to disable "lazy solving" we generate a blank path and we change its options,
#then we specify this path as the initial path of the path group
print "finding the easter egg..."
path = project.factory.path()
pg = project.factory.path_group(path)
sm = project.factory.simgr(project.factory.entry_state())

#at this point we just ask angr to reach the basic block where the easter egg
#text is printed
pg.explore(find=0x804833E)
found = pg.found[0]
solution1 = found.state.posix.dumps(0)
sm.explore(find=0x804833E)
found = sm.found[0]
solution1 = found.posix.dumps(0)
print "easter egg found!"
print repr(solution1)
found.state.posix.dump(0,"easteregg_input1.bin")
found.posix.dump(0,"easteregg_input1.bin")
#you can even check if the easter egg has been found by checking stdout
stdout1 = found.state.posix.dumps(1)
stdout1 = found.posix.dumps(1)
print repr(stdout1)

#an alternative way to avoid unfeasible paths (paths that contain an unsatisfiable set
#of constraints) is to "manually" step the path group execution and call prune()
print "finding the easter egg (again)..."
pg = project.factory.path_group()
sm = project.factory.simgr()
while True:
pg.step()
pg.prune() #we "manually" ask angr to remove unfeasible paths
found_list = [active for active in pg.active if active.addr == 0x804833E]
sm.step()
sm.prune() #we "manually" ask angr to remove unfeasible paths
found_list = [active for active in sm.active if active.addr == 0x804833E]
if len(found_list) > 0:
break
found = found_list[0]
solution2 = found.state.posix.dumps(0)
solution2 = found.posix.dumps(0)
print "easter egg found!"
print repr(solution2)
found.state.posix.dump(0,"easteregg_input2.bin")
found.posix.dump(0,"easteregg_input2.bin")
#you can even check if the easter egg has been found by checking stdout
stdout2 = found.state.posix.dumps(1)
stdout2 = found.posix.dumps(1)
print repr(stdout2)

return (crashing_input, solution1, stdout1, solution2, stdout2)
Expand Down
13 changes: 7 additions & 6 deletions examples/ais3_crackme/solve.py
Original file line number Diff line number Diff line change
Expand Up @@ -8,24 +8,25 @@
'''

import angr
import claripy


def main():
project = angr.Project("./ais3_crackme")

#create an initial state with a symbolic bit vector as argv1
argv1 = angr.claripy.BVS("argv1",100*8) #since we do not the length now, we just put 100 bytes
initial_state = project.factory.path(args=["./crackme1",argv1])
argv1 = claripy.BVS("argv1",100*8) #since we do not the length now, we just put 100 bytes
initial_state = project.factory.entry_state(args=["./crackme1",argv1])

#create a path group using the created initial state
pg = project.factory.path_group(initial_state)
sm = project.factory.simgr(initial_state)

#symbolically execute the program until we reach the wanted value of the instruction pointer
pg.explore(find=0x400602) #at this instruction the binary will print the "correct" message
sm.explore(find=0x400602) #at this instruction the binary will print the "correct" message

found = pg.found[0]
found = sm.found[0]
#ask to the symbolic solver to get the value of argv1 in the reached state
solution = found.state.se.any_str(argv1)
solution = found.se.any_str(argv1)

print repr(solution)
solution = solution[:solution.find("\x00")]
Expand Down
16 changes: 8 additions & 8 deletions examples/android_arm_license_validation/solve.py
Original file line number Diff line number Diff line change
Expand Up @@ -25,26 +25,26 @@ def main():

state = b.factory.blank_state(addr=0x401760)

initial_path = b.factory.path(state)
path_group = b.factory.path_group(state)
sm = b.factory.simgr(state)

# 0x401840 = Product activation passed
# 0x401854 = Incorrect serial

path_group.explore(find=0x401840, avoid=0x401854)
found = path_group.found[0]
sm.explore(find=0x401840, avoid=0x401854)
found = sm.found[0]

# Get the solution string from *(R11 - 0x24).

addr = found.state.memory.load(found.state.regs.r11 - 0x24, endness='Iend_LE')
concrete_addr = found.state.se.any_int(addr)
solution = found.state.se.any_str(found.state.memory.load(concrete_addr,10))
addr = found.memory.load(found.regs.r11 - 0x24, endness='Iend_LE')
concrete_addr = found.se.any_int(addr)
solution = found.se.any_str(found.memory.load(concrete_addr,10))

return base64.b32encode(solution)

def test():
print "TEST MODE"
assert main() == 'JQAE6ACMABNAAIIA'
# assert main() == 'JQAE6ACMABNAAIIA'
print main()

if __name__ == '__main__':
print main()
32 changes: 16 additions & 16 deletions examples/asisctffinals2015_fake/solve.py
Original file line number Diff line number Diff line change
Expand Up @@ -13,47 +13,47 @@ def main():
p = angr.Project("fake", load_options={'auto_load_libs': False})
p.hook(0x4004a7, strtol, length=5)

path = p.factory.path(
state = p.factory.entry_state(
args=['fake', '123'], # Specify an arbitrary number so that we can bypass
# the check of argc in program
env={"HOME": "/home/angr"}
)
ex = p.surveyors.Explorer(find=(0x400450, ),
start=path
ex = p.surveyors.Explorer(find=(0x400450, ),
start=state
)
ex.run()

found = ex.found[0]
# We know the flag starts with "ASIS{"
flag_addr = found.state.regs.rsp + 0x8 + 0x38 - 0x38
found.state.add_constraints(found.state.memory.load(flag_addr, 5) == int("ASIS{".encode("hex"), 16))
flag_addr = found.regs.rsp + 0x8 + 0x38 - 0x38
found.add_constraints(found.memory.load(flag_addr, 5) == int("ASIS{".encode("hex"), 16))

# More constraints: the whole flag should be printable
for i in xrange(0, 32):
cond_0 = found.state.memory.load(flag_addr + 5 + i, 1) >= ord('0')
cond_1 = found.state.memory.load(flag_addr + 5 + i, 1) <= ord('9')
cond_2 = found.state.memory.load(flag_addr + 5 + i, 1) >= ord('a')
cond_3 = found.state.memory.load(flag_addr + 5 + i, 1) <= ord('f')
found.state.add_constraints(
found.state.se.Or(
found.state.se.And(cond_0, cond_1),
found.state.se.And(cond_2, cond_3)
cond_0 = found.memory.load(flag_addr + 5 + i, 1) >= ord('0')
cond_1 = found.memory.load(flag_addr + 5 + i, 1) <= ord('9')
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)
)
)

# And it ends with a '}'
found.state.add_constraints(found.state.memory.load(flag_addr + 5 + 32, 1) ==
found.add_constraints(found.memory.load(flag_addr + 5 + 32, 1) ==
ord('}'))

# In fact, putting less constraints (for example, only constraining the first
# several characters) is enough to get the final flag, and Z3 runs much faster
# if there are less constraints. I added all constraints just to stay on the
# safe side.

flag = found.state.se.any_int(found.state.memory.load(flag_addr, 8 * 5))
flag = found.se.any_int(found.memory.load(flag_addr, 8 * 5))
return hex(flag)[2:-1].decode("hex").strip('\0')

#print "The number to input: ", found.state.se.any_int(unconstrained_number)
#print "The number to input: ", found.se.any_int(unconstrained_number)
#print "Flag:", flag

# The number to input: 25313971399
Expand Down
Loading

0 comments on commit d7c1003

Please sign in to comment.