Using Build-Integrated Static Checking to Preserve Correctness Invariants

摘要

A key missing link in the creation of secure and robust systems is finding a cost effective way to demonstrate and preserve correspondence between a software design and its implementation. This paper explores the use of software model checking techniques to validate selected design invariants in the EROS operating system kernel. Several global consistency policies in the EROS kernel can be expressed as finite state automata. Using the MOPS static checker, we have been able to validate the EROS kernel implementation against these automata. In the process, we have confirmed the practical utility of the basic verification technique, identified a number of desirable enhancements in MOPS, and located bugs in the EROS implementation. A key contribution of this paper is establishing that it is practical to integrate software model checking into normal development life cycle. Model checking is efficient enough that it does not add noticeably to our build times. This allows us to view it as a tool for error prevention rather than detection. Our work with EROS and MOPS suggests that domain specific application of software model checking is a practical and powerful technique for software assurance and maintenance.