Applying Concolic Testing to the Automotive Domain 2024-01-2802

Symbolic code execution is a powerful cybersecurity testing approach that facilitates the systematic exploration of all paths within a program to uncover previously unknown cybersecurity vulnerabilities. This is achieved through a Satisfiability Modulo Theory (SMT) solver, which operates on symbolic values for program inputs instead of using their concrete counterparts. However, in complex code bases, this approach faces significant limitations, such as program path explosions or unavailable dependencies, which can result in conditions that the SMT solver cannot reason about. Consequently, SMT solvers are often considered as too costly to implement for automotive testing use cases and are rarely employed within this domain. In contrast, fuzz testing has recently gained traction in the automotive industry as an invaluable testing technique for identifying previously unknown vulnerabilities. Its initial setup is straightforward and typically yields useful findings. However, achieving high code coverage with fuzz testing is quite challenging and requires a sophisticated instrumentation and guidance setup. A promising approach to address this challenge of insufficient code coverage involves combining symbolic code execution with substituted values from the fuzzing engine for complex conditions, enabling the SMT solver to handle them effectively. In this paper, we present an overview of the current state of concolic testing tools and their applicability in the automotive domain. We compare concolic testing to conventional fuzz testing setups commonly observed in the automotive industry and outline the conditions necessary to achieve greater code coverage, thereby increasing the likelihood of discovering vulnerabilities.