Sciweavers

SP
2006
IEEE

Automatically Generating Malicious Disks using Symbolic Execution

13 years 9 months ago
Automatically Generating Malicious Disks using Symbolic Execution
Many current systems allow data produced by potentially malicious sources to be mounted as a file system. File system code must check this data for dangerous values or invariant violations before using it. Because file system code typically runs inside the operating system kernel, even a single unchecked value can crash the machine or lead to an exploit. Unfortunately, validating file system images is complex: they form DAGs with complex dependency relationships across massive amounts of data bound together with intricate, undocumented assumptions. This paper shows how to automatically find bugs in such code using symbolic execution. Rather than running the code on manually-constructed concrete input, we instead run it on symbolic input that is initially allowed to be “anything.” As the code runs, it observes (tests) this input and thus constrains its possible values. We generate test cases by solving these constraints for concrete values. The approach works well in practice: ...
Junfeng Yang, Can Sar, Paul Twohey, Cristian Cadar
Added 12 Jun 2010
Updated 12 Jun 2010
Type Conference
Year 2006
Where SP
Authors Junfeng Yang, Can Sar, Paul Twohey, Cristian Cadar, Dawson R. Engler
Comments (0)