Automatic verification of active device drivers

Abstract

We develop a practical solution to the problem of automatic verification of the interface between device drivers and the operating system. Our solution relies on a combination of improved driver architecture and verification tools. Unlike previous proposals for verification-friendly drivers, our methodology supports drivers written in C and can be implemented in any existing OS. Our Linuxbased evaluation shows that this methodology amplifies the power of existing model checking tools in detecting driver bugs, making it possible to verify properties that are beyond the reach of traditional techniques.

References

1. ADYA, A., HOWELL, J., THEIMER, M., BOLOSKY, W., AND DOUCEUR, J. Cooperative task management without manual stack management. In 2002 USENIX (Monterey, CA, USA, Jun 2002), pp. 289--302.
2. BALL, T., BOUNIMOVA, E., COOK, B., LEVIN, V., LICHTENBERG, J., MCGARVEY, C., ONDRUSEK, B., RAJAMANI, S. K., AND USTUNER, A. Thorough static analysis of device drivers. In 1st EuroSys Conf. (Leuven, Belgium, Apr 2006), pp. 73--85.
3. BALL, T., COOK, B., DAS, S., AND RAJAMANI, S. K. Refining approximations in software predicate abstraction. In TACAS (Mar 2004), pp. 388--403.
4. BARNES, F., AND RITSON, C. Checking process-oriented operating system behaviour using CSP and refinement. Operat. Syst. Rev. 43, 4 (Oct 2009), 45--49.
5. BASLER, G., DONALDSON, A. F., KAISER, A., KROENING, D., TAUTSCHNIG, M., AND WAHL, T. SatAbs: A bit-precise verifier for C programs - (competition contribution). In TACAS (Mar 2012), pp. 552--555.
6. BASLER, G., HAGUE, M., KROENING, D., ONG, C.-H. L., WAHL, T., AND ZHAO, H. Boom: Taking boolean program model checking one step further. In TACAS (2010), vol. 6015 of Lecture Notes in Computer Science, Springer, pp. 145--149.
7. BERRY, G., GONTHIER, G., GONTHIER, A. B. G., AND LALTTE, P. S. The esterel synchronous programming language: Design, semantics, implementation, 1992.
8. CHANDRASEKARAN, P., CONWAY, C. L., JOY, J. M., AND RAJAMANI, S. K. Programming asynchronous layers with CLARITY. In 6th ESEC (Dubrovnik, Croatia, 2007), pp. 65--74.
9. CHOU, A., YANG, J.-F., CHELF, B., HALLEM, S., AND ENGLER, D. An empirical study of operating systems errors. In 18th SOSP (Lake Louise, Alta, Canada, Oct 2001), pp. 73--88.
10. CLARKE, E. M., KROENING, D., SHARYGINA, N., AND YORAV, K. Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design 25, 2-3 (2004), 105--127.
11. COOK, B., PODELSKI, A., AND RYBALCHENKO, A. Termination proofs for systems code. In 2006 PLDI (Ottawa, Ontario, Canada, 2006), pp. 415--426.
12. DESAI, A., GUPTA, V., JACKSON, E., QADEER, S., RAJAMANI, S., AND ZUFFEREY, D. P: safe asynchronous eventdriven programming. In PLDI (Seattle,Washington, USA, 2013), pp. 321--332.
13. FAHNDRICH, M., AIKEN, M., HAWBLITZEL, C., HODSON, O., HUNT, G. C., LARUS, J. R., AND LEVI, S. Language support for fast and reliable message-based communication in Singularity OS. In 1st EuroSys Conf. (Apr 2006), pp. 177--190.
14. FEHNKER, A., HUUCK, R., JAYET, P., LUSSENBURG, M., AND RAUCH, F. Goanna -- A Static Model Checker. In 11th FMICS (Bonn, Germany, Aug 2006), pp. 297--300.
15. GANAPATHI, A., GANAPATHI, V., AND PATTERSON, D. Windows XP kernel crash analysis. In 20th LISA (Washington, DC, USA, 2006), pp. 101--111.
16. HAREL, D. Statecharts: A visual formalism for complex systems. Science of Computer Programming 8, 3 (Jun 1987), 231--274.
17. HENZINGER, T. A., JHALA, R., MAJUMDAR, R., NECULA, G. C., SUTRE, G., AND WEIMER, W. Temporal-safety proofs for systems code. In 14th CAV (2002), pp. 526--538.
18. HOLZMANN, G. J. Logic verification of ANSI-C code with SPIN. In 7th SPIN (2000), pp. 131--147.
19. HOLZMANN, G. J. The SPIN Model Checker: Primer and Reference Manual, 1st ed. Addison-Wesley Professional, 2003.
20. LIEDTKE, J., BARTLING, U., BEYER, U., HEINRICHS, D., RULAND, R., AND SZALAY, G. Two years of experience with a ?-kernel based OS. Operat. Syst. Rev. 25, 2 (Apr 1991), 51--62.
21. PADIOLEAU, Y., LAWALL, J., HANSEN, R. R., AND MULLER, G. Documenting and automating collateral evolutions in Linux device drivers. In 3rd EuroSys Conf. (Glasgow, UK, Apr 2008), pp. 247--260.
22. PALIX, N., THOMAS, G., SAHA, S., CALV`ES, C., LAWALL, J., AND MULLER, G. Faults in Linux: ten years later. In ASPLOS (Newport Beach, CA, USA, Mar 2011), pp. 305--318.
23. RYZHYK, L., CHUBB, P., KUZ, I., AND HEISER, G. Dingo: Taming device drivers. In 4th EuroSys Conf. (Apr 2009).
24. RYZHYK, L., CHUBB, P., KUZ, I., AND HEISER, G. Dingo: Taming device drivers. In 4th EuroSys Conf. (Nuremberg, Germany, Apr 2009).
25. WITKOWSKI, T., BLANC, N., KROENING, D., AND WEISSENBACHER, G. Model checking concurrent Linux device drivers. In 22nd ASE (Atlanta, Georgia, USA, 2007), pp. 501--504.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Contextual software domains

      • Operating systems

    • Software functional properties

      • Formal methods

        • Model checking

• Theory of computation

  • Semantics and reasoning

    • Program semantics