Modal Verification Patterns for Systems Software

TL;DR

This paper advocates for using modal logic as a primary approach to specify and verify low-level systems software, emphasizing resource contexts and illustrating successful prior applications.

Contribution

It introduces the concept of resource contexts to guide the design of modal verification methods for systems code, proposing a unified verification pattern.

Findings

Modal logic effectively models low-level systems behaviors.

Resource contexts assist in designing verification modalities.

Prior systems successfully applying modalities support this approach.

Abstract

Although they differ in the functionality they offer, low-level systems exhibit certain patterns of design and utilization of computing resources. In this paper, we argue the position that modalities, in the sense of modal logic, should be a go-to approach when specifying and verifying low-level systems code. We explain how the concept of a resource context helps guide the design of new modalities for verification of systems code, and we justify our perspective by discussing prior systems that have used modalities for systems verification successfully, arguing that they fit into the verification design pattern we articulate, and explaining how this approach might apply to other systems verification challenges.