Finding Misuses of Unsigned Integers in Linux Device Driver Code

Martin Rathgeber, Christoph Zengler and Wolfgang Küchlin, Universität Tübingen, Germany

A large number of operating system crashes is due to device driver errors. Chou et al showed in [1], that device drivers have error rates up to three to seven times higher than the rest of the kernel. This observation led to the start of the Microsoft SLAM project in 2000. The project's goal was the development of a set of tools helping driver developers to test and verify their code. For the verification part, successful ideas of the area of symbolic model checking and automated theorem proving were reused. The tool set, resulting of Microsoft's efforts, was released under the name "Static Driver Verifier" (SDV) [2]. To stay competitive, the Linux community had to come up with similar tools to support their developers. One possible tool for this task is Avinux, developed by Post et al [3]. Avinux checks thousands of Linux device drivers for the absence of certain kinds of errors.

For our present work we chose to verify one Linux device driver in depth: The EHCA device driver. EHCA is an IBM specific implementation of the Infiniband standard and is used on IBM's Z series main frames. Infiniband is a switched fabric communications link used in high performance computing and therefore device drivers for Infiniband are highly security critical. Our approach bases on the work of Post. We use CBMC, a bounded model checker for the language C [4] in order to prove or disprove certain properties of the EHCA device driver.

For this paper we focus on a family of errors resulting from the misuse of unsigned integers. If an unsigned integer variable is assigned to the return value of a function, one has to assure, that this function only returns non-negative values. But in our analysis we found situations in which this condition was not always true, meaning, an unsigned integer variable can be assigned to negative values in the current EHCA code (and other code surrounding this module). Errors of this kind were already fixed in the last months (c.f. the EHCA patches), but apparently not all occurrences were found. We developed a tool which incorporates CMBC to systematically detect all errors of this kind at compile time and therefore helps developers to produce more reliable code in the future.

[1] Chou, Andy and Yang, Junfeng and Chelf, Benjamin and Hallem, Seth and Engler, Dawson: An empirical Study of Operating Systems Errors, Proceedings of the SOSP 2001

[2] Ball, Thomas and Bounimova, Ella and Levin, Vladimir and Kumar, Rahul and Lichtenberg, Jakob: The Static Driver Verifier Research Platform, Proceedings of the CAV 2010

[3] Post, Hendrik and Küchlin, Wolfgang: Integration of static analysis for Linux device driver verification, Proceedings of IFM 2007

[4] Clarke, Edmund M. and Kroening, Daniel and Lerda, Flavio: A Tool for Checking ANSI-C Programs, Tools and Algorithms for the Construction and Analysis of Systems 2004