Symbolic Execution in Practice: A Survey of Applications in Vulnerability, Malware, Firmware, and Protocol Analysis

TL;DR

This survey reviews how symbolic execution is applied across various domains like vulnerability, malware, firmware, and protocol analysis, highlighting strategies to overcome path explosion and suggesting future research directions.

Contribution

It provides a systematic taxonomy of techniques to make symbolic execution practical and surveys its applications in multiple security-related domains.

Findings

Strategies like scope reduction and guidance heuristics improve symbolic execution.

Symbolic execution is effectively used in vulnerability and malware analysis.

Future research includes applying symbolic execution to real-time OS and type-safe languages.

Abstract

Symbolic execution is a powerful program analysis technique that allows for the systematic exploration of all program paths. Path explosion, where the number of states to track becomes unwieldy, is one of the biggest challenges hindering symbolic execution's practical application. To combat this, researchers have employed various strategies to enable symbolic execution on complex software systems. This paper introduces a systematic taxonomy of these strategies, categorizing them into two primary approaches: Scope Reduction, which aims to reduce the scope of symbolic execution to manageable portions of code, and Guidance Heuristics, which steer the symbolic execution engine toward promising paths. Using this taxonomy as a lens, we survey applications of symbolic executions in several domains such as vulnerability analysis, malware analysis, firmware re-hosting, and network protocol analysis. Finally, we identify promising directions for future research, including the application of symbolic execution to real-time operating systems and modern, type-safe languages.