Efficient, usable proof-construction strategies for distributed access-control systems

Distributed access-control systems implemented using formal logic have several advantages over conventional access-control systems; namely, they allow for decentralized policy administration, can express a wide variety of policies without ambiguity, and provide greater assurance that granted accesses comply with access-control policy. Access is granted only if the system can construct a proof, in formal logic, that demonstrates that the access is authorized. The efficiency of the proof-construction algorithm is therefore of great interest, as it resides on the critical path to an access being granted. Any delay in proof construction will delay access, which can significantly impact the usability and effectiveness of the system. However, it can be challenging to efficiently construct a proof in such a system. The credentials that encode access-control policy may be distributed among distant nodes in the system, or may not have been created yet. Users should be able to extend access-control policy in response to a requested access, and they should be guided through this process to ensure that the new credential will result in access being granted. Additionally, user input must be considered to ensure that, e.g., a request that Alice create a new credential does not disturb her at an inappropriate time. The objective of this thesis is therefore to describe a suite of techniques that enable the efficient construction of a proof of access. We demonstrate that these techniques are practical using policies, data, and experience drawn from an experimental access-control system deployed at our university. This suite of techniques consists of three main components: an algorithm for distributing the proof construction process, an efficient proof-construction strategy that incorporates human interaction, and techniques for identifying and resolving misconfigurations in access-control policy before they delay or deny a legitimate access. Distributed proof construction. We introduce a distributed approach to proof construction and show that this approach substantially reduces the amount of communication required to construct a proof when compared to prior work, which employs a centralized approach with straightforward extensions for collecting credentials from remote nodes. These gains result from both ensuring that each component of the proof is assembled by the party with the most relevant knowledge and effectively utilizing a distributed cache. We show analytically that our approach will find a proof whenever the centralized approach will do so. The distributed approach allows each party a great deal of flexibility as to how they attempt to construct a proof. This flexibility enables us to explore the efficient, usable proof-construction techniques that represent the second component of this thesis. Efficient, usable proof construction. Preliminary experience with our access-control testbed indicated that a practical proof-construction strategy must allow users to direct the proof search (as it might, e.g., involve bothering another user), identify situations in which the proof could be completed with the creation of a new credential, and to maximize the usage of locally cached credentials. We present a strategy for constructing proofs in such an environment and show that, through the effective use of precomputed results, we achieve dramatic improvements over prior work in terms of computational efficiency at the time of access. As before, we show that these gains do not entail any loss in proving ability. These techniques have been deployed for almost two years, and their efficiency is instrumental to the continued success of our experimental system. Identifying and resolving policy misconfigurations. A misconfiguration in access-control policy can result in a legitimate access being delayed or denied. This can be highly annoying to users, and may have severe consequences if timely access is critical. We show how rule mining techniques may be applied to access logs to identify potential misconfigurations in policy before they result in an access being denied. We also describe a technique by which past user behavior can be utilized to direct requests for policy corrections to the appropriate administrator. Using data collected from our testbed, we show that these techniques can correct a significant faction of misconfigurations before they impact a legitimate access, and that we can detect most of the discrepancies between the policy that an administrator implemented and the policy that was intended. The three components of this thesis, when combined, represent a cohesive strategy for constructing proofs of access in an efficient and usable manner in a distributed access-control system that is implemented using formal logic. To our knowledge, this thesis represents the first such strategy to effectively address the requirements of such a system that is deployed and in active use.