Symbolic Security Predicates: Hunt Program Weaknesses

TL;DR

This paper introduces security predicates for dynamic symbolic execution to improve bug detection in programs, modeling function semantics to enhance efficiency and accuracy, demonstrated through the Sydr tool with high detection accuracy.

Contribution

It proposes security predicates and function semantics modeling for dynamic symbolic execution, enhancing bug detection and path exploration efficiency in tools like Sydr.

Findings

Sydr achieves 95.59% accuracy on Juliet CWEs.

Function semantics modeling speeds up bug detection.

Security predicates effectively identify various memory errors.

Abstract

Dynamic symbolic execution (DSE) is a powerful method for path exploration during hybrid fuzzing and automatic bug detection. We propose security predicates to effectively detect undefined behavior and memory access violation errors. Initially, we symbolically execute program on paths that don't trigger any errors (hybrid fuzzing may explore these paths). Then we construct a symbolic security predicate to verify some error condition. Thus, we may change the program data flow to entail null pointer dereference, division by zero, out-of-bounds access, or integer overflow weaknesses. Unlike static analysis, dynamic symbolic execution does not only report errors but also generates new input data to reproduce them. Furthermore, we introduce function semantics modeling for common C/C++ standard library functions. We aim to model the control flow inside a function with a single symbolic formula. This assists bug detection, speeds up path exploration, and overcomes overconstraints in path predicate. We implement the proposed techniques in our dynamic symbolic execution tool Sydr. Thus, we utilize powerful methods from Sydr such as path predicate slicing that eliminates irrelevant constraints. We present Juliet Dynamic to measure dynamic bug detection tools accuracy. The testing system also verifies that generated inputs trigger sanitizers. We evaluate Sydr accuracy for 11 CWEs from Juliet test suite. Sydr shows 95.59% overall accuracy. We make Sydr evaluation artifacts publicly available to facilitate results reproducibility.