详细内容或原文请订阅后点击阅览
形式验证系统在标准 SELinux 策略中发现漏洞
已经开发出一种工具，可以自动验证负责加强操作系统安全的 Linux 组件的访问控制规则。
来源:OSP网站大数据新闻SELinux是负责强制访问控制的Linux内核模块，其安全策略由数千条规则组成，非常复杂。手动检查它们几乎是不可能的。然而，在工业设施等关键环境中，需要对配置的可靠性进行严格的数学证明。现有的自动审计工具只能解决特定问题，例如检查规则的完整性或一致性，但尚不存在通用的方法。
来自浙江大学（中国）的科学家提出了一个解决方案：他们使用 K Framework（一种编程语言的数学验证环境）描述了 SELinux 规则语言。它的公式描述了语言的语法和规律，K Framework 生成一个语言模拟器，可以根据这些规律逐步执行命令。此外，该环境还提供了定理证明模块，可以让您逻辑地检查某种情况在被验证的系统中是否可能。
作者创建了一个基于 K Framework 的软件包，该软件包在模拟器上运行 SELinux 规则并使用定理证明器对其进行验证。同时，该工具使用户有机会以单一格式设置任何要求，包括基本要求（机密性、完整性等）和特殊要求，具体取决于场景和环境。
系统原型使用真实的 SElinux 策略 - refpolicy 和 AOSP 进行了测试。第一个是各种系统的参考基线策略，第二个是由 Google 开发的，定义了 Android 中隔离应用程序和系统服务的规则。综合体发现两者都存在大量问题，包括逻辑矛盾、隐藏冲突、特权过多等。
未来，作者打算加快该工具的运行速度并简化其界面，以便系统管理员不需要深厚的数理逻辑知识来分析规则。