SMT-based verification of dynamic access control policies
No Thumbnail Available
Authors
Meeting name
Sponsors
Date
Journal Title
Format
Thesis
Subject
Abstract
Modern software systems increasingly depend on dynamic access control to manage evolving privileges in complex workflows across safety-critical domains such as healthcare, finance, academia, government, and defense. As users create, review, or modify digital artifacts, their access rights must dynamically adjust in real time to maintain security and operational continuity. However, ensuring that these dynamic privilege changes remain correct and consistent presents a fundamental challenge, as subtle errors or unintended interactions in administrative logic can silently compromise authorization integrity, leading to privilege escalation or the denial of legitimate access. This dissertation introduces the Policy Machine Analyzer (POMA), an integrated framework for the formal verification of dynamic access control policies governed by administrative obligations. Administrative obligations define conditional rules that automatically trigger policy updates in response to access events, enabling flexible yet complex runtime authorization. To address this complexity, POMA establishes the first SMT-based verification framework capable of reasoning about evolving authorization states. It systematically determines whether sequences of obligation-triggered updates satisfy or violate access control requirements, ensuring both safety and liveness properties within continuously changing policy configurations. Beyond reachability verification, this dissertation identifies and formalizes a novel problem in access control: the obligation race condition, a concurrency conflict that arises when multiple administrative obligations triggered by the same event simultaneously attempt to modify the authorization state. This class of race conditions has not been previously addressed in the literature and represents a new dimension of policy-level interference. By encoding concurrent obligations and their effects as satisfiability constraints, the framework detects nondeterministic or unsafe authorization outcomes before they manifest at runtime or proves their absence through formal reasoning. In summary, this research establishes a unified, solver-based foundation for verifying adaptive access control systems and introduces the first formal treatment of obligation races, paving the way toward safer, more predictable, and verifiable security in modern automated environments.
Table of Contents
Introduction -- Related work -- Formalization of dynamic access control policies -- An SMT-based framework for dynamic access control policy verification -- Verification of dynamic access control requirements -- Obligation race detection -- GPMS-NGAC: a benchmark application -- Tool implementation -- Experiments -- Conclusions
DOI
PubMed ID
Degree
Ph.D. (Doctor of Philosophy)