[angr] Advice on Coping with Loops

Chris Salls chrissalls5 at gmail.com
Thu Sep 29 00:22:28 PDT 2016


Hi Berne,

This one seems pretty bad for symbolic execution, the path explosion is
pretty insane. I would be very impressed if a symbolic execution tool
solved it.

There are some ways to reduce path explosion. As you mentioned, veritesting
works in some cases, although here the explosion will likely still be too
much.
Other times a manual filtering or prioritization is your best bet. In some
cases a depth-first search type thing helps. Make sure to remove lazy
solves, this reduces path explosion at the cost of some extra solving.

However, with this one branching at every character, for 256 characters, I
would not expect symbolic execution to be able to handle it, without a lot
of help.
It kinda seems that many states will be similar, maybe there is some way
you can filter the ones that you've already seen? On one example I've seen
it was enough to filter any state with the same register values as a
previous state.

I was able to get it to work with constraining the 256 first characters and
disabling lazy solves. Here's the code I used:

import angr
proj = angr.Project("./vortex1")
s = proj.factory.entry_state()
s.add_constraints(s.posix.read_from(0,256)=="\\"*256)
s.posix.get_file(0).seek(0)
s.options.discard("LAZY_SOLVES")
pg = proj.factory.path_group(s)
pg.explore(find=0x804862C)
print pg.found[0].state.posix.dumps(0)

-Salls



On Mon, Sep 26, 2016 at 5:13 PM, Berne Campbell <berne.campbell at gmail.com>
wrote:

> Hello,
>
> After attending Defcon 24 I've become interested in Angr. As part of
> learning how to use it I've tried to write a solution to OverTheWire's
> Vortex Level 1, which I've already solved manually.
>
> http://overthewire.org/wargames/vortex/vortex1.html.
>
> I've attached the challenge's source and binary, my attempt at solving it
> (I've tried different things so the code is a bit all over the shop), and
> my old notes on the solution.
>
> My initial attempts would die do to Out of Memory (OOM) etc.
>
> I tried constraining the first 256 characters to backslashes to try to
> cheat a bit to give it a boost etc. but that still failed (it would need to
> find 6 more characters).
>
> I tried disabling lazy solves, so that it would be able to trim/collapse
> paths.
>
> I tried enabling veritesting etc.. I'm fairly new to SAT/SMT, etc. I tried
> reading some of the literature etc. which is where I learnt of the
> veriteting technique that might help. I found an angr example using the
> older style explore, I couldn't find a pathgroup style example but I worked
> it out from the API docs.
>
> I'm not sure if with my first use I've just stumbled on some pathological
> case where due to loops there' combinational explosion and it's hard or
> more likely I just don't grok the tool and techniques enough to be able to
> tune it correctly to work.
>
> I'd appreciate some tips, or hints, or even a basic solution.
>
> Also if you know of any users in Sydney Australia, I'd like host a  demo,
> workshop, and/or talk at Ruxmon Sydney. I think the tool is really cool,
> and I think this sort of thing is the future. Thanks for releasing it open
> source and I hope to get better.
>
> Cheers,
> Berne
>
>
>
> _______________________________________________
> angr mailing list
> angr at lists.cs.ucsb.edu
> https://lists.cs.ucsb.edu/mailman/listinfo/angr
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cs.ucsb.edu/pipermail/angr/attachments/20160929/43609584/attachment.html>


More information about the angr mailing list