loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2006 IEEE Symposium on Security and Privacy (S&P'06)
Automatically Generating Malicious Disks using Symbolic Execution
Berkeley/Oakland, California
May 21-May 24
ISBN: 0-7695-2574-1
Junfeng Yang, Stanford University
Can Sar, Stanford University
Paul Twohey, Stanford University
Cristian Cadar, Stanford University
Dawson Engler, Stanford University
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: we checked the disk mounting code of three widely-used Linux file systems: ext2, ext3, and JFS and found bugs in all of them where malicious data could either cause a kernel panic or form the basis of a buffer overflow attack.
Citation:
Junfeng Yang, Can Sar, Paul Twohey, Cristian Cadar, Dawson Engler, "Automatically Generating Malicious Disks using Symbolic Execution," sp, pp.243-257, 2006 IEEE Symposium on Security and Privacy (S&P'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.