Abstract
We port verification techniques for device drivers from the Windows domain to Linux, combining several tools and techniques into one integrated tool-chain. Building on ideas from Microsoft’s Static Driver Verifier (SDV) project, we extend their specification language and combine its implementation with the public domain bounded model checker CBMC as a new verification back-end. We extract several API conformance rules from Linux documentation and formulate them in the extended language SLICx. Thus SDV-style verification of temporal safety specifications is brought into the public domain. In addition, we show that SLICx, together with CBMC, can be used to simulate preemption in multi-threaded code, and to find race conditions and to prove the absence of deadlocks and memory leaks.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Swift, M.M., Bershad, B.N., Levy, H.M.: Improving the reliability of commodity operating systems. In: 19th ACM Symp. on Operating Systems Principles, Proc., pp. 207–222. ACM Press, New York (2003)
Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. ACM SIGOPS Oper. Syst. Rev. 40(4), 73–85 (2006)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)
Ball, T., Rajamani, S.K.: SLIC: A specification language for interface checking. Technical report, Microsoft Research (2001)
Various: The SLAM Project (2006), http://research.microsoft.com/slam/
Post, H., Sinz, C., Küchlin, W.: Avinux: Towards automatic verification of Linux device drivers (2007), Available at http://www-sr.informatik.uni-tuebingen.de/~post/avinux
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with blast. In: Ball, T., Rajamani, S.K. (eds.) Model Checking Software. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Păsăreanu, C.S., Robby, Z.H.: Bandera: extracting finite-state models from Java source code. In: Software Engineering, 22nd Intl. Conf., Proc., pp. 439–448. ACM Press, New York (2000)
Various: Linux kernel releases (Available online under http://www.kernel.org )
Corbet, J., Rubini, A., Kroah-Hartman, G.: Linux Device Drivers, 3rd edn. O’Reilly Media, Inc. (2005)
Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: ACM SIGPLAN Conf. on Programming Language Design and Implementation, Proc., vol. 39, pp. 14–24. ACM Press, New York (2004)
Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. pp. 82–97
Coffman, E.G., Elphick, M., Shoshani, A.: System deadlocks. ACM Comput. Surv. 3(2), 67–78 (1971)
Mühlberg, J.T., Lüttgen, G.: Blasting Linux Code. In: Brim, L., Haverkort, B., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 211–226. Springer, Heidelberg (2007)
Post, H., Küchlin, W.: Automatic data environment construction for static device drivers analysis. In: Conf. on Specification and verification of component-based systems, Proc., pp. 89–92. ACM Press, New York (2006)
Yang, J., Twohey, P., Engler, D., Musuvathi, M.: Using model checking to find serious file system errors. ACM Trans. Comput. Syst. 24(4), 393–423 (2006)
Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for c. In: Wermelinger, M., Gall, H. (eds.) ESEC/SIGSOFT FSE, pp. 263–272. ACM Press, New York (2005)
Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: Cil: Intermediate language and tools for analysis and transformation of c programs. In: Horspool, R.N. (ed.) CC 2002 and ETAPS 2002. LNCS, vol. 2304, pp. 213–228. Springer, Heidelberg (2002)
Sauter, M.: Automatisierung und Integration regelbasierter Verifikation für Linux Gerätetreiber. Master’s Thesis (to appear, 2007)
Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: Software Engineering. 25th Intl. Conf., Proc, pp. 385–395. IEEE Computer Society, Washington, DC (2003)
Chen, H., Wagner, D.: MOPS: an infrastructure for examining security properties of software. In: Atluri, V. (ed.) ACM Intl. Conf. on Computer and Communications Security, Proc., pp. 235–244. ACM, New York (2002)
Cousot, P.: Abstract interpretation. ACM Comput. Surv. 28(2), 324–328 (1996)
Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: Software verification platform. [33], pp. 301–306
Sethi, N., Barrett, C.: Cascade: C assertion checker and deductive engine. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 166–169. Springer, Heidelberg (2006)
Chaki, S., Clarke, E.M., Kidd, N., Reps, T.W., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 334–349. Springer, Heidelberg (2006)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society, Los Alamitos (2002)
Various: Linux standard base project, (Available online under http://www.linuxbase.org )
Various: The OLVER project, (Available under http://linuxtesting.org )
Chen, H., Dean, D., Wagner, D.: Model checking one million lines of C code. In: NDSS, The Internet Society (2004)
Engler, D., Ashcraft, K.: RacerX: effective, static detection of race conditions and deadlocks. In: 19th ACM Symp. on Operating Systems Principles, Proc., pp. 237–252. ACM Press, New York (2003)
Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: 32nd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, Proc., pp. 351–363. ACM Press, New York (2005)
Meissner, F.: Regelbasierte Spezifikation von Linux Kernel-Schnittstellen mit SLIC. Master’s Thesis (to appear, 2007)
Etessami, K., Rajamani, S.K. (eds.): CAV 2005. LNCS, vol. 3576, pp. 6–10. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Post, H., Küchlin, W. (2007). Integrated Static Analysis for Linux Device Driver Verification. In: Davies, J., Gibbons, J. (eds) Integrated Formal Methods. IFM 2007. Lecture Notes in Computer Science, vol 4591. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73210-5_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-73210-5_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73209-9
Online ISBN: 978-3-540-73210-5
eBook Packages: Computer ScienceComputer Science (R0)