Policy Description Language for Authorization using Logic-Based Programming

This paper proposes a Datalog-based policy description language that enables fine-grained access control by incorporating dynamic application process states, demonstrating its effectiveness through the successful composition and evaluation of SELinux policies within a Defense-in-Depth strategy.

The Gist

Imagine you are the head of security for a massive, high-tech castle. Your goal is to protect the most valuable treasures inside. In the past, security guards (the "policies") would stand at every single door and check a long, handwritten list of rules for every single person trying to enter.

The Problem: The "Wall of Paper" Issue
The authors of this paper argue that modern computer systems are like castles that have grown so huge and complex that writing a unique rule for every single door and every single person is impossible.

• The Old Way (like SELinux): Imagine a security guard holding a stack of 40,000 individual index cards. Each card says, "Person A can open Door B with Key C." If you want to change the rules for a whole group of people, you have to rewrite thousands of cards. It's messy, hard to read, and easy to make a mistake.
• The Goal: The authors want to stop writing 40,000 separate cards and instead write a single, smart "instruction manual" that covers all of them.

The Solution: A "Smart Recipe Book" (Logic-Based Programming)
The authors propose a new language that acts like a smart recipe book or a computer program for security rules. Instead of listing every single permission, you write "recipes" (logic programs) that explain how permissions work.

Here is how their "recipe book" works, using simple analogies:

1. Grouping (The "Uniform" Analogy):
   Instead of saying "Bob can open the vault," "Alice can open the vault," and "Charlie can open the vault," you write one rule: "Anyone wearing a Manager's Uniform can open the vault."
   In the paper, this is called hierarchical inheritance. If you put a "Manager's Uniform" on Bob, he automatically gets all the rules for managers. You don't have to write a new rule for him; the system knows he belongs to that group.

2. Subroutines (The "Assembly Line" Analogy):
   Imagine a factory where a product goes through three steps: Prep, Cook, and Pack. Instead of writing a new rule for every worker at every station, you write one rule for the "Prep Station" and one for the "Cook Station."
   The authors call this subroutinization. You can define a "step" in a process (like a transaction) and say, "Once the 'Prep' step is done, the worker automatically moves to the 'Cook' step." This lets you describe complex, multi-step security processes with just a few lines of text instead of thousands.

3. Dynamic Status (The "Traffic Light" Analogy):
   Sometimes, a rule depends on what is happening right now. For example, "You can only enter the kitchen if the 'Fire Alarm' is off."
   The new language can handle these changing conditions. It can say, "If the system is currently 'tainted' (like a red traffic light), no one can enter." This allows security to react to the current state of the computer, not just static lists.

The Experiment: Testing the New System
The authors didn't just write the recipe book; they tested it against the real thing.

• The Test: They took the massive security policy of SELinux (a real, widely-used security system for Linux) and translated it into their new "recipe book" language.
• The Result (Accuracy): They asked both the old system and the new system the same 15 million questions (e.g., "Can User X do Action Y?"). The answers matched 99% of the time. This proves the new language is just as accurate as the old, complex one.
• The Result (Efficiency): This is where the magic happened. The original SELinux policy took 6,524 lines of code (and 133 pages of paper). The new language described the exact same security rules in just 335 lines (95 pages). They shrank the policy by about 95%.

Why This Matters
The paper concludes that while the old way (writing every rule individually) is easy to understand if you look at just one rule, it becomes a nightmare when you look at the whole system.

The new language is like switching from writing a dictionary of 40,000 individual words to writing a grammar book.

• Pros: It makes the whole system much smaller, easier to manage, and easier to see the "big picture." It allows security to be more flexible and adaptable.
• Cons: If you look at just one single rule in the new system, it might look a bit more abstract (like a math formula) than a simple sentence. But for managing a massive, complex system, the "grammar book" approach is far superior.

In short, the authors built a tool that lets security experts describe complex, multi-layered defenses using smart, reusable logic instead of drowning in a sea of repetitive, individual rules.

Technical Summary

Technical Summary: Policy Description Language for Authorization Using Logic-Based Programming

Problem Statement

Modern information systems are increasingly large-scale and complex, making it impossible to eradicate all vulnerabilities. Consequently, the Defense-in-Depth strategy is adopted, which relies on strict multi-layer partitioning of systems to delay attacks and localize damage. The effectiveness of this strategy depends on fine-grained mandatory access control (MAC). However, implementing fine-grained MAC presents a significant challenge: the volume of access control rules required becomes enormous.

