Using redundancies to find errors

ABSTRACT

This paper explores the idea that redundant operations, like type errors, commonly flag correctness errors. We experimentally test this idea by writing and applying four redundancy checkers to the Linux operating system, finding many errors. We then use these errors to demonstrate that redundancies, even when harmless, strongly correlate with the presence of traditional hard errors (e.g., null pointer dereferences, unreleased locks). Finally we show that how flagging redundant operations gives a way to make specifications "fail stop" bydetecting dangerous omissions.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: Alexander Aiken , Manuel Fähndrich , Zhendong Su, Detecting Races in Relay Ladder Logic Programs, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.184-200, March 28-April 04, 1998
• 3: Ken Ashcraft , Dawson Engler, Using Programmer-Written Compiler Extensions to Catch Security Holes, Proceedings of the 2002 IEEE Symposium on Security and Privacy, p.143, May 12-15, 2002
• 4: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 5: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H ]
• 6: G. Casella and R. L. Berger. Statistical Inference. Wadsworth Group, Pacific Grove, CA, 2002.
• 7: Fun Ting Chan , Tsong Yueh Chen, AIDA—a dynamic data flow anomaly detection system for Pascal programs, Software—Practice & Experience, v.17 n.3, p.227-239, March 1987 [doi>10.1002/spe.4380170306]
• 8: Andy Chou , Junfeng Yang , Benjamin Chelf , Seth Hallem , Dawson Engler, An empirical study of operating systems errors, Proceedings of the eighteenth ACM symposium on Operating systems principles, October 21-24, 2001, Banff, Alberta, Canada
• 9: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 10: D. L. Detlefs. An overview of the extended static checking system. In Proceedings of the First Workshop on Formal Methods in Software Practice, pages 1--9, January 1996.
• 11: Peter J. Downey , Ravi Sethi , Robert Endre Tarjan, Variations on the Common Subexpression Problem, Journal of the ACM (JACM), v.27 n.4, p.758-771, Oct. 1980 [doi>10.1145/322217.322228]
• 12: David Evans , John Guttag , James Horning , Yang Meng Tan, LCLint: a tool for using specifications to check code, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.87-96, December 06-09, 1994, New Orleans, Louisiana, United States
• 13: Ira R. Forman, An algebra for data flow anomaly detection, Proceedings of the 7th international conference on Software engineering, p.278-286, March 26-29, 1984, Orlando, Florida, United States
• 14: Lloyd D. Fosdick , Leon J. Osterweil, Data Flow Analysis in Software Reliability, ACM Computing Surveys (CSUR), v.8 n.3, p.305-330, Sept. 1976 [doi>10.1145/356674.356676]
• 15: D. Freedman, R. Pisani, and R. Purves. Statistics. W.W. Norton, third edition edition, 1998.
• 16: Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 17: J. C. Huang. Detection of data flow anomaly through program instrumentation. IEEE Transactions on Software Engineering, 5(3):226--236, May 1979.
• 18: L. J. Osterweil and L. D. Fosdick. Dave--a validation error detection and documentation system for fortran programs. Software: Practice and Experience, 6(4):473--486, December 1976.
• 19: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 20: N. Sterling. WARLOCK - a static data race analysis tool. In USENIX Winter, pages 97--106, 1993.
• 21: D. Wagner, J. Foster, E. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In The 2000 Network and Distributed Systems Security Conference. San Diego, CA, February 2000.

INDEX TERMS

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

General Terms:
Reliability, Security, Verification

Keywords:
error detection, extensible compilation