Automated firmware testing using firmware-hardware interaction patterns

ABSTRACT

Firmware is low-level software which can directly access hardware and is often shipped with the hardware platform. This component of the system is increasing in scale and importance, and thus firmware validation is a critical part of system validation. Firmware validation relies on the interacting hardware components which are usually not available until the late design stages. This is generally addressed through co-simulating C/C++ based firmware code and HDL hardware models (including SystemC). However, this tends to be slow, and is further exacerbated by the large number of possible interleavings between the concurrent firmware and hardware threads. Typically, in the co-simulation, the scheduler, such as the SystemC scheduler, will only explore a single, or at best a small number of possible firmware-hardware interleavings and thus may miss critical bugs. In this paper we present an alternative approach to firmware validation that is based on automatically generating a test-set for the firmware with the goal of complete path coverage while considering its interactions with hardware and other firmware threads. It uses a service-function based Transaction Level Model (TLM) which has been used in the past for firmware-hardware codesign. The test generation is based on concolic testing which has been used successfully in software test generation. However, existing concolic testing tools are used for test-generation of sequential code, and cannot directly consider the interaction of other hardware/firmware threads with the target firmware thread during test generation. We address this limitation by exploiting specific interaction patterns between the firmware and hardware threads that can be analyzed from the TLM. We show how these patterns, along with the firmware and hardware threads are used to automatically generate a sequential program that is test-equivalent to the target firmware transaction and that can be used with a standard sequential program concolic test generator. The tests generated can be (i) directly used for the firmware transaction and (ii) account for the multi-threaded interactions. These interaction patterns are practically relevant as they occur often in practice in real firmware benchmarks such as Linux device driver code, and its interacting QEMU emulated hardware code. Finally, we demonstrate the efficacy of our techniques for these benchmarks through a practical implementation that is automated and built on top of Frama-C, a static code analyzer, and KLEE, a concolic testing tool.

References

1. Rockbox - Free Music Player Firmware. http://www.rockbox.org.
2. S. Ahn and S. Malik. Modeling firmware as service functions and its application to test generation. In Hardware and Software: Verification and Testing, pages 61--77. Springer, 2013.
3. N. Blanc and D. Kroening. Race analysis for SystemC using model checking. ACM TODAES, 15(3):21, 2010.
4. C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX conference on Operating systems design and implementation, pages 209--224, 2008.
5. K. T. Cheng and A. Krishnakumar. Automatic functional test generation using the extended finite state machine model. In Proceedings of the 30th international Design Automation Conference, pages 86--91. ACM, 1993.
6. E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems, pages 168--176. Springer, 2004.
7. J. Corbet, A. Rubini, and G. Kroah-Hartman. Linux device drivers. O'reilly, 2009.
8. P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-c. In Software Engineering and Formal Methods, pages 233--247. Springer, 2012.
9. P. Godefroid, N. Klarlund, and K. Sen. DART: directed automated random testing. In ACM Sigplan Notices, volume 40. ACM, 2005.
10. P. Godefroid, J. van Leeuwen, J. Hartmanis, G. Goos, and P. Wolper. Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. Springer, 1996.
11. A. Horn, M. Tautschnig, C. Val, L. Liang, T. Melham, J. Grundy, and D. Kroening. Formal co-validation of low-level hardware/software interfaces. In FMCAD. IEEE, 2013.
12. J. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385--394, 1976.
13. A. Lal and T. Reps. Reducing concurrent analysis under a context bound to sequential analysis. In Computer Aided Verification, pages 37--51. Springer, 2008.
14. A. Liguori. QEMU emulator user documentation. 2010. http://wiki.qemu.org/download/qemu-doc.html.
15. I. Mohor. Ethernet MAC 10/100 mbps. 2011. http://opencores.org/project,ethmac.
16. M. Musuvathi and S. Qadeer. CHESS: Systematic stress testing of concurrent software. In Logic-Based Program Synthesis and Transformation, pages 15--16. Springer, 2007.
17. S. Qadeer and D. Wu. KISS: keep it simple and sequential. ACM SIGPLAN Notices, 39, 2004.
18. L. Séméria and A. Ghosh. Methodology for hardware/software co-verification in c/c++. In Proceedings of the 2000 Asia and South Pacific Design Automation Conference. ACM, 2000.
19. K. Sen, D. Marinov, and G. Agha. CUTE: a concolic unit testing engine for C, volume 30. ACM, 2005.
20. S. Swan. SystemC transaction level models and RTL verification. In Proceedings of the 43rd annual Design Automation Conference, pages 90--92. ACM, 2006.
21. M. M. Swift, B. N. Bershad, and H. M. Levy. Improving the reliability of commodity operating systems. ACM SIGOPS Operating Systems Review, 37(5):207--222, 2003.
22. Texas Instruments. Digital Temperature Sensor with 2-Wire Interface. 2011.
23. F. Vahid and J. Wiley. Digital design. Wiley, 2006.

Index Terms

• Computer systems organization

  • Dependable and fault-tolerant systems and networks

  • Embedded and cyber-physical systems

  • Real-time systems

• General and reference

  • Cross-computing tools and techniques

    • Performance

• Networks

  • Network performance evaluation

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Software defect analysis

        • Software testing and debugging