Skip to Main content Skip to Navigation
Conference papers

Static conflict detection for a policy language

Abstract : We present a static control flow analysis used in the Simple Unified Policy Programming Language (Suppl) compiler to detect internally inconsistent policies. For example, an access control policy can decide to both "allow" and "deny" access for a user; such an inconsistency is called a conflict. Policies in Suppl follow the Event-Condition-Action paradigm; predicates are used to model conditions and event handlers are written in an imperative way. The analysis is twofold; it first computes a superset of all conflicts by looking for a combination of actions in the event handlers that might violate a user-supplied definition of conflicts. SMT solvers are then used to try to rule out the combinations that cannot possibly be executed. The analysis is formally proven sound in Coq in the sense that no actual conflict will be ruled out by the SMT solvers. Finally, we explain how we try to show the user what causes the conflicts, to make them easier to solve.
Document type :
Conference papers
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download

https://hal.inria.fr/hal-01099124
Contributor : David Baelde <>
Submitted on : Wednesday, December 31, 2014 - 3:14:36 PM
Last modification on : Wednesday, August 21, 2019 - 3:14:05 PM
Long-term archiving on: : Wednesday, April 1, 2015 - 10:10:38 AM

File

jfla15_submission_3.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01099124, version 1

Collections

Citation

Alix Trieu, Robert Dockins, Andrew Tolmach. Static conflict detection for a policy language. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), David Baelde; Jade Alglave, Jan 2015, Le Val d'Ajol, France. ⟨hal-01099124⟩

Share

Metrics

Record views

210

Files downloads

225