使用 SMT 自动化验证 SELinux RBAC 策略
Automated SELinux RBAC Policy Verification Using SMT
AI总结：
本文提出将 SELinux RBAC 策略自动转换为 SMT 并借助定理证明检查其与预期规范一致性的工具，以发现常见策略错误配置。
摘要：
Security-Enhanced Linux（SELinux）是一个 Linux 内核模块，支持基于角色的访问控制（RBAC）机制。它提供了一个细粒度安全框架，使系统管理员能够在系统和应用层面定义安全策略。尽管 SELinux 通过可定制且强大的 RBAC 模型提供了稳健的安全特性，但其手动策略管理容易出错，使系统面临意外错误配置或漏洞的风险。我们提出一种工具，可将 SELinux 策略自动转换为可满足性模理论（SMT），从而利用自动定理证明验证预期的安全配置。该工具能够通过在 SMT 中断言所提供的 RBAC 策略与用户预期规范之间的一致性，标记常见的策略错误配置。RBAC 策略本质上复杂，难以完全验证。我们设想，本文提出的自动化工具可进一步扩展，以识别范围更广的策略错误配置，减轻系统管理员管理复杂策略的负担。
英文摘要：
Security-Enhanced Linux (SELinux) is a Linux kernel module that allows for a role-based access control (RBAC) mechanism. It provides a fine-grained security framework enabling system administrators to define security policies at the system and application level. Whilst SELinux offers robust security features through a customisable, powerful RBAC model, its manual policy management is prone to error, leaving the system vulnerable to accidental misconfigurations or loopholes. We present a tool to automate the conversion of SELinux policies into satisfiability modulo theories (SMT), enabling the verification of the intended security configurations using automated theorem proving. Our tool is capable of flagging common policy misconfigurations by asserting consistency between supplied RBAC policies and the intended specification by the user in SMT. RBAC policies are inherently complicated to verify entirely. We envision that the automated tool presented here can be further extended to identify an even broader range of policy misconfigurations, relieving the burden of managing convoluted policies on system administrators.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
