OSVAuto: automatic proofs about functional specifications in OS verification

TL;DR

OSVAuto is an automated proof system tailored for verifying functional specifications in OS kernels, efficiently handling common data types and reducing manual proof effort through SMT solving techniques.

Contribution

It introduces an algorithm supporting native OS verification data types and extends quantifier instantiation methods for sequences, enabling more automatic proofs.

Findings

Successfully applied to uC-OS/II kernel proofs

Automatically solved many proof obligations

Reduced manual proof effort significantly

Abstract

We present OSVAuto for automatic proofs about functional specifications that commonly arise when verifying operating system kernels. The algorithm behind OSVAuto is designed to support natively those data types that commonly occur in OS verification, including sequences, maps, structures and enumerations. Propositions about these data are encoded into a form that is suitable for SMT solving. For quantifier instantiation, we propose an extension of recent work for automatic proofs about sequences. We evaluate the algorithm on proof obligations adapted from existing verification of the uC-OS/II kernel in Coq, demonstrating that a large number of proof obligations can be solved automatically, significantly reducing the proof effort on the functional side.