  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.

Cryptography and Security;Logic in Computer Science