• Manticore
• security
• static analysis
• symbolic execution
• target-oriented approach
• vulnerability detection
• Wassail
• WebAssembly (WASM)

During security evaluations, particularly for binary black-box targets, symbolic execution is a valuable technique for security analysts. It enables the verification of assumptions, the discovery of relevant program behaviors, and the identification of points of interest for deeper analysis. Most existing symbolic execution tools adopt a coverage-first approach, seeking to explore as many reachable functions as possible.

The primary limitation of symbolic execution, however, is its high computational cost. Because the tool must emulate program execution and explore all possible symbolic states, it quickly faces the well-known problem of path explosion.

In this thesis, we propose a target-oriented approach to mitigate this challenge. Rather than maximizing coverage, our method concentrates on determining the constraints required to reach specific states of interest, defined through custom rules provided by the analyst. To realize this approach, we extend state-of-the-art tools such as Wassail and Manticore, adapting them to support our target-oriented methodology. In addition, we address performance bottlenecks by introducing a parallelized execution strategy that leverages memoization, significantly improving the speed and practicality of the tool.