Toward compositional verification of interruptible OS kernels and device drivers

DOI10.1007/S10817-017-9446-0MaRDI QIDQ1663225zbMATH OpenOpenAlexFDO

Authors Hao Chen, Xiongnan Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu

Publication date 21 August 2018

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-017-9446-0

zbMATH Keywords

modularityprogram verificationinterruptsabstraction layercertified OS kernelsdevice drivers

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
• Theorem Proving in Higher Order Logics
• Formal memory models for the verification of low-level operating-system code
• From a proven correct microkernel to trustworthy large systems
• Operating system verification---an overview

Cites work

• CONCUR 2004 - Concurrency Theory
• Certifying low-level programs with hardware interrupts and preemptive threads
• Dafny: an automatic program verifier for functional correctness
• Deep specifications and certified abstraction layers
• Formal verification of a C-like memory model and its uses for verifying program transformations
• Forward and backward simulations. I. Untimed Systems
• Isabelle. A generic theorem prover
• Mechanized semantics for the clight subset of the C language
• Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
• Toward compositional verification of interruptible OS kernels and device drivers

Cited in

(12)

• Theorem Proving in Higher Order Logics
• Modular verification of preemptive OS kernels
• Safe functional systems through integrity types and verified assembly
• Towards applying the composition principle to verify a microkernel operating system
• A modeling concept for formal verification of OS-based compositional software
• Modular verification of preemptive OS kernels
• Toward compositional verification of interruptible OS kernels and device drivers
• Certifying low-level programs with hardware interrupts and preemptive threads
• Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
• Noninterference for operating system kernels
• Formally verifying exceptions for low-level code with separation logic
• Deep specifications and certified abstraction layers

Describes a project that uses

Uses Software

• CertiKOS
• seL4
• CompCert
• z3
• SLAM
• Isabelle
• Dafny
• Coq

This page was built for publication: Toward compositional verification of interruptible OS kernels and device drivers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663225)