Proving memory safety of floating-point computations by combining static and dynamic program analysis

Whitebox fuzzing is a novel form of security testing based on dynamic symbolic execution and constraint solving. Over the last couple of years, whitebox fuzzers have found many new security vulnerabilities (buffer overflows) in Windows and Linux applications, including codecs, image viewers and media players. Those types of applications tend to use floating-point instructions available on modern processors, yet existing whitebox fuzzers and SMT constraint solvers do not handle floating-point arithmetic. Are there new security vulnerabilities lurking in floating-point code? A naive solution would be to extend symbolic execution to floating-point (FP) instructions (months of work), extend SMT solvers to reason about FP constraints (months of work or more), and then face more complex constraints and an even worse path explosion problem. Instead, we propose an alternative approach, based on the rough intuition that FP code should only perform memory safe data-processing of the “pa...

• Type: Conference
• Year: 2010
• Where: ISSTA
• Authors: Patrice Godefroid, Johannes Kinder
• Keywords: FP Code, ISSTA 2010, Memory Address Computations, Software Engineering, Whitebox Fuzzers