Error propagation analysis for file systems

ABSTRACT

Unchecked errors are especially pernicious in operating system file management code. Transient or permanent hardware failures are inevitable, and error-management bugs at the file system layer can cause silent, unrecoverable data corruption. We propose an interprocedural static analysis that tracks errors as they propagate through file system code. Our implementation detects overwritten, out-of-scope, and unsaved unchecked errors. Analysis of four widely-used Linux file system implementations (CIFS, ext3, IBM JFS and ReiserFS), a relatively new file system implementation (ext4), and shared virtual file system (VFS) code uncovers 312 error propagation bugs. Our flow- and context-sensitive approach produces more precise results than related techniques while providing better diagnostic information, including possible execution paths that demonstrate each bug found.

REFERENCES

• 1: M. W. Bigrigg and J. J. Vos. The set-check-use methodology for detecting error propagation failures in I/O routines. In Workshop on Dependability Benchmarking, Washington, DC, June 2002.
• 2: Randal E. Bryant, Binary decision diagrams and beyond: enabling technologies for formal verification, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.236-243, November 05-09, 1995, San Jose, California, United States
• 3: D. Callahan, The program summary graph and flow-sensitive interprocedual data flow analysis, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.47-56, June 20-24, 1988, Atlanta, Georgia, United States
• 4: George Candea , Mauricio Delgado , Michael Chen , Armando Fox, Automatic Failure-Path Inference: A Generic Introspection Technique for Internet Applications, Proceedings of the The Third IEEE Workshop on Internet Applications, p.132, June 23-24, 2003
• 5: A. Dilger. Error propagation bugs in ext4. Personal communication, Nov. 2008.
• 6: D. Evans. LCLint User's Guide. University of Virginia, May 2000.
• 7: C. A. Flanagan and M. Burrows. System and method for dynamically detecting unchecked error condition values in computer programs. United States Patent #6,378,081 B1, Apr. 2002.
• 8: John B. Goodenough, Structured exception handling, Proceedings of the 2nd ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.204-224, January 20-22, 1975, Palo Alto, California [doi>10.1145/512976.512997]
• 9: Tarak Goradia, Dynamic impact analysis: a cost-effective technique to enforce error-propagation, Proceedings of the 1993 ACM SIGSOFT international symposium on Software testing and analysis, p.171-181, June 28-30, 1993, Cambridge, Massachusetts, United States
• 10: A. D. Groce. Problem solved. Personal communication, Jan. 2009.
• 11: Haryadi S. Gunawi , Cindy Rubio-González , Andrea C. Arpaci-Dusseau , Remzi H. Arpaci-Dussea , Ben Liblit, EIO: error handling is occasionally correct, Proceedings of the 6th USENIX Conference on File and Storage Technologies, p.1-16, February 26-29, 2008, San Jose, California
• 12: Philip J. Guo , Jeff H. Perkins , Stephen McCamant , Michael D. Ernst, Dynamic inference of abstract types, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146268]
• 13: Martin Hiller , Arshad Jhumka , Neeraj Suri, An Approach for Analysing the Propagation of Data Errors in Software, Proceedings of the 2001 International Conference on Dependable Systems and Networks (formerly: FTCS), p.161-172, July 01-04, 2001
• 14: Martin Hiller , Arshad Jhumka , Neeraj Suri, PROPANE: an environment for examining the propagation of errors in software, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 15: Martin Hiller , Arshad Jhumka , Neeraj Suri, EPIC: Profiling the Propagation and Effect of Data Errors in Software, IEEE Transactions on Computers, v.53 n.5, p.512-530, May 2004 [doi>10.1109/TC.2004.1275294]
• 16: A. Jhumka, M. Hiller, and N. Suri. Assessing inter-modular error propagation in distributed software. In SRDS, pages 152--161. IEEE Computer Society, 2001.
• 17: Andreas Johansson, Error Propagation Profiling of Operating Systems, Proceedings of the 2005 International Conference on Dependable Systems and Networks, p.86-95, June 28-July 01, 2005 [doi>10.1109/DSN.2005.45]
• 18: N. Kidd, T. Reps, and A. Lal. WALi: A C++ library for weighted pushdown systems. http://www.cs.wisc.edu/wpis/wpds/download.php, 2008.
• 19: A. Lal, T.W. Reps, and G. Balakrishnan. Extended weighted pushdown systems. In K. Etessami and S. K. Rajamani, editors, CAV, volume 3576 of Lecture Notes in Computer Science, pages 434--448. Springer, 2005.
• 20: A. Lal, N. Kidd, T.W. Reps, and T. Touili. Abstract error projection. In H. R. Nielson and G. Filé, editors, SAS, volume 4634 of Lecture Notes in Computer Science, pages 200--217. Springer, 2007.
• 21: A. Lal, T. Touili, N. Kidd, and T. Reps. Interprocedural analysis of concurrent programs under a context bound. Technical Report 1598, University of Wisconsin--Madison, July 2007.
• 22: J. Lind-Nielsen. BuDDy -- A Binary Decision Diagram Package. http://sourceforge.net/projects/buddy, 2004.
• 23: Barbara Liskov, A history of CLU, The second ACM SIGPLAN conference on History of programming languages, p.133-147, April 20-23, 1993, Cambridge, Massachusetts, United States
• 24: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 25: Thomas Reps , Stefan Schwoon , Somesh Jha , David Melski, Weighted pushdown systems and their application to interprocedural dataflow analysis, Science of Computer Programming, v.58 n.1-2, p.206-263, October 2005 [doi>10.1016/j.scico.2005.02.009]
• 26: P. Sacramento, B. Cabral, and P. Marques. Unchecked exceptions: Can the programmer be trusted to document exceptions? In Second International Conference on Innovative Views of .NET Technologies, Florianópolis, Brazil, Oct. 2006. Microsoft.
• 27: S. Schwoon. Model-Checking Pushdown Systems. PhD thesis, Technical Univ. of Munich, Munich, Germany, July 2002.
• 28: K. G. Shin , T.-H. Lin, Modeling and Measurement of Error Propagation in a Multimodule Computing System, IEEE Transactions on Computers, v.37 n.9, p.1053-1066, September 1988 [doi>10.1109/12.2256]
• 29: Sun Microsystems, Inc. Unchecked exceptions -- the controversy. http://java.sun.com/docs/books/tutorial/essential/exceptions/runtime.html, Aug. 2007.
• 30: Marko van Dooren , Eric Steegmans, Combining the robustness of checked exceptions with the flexibility of unchecked exceptions using anchored exception declarations, Proceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 31: Mark N. Wegman , Frank Kenneth Zadeck, Constant propagation with conditional branches, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.291-299, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318659]
• 32: Junfeng Yang , Paul Twohey , Dawson Engler , Madanlal Musuvathi, Using model checking to find serious file system errors, ACM Transactions on Computer Systems (TOCS), v.24 n.4, p.393-423, November 2006 [doi>10.1145/1189256.1189259]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability; Validation
      D.2.5 Testing and Debugging
          Subjects: Error handling and recovery

General Terms:
Algorithms, Languages, Reliability, Verification

Keywords:
binary decision diagrams, copy constant propagation, interprocedural dataflow analysis, static program analysis, weighted pushdown systems