[angr] Does angr support symbolic execution on multi-threaded program?

Song Yang dr4lamb at gmail.com
Thu May 4 05:07:47 PDT 2017


Thanks guys, it really helps.

The test program was simplified to focus on the error. The added thread was
meant to interact with the main thread. Therefore, the problem cannot be
solved by modeling pthread_create as a fork.

Still, angr is a great progress. Good job.

BR
Connar

2017-05-04 7:28 GMT+08:00 Andrew Dutcher <andrew at andrewdutcher.com>:

> I would also like to point out that we do currently model pthread_create
> as a fork. I don't know why your test program fails, but we have in the
> past analyzed programs which used threading for concurrency without
> interaction between the threads.
>
> On Wed, May 3, 2017 at 2:06 PM, Yan <zardus at gmail.com> wrote:
>
>> Hello,
>>
>> angr currently has no concept of threads. There are a few missing pieces:
>>
>> 1. Thread yielding and preemption. In the real world, threads can be
>> scheduled in any sequence. We have no good way to model this symbolically
>> without leading to massive path explosion. This is probably the biggest
>> conceptual/research issue.
>> 2. We need a concept of threads in angr, including properly switching
>> between thread local storage and thread stacks. This shouldn't be that
>> hard, but it still doesn't exist.
>> 3. We need pthread simprocedures and/or support for the clone syscall.
>>
>> Because the attached example has no interaction between the threads, it
>> might be enough to simply model `pthread_create` as a fork in this case. Of
>> course, that's not really threading.
>>
>> - Yan
>>
>> On Tue, May 2, 2017 at 7:10 PM, Song Yang <dr4lamb at gmail.com> wrote:
>>
>>> Dear,
>>>
>>> Angr is great and helpful. Thanks a lot for the efforts.
>>>
>>> I am curious to know if angr support symbolic execution on
>>> multi-threaded program since most of programs uses multi-threading nowadays.
>>>
>>> A few tests were made and it is shown that angr MIGHT NOT support
>>> multi-threaded program. As is shown in the attachment, a thread which
>>> simply prints a helloworld was added to the "fauxware" example. However,
>>> the solve.py find only one error path which ends at "0x0" addr.
>>> I am not sure if there's anything I can do to make angr support the
>>> attached program. ANY HELP IS REALLY APPRECIATED.
>>>
>>> Thanks again for your great work.
>>>
>>> BR.
>>> Connar
>>>
>>> _______________________________________________
>>> angr mailing list
>>> angr at lists.cs.ucsb.edu
>>> https://lists.cs.ucsb.edu/mailman/listinfo/angr
>>>
>>>
>>
>> _______________________________________________
>> 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/20170504/bc0f80e2/attachment.html>


More information about the angr mailing list