Automatic kernel code synthesis and verification

Qiang Zhang

doi:10.1016/j.cose.2020.101733

Automatic kernel code synthesis and verification

2020-04-01

2

PRE

AI

DOI：10.1016/j.cose.2020.101733

Original

Original request for help

Save

Abstract

En 中文

Formal verification of an OS kernel is widely considered a major challenge; however, traditional interactive theorem provers used in OS kernel verification require manually written proofs and come with a non-trivial cost. In this paper, we propose a formal verification framework to build a verifiably correct OS kernel, named iv6, with a high degree of proof automation and a low burden of proof. Using this framework, programmers only need to write the specification as required, and it can be translated into the corresponding implementation of C code automatically. The verification framework can guarantee that the behaviour of the implementation code adheres to its specifications. Iv6 introduces four key ideas to achieve proof automation: its interfaces and corresponding specifications are designed to be finite to avoid unbounded loops or recursion; it separates kernel and user address spaces using a kernel page table isolation approach to simplify reasoning about virtual memory; it partitions the modules of a kernel state machine according to a state transition function to improve verification performance; and to avoid modelling complicated C semantics, it performs verification at the LLVM intermediate representation level. A total of 48 system calls and some high-level system properties in iv6 have been verified using this method. Experience shows that this framework can reduce the impact of human error on kernel development and make the verification of iv6 more efficient and straightforward. (C) 2020 Elsevier Ltd. All rights reserved.

Keywords:

Operating system

Formal verification

Functional correctness

Symbolic execution

RISCV

Code synthesis

Automatic kernel code synthesis and verification

Abstract

AI Summary

Journal

Organization

Cited Papers