计算机工程

作者：王梓, 王洪强, 杨晓艺, 兰雨晴

单位：1. 北京航空航天大学网络空间安全学院, 北京 1001912. 北京航空航天大学软件学院, 北京 100191

关键词：操作系统,形式化方法,形式规约,形式验证,系统安全

操作系统(OS)作为信息时代关键基础设施, 广泛应用于军事、工业、医疗等核心领域。其可靠性与安全性直接决定关键领域运行稳定, 漏洞易致系统崩溃、数据泄露等严重后果, 因此构建系统化安全保障体系具有重要理论与工程价值。以"形式规约-形式验证-工程落地"为框架, 梳理近十年该领域研究成果, 剖析技术路径与实践应用。在形式规约层面, 明确基于迁移系统等数学结构描述系统功能的模型规约与基于线性时序逻辑(LTL)定义安全、活性需求的性质规约的差异, 从功能正确性和安全属性两个方面进行阐述, 其中, 功能正确性涵盖任务管理调度、内存分配回收、异常中断处理、任务间通信与文件系统读写一致性, 安全属性聚焦访问控制的BLP模型与BIBA模型、分离内核多域隔离、信息流无干扰与无泄漏理论。在形式验证层面, 阐述依托霍尔逻辑验证程序一致性的推理证明、基于LTL与计算树逻辑(CTL)验证时序属性的模型检测、属性验证标准化流程3类核心方法, 并以首个通过机器证明实现功能正确与信息流无干扰的seL4微内核为案例, 揭示理论到工程的转化路径。在工程应用上, 总结汽车领域控制器局域网(CAN)总线通信验证、智能手机Android系统组件间通信鲁棒性检测的成果。本文的系统性梳理旨在为相关领域的研究奠定基础, 为大语言模型提供数据集支持, 并为最终的技术工程落地提供参考。

来源：2026年第2期

《计算机工程》期刊编辑部

查看计算机工程杂志2026年第2期