Numeric Truncation Security Predicate
Timofey Mezhuev, Ilay Kobrin, Alexey Vishnyakov, Daniil Kuts
TL;DR
This work tackles numeric truncation errors arising when large-width values are converted to smaller types in statically-typed languages. It introduces a dynamic symbolic execution–based security predicate, built on Sydr with Triton, and enhances precision with a symbolic shadow stack and shadow registers to minimize false positives. The approach constructs and solves truncation predicates for relevant instructions, generating error-reproducing inputs via an SMT solver when satisfiable. Empirical evaluation on Juliet Dynamic yields 100% accuracy, and application to real-world OSS identifies 12 new truncation bugs across five projects, most of which were fixed by maintainers, demonstrating practical impact. The results suggest that the combination of DSE-based predicates and shadow-tracking yields effective, automatable detection of numerical truncation vulnerabilities in binaries.
Abstract
Numeric truncation is a widely spread error in software written in languages with static data typing, such as C/C++ or Java. It occurs when the significant bits of the value with a bigger type size are truncated during value conversion to the smaller type. Utilizing one of the most powerful methods for path exploration and automated bug detection called dynamic symbolic execution (DSE), we propose the symbolic security predicate for numeric truncation error detection, developed on top of DSE tool Sydr. Firstly, we execute the program on the data, which does not lead to any errors. During program execution we update symbolic shadow stack and shadow registers to track symbolic sizes of the symbolic variables to avoid false positives. Then, if we meet the instruction, which truncates the symbolic variable, we build the security predicate, try to solve it with the SMT-solver and in case of success save new input file to reproduce the error. We tested our approach on Juliet Dynamic test suite for CWE-197 and achieved 100% accuracy. We approved the workability of our approach by detecting 12 new errors of numeric truncation in 5 different real-world open source projects within OSS-Sydr-Fuzz project. All of the errors were reported, most of the reports were equipped with appropriate fixes, successfully confirmed and applied by project maintainers.