Automatic data environment construction for static device drivers analysis

ABSTRACT

Linux contains thousands of device drivers that are developed independently by many developers. Though each individual driver source code is relatively small---≈10k lines of code---the whole operating system contains a few million lines of code. Therefore Linux device drivers offer a useful application area for modular analysis.Our finding is that despite the precise modeling of most features of the standard systems programming language C, model checking software verification tools for C fail to provide means for modular analysis of device drivers. We inspected CBMC [2], SLAM-SDV [3], MAGIC [1], BLAST [4] and others and found that a rich additional environment model for every device driver is needed. This model must provide information on out-of-scope initialized pointers and complex data structures. We present strategies to automatically create feasible, bounded data environments for Linux device drivers instead of creating them manually. Our solution differs from general interface generation mechanisms (e.g. CUTE[5]), because is it specialised on bounded model checking of Linux device drivers written in C. Our contribution is a preprocessing step that extends the usability of CBMC for modular Linux device driver analysis.

REFERENCES

• 1: Sagar Chaki , Edmund Clarke , Alex Groce , Somesh Jha , Helmut Veith, Modular verification of software components in C, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 2: E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In K. Jensen and A. Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2988 of LNCS, pages 168--176. Springer, 2004.
• 3: V. Contributors. The SLAM Project. http://research.microsoft.com/slam/, 2006.
• 4: T. Henzinger, R. Jhala, R. Majumdar, and G. SUTRE. Software verification with BLAST. In Proc. 10th Int. SPIN Workshop (SPIN'2003), Portland, OR, USA, May 2003, volume 2648 of LNCS, pages 235--239. Springer, 2003.
• 5: Koushik Sen , Darko Marinov , Gul Agha, CUTE: a concolic unit testing engine for C, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 6: D. van Leeuwen, E. Anderson, and J. Axboe. A Linux Cdrom Standard, kernel 2.6.15 edition, March 1999. Found in Documentation/cdrom.
• 7: T. Xie, D. Marinov, W. Schulte, and D. Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 365--381, Edinburgh, UK, April 2005.
• 8: Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.351-363, January 12-14, 2005, Long Beach, California, USA
• 9: J. Yang, P. Twohey, D. R. Engler, and M. Musuvathi. Using model checking to find serious file system errors. In Proc. of the 16th Int. Conf. on Computer Aided Verification (CAV), volume 3114 of LNCS, pages 273--288. Springer Berlin / Heidelberg, 2004.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.5 Reliability
          Subjects: Verification

General Terms:
Experimentation, Verification

Keywords:
Linux, bounded model checking, environment modelling, software verification