The SLAM project: debugging system software via static analysis

ABSTRACT

The goal of the SLAM project is to check whether or not a program obeys "API usage rules" that specify what it means to be a good client of an API. The SLAM toolkit statically analyzes a C program to determine whether or not it violates given usage rules. The toolkit has two unique aspects: it does not require the programmer to annotate the source program (invariants are inferred); it minimizes noise (false error messages) through a process known as "counterexample-driven refinement". SLAM exploits and extends results from program analysis, model checking and automated deduction. We have successfully applied the SLAM toolkit to Windows XP device drivers, to both validate behavior and find defects in their usage of kernel APIs.

REFERENCES

• 1: Glenn Ammons , Rastislav Bodík , James R. Larus, Mining specifications, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.4-16, January 16-18, 2002, Portland, Oregon
• 2: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 3: T. Ball, T. Millstein, and S. K. Rajamani. Polymorphic predicate abstraction. Technical Igeport MSIg-TI%-2001-10, Microsoft Igesearch, 2001.
• 4: Thomas Ball , Andreas Podelski , Sriram K. Rajamani, Boolean and Cartesian Abstraction for Model Checking C Programs, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.268-283, April 02-06, 2001
• 5: T. Ball, A. Podelski, and S. K. Rajamani. Oil the relative completeness of abstraction refinement. Technical Report MSR-TR- 2001-106, Microsott Research, 2001.
• 6: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 7: 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
• 8: Thomas Ball , Sriram K. Rajamani, Bebop: a path-sensitive interprocedural dataflow engine, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.97-103, June 2001, Snowbird, Utah, United States [doi>10.1145/379605.379690]
• 9: T. Ball and S. K. Rajamani. SLIC: A specification language tbr interface checking. TechnicM Report MSR-TR-2001-21, Microsoft Research, 2001.
• 10: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 11: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 12: 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]
• 13: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 14: Manuvir Das, Unification-based pointer analysis with directional assignments, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.35-46, June 18-21, 2000, Vancouver, British Columbia, Canada
• 15: Satyaki Das , David L. Dill, Successive Approximation of Abstract Transition Relations, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.51, June 16-19, 2001
• 16: D. L. Detlet, K. E. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Technical Report Research Report 159, Compaq Systems Igesearch Center, December 1998.
• 17: Matthew B. Dwyer , John Hatcliff , Roby Joehanes , Shawn Laubach , Corina S. Păsăreanu , Hongjun Zheng , Willem Visser, Tool-supported program abstraction for finite-state verification, Proceedings of the 23rd International Conference on Software Engineering, p.177-187, May 12-19, 2001, Toronto, Ontario, Canada
• 18: D. Engler, B. Chelf, A. Chou, and S. tiallem. Checking system rules using system-specific, programmer-written compiler extensions. In Oh'D1 00: Operating System Design and lmplementation. Usenix Association, 2000.
• 19: David Evans, Static detection of dynamic memory errors, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.44-53, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 20: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 21: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 22: Gerard J. Holzmann, Logic Verification of ANSI-C Code with SPIN, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.131-147, August 30-September 01, 2000
• 23: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 24: L. Lamport. Proving the correctness of multiprocess programs. 1EEE Transactions on software Engineering, S19-3(2):125 143, 1977.
• 25: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 26: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 27: Vlad Rusu , Eli Singerman, On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.178-192, March 22-28, 1999
• 28: Hassen Saïdi , Natarajan Shankar, Abstract and Model Check While You Prove, Proceedings of the 11th International Conference on Computer Aided Verification, p.443-454, July 06-10, 1999
• 29: Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000 [doi>10.1145/353323.353382]
• 30: M. Y. Vardi and P. Wolper. An automata theoretic apporach to automatic program verification. In L1US 86: Logic in Computer Science, pages 332 344. I191919 Computer Society Press, 1996.