TEpla: A Certified Type Enforcement Access-Control Policy Language

Abstract

In today's information era, the security of computer systems as resources of invaluable information is of crucial importance not just to security administrators but also to users of these systems. Access control is an information security process which guards protected resources against unauthorized access as specified by restrictions in security policies. One significant obstacle to regulate access in secure systems is the lack of formal semantics and specifications for the policy languages which are used in writing security policies.

Expressing security policies that are implemented pursuant to required security goals and that accommodate security policy rules correctly is of high importance to the system's integrity, confidentiality, and availability. The semantics of the most widely used policy languages such as SELinux is expressed in a declarative manner using a colloquial natural language (e.g., English), which leads to ambiguity in the interpretation of the policy statements. For this reason, both the development and the analysis of security policies are generally imprecise and based on cognitive concepts; that is to say, they are not conducted in a mathematically-precise and verifiable way.

Type Enforcement (TE) is a MAC (Mandatory Access Control) access control mechanism that is used in the SELinux security module. Type Enforcement (TE) is implemented based on the type/domain field of security contexts. TE allows the creation of different domains in the system by assigning subjects to domains and subsequently associating them with objects. TE mandates a central policy-driven approach to access control.

We propose a small and certifiably correct TE policy language, TEpla, as an appropriate candidate for the primary access control feature of SELinux, Type Enforcement. TEpla can provide ease of use, analysis, and verification of its properties. TEpla is a certified policy language with formal semantics, exposing ease of reasoning and allowing verification. We use the Coq proof assistant to mechanize semantics and to machine-check the proofs of TEpla, ensuring correctness guarantees are provided. Having a certified semantics simplifies and fosters the development of certified tools for policy-related tasks such as automating various kind of policy analyses.