Sciweavers

Share
ISSTA
2010
ACM

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

9 years 7 months ago
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...
Patrice Godefroid, Johannes Kinder
Added 15 Aug 2010
Updated 15 Aug 2010
Type Conference
Year 2010
Where ISSTA
Authors Patrice Godefroid, Johannes Kinder
Comments (0)
books