Enforceable and Verifiable Stale-Safe Security Properties in Distributed Systems

dc.contributor.authorNiu, Jianwei
dc.contributor.authorKrishnan, Ram
dc.contributor.authorBennatt, Jared F.
dc.contributor.authorSandhu, Ravi
dc.contributor.authorWinsborough, William H.
dc.date.accessioned2023-10-26T14:41:10Z
dc.date.available2023-10-26T14:41:10Z
dc.date.issued2011-04
dc.description.abstractAttribute 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.
dc.description.departmentComputer Science
dc.identifier.urihttps://hdl.handle.net/20.500.12588/2173
dc.language.isoen_US
dc.publisherUTSA Department of Computer Science
dc.relation.ispartofseriesTechnical Report; CS-TR-2011-002
dc.subjectsecurity
dc.subjectverification
dc.subjectattribute-based access control
dc.subjecttemporal logic
dc.subjectmodel checking
dc.subjectsecurity properties
dc.subjectstale-safety
dc.titleEnforceable and Verifiable Stale-Safe Security Properties in Distributed Systems
dc.typeTechnical Report

Files

Original bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Niu_et_al_CS-TR-2011-002.pdf
Size:
571.25 KB
Format:
Adobe Portable Document Format

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.86 KB
Format:
Item-specific license agreed upon to submission
Description: