Published In

Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015)

Document Type

Post-Print

Publication Date

1-7-2015

Subjects

Programming Languages -- Compilers -- Interpreters, Mathematical Logic and Formal Languages

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.

Persistent Identifier

http://archives.pdx.edu/ds/psu/16820

Download

Share

COinS