Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost

摘要

Microsoft's Static Driver Verifier (SDV) pioneered the use of software model checking for ensuring that device drivers correctly use operating system (OS) APIs. However, the verification methodology has been difficult to extend in order to support either (a) new classes of drivers for which SDV does not already have a harness and stubs, or (b) memory-corruption properties. Any attempt to apply SDV out-of-the-box results in either false alarms due to the lack of environment modeling, or scalability issues when finding deeply nested bugs in the presence of a very large number of memory accesses. In this paper, we describe our experience designing and shipping a new class of checks known as angelic checks through SDV with the aid of angelic verification (AV) [1] technology, over a period of 4 years. AV pairs a precise inter-procedural assertion checker with automatic inference of likely specifications for the environment. AV helps compensate for the lack of environment modeling and regains scalability by making it possible to find deeply nested bugs, even for complex memory-corruption properties. These new rules have together found over a hundred confirmed defects during internal deployment at Microsoft, including several previously unknown high-impact potential security vulnerabilities. AV considerably increases the reach of SDV, both in terms of drivers as well as rules that it can support effectively.