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: ...

• Type: Conference
• Year: 2006
• Where: SP
• Authors: Junfeng Yang, Can Sar, Paul Twohey, Cristian Cadar, Dawson R. Engler
• Keywords: Code, File System Code, Security Privacy, SP 2006, file Systems