Date: Tuesday, February 4th 2025 – 13h00
Place: A008
Title: A scalable framework for backward bounded static symbolic execution
Many programs (e.g. malware) hide their behavior by using obfuscations such as opaque predicates.
Automatic methods have been developed to detect such obfuscations. In this presentation, we will focus on static symbolic backward bounded execution, a method that enumerates backward bounded paths from a potential opaque predicate and uses symbolic execution to check whether all enumerated paths have the same predicate value.
We’ll show how this method can be generalized using a lattice-based framework and how to scale up such methods to efficiently analyze whole programs.
