angr outputs killed

[leithon]

Dear all,

I took angr to symbolically execute an example in the veritesting paper,
after has run for about 1h 30m, angr outputs "killed".
What does it mean?

Thanks.

[rhelmot]

It probably means that your computer ran out of ram, and the angr process was killed by your operating system.

[leithon]

Many thanks for your reply.
I thought of another similar question.
As the SoK paper demonstrates, angr implements the dynamic symbolic execution as Mayhem.
To my knowledge, Mayhem set a checkpoint to check the number of executors. If the number of executors exceeds the configured number, then Mayhem will not fork to generate new executors.
I am wandering, could I set the number of maximum executors when running the DSE in angr?
Thanks.

[rhelmot]

It's been a while since I've read Mayhem, but this question is talking about concurrency in the symbolic executor, right?

angr does not use concurrency by default. This is because python code is very very hard to parallelize correctly. There is a threading mixin that you can enable for a path group with a defined number of worker threads, but this is only useful for paths that take a long time in the constraint solving phase, since only one thread can be running python code (as opposed to C code) at once due to the GIL. The code to enable this mixin is path_group.use_technique(angr.exploration_techniques.Threading(num_threads).

[leithon]

Sorry, I did mean the concurrency.

For the problem of ram exhausting I encountered, the reason should be the number of paths or states are very large, say path explosion.

To address the path explosion problem, Mayhem employs a checkpoint to check whether the number of states has exceeded the threshold. If so, Mayhem will not generate new paths or states. Instead, Mayhem will generate a concrete input and store it into the disk. Whenever the ram is not busy, then Mayhem reloads the concrete the input, and performs a trace-based dynamic symbolic execution.

As the demonstration in the paper of Mayhem, there should not be the problem of space explosion as I encountered, with the cost that Mayhem may run a long time.

Is my understanding right?

[rhelmot]

I can't comment on your understanding of Mayhem other than to say it sounds about right.

Our implementation of Mayhem is not publicly available, but it was written a pretty long time ago - these days, it might be pretty trivial to re-implement using the new Exploration Technique (also known as "otiegnqwvk") interface. The Threading mixin I showed you earlier is an otiegnqwvk.

One simple solution to the out-of-memory problem is the depth-first search otiegnqwvk, found in angr.exploration_techniques.DFS. The default path group behavior is to keep all active paths and step every active path at each step, clearly leading to an OOM unless you deal with it, so using DFS is a cheap way to only use O(n) memory, where n is the length of the longest path.

The DFS is obviously pretty primitive, but if you wanted to write a more complicated otiegnqwvk it's a good place to start. The full otiegnqwvk API reference is here: http://angr.io/api-doc/angr.html#angr.exploration_techniques.ExplorationTechnique

One thing to keep in mind is that veritesting is also implemented as an otiegnqwvk. Multiple otiegnqwvks can be applied to a single path group and their affects will combine, but the results can be unexpected.

I hope all this was helpful! Please let me know if you have any more specific questions about writing otiegnqwvks or using angr efficiently.

[leithon]

Thank you very much, Andrew.
All your comments make sense.