Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
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
Contributor : David Baelde Connect in order to contact the contributor
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


Files produced by the author(s)


  • HAL Id : hal-01099124, version 1



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⟩



Record views


Files downloads