Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

OSVAuto: automatic proofs about functional specifications in OS verification

Yulun Wu, Bican Xia, Jiale Xu, Bohua Zhan, Tianqi Zhao

TL;DR

OSVAuto addresses the automation gap in proving functional specifications for OS kernel verification by extending sequence-oriented quantifier instantiation to nested sequences, maps, structures, and enumerations. It introduces a specialized language and a four-step algorithm (Normalize, Instantiation, Encoding, Solve) with a classification-graph mechanism and heuristic generation cutoffs to drive SMT solving. Implemented in Python and interfaced with Z3, OSVAuto is evaluated on the μC/OS-II kernel verification in Coq, solving many obligations automatically and reducing manual proof effort. The work demonstrates practical automation for OS verification data types and discusses limitations and avenues for improving completeness and handling uniqueness constraints in proof goals.

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.

OSVAuto: automatic proofs about functional specifications in OS verification

TL;DR

OSVAuto addresses the automation gap in proving functional specifications for OS kernel verification by extending sequence-oriented quantifier instantiation to nested sequences, maps, structures, and enumerations. It introduces a specialized language and a four-step algorithm (Normalize, Instantiation, Encoding, Solve) with a classification-graph mechanism and heuristic generation cutoffs to drive SMT solving. Implemented in Python and interfaced with Z3, OSVAuto is evaluated on the μC/OS-II kernel verification in Coq, solving many obligations automatically and reducing manual proof effort. The work demonstrates practical automation for OS verification data types and discusses limitations and avenues for improving completeness and handling uniqueness constraints in proof goals.

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.
Paper Structure (21 sections, 1 theorem, 17 equations, 3 figures, 1 table)

This paper contains 21 sections, 1 theorem, 17 equations, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Automation of sequence theory
  4. Verification of the $\mu$C/OS-II kernel
  5. Language
  6. Types
  7. Terms
  8. Function definitions and proof obligations
  9. Generalized atomic terms
  10. Algorithm
  11. Normalization
  12. Quantifier instantiation
  13. SMT Encoding
  14. Examples
  15. Variant of the append example
  16. ...and 6 more sections

Key Result

theorem 1

The above normalization procedure results in a proof goal consisting only of generalized atomic terms, constants, logical and arithmetic operators (including if-then-else), and quantifiers. Equalities are applied only to terms of primitive type.

Figures (3)

  • Figure 1: Examples of high-level and low-level task control blocks.
  • Figure 2: Part of the refinement relation for task control blocks (task is suspended while also waiting for a semaphore).
  • Figure 3: An example of proof obligation from verifying API function for suspending a task. The predicates RL_TCB_P and RL_Tbl_Grp_P are invariants on the low-level global state. OSTaskSuspend and OSTaskSuspendAbs are functional specifications for suspend on the low-level and high-level respectively. Some definitions are omitted for reason of space.

Theorems & Definitions (2)

  • definition 1
  • theorem 1