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.

翻译：安全增强型Linux（SELinux）是一种支持基于角色访问控制（RBAC）机制的Linux内核模块。它提供了细粒度的安全框架，使系统管理员能够在系统和应用程序层面定义安全策略。尽管SELinux通过可定制且功能强大的RBAC模型提供了稳健的安全特性，但其手工策略管理容易出错，导致系统可能因意外配置错误或漏洞而存在安全隐患。我们提出了一种工具，可将SELinux策略自动转换为可满足性模理论（SMT），从而利用自动化定理证明验证预期的安全配置。该工具能够通过断言用户提供的RBAC策略与SMT中指定的意图规范之间的一致性，标记常见的策略配置错误。RBAC策略本质上难以进行全面验证。我们预期，此处提出的自动化工具可进一步扩展，以识别更广泛的策略配置错误，从而减轻系统管理员管理复杂策略的负担。