本文针对操作系统内核中 I/O 分离不足导致的安全问题，提出了一种形式化的 I/O 分离模型。该模型基于 I/O 传输授权定义分离策略，与具体硬件无关，能够防止恶意驱动通过操控设备绕过 I/O 隔离。作者在 Dafny 语言中对该模型进行了形式化规约、精化以及在 Wimpy 内核设计中的实例化验证，并自动生成了经过验证的正确汇编代码。通过形式化建模，发现了原 Wimpy 内核中先前未知的设计与实现漏洞。最后，论文概述了该模型在其他 I/O 内核上的适用性。本研究为高可信的 I/O 安全内核开发提供了理论基础和自动化工具，适合操作系统安全、形式化验证领域的研究者阅读。