search

borzacchiello / seninja

symbolic execution plugin for binary ninja
BSD 2-Clause "Simplified" License
244 stars 22 forks source link

Pthread basic support #10

Closed cmd-theo closed 1 year ago

cmd-theo commented 1 year ago

Could it be possible to intergrate models for symbolic execution of threads or synchronisation primitives like mutex ?

borzacchiello commented 1 year ago

Hi, Thread support in a symbolic engine is a very hard problem, for sure outside the scope of SENinja. However, in many cases, you can still use SENinja to analyze small portions of the program.

If you give me a concrete example, or if you can share the binary that you want to analyze maybe I can answer more precisely :)

cmd-theo commented 1 year ago

Hello, thank you for the response, I will consider it. The context was the pthread library.

cmd-theo commented 1 year ago

Maybe dynamic analysis is more appropriated to this problem .