Existing implementations, such as SELinux, describe policies by listing individual access control rules directly. As granularity increases, the policy description grows huge, making it difficult to grasp the policy's overall behavior without dedicated verification tools. Furthermore, conventional policy description languages (e.g., SDSI, SPKI, PolicyMaker) often lack the flexibility to define application-specific predicates or handle the structural complexity required for efficient policy management in multi-layer defense scenarios. The core problem is the lack of a policy description language that can concisely describe huge policies while maintaining logical correctness and supporting structural abstraction.

Methodology

The authors propose a Policy Description Language based on logic-based programming, specifically implemented using Datalog (a subset of Prolog). The methodology involves three main components:

1. Language Design

The language defines a policy as a set of Declarative Statements (DS) and allows for Authorization Queries (Q).

• Syntax: The language uses a syntax similar to English, based on predicate logic. Key predicates include:
  • is permitted to / is forbidden to: Defines access rights between a subject and an object.
  • moves to: Defines state transitions of a subject triggered by an operation.
  • inherits: Allows attributes to inherit permissions from other attributes.
• Formal Semantics: The language defines formal inference rules to derive facts:
  • Inference Rule (a): Automatically derives specific facts from conditional statements when variable terms are substituted with constants.
  • Inference Rule (b): Automatically derives permissions for an attribute that inherits from another attribute, enabling hierarchical permission propagation.
• Implementation: The language is translated into Datalog programs. Declarative statements become Datalog clauses, and authorization queries are evaluated against these clauses using the XSB Datalog system, which supports well-founded semantics and tabled predicates to prevent infinite loops.

2. Structural Description Methods

To address the complexity of policy description, the authors propose two structural techniques:

• Hierarchization of Elements: Similar to Role-Based Access Control (RBAC), this groups access control rules under abstract attributes (e.g., roles). Rules are defined for variables (e.g., x tagged MANAGER) and expanded when specific subjects are assigned those attributes.
• Structuring Authorization Procedures: Similar to Task-Based Access Control (TBAC), this subroutinizes authorization procedures. The moves to predicate allows the language to abstract state transitions (e.g., moving from a PREPARE_PHASE to a COMMIT_PHASE), allowing complex transaction flows to be described concisely.

3. Evaluation Strategy

The authors constructed an experimental system to evaluate the language:

• Validity: They translated the existing SELinux policy into the proposed language. They compared the authorization decisions (Access Vectors) generated by the original SELinux kernel mechanism against those generated by the Datalog implementation across 15,100,162 query combinations.
• Expressiveness: They compared the source-code line count and listing page count of the original SELinux policy against the proposed language's C-List style and ACL style implementations.

Key Contributions

1. A Logic-Based Policy Language: The proposal of a language that expresses access control rules as logic programs, enabling attribute inheritance and subroutine-like structuring of authorization procedures.
2. Formal Semantics and Inference Rules: The definition of formal semantics and inference rules that allow for the automatic derivation of permissions based on attribute hierarchies and conditional transitions.
3. Datalog Implementation: A concrete implementation using XSB that translates the policy language into a rule-based system capable of handling large-scale data exchange.
4. Structural Abstraction for MAC: A method to describe access control models (like RBAC and TBAC) structurally, reducing the need to list every individual rule explicitly.

Results

• Validity: In the comparison with SELinux, the proposed language produced identical authorization responses (Access Vectors) for 99.95% of the 15,100,162 queries tested. The remaining ~0.05% of mismatches were attributed to queries involving dynamically generated contexts during system operation, which depend on argument passing mechanisms outside the core authorization logic. The authors conclude that the language operates logically correctly.
• Expressiveness (Description Reduction):
  • The original SELinux policy source contained 6,524 lines and 133 pages.
  • The proposed language (C-List style) reduced this to 335 lines and 95 pages.
  • The proposed language (ACL style) reduced this to 356 lines and 96 pages.
  • This represents a reduction of approximately 95% in source-code lines and 28% in listing pages.

Significance and Claims

The paper claims that the proposed language successfully addresses the complexity of policy description in multi-layer defense strategies. By raising the level of abstraction through logic programming, the language allows for:

• Concise Policy Description: Drastically reducing the volume of code required to describe complex policies, making them more manageable.
• Logical Correctness: Ensuring that authorization decisions are derived mathematically and logically, facilitating verification.
• Flexibility: Enabling the description of dynamic conditions (e.g., "being stopped" or "being tainted") and complex state transitions that are difficult to express in flat, rule-listing languages.

The authors note that while the language improves the overview of the policy as a whole, the readability of individual rules may be lower compared to direct element designation (like SELinux). Therefore, the language is particularly suitable for scenarios involving many shared access procedures or huge numbers of rules requiring flexible structuring, rather than for strictly defining a small number of unrelated rules.

Future work, as outlined by the authors, includes realizing applications such as policy verification as a condition for access control, managing rule changes via meta-rules, and embedding the Datalog processing system directly into the OS kernel to improve performance and security.