论文标题：K-SELinux: formal analysis and verification of SELinux policies via semantic execution

期刊：Frontiers of Computer Science

作者：Jinhui KANG, Jianhong ZHAO, Yongwang ZHAO

发表时间：9 Dec 2024

DOI：10.1007/s11704-024-40495-7

微信链接：点击此处阅读微信文章

引用格式：

Jinhui KANG, Jianhong ZHAO, Yongwang ZHAO. K-SELinux: formal analysis and verification of SELinux policies via semantic execution. Front. Comput. Sci., 2026, 20(6): 2006201

阅读原文：

摘要

SELinux（安全增强型 Linux）是实现强制访问控制（MAC）的核心机制，但其策略语言极其复杂，且缺乏统一的形式化定义。浙江大学赵永望团队提出“语义执行验证”新视角，在 K 框架下首次全面形式化了 SELinux 策略语言的语义。基于此开发的 K-SELinux 框架集成了符号执行与状态搜索技术，能够对数万条策略语句进行自动化一致性检查与安全性验证。实验证明，该方法在处理主流发行版及 Android AOSP 策略时，能有效发现潜在的安全漏洞，且具备严谨的形式化保障。

文章精要

现代操作系统安全性高度依赖于 SELinux 等强制访问控制机制，但其策略管理面临一个核心技术痛点：策略语言的复杂性与规模呈指数级增长。一个典型的 Linux 发行版策略往往包含数万条规则，依靠人工审计几乎不可能确保其逻辑的完备性与一致性。现有的策略分析工具大多局限于特定的语义子集或简单的完整性检查，缺乏对策略执行路径的深度挖掘，更无法为严苛安全环境（如航空航天、金融核心网）提供数学意义上的形式化安全保证。

为了解决这一难题，浙江大学赵永望团队提出了 K-SELinux 框架。该研究摒弃了传统的经验式分析，转而利用形式化方法领域的“K 框架”为 SELinux 策略赋予了精确的数学语义。框架核心包含两个关键阶段：首先，通过对 SELinux 的类型强制（TE）、角色访问控制（RBAC）等核心组件进行严谨建模，构建了其运行时的动态语义；其次，引入语义执行（Semantic Execution）技术，支持通过符号化搜索直接验证特定的安全属性（如：某些特权进程是否可能越权访问敏感文件）。这种设计使得安全管理员能够像调试程序代码一样，对庞杂的策略库进行逻辑归纳与漏洞探测。

研究表明，在对 Fedora、Refpolicy 以及多个 Android 版本（如 Android 8/9/10）的实际策略进行评估时，K-SELinux 展现出了卓越的分析深度。数据显示，该方案不仅能精准复现已知的权限配置错误，还揭示了传统工具难以察觉的隐蔽冲突路径。通过形式化语义验证，策略的误配置风险大幅降低。这一研究不仅为操作系统安全策略的生命周期管理提供了强有力的理论支撑，也为构建具备可证明安全性的下一代可信操作系统提供了关键的技术路径。

期刊简介

Frontiers of Computer Science （FCS）是由教育部主管、高等教育出版社和北京航空航天大学共同主办，南京大学支持，SpringerNature 公司海外发行的英文学术期刊。本刊于 2007 年创刊，月刊，全球发行。主要刊登计算机科学领域具有创新性的综述论文、研究论文等。本刊主编为周志华院士，共同主编为熊璋教授。编委会及青年 AE 团队由国内外知名学者及优秀青年学者组成。本刊被 SCI、Ei、DBLP、INSPEC、SCOPUS 和中国科学引文数据库（CSCD）核心库等收录，为 CCF 推荐B类期刊；两次入选“中国科技期刊国际影响力提升计划”；入选“第4届中国国际化精品科技期刊”；两次入选“中国科技期刊卓越行动计划”（一期梯队、二期领军）。