Research on Software Security
Our research about software security focus on the issues of automatic bug finding. There are two mainly two methods for automatic vulnerability analysis - Fuzzing and Symbolic execution. Our research group aims to optimize the technique of automatic vulnerability analysis. Below are the brief introduction and achievement of our projects on software security:
Dynamic Path Pruning in Symbolic Execution
Path pruning can alleviate path explosion in symbolic execution by removing unsatisfiable paths at an early stage before they multiply. Although existing symbolic execution tools have implemented several strategies to remove unsatisfiable paths, it remains unclear how effective these strategies are because checking a path's satisfiability takes non-negligible time. This work formulates the path pruning problem and demonstrates that existing path pruning strategies suffer from unacceptable worst-case performance due to their program-independent behaviors. To this end, we propose dynamic path pruning (DPP), a strategy that consistently achieves near-optimal exploration time for a wide spectrum of programs. The intuition behind DPP is to assign a higher checking rate to paths that are more likely to be unsatisfiable. DPP finds the optimal checking rate by solving an optimization problem and adjusts to thise optimal rate based on the observed program's characteristics, including the observed percentage of satisfiable paths. DPP is implemented on top of an open source symbolic execution platform in only a few hundred lines. Our evaluation shows that using DPP to analyze the coreutils will always yield near-optimal exploration time. We can also further optimize the checking range and timeout in DPP in future work.