Title	
Language-Support for Correct and Reliable Enforcement of Access Control Policies

Authors	
Peter Amthor

E-Mail	
peter.amthor@tu-ilmenau.de

Affiliation	
Technische Universität Ilmenau

Abstract	

As highlighted by security-focused OS mechanisms such as SELinux, Solaris Trusted Extensions, or TaintDroid, a mandatory access control (AC) policy is the fundamental corner stone of any security guarantees. A correct and reliably enforced AC policy provides a solid and reliable defense against privilege escalation attacks, i.e. threats such as root kit malware and ransomware. Both requirements are covered in the well-known reference monitor (RM) principle: while the verifiability requirement demands both correctness by design and formally provable properties, the total mediation and tamperproofness requirements focus on reliable enforcement of a policy. Such abstract requirements contrast with a practical process of design, specification and implementation of an AC policy, which inevitably introduces the human element of de-abstraction and decision-making. To minimize the impact of this, specialized languages used for these tasks have to satisfy a diverse range of requirements: **Adequate abstractions:** The semantics and granularity of abstractions used to specify a policy, e.g. user attributes, object classes, domains etc., should match those used in the enforcing system. A widely adopted approach is the use of a specification language for attribute-based access control (ABAC). **Verifiability:** The policy logic should be verifiable against formal properties, e.g. privilege escalation _safety_ or _workflow satisfiability_. This inevitably involves representing the policy in an adequately expressive formal calculus. **Ergonomics:** Syntax, semantics and idiomatics of a language used to implement the policy, e.g. in an OS kernel module or a server process, should constructively avoid errors that invalidate any previously achieved correctness guarantees. **Reliable enforcement:** As an interface to enforce a policy, a generalized runtime environment (RTE) is required which enforces both total mediation and tamperproofness of the policy implementation, independent of their OS- and application-specific specification. As becomes apparent, all four requirements depend on languages to represent an AC policy that significantly differ in level of abstraction, expressiveness, syntax, and semantics. This results in several, possibly error-prone translation steps. Paradoxically, such translations counter the very goal of the individual languages in this process, since they again allow errors to be introduced through manual interpretation and rewriting. In our work to be presented based on this abstract, we argue for an approach to AC policy engineering and implementation that aims at two goals: (1) whenever possible, translations between heterogeneous policy representations should be done automatically; (2) whenever inevitable, manual translations effort should be as low as possible. Based on original contributions towards these goals, we illustrate how we can already model, specify and translate an ABAC policy to an actual implementation in the Rust programming language. We introduce DynaMo, a novel policy specification language, which features a syntax and semantics derived from mathematical notation conventions of a flexible formal ABAC calculus. Based on a state-machine simulation implemented for this calculus, it enables automated analyses of dynamic security properties. We further present as ongoing work: a transpiler from to the Rust programming language for correct policy implementation. We conclude with `dabac-rs`, a prototype of a policy-neutral RTE, to be integrated in systems software as a ready-made Rust crate.

Language of the Presentation	
English