skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: Types and Abstract Interpretation for Authorization Hook Advice
Authorization hooks are access control checks that prevent unauthorized principals from interacting with some protected resource, and are used extensively in critical software such as operating systems, middleware, and server programs. They are often intended to mediate information flow between subjects (e.g., file owners), but typically in an ad-hoc manner. In this paper we present a static type and effect system for detecting whether authorization hooks in programs properly defend against undesired information flow between subjects. A significant novelty of our approach is an integrated abstract interpretation-based tool that guides system clients through the information flow consequences of access control policy decisions.  more » « less
Award ID(s):
1816282
PAR ID:
10168736
Author(s) / Creator(s):
Date Published:
Journal Name:
Proceedings of the 2020 IEEE Computer Security Foundations Symposium (CSF)
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. null (Ed.)
    Authorization hooks are access control checks that prevent unauthorized principals from interacting with some protected resource, and are used extensively in critical software such as operating systems, middleware, and server programs. They are often intended to mediate information flow between subjects (e.g., file owners), but typically in an ad-hoc manner. In this paper we present a static type and effect system for detecting whether authorization hooks in programs properly defend against undesired information flow between subjects. A significant novelty of our approach is an integrated abstract interpretation-based tool that guides system clients through the information flow consequences of access control policy decisions. 
    more » « less
  2. null (Ed.)
    We present the Flow-Limited Authorization First-Order Logic (FLAFOL), a logic for reasoning about authorization decisions in the presence of information-flow policies. We formalize the FLAFOL proof system, characterize its proof-theoretic properties, and develop its security guarantees. In particular, FLAFOL is the first logic to provide a non-interference guarantee while supporting all connectives of first-order logic. Furthermore, this guarantee is the first to combine the notions of non-interference from both authorization logic and information-flow systems. All the theorems in this paper are proven in Coq. 
    more » « less
  3. Obtaining an accurate specification of the access control policy enforced by an application is essential in ensuring that it meets our security/privacy expectations. This is especially important as many of real-world applications handle a large amount and variety of data objects that may have different applicable policies. We investigate the problem of automated learning of access control policies from web applications. The existing research on mining access control policies has mainly focused on developing algorithms for inferring correct and concise policies from low-level authorization information. However, little has been done in terms of systematically gathering the low-level authorization data and applications' data models that are prerequisite to such a mining process. In this paper, we propose a novel black-box approach to inferring those prerequisites and discuss our initial observations on employing such a framework in learning policies from real-world web applications. 
    more » « less
  4. Access control policies are crucial in securing data in information systems. Unfortunately, often times, such policies are poorly documented, and gaps between their specification and implementation prevent the system users, and even its developers, from understanding the overall enforced policy of a system. To tackle this problem, we propose the first of its kind systematic approach for learning the enforced authorizations from a target system by interacting with and observing it as a black box. The black-box view of the target system provides the advantage of learning its overall access control policy without dealing with its internal design complexities. Furthermore, compared to the previous literature on policy mining and policy inference, we avoid exhaustive exploration of the authorization space by minimizing our observations. We focus on learning relationship-based access control (ReBAC) policy, and show how we can construct a deterministic finite automaton (DFA) to formally characterize such an enforced policy. We theoretically analyze our proposed learning approach by studying its termination, correctness, and complexity. Furthermore, we conduct extensive experimental analysis based on realistic application scenarios to establish its cost, quality of learning, and scalability in practice. 
    more » « less
  5. Zero trust (ZT) is the term for an evolving set of cybersecurity paradigms that move defenses from static, network-based perimeters to focus on users, assets, and resources. It assumes no implicit trust is granted to assets or user accounts based solely on their physical or network location. We have billions of devices in IoT ecosystems connected to enable smart environments, and these devices are scattered around different locations, sometimes multiple cities or even multiple countries. Moreover, the deployment of resource-constrained devices motivates the integration of IoT and cloud services. This adoption of a plethora of technologies expands the attack surface and positions the IoT ecosystem as a target for many potential security threats. This complexity has outstripped legacy perimeter-based security methods as there is no single, easily identified perimeter for different use cases in IoT. Hence, we believe that the need arises to incorporate ZT guiding principles in workflows, systems design, and operations that can be used to improve the security posture of IoT applications. This paper motivates the need to implement ZT principles when developing access control models for smart IoT systems. It first provides a structured mapping between the ZT basic tenets and the PEI framework when designing and implementing a ZT authorization system. It proposes the ZT authorization requirements framework (ZT-ARF), which provides a structured approach to authorization policy models in ZT systems. Moreover, it analyzes the requirements of access control models in IoT within the proposed ZT-ARF and presents the vision and need for a ZT score-based authorization framework (ZT-SAF) that is capable of maintaining the access control requirements for ZT IoT connected systems. 
    more » « less