Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Automatically Tightening Access Control Policies with Restricter

Ka Lok Wu, Christa Jenkins, Scott D. Stoller, Omar Chowdhury

TL;DR

This work tackles the challenge of over-permissive access control policies by introducing Restricter, an automated method that tightens Cedar policies through log-guided, rule-by-rule refinement. The approach combines SMT-based symbolic encoding with SyGuS-driven synthesis to add conjunctions to permit rules while preserving the log-consistent behavior and the overall least-privilege principle. Through two realistic case studies, Restricter demonstrates scalability and effectiveness, tightening most loosened rules and preserving intended permissions, with scalability primarily affected by entity-store size rather than log density. The work contributes a formal problem formulation, a local tightening strategy, and a practical implementation that can extend to other ABAC languages beyond Cedar, advancing automated policy maintenance in secure systems.

Abstract

Robust access control is a cornerstone of secure software, systems, and networks. An access control mechanism is as effective as the policy it enforces. However, authoring effective policies that satisfy desired properties such as the principle of least privilege is a challenging task even for experienced administrators, as evidenced by many real instances of policy misconfiguration. In this paper, we set out to address this pain point by proposing Restricter, which automatically tightens each (permit) policy rule of a policy with respect to an access log, which captures some already exercised access requests and their corresponding access decisions (i.e., allow or deny). Restricter achieves policy tightening by reducing the number of access requests permitted by a policy rule without sacrificing the functionality of the underlying system it is regulating. We implement Restricter for Amazon's Cedar policy language and demonstrate its effectiveness through two realistic case studies.

Automatically Tightening Access Control Policies with Restricter

TL;DR

This work tackles the challenge of over-permissive access control policies by introducing Restricter, an automated method that tightens Cedar policies through log-guided, rule-by-rule refinement. The approach combines SMT-based symbolic encoding with SyGuS-driven synthesis to add conjunctions to permit rules while preserving the log-consistent behavior and the overall least-privilege principle. Through two realistic case studies, Restricter demonstrates scalability and effectiveness, tightening most loosened rules and preserving intended permissions, with scalability primarily affected by entity-store size rather than log density. The work contributes a formal problem formulation, a local tightening strategy, and a practical implementation that can extend to other ABAC languages beyond Cedar, advancing automated policy maintenance in secure systems.

Abstract

Robust access control is a cornerstone of secure software, systems, and networks. An access control mechanism is as effective as the policy it enforces. However, authoring effective policies that satisfy desired properties such as the principle of least privilege is a challenging task even for experienced administrators, as evidenced by many real instances of policy misconfiguration. In this paper, we set out to address this pain point by proposing Restricter, which automatically tightens each (permit) policy rule of a policy with respect to an access log, which captures some already exercised access requests and their corresponding access decisions (i.e., allow or deny). Restricter achieves policy tightening by reducing the number of access requests permitted by a policy rule without sacrificing the functionality of the underlying system it is regulating. We implement Restricter for Amazon's Cedar policy language and demonstrate its effectiveness through two realistic case studies.
Paper Structure (18 sections, 5 figures, 1 table, 2 algorithms)

This paper contains 18 sections, 5 figures, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Background on Cedar
  3. Cedar Primer
  4. Problem Definition
  5. Motivating Example
  6. Notations and Problem Definition
  7. Design Dimensions
  8. Restricter's Approach
  9. Synthesizing a tighter permit rule (Step ➋).
  10. Choosing Concrete Requests to Deny
  11. Implementation
  12. Symbolic Encoding of Cedar
  13. Syntactic Constraints
  14. Evaluation
  15. Design of Case Studies
  16. ...and 3 more sections

Figures (5)

  • Figure 1: Example Cedar schemas and policies
  • Figure 2: Modified Cedar policy
  • Figure 3: An illustration of Restricter's main idea for Step ➋. Restricter chooses requests in the set of potential over-privileges to be denied by a conjunct $\phi$ (to be synthesized with SyGuS) while keeping the log slices permitted.
  • Figure 4: Example corresponding rule pair (HotCRP)
  • Figure 5: Excerpt of the evaluation results in terms of semantic similarity of the generated rules versus the ideal ones and the scalability.