基于 SeL4 的 OpenBSD 设备驱动形式化验证
密码学与安全
2023-11-08 v1 计算机科学中的逻辑
操作系统
摘要
seL4 微内核是目前唯一经过完全形式化验证的内核。总体而言，对确保内核代码安全性的日益关注源于其在整个操作系统中的重要角色。操作系统的基本特性之一是抽象对设备的处理。这种抽象由设备驱动程序——管理硬件的软件——来体现。对软件组件的正确验证可确保设备正常工作，除非发生硬件故障。本文中，我们选择对设备驱动的行为建模，并构建代码实现与预期行为相符的证明。该证明在 Isabelle/HOL 中撰写，从 C 到 Isabelle 的代码翻译通过 C-to-Isabelle Parser 与 AutoCorres 工具自动完成。我们选择 Isabelle 定理证明器，是因为其效率已通过 seL4 微内核的验证得到证实。
引用
@article{arxiv.2311.03585,
title = {OpenBSD formal driver verification with SeL4},
author = {Adriana Nicolae and Paul Irofti and Ioana Leustean},
journal= {arXiv preprint arXiv:2311.03585},
year = {2023}
}