Abstract
The analysis described in this article detects about two real and uncorrected deadlock situations per thousand C source files or million lines of code in the Linux kernel source, and three accesses to freed memory, at a few seconds per file. In distinction to model-checking techniques, the analysis applies a configurable “3-phase” Hoare-style logic to an abstract interpretation of C code to obtain its results.
Chapter PDF
Similar content being viewed by others
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.
References
Breuer, P.T., Martínez Madrid, N., Sánchez, L., Marín, A., Delgado Kloos, C.: A formal method for specification and refinement of real-time systems. In: Proc. 8’th EuroMicro Workshop on Real Time Systems, L’aquilla, Italy, pp. 34–42. IEEE Press, Los Alamitos (1996)
Breuer, P.T., Delgado Kloos, C., Martínez Madrid, N., López Marin, A., Sánchez, L.: A Refinement Calculus for the Synthesis of Verified Digital or Analog Hardware Descriptions in VHDL. ACM Transactions on Programming Languages and Systems (TOPLAS) 19(4), 586–616 (1997)
Breuer, P.T., Valls, M.G.: Static Deadlock Detection in the Linux Kernel. In: Llamosí, A., Strohmeier, A. (eds.) Ada-Europe 2004. LNCS, vol. 3063, pp. 52–64. Springer, Heidelberg (2004)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. 4th ACM Symp. on the Principles of Programming Languages, pp. 238–252 (1977)
Foster, J.S., Fähndrich, M., Aiken, A.: A Theory of Type Qualifiers. In: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 1999), Atlanta, Georgia (May 1999)
Foster, J.S., Terauchi, T., Aiken, A.: Flow-Sensitive Type Qualifiers. In: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2002), Berlin, Germany, June 2002, pp. 1–12 (2002)
Johnson, R., Wagner, D.: Finding User/Kernel Pointer Bugs With Type Inference. In: Proc. 13th USENIX Security Symposium, San Diego, CA, USA, August 9-13 (2004)
Wagner, D., Foster, J.S., Brewer, E.A., Aiken, A.: A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities. In: Proc. Network and Distributed System Security (NDSS) Symposium, San Diego, CA, USA, February 2-4 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Breuer, P.T., Pickin, S. (2006). Checking for Deadlock, Double-Free and Other Abuses in the Linux Kernel Source Code. In: Alexandrov, V.N., van Albada, G.D., Sloot, P.M.A., Dongarra, J. (eds) Computational Science – ICCS 2006. ICCS 2006. Lecture Notes in Computer Science, vol 3994. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11758549_103
Download citation
DOI: https://doi.org/10.1007/11758549_103
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34385-1
Online ISBN: 978-3-540-34386-8
eBook Packages: Computer ScienceComputer Science (R0)