Enforceable and Verifiable Stale-Safe Security Properties in Distributed Systems

Attribute staleness arises due to the physical distribution of authorization information, decision and enforcement points. This is a fundamental problem in virtually any secure distributed system in which the management and representation of authorization state are not globally synchronized. This problem is so intrinsic that it is inevitable an access decision will be made based on attribute values that are stale. While it may not be practical to eliminate staleness, we can limit unsafe access decisions made based on stale user and object attributes. In this article, we propose two properties and specify a few variations which limit such incorrect access decisions. We use temporal logic to formalize these properties which are suitable to be verified, for example, by using model checking. We present a case study of the uses of these properties in the specific context of an application called Group-Centric Secure Information Sharing (g-SIS). We specify the authorization information, decision and enforcement points of the g-SIS system for the case with only a single user, object, and group (the small enforcement model) in terms of State Machine (SM) and show how these SMs can be designed so as to satisfy the stale-safe security properties. Next, we formally verify that the small model satisfies these properties and enforces a g-SIS authorization policy using the NuSMV model checker. Finally, we show that by generalizing the verification results of the small model that a large enforcement model, comprising an unbounded number of users, objects, and groups, satisfies these properties.