In bottom-up role mining, the input consists of a set of users and the permissions each user is authorized to perform, and the objective is to derive a role-based access control (RBAC) policy that preserves these authorizations. When the goal is to minimize the number of roles, the problem is NP-hard, and exact algorithms are infeasible on worst-case instances. Recent work introduced a maximal biclique enumeration-based approach and presented an extensive empirical evaluation on benchmark inputs. While this approach yields optimal solutions for most instances, it stalls on hard instances due to exponential growth in maximal bicliques.

Role hierarchies in Role-Based Access Control (RBAC) enable scalable administration by allowing permissions to be inherited among roles. However, deriving high-quality hierarchies from existing flat RBAC policies remains a challenging combinatorial problem. We present two new algorithms for the Role Hierarchy Mining Problem (RHMP) that construct compact and well-structured hierarchies while preserving all user--permission authorizations. The first algorithm, MinRolesRH, restructures a minimal-role RBAC policy into a multi-layer hierarchy without introducing new roles, optimizing for maximal depth and minimal edge count. The second algorithm, NewRolesRH, generalizes this approach by introducing new intermediate roles to maximize hierarchical depth. To further minimize redundant edges, we formulate Integer Linear Programs (ILPs) that prune edges while preserving authorizations. We evaluate the resulting hierarchies using both Weighted Structural Complexity (WSC) and a random-walk based navigability metric, which estimates the expected traversal steps from users to permissions. Experimental results on standard benchmarks and RMPLib datasets demonstrate that our algorithms consistently achieve lower WSC and improved navigability compared to existing algorithms, including RHMiner and Role Generation + Elimination. All implementations are available as open source.

We address a particular kind of composition of access control schemes which include both a model to encode authorizations, and an administrative model to encode the manner in which such authorizations can change. The kind of composition we address is co-existence: two schemes working side-by-side in the same system in protection of the same set of resources with the same principals who seek access. We observe that practice appears to be ahead of research in this regard, and discuss case-studies we have carried out of three real-world compositions. We then articulate takeaways from the case-studies.

Predictable wavefront splitting (PWS) is an optimization technique for graphics processing units (GPUs) to address the performance and worst-case execution time (WCET) impacts of branch divergence. PWS relies on manual annotation by the GPU programmer; these choices affect the resulting WCET. This work automates this process with two key approaches. First, we formulate the optimal annotation as an integer quadratic programming (IQP) problem such that the solution guarantees the lowest WCET. Second, we show that the problem can be solved with an optimal polynomial-time dynamic programming algorithm that achieves the same solutions as the IQP. We implement our algorithm in a compiler flow for an AMD GPU, and we deploy the annotated executable on a gem5 micro-architectural implementation of the AMD GCN3 GPU. We evaluate our implementation on a benchmark suite provided by AMD and supplement it with an extensive set of synthetic benchmarks. Our evaluation shows that these two approaches are able to reduce the WCET by between 13% and 31% compared to five baseline algorithms.

We present a compiler phase for GPUs enabled with predictable wavefront splitting (PWSG) that implements an optimal algorithm to split diverging GPU wavefronts into separate scheduleable entities. This algorithm selects branches in the GPU kernel that guarantee the lowest worst-case execution time (WCET) for the kernel. We implement our algorithm in a compiler flow for an AMD GPU, and we deploy the resulting binary on a gem5 micro-architectural implementation of the AMD GCN3 GPU. We evaluate our implementation on an extensive set of synthetic benchmarks. Our experiments show that by automatically selecting points in the GPU kernel to split wavefronts, we are able to reduce the WCET ranging from 34% to 52% reduction compared to five alternative approaches.

The problem of learning access control policies is receiving increasing attention in research. We contribute to the foundations of this problem by posing and addressing meaningful questions on computational hardness. Our work addresses learning access control policies in the context of three different models from the literature: the access matrix, and Role- and Relationship-Based Access Control (RBAC and ReBAC, respectively). Our underlying theory is the well-established notion of Probably Approximately Correct (PAC), with careful extensions for our setting. The data, or examples, a learning algorithm is provided in our setup is that related to access enforcement, which is the process by which a request for access to a resource is decided. For the access matrix, we pose a learning problem that turns out to be computationally easy, and another that we prove is computationally hard. We generalize the former result so we have a sufficient condition for establishing other problems to be computationally easy. With these results as the basis, we consider five learning problems in the context of RBAC, two of which turn out to be computationally hard. Finally, we consider four learning problems in the context of ReBAC, all of which turn out to be computationally easy. Every proof for a problem that is computationally easy is constructive, in that we propose a learning algorithm for the problem that is efficient, and probably, approximately correct. As such, our work makes contributions at the foundations of an important, emerging aspect of access control, and thereby, information security.

Abstract The usability of Access Control Lists (ACLs) of a widely used enterprise software for directory information services called OpenLDAP is addressed. A directory service is used to store a variety of data such as employee information and passwords, and can be seen as a critical infrastructure component of an enterprise. Security and in particular, access control of such data is of paramount importance, and OpenLDAP provides ACLs for this purpose that an administrator can configure. The usability, that is, the ease with which a human administrator can express a policy in an ACL, is then an important issue because misconfigurations are known to be a major cause of security vulnerabilities. Motivated by public pronouncements regarding the poor usability of OpenLDAP ACLs, a systematic study towards evaluating their usability is carried out. The authors begin with a cognitive walkthrough, which identifies the broad issues, which then informs the design of an ethics‐approved study of 50 human participants. This study reveals that indeed, even with a limited syntax, adequate training and a focus only on devising a policy from scratch, OpenLDAP ACLs suffer from poor usability. The data gathered from this study is analysed further, and more detailed observations are made such as those regarding the difference in difficulty for different kinds of policy goals, and the nature of errors human participants make with OpenLDAP ACLs. As such, this work makes an important contribution to enterprise security and provides important insights for a (re)design of ACLs, in particular for OpenLDAP.

We address least-privilege in a particular context of public cloud computing: calls to Amazon Web Services (AWS) Application Programming Interfaces (APIs). AWS is, by far, the largest cloud provider, and therefore an important context in which to consider the fundamental security design principle of least-privilege, which states that a thread of execution should possess only those privileges it needs. There have been reports of over-privilege being a root cause of attacks against AWS cloud applications, and a least-privilege set for an API call is a necessary building-block in devising a least-privilege policy for a cloud application. We observe that accurate information on a least-privilege set for an invoker of a method to possess is simply not available for most such methods in AWS. We provide a meaningful characterization of least-privilege in this context. We then propose techniques to determine such sets, and discuss a black-box process we have devised and carried out to identify such sets for all 707 API methods we are able to invoke across five AWS services. We discuss a number of interesting discoveries we have made, some of which are surprising and some alarming, that we have reported to AWS. Our work has resulted in a database of least-privilege sets for API calls to AWS, which we make available publicly. Developers can consult our database when configuring security policies for their cloud applications, and we welcome contributors that augment our database. Also, we discuss example uses of our database via an assessment of two repositories and two full-fledged serverless applications that are available publicly and have policies published alongside. We observe that the vast majority of policies are over-privileged. Our work contributes constructively to securing cloud applications in the largest cloud provider.

A graph is a powerful abstraction for representing information. We address the problem of publishing a secure version of a graph that does not leak information to an adversary who may possess prior information about portions of the graph, and may have unbounded computational power. In this context, we revisit four notions of security, all of which are based on variants of graph isomorphism, that have been proposed in two different application contexts in the literature. We compare the four notions to one another, first from the standpoint of strength, i.e., whether meeting one notion implies meeting another, and then from the standpoint of computational hardness, i.e., what the exact computational complexity is for the problem of checking whether a graph meets a notion. For the latter, we identify that for two of the notions we consider, the problem is$\mathbf{NP}\text{-complete}$, and for the two others, it isISO-complete, whereISOis the class of problems induced by graph isomorphism. We observe that strength is not necessarily correlated to computational hardness. In summary, our work makes contributions at the foundations of an important notion of security for graphs.

We address logic locking, a mechanism for securing digital Integrated Circuits (ICs) from piracy by untrustworthy foundries. We discuss previous work and the state-of-the-art, and observe that, despite more than a decade of research that has gone into the topic (resulting in both powerful attacks and subsequent defenses), there is no consensus on what it means for a particular locking mechanism to be secure. This paper attempts to remedy this situation. Specifically, it formulates a definition of security for a logic locking mechanism based on indistinguishability and relates the definition to security from actual attackers in a precise and unambiguous manner. We then describe a mechanism that satisfies the definition, thereby achieving (provable) security from all prior attacks. The mechanism assumes the existence of both a puncturable pseudorandom function family and an indistinguishability obfuscator, two cryptographic primitives that exist under well-founded assumptions. The mechanism builds upon the Stripped-Functionality Logic Locking (SFLL) framework, a state-of-the-art family of locking mechanisms whose potential for ever achieving security is currently in question. Along the way, partly as motivation, we present additional results, such as a reason founded in average-case complexity for why benchmark circuits locked with a prior scheme are susceptible to the well-known SAT attack against such schemes, and why provably thwarting the SAT attack is insufficient as a meaningful notion of security for logic locking.

We propose a notion that we call the secrecy resilience of an access control policy that, to our knowledge, has not been explored in prior work. We seek to capture with this notion the property inherent to an access control policy that measures its resistance to disclosure. We motivate and then propose a definition for secrecy resilience that is based on the notion of entropy from information theory. We focus on policies expressed in Role-Based Access Control (RBAC), and contrast RBAC from the access matrix from the standpoint of secrecy resilience. We observe that similar to other objectives such as the minimization of the number of roles, an RBAC policy with the best secrecy resilience can be a desirable objective of bottom-up role-mining, with which we seek to compute an RBAC policy given as input an access matrix. We have carried out an empirical assessment of several role-mining algorithms from the standpoint of secrecy resilience for two underlying distribution-events pairs each of which captures a kind of best-case from the standpoint of a defender. Towards carrying out the empirical assessment, we make an additional contribution to role-mining: we propose new reductions for the two problems of minimizing the number of roles and the number of edges, and discuss the manner in which our reductions are superior to reductions in existing work.

Access control deals with the roles and privileges to which a user is authorized, and is an important aspect of the security of a system. As enterprise access control systems need to scale to several users, roles and privileges, it is common for access control models to support delegation: a trusted security administrator is able to give semi-trusted users the ability to change portions of the authorization state. With delegation comes the danger that semi-trusted users, perhaps in collusion, may effect a state that violates enterprise policy, which in turn results in the problem called safety analysis, which is regarded as a fundamental and technically challenging problem in access control. Safety analysis is used by a trusted security administrator to answer “what if” questions before she grants privileges to a semi-trusted user. Safety analysis has been studied for various access control schemes in the literature; we address safety analysis in the context of Administrative Temporal Role-Based Access Control (ATRBAC), an administrative model for TRBAC, which is an extension to the traditional RBAC. ATRBAC has new features, which introduce new technical challenges for safety analysis: (i) a time-dimension: two new components in each administrative rule that specify in which time periods an administrative action may be effected, and a user is authorized to a role, and, (ii) two new kinds of rules for whether a role is enabled for administrative action. We propose a software tool, which we call Cree, for safety analysis of ATRBAC policies. In Cree we reduce ATRBAC-Safety to model checking and use an off-the-shelf model checker, NuSMV. The foundation for Cree is the observation from our prior work that ATRBAC safety is PSPACE. Along with an efficient reduction to model checking, we include in Cree four techniques to further improve performance: Polynomial Time Solving when possible, Forward and Backwards Pruning, Abstraction Refinement, and Bound Estimation. These are inspired by prior work, but our algorithms are different in that they address the new challenges that ATRBAC introduces. We discuss our design of Cree, and the results of a thorough empirical assessment across our approach, and five other prior tools for ATRBAC safety. Our results suggest that there are input classes for which Cree outperforms existing tools, and for the remainder, Cree's performance is no worse. We have made Cree available as open-source for public download.

We pose and study forensic analysis in the context of access control systems in a manner that prior work has not. Forensics seeks to answer questions about past states of a system, and thereby provides important clues and evidence in the event of a security incident. Access control deals with who may perform what action on a resource and is a critical security function. Our focus is access control systems that allow for changes to the authorization state to be delegated to potentially untrusted users. We argue that this context in access control is an important one in which to consider forensic analysis, and observe that it is a natural complement of safety analysis, which has been considered extensively in the literature. We pose the forensic analysis problem for such access control systems abstractly, and instantiate it for three schemes from the literature: a well-known access matrix scheme, a role-based scheme, and a discretionary scheme. We identify the computational complexity of forensic analysis, and compare it to that of safety analysis for each of the schemes. We consider also the notion of logs, i.e., data that can be collected over time to aid forensic analysis.

Integrated circuit (IC) camouflaging is a promising defense against so-called IC extraction attacks that seek to reverse engineer the netlist of a packaged IC using delayering and imaging techniques. Camouflaging works by hiding the Boolean functionality of selected gates in the netlist from reverse engineering, albeit at the cost of increased gate area and power. The intuitive security claim then is that the attacker cannot infer the netlist's exact Boolean functionality. This paper describes a powerful class of attacks on IC camouflaging referred to as SAT attacks; the attacks use the input/output (I/O) behavior of a functional camouflaged IC along with the Boolean satisfiability (SAT)-based inference to reverse the Boolean functionalities of camouflaged gates. The SAT attack is rooted in a foundational complexity theory mindset and is shown to defeat defenses that previously claimed to secure against even the most determined adversaries. This paper then highlights the subsequent impact of the SAT attack in terms of new SAT-resilient defenses that emerged, their vulnerability to enhancements of the SAT attack, and implications of the attack on provably secure defense mechanisms.

Recent work suggests that scheduling, with security as a consideration, can be effective in minimizing information leakage, via side-channels, that can exist when virtual machines (VMs) co-reside in clouds. We analyze the overhead that is incurred by such an approach. We first pose and answer a fundamental question: is the problem tractable? We show that the seemingly simpler sub-cases of initial placement and migration across only two equal-capacity servers are both intractable (NP-hard). However, a decision version of the general problem to which the optimization version is related polynomially is in NP. With these results as the basis, we make several other contributions. We revisit recent work that proposes a greedy algorithm for this problem, called Nomad. We establish that if P ≠ NP, then there exist infinitely many classes of input, each with an infinite number of inputs, for which a decrease in information leakage is possible, but Nomad provides none, let alone minimize it. We establish also that a mapping to Integer Linear Programming (ILP) in prior work is deficient in that the mapping can be inefficient (exponential-time), and therefore does not accurately convey the overhead of such an approach that, unlike Nomad, actually decreases information leakage. We present our efficient reductions to ILP and boolean satisfiability in conjunctive normal form (CNF-SAT). We have implemented these approaches and conducted an empirical assessment using the same ILP solver as prior work, and a SAT solver. Our analytical and empirical results more accurately convey the overhead that is incurred by an approach that actually provides security (decrease in information leakage).

We explore the idea of composing PUFs with the intent that the resultant PUF is stronger than the constituent PUFs. Prior work has proposed a construction, which subsequent work has shown to be weak. We revisit this prior construction and observe that it is actually weaker than previously thought when the constituent PUFs are arbiter PUFs. This weakness is demonstrated via our adaptation of the previously proposed Logistic Regression (LR) attack. We then propose new constructions called PUFs-composed-with-PUFs (PoP). In particular, we retain a two-layer construction, but allow the same input to the composite PUF to be input to more than one constituent PUF at the first layer. We explore this family of constructions, with arbiter PUFs serving as the constituent PUFs. In particular, we identify several axes which we can vary, and empirically study the resilience of our constructions compared to the prior construction and one another from the standpoint of LR attacks. As insight into why our family of constructions is stronger, we prove, under some idealized conditions, that the lower-bound on an attacker is indeed higher under our constructions than the upper-bound on an attacker for the prior construction. As such, our work suggests that composition can be a promising approach to strengthening PUFs, contrary to what prior work suggests.

We address security in the context of the Resource Description Framework (RDF), a graph-like data model for the web. One of RDF's compelling features is a precise, model-theoretic semantics. We first propose a threat model, and under it, observe that the technical challenge is really in hiding information that may be revealed by the structure of an RDF graph. We choose two quantitative, unconditional notions for securing graph-structure from the literature that address the threat model, and adapt them for RDF. We then consider the problem of devising algorithms for achieving a certain level of security while preserving the semantics of the input RDF graph. We observe that there are operations we can perform on an RDF graph that both provide such security and preserve semantics. We observe, further, that there is a natural way to quantify information-loss under these operations, and that there appears to be a natural trade-off between security and information-quality. We study this trade-off and establish fundamental results. We show that the RDF graphs that result from applying the operations induce a lattice that leads to a natural quantification of information-quality. We show also that achieving a certain level of security while retaining a certain level of information-quality is NP-complete under polynomial-time Turing reductions. Finally, towards an empirical assessment, we discuss our design and implementation of a reduction to CNF-SAT, and empirical results for two classes of RDF graphs. In summary, our work makes fundamental and practical contributions to semantics-preserving security for RDF.

We emphasize the need to articulate precise, declarative properties in the context of securing Digital ICs. We do this by discussing two pieces of our work on securing Digital ICs. In one, we discuss a seemingly compelling approach to protecting Intellectual Property -- IC camouflaging. We demonstrate that an adversary can carry out a decamouflaging attack, in practice, much more efficiently than previously thought. Underlying our attack is strong foundations: an identification of the computational-complexity of the problems an attacker faces, and how they can be addressed using off-the-shelf constraint solvers. We identify the lack of a precise characterization of "security" in this context as an issue. In the other piece of work, we present an example of the articulation of such a security property for 3D IC technology, in the context of securing a supply-chain. The property is articulated declaratively, with explicit assumptions that underlie the threat model.

Integrated circuit (IC) camouflaging is a promising technique to protect the design of a chip from reverse engineering. However, recent work has shown that even camouflaged ICs can be reverse engineered from the observed input/output behaviour of a chip using SAT solvers. However, these so-called SAT attacks have so far targeted only camouflaged combinational circuits. For camouflaged sequential circuits, the SAT attack requires that the internal state of the circuit is controllable and observable via the scan chain. It has been implicitly assumed that restricting scan chain access increases the security of camouflaged ICs from reverse engineering attacks. In this paper, we develop a new attack methodology to decamouflage sequential circuits without scan access. Our attack uses a model checker (a more powerful reasoning tool than a SAT solver) to find a discriminating set of input sequences, i.e., one that is sufficient to determine the functionality of camouflaged gates. We propose several refinements, including the use of a bounded model checker, and sufficient conditions for determining when a set of input sequences is discriminating to improve the run-time and scalabilty of our attack. Our attack is able to decamouflage a large sequential benchmark circuit that implements a subset of the VIPER processor.

We address query-anonymity, the property that the destination of a client's query is indistinguishable from other potential destinations, in the context of wireless sensor networks. Prior work has established that this is an important issue, and has also pointed out that there appears to be a natural trade-off between query-anonymity and communication-cost. We explore what we call the limits of this trade-off: what is the communication-cost that is sufficient to achieve a certain query-anonymity, and what is the communication-cost that we must necessarily incur to achieve a certain query-anonymity? Towards this, we point out that two notions of query-anonymity that prior work in this context proposes are not meaningful. We propose an unconditional notion of query-anonymity that we argue has intuitive appeal. We then establish the limits of the trade-off. In particular, we show that in wireless sensor networks whose topology is a square grid and are source-routed, the necessary and sufficient communication-cost for query-anonymity asymptotically smaller than n, where n is the number of nodes in the network, is dependent on n only, and the necessary and sufficient communication-cost for query-anonymity larger than n is dependent on the desired query-anonymity only. We then generalize to topologies that are arbitrary connected undirected graphs, an exercise that involves a novel approach based on a spanning tree for the graph. We show that the diameter of the graph is the inflection point in the trade-off. We discuss extensions of our results to other settings, such as those in which routes are not necessarily shortest-paths. We also validate our analytical insights empirically, via simulations in Tossim, a de facto standard approach for wireless sensor networks. In summary, our work establishes sound and interesting theoretical results for query-anonymity in wireless sensor networks, and validates them empirically.

Research in concurrent in-memory data structures has focused almost exclusively on models where processes are either reliable, or may fail by crashing permanently. The case where processes may recover from failures has received little attention because recovery from conventional volatile memory is impossible in the event of a system crash, during which both the state of main memory and the private states of processes are lost. Future hardware architectures are likely to include various forms of non-volatile random access memory (NVRAM), creating new opportunities to design robust main memory data structures that can recover from system crashes. In this paper we advance the theoretical foundations of such data structures in two ways. First, we review several known variations of Herlihy and Wing's linearizability property that were proposed in the context of message passing systems but also apply in our NVRAM-based model, we discuss the limitations of these properties with respect to our specific goals, and we propose an alternative correctness condition called recoverable linearizability. Second, we discuss techniques for implementing shared objects that satisfy such properties with a focus on wait-free implementations. Specifically, we demonstrate how to achieve different variations of linearizability in our model by transforming two classic wait-free constructions.

We address the generation and analysis of hard instances for verification problems in access control that are NP-hard. Given the customary assumption that P ≠ NP, we know that such classes exist. We focus on a particular problem, the user-authorization query problem (UAQ) in Role-Based Access Control (RBAC). We show how to systematically generate hard instances for it. We then analyze what we call the structure of those hard instances. Our work brings the important aspect of systematic investigation of hard input classes to access control research.

Safety analysis is recognized as a fundamental problem in access control. It has been studied for various access control schemes in the literature. Recent work has proposed an administrative model for Temporal Role-Based Access Control (TRBAC) policies called Administrative TRBAC (ATRBAC). We address ATRBAC-safety. We first identify that the problem is PSPACE-Complete. This is a much tighter identification of the computational complexity of the problem than prior work, which shows only that the problem is decidable. With this result as the basis, we propose an approach that leverages an existing open-source software tool called Mohawk to address ATRBAC-safety. Our approach is to efficiently reduce ATRBAC-safety to ARBAC-safety, and then use Mohawk. We have conducted a thorough empirical assessment. In the course of our assessment, we came up with a "reduction toolkit," which allows us to reduce Mohawk+T input instances to instances that existing tools support. Our results suggest that there are some input classes for which Mohawk+T outperforms existing tools, and others for which existing tools outperform Mohawk+T. The source code for Mohawk+T is available for public download.

We revisit the setuid family of calls for privilege management that is implemented in several widely-used operating systems. Three of the four commonly used calls in the family are standardized by POSIX. We investigate the current status of setuid, and in the process, challenge some assertions in prior work. We address three sets of questions with regards to the setuid family. (1) Is the POSIX standard indeed broken as prior work suggests? (2) Are implementations POSIX-compliant as claimed? (3) Are the wrapper functions that prior work proposes to circumvent issues with setuid calls correct and usable? Towards (1), we express the standards in a precise syntax that allows us to assess whether they are unambiguous, logically consistent descriptions of well-formed functions. We have discovered that two of the three functions that are standardized fit these criteria, thereby challenging assertions in prior work regarding the quality of the standard. In cases wherein the standard is broken, we give a clear characterization, and suggest that the standard can be fixed easily, but at the cost of backwards-compatibility. Towards (2), we perform a state-space enumeration as in prior work, report on our discoveries, and discuss the implications of non-conformance and differences in implementation. Towards (3), we discuss some issues that we have discovered with prior wrappers. We then propose a new suite of wrapper functions which are designed with a different mindset from prior work, and provide both stronger guarantees with respect to atomicity and a clearer semantics for permanent and temporary changes in process identity. With a fresh approach, our work is a contribution to a well-established approach to privilege management.

mTags is an efficient mechanism that augments inter-thread messages with lightweight metadata. We introduce and discuss a case study that we have conducted in the use of mTags for realizing a kind of mandatory security. Although mTags can be implemented for any message passing thread-based system, we consider an implementation of it in the POSIX-compliant QNX Neutrino, a commercial microkernel-based system. The approach to mandatory security that we adopt is Usable Mandatory Integrity Protection, which has been proposed in recent research. We call our adaptation of Usable Mandatory Integrity Protection using mTags, μMIP. We discuss the challenges we faced, and our design and implementation that overcomes these challenges. We discuss the performance of our implementation for well-established benchmarks. We conclude with the observation that mTags can be useful and practical to realize mandatory security in realistic systems. Copyright © 2013 John Wiley & Sons, Ltd.

We motivate and present two designs for the composition of the authentication protocol, Kerberos, and the key transport protocol, Multimedia Internet KEYing (MIKEY) for authenticated transport of cryptographic keys for secure group-communication in enterprise and public-safety settings. A technical challenge, and our main contribution, is the analysis of the security of the composition. Towards this, we design our compositions to have intuitive appeal and thereby less prone to security vulnerabilities. We then employ protocol composition logic (PCL), a state-of-the-art approach for analyzing our composition. For this, we first articulate two properties that are of interest. Both properties are on the group key that is transported; we call them Group Key Confidentiality and Acquisition. Group Key Confidentiality is the property that if a principal possesses the key, then it is an authorized member of the group. Group Key Acquisition is the property that if a principal is a member of the group, then it is able to acquire the group key. In the course of our rigorous analysis, we discovered a flaw in our first design, which we point out, and which lead us to our second design. We have implemented both designs starting with the publicly available reference implementation of Kerberos, and an open-source implementation of MIKEY. Our implementations are available as open-source. We discuss our experience from the implementation, and present empirical results.

This panel will address the following question. Does an increase in the granularity of access control systems produce a measurable reduction in risk and help meet the goals of the organization, or is the cost prohibitively high?

We motivate and address the problem of testing for properties of interest in real-world implementations of authorization systems. We adopt a 4-stage process: (1) express a property precisely using existential second-order logic, (2) establish types of traces that are necessary and sufficient to establish a property, (3) adopt finitizing assumptions and show that under those assumptions, verifying a property is in PSPACE, and, (4) use a model-checker as a trace-generator to generate instances of traces, and exercise the implementation to check for those traces. We discuss our design of a corresponding testing-system, and its use to test for qualitatively different kinds of properties in two commercial authorization systems. One is a database system that we call the D system, and the other is a file-sharing system that we call the I system. (We use pseudonyms at the request of the respective vendors.) In the context of the D system, our testing has uncovered several issues with its authorization system in the context of procedures that aggregate SQL statements that, to our knowledge, are new to the research literature. For the I system, we have established that it possesses several properties of interest.

The Chinese Wall security policy states that information from objects that are to be confidential from one another should not flow to a subject. It addresses conflict of interest, and was first articulated in the well-cited work of Brewer and Nash, which proposes also an enforcement mechanism for the policy. Work subsequent to theirs has observed that their enforcement mechanism is overly restrictive -- authorization states in which the policy is not violated may be rendered unreachable. We present two sets of novel results in this context. In one, we present an enforcement mechanism for the policy that is simple and efficient, and least-restrictive -- an authorization state is reachable if and only if it does not violate the policy. In our enforcement mechanism, the actions of a subject can constrain the prospective actions of another, a trade-off that we show every enforcement mechanism that is least-restrictive must incur. Our other set of results is that the enforcement mechanism of Brewer-Nash is even more restrictive than previous work establishes. Specifically, we show: (1) what is called the *-rule is overspecified in that one of its sub-rules implies the other, and, (2) if a subject is authorized to write to an object that contains confidential information, then all objects that contain confidential information must belong to the same conflict of interest class. Our work sheds new light on what is generally considered to be important work in information security.

The work by Harrison, Ruzzo, and Ullman (the HRU paper) on safety in the context of the access matrix model is widely considered to be foundational work in access control. In this paper, we address two errors we have discovered in the HRU paper. To our knowledge, these errors have not been previously reported in the literature. The first error regards a proof that shows that safety analysis for mono-operational HRU systems is in NP. The error stems from a faulty assumption that such systems are monotonic for the purpose of safety analysis. We present a corrected proof in this paper. The second error regards a mapping from one version of the safety problem to another that is presented in the HRU paper. We demonstrate that the mapping is not a reduction, and present a reduction that enables us to infer that the second version of safety introduced in the HRU paper is also undecidable for the HRU scheme. These errors lead us to ask whether the notion of safety as defined in the HRU paper is meaningful. We introduce other notions of safety that we argue have more intuitive appeal, and present the corresponding safety analysis results for the HRU scheme.

Verifying that access-control systems maintain desired security properties is recognized as an important problem in security. Enterprise access-control systems have grown to protect tens of thousands of resources, and there is a need for verification to scale commensurately. We present techniques for abstraction-refinement and bound-estimation for bounded model checkers to automatically find errors in Administrative Role-Based Access Control (ARBAC) security policies. ARBAC is the first and most comprehensive administrative scheme for Role-Based Access Control (RBAC) systems. In the abstraction-refinement portion of our approach, we identify and discard roles that are unlikely to be relevant to the verification question (the abstraction step). We then restore such abstracted roles incrementally (the refinement steps). In the bound-estimation portion of our approach, we lower the estimate of the diameter of the reachability graph from the worst-case by recognizing relationships between roles and state-change rules. Our techniques complement one another, and are used with conventional bounded model checking. Our approach is sound and complete: an error is found if and only if it exists. We have implemented our technique in an access-control policy analysis tool called Mohawk . We show empirically that Mohawk scales well to realistic policies, and provide a comparison with prior tools.

This work presents a method to reliably perform computations in the presence of hard faults arising from aggressive technology scaling, and design defects from human error. Our method is based on an observation that a single Turing-complete instruction can mirror the semantics of any other instruction. One such instruction is the subleq instruction, which has been used for instructional purposes in the past. We find that the scope for using such a Turing-complete instruction is far greater, and in this paper, we present its applicability to fault tolerance. In particular, we extend a MIPS processor with a co-processor (called ultra-reduced instruction set co-processor -- URISC) that implements the subleq instruction. We use the URISC to execute sequences of subleq that are semantically equivalent to the faulty instructions. We formally prove this, and implement the translations in the back-end of the LLVM compiler. We generate binaries for our hardware prototype called MIPS-URISC, which we synthesize and execute on an Altera FPGA. Our experiments indicate the performance and area overheads, and the efficacy of the proposed approach.

Usability is widely recognized as a problem in the context of the administration of access control systems. We seek to relate the notion of declarative semantics, a recurring theme in research in access control, with usability. We adopt the concrete context of POSIX ACLs and the traditional interface for it that comprises two utilities getfacl and setfacl whose natural semantics is operational. We have designed and implemented an alternate interface that we call askfacl whose natural semantics is declarative. We discuss our design of askfacl. We then discuss a human-subject usability study that we have designed and conducted that compares the two interfaces. Our results measurably demonstrate the goodness of declarative semantics in access control.

With the recent advent of cloud computing, the concept of outsourcing computations, initiated by volunteer computing efforts, is being revamped. While the two paradigms differ in several dimensions, they also share challenges, stemming from the lack of trust between outsourcers and workers. In this work, we propose a unifying trust framework, where correct participation is financially rewarded: neither participant is trusted, yet outsourced computations are efficiently verified and validly remunerated. We propose three solutions for this problem, relying on an offline bank to generate and redeem payments; the bank is oblivious to interactions between outsourcers and workers. We propose several attacks that can be launched against our framework and study the effectiveness of our solutions. We implemented our most secure solution and our experiments show that it is efficient: the bank can perform hundreds of payment transactions per second and the overheads imposed on outsourcers and workers are negligible.

Verifying that access-control systems maintain desired security properties is recognized as an important problem in security. Enterprise access-control systems have grown to protect tens of thousands of resources, and there is a need for verification to scale commensurately. We present a new abstraction-refinement technique for automatically finding errors in Administrative Role-Based Access Control (ARBAC) security policies. ARBAC is the first and most comprehensive administrative scheme for Role-Based Access Control (RBAC) systems. Underlying our approach is a change in mindset: we propose that error finding complements verification, can be more scalable, and allows for the use of a wider variety of techniques. In our approach, we use an abstraction-refinement technique to first identify and discard roles that are unlikely to be relevant to the verification question (the abstraction step), and then restore such abstracted roles incrementally (the refinement steps). Errors are one-sided: if there is an error in the abstracted policy, then there is an error in the original policy. If there is an error in a policy whose role-dependency graph diameter is smaller than a certain bound, then we find the error. Our abstraction-refinement technique complements conventional state-space exploration techniques such as model checking. We have implemented our technique in an access-control policy analysis tool. We show empirically that our tool scales well to realistic policies, and is orders of magnitude faster than prior tools.

We consider the distributed access enforcement problem for Role-Based Access Control (RBAC) systems. Such enforcement has become important with RBAC's increasing adoption, and the proliferation of data that needs to be protected. We assess six approaches, each of which has either been proposed in the literature, or is a natural candidate for access enforcement. The approaches are: directed graph, access matrix, authorization recycling, cpol, Bloom filter and cascade Bloom filter. We consider encodings of RBAC sessions in each, and propose and justify a benchmark for the assessment. We present our results from an empirical assessment of time, space and administrative efficiency based on the benchmark. We conclude with inferences we can make regarding the best approach to access enforcement for particular RBAC deployments based on our assessment.

We present gitolite, an authorization scheme for Version Control Systems (VCSes). We have implemented it for the Git VCS. A VCS enables versioning, distributed collaboration and several other features, and is an important context for authorization and access control. Our main consideration behind the design of gitolite is the balance between expressive power, correctness and usability in realistic settings. We discuss our design of gitolite, and in particular the four user-classes in its delegation model, and the administrative actions a user at each class performs. We discuss also our ongoing work on expressing gitolite precisely in first-order logic, to thereby give it a precise semantics and establish correctness properties. gitolite has been adopted in open-source software development, university and industry settings. We discuss our experience with these deployments, and present some performance results related to access enforcement from a real deployment.

Access control is acknowledged to be one of the most important aspects of security. Research and deployments related to access control in computers and networks dates back several decades.

We propose a new approach for applying Role-Based Access Control (RBAC) to methods in objects in the Java programming language. In our approach, a policy implementer (usually a developer) annotates methods, interfaces, and classes with roles. Our system automatically creates proxy objects which only contain methods to which a client is authorized access based on the role specifications. Potentially untrusted clients that use Remote Method Invocation (RMI) then receive proxy objects rather than the originals.

Initiated by volunteer computing efforts, the computation outsourcing problem can become a compelling application for networked set-top-boxes and mobile devices. In this paper we extend such environments with the ability to provide secure payments in exchange for outsourced CPU cycles. Previous contributions in wired networks have almost exclusively tackled only one side of the problem -- offering incentives for volunteer participation and preventing worker laziness. This makes sense in static environments where reputable outsourcers have little to gain from incorrectly rewarding honest participation. However, this assumption is no longer valid in ad hoc environments, where unique identities are difficult to provide and anyone can outsource computations. In this paper we propose a solution that simultaneously ensures correct remuneration for jobs completed on time and prevents worker laziness. Our solution relies on an offline bank to generate and redeem payments; the bank is oblivious to interactions between outsourcers and workers. In particular, the bank is not involved in job computation or verification. Our experiments show that the solution is efficient: the bank can perform hundreds of payment transactions per second and the overheads imposed on outsourcers and workers are negligible.

We address the distributed setting for enforcement of a centralized Role-Based Access Control (RBAC) protection state. We present a new approach for time- and space-efficient access enforcement. Underlying our approach is a data structure that we call a cascade Bloom filter. We describe our approach, provide details about the cascade Bloom filter, its associated algorithms, soundness and completeness properties for those algorithms, and provide an empirical validation for distributed access enforcement of RBAC. We demonstrate that even in low-capability devices such as WiFi network access points, we can perform thousands of access checks in a second.

We introduce the notion of resiliency policies in the context of access control systems. Such policies require an access control system to be resilient to the absence of users. An example resiliency policy requires that upon removal of any s users, there should still exist d disjoint sets of users such that the users in each set together possess certain permissions of interest. Such a policy ensures that even when emergency situations cause some users to be absent, there still exist independent teams of users that have the permissions necessary for carrying out critical tasks. The Resiliency Checking Problem determines whether an access control state satisfies a given resiliency policy. We show that the general case of the problem and several subcases are intractable ( NP -hard), and identify two subcases that are solvable in linear time. For the intractable cases, we also identify the complexity class in the polynomial hierarchy to which these problems belong. We discuss the design and evaluation of an algorithm that can efficiently solve instances of nontrivial sizes that belong to the intractable cases of the problem. Furthermore, we study the consistency problem between resiliency policies and static separation of duty policies. Finally, we combine the notions of resiliency and separation of duty to introduce the resilient separation of duty policy, which is useful in situations where both fault-tolerance and fraud-prevention are desired.

The IEEE 802.11s working group is tasked to provide ways of establishing and securing a wireless mesh network. One proposal establishes a Mesh Security Architecture (MSA), with a developed key hierarchy and full protocol definitions. This paper examines the correctness and security of the MSA proposal and its corresponding protocols. We utilize Protocol Composition Logic (PCL) to prove individual protocols secure, as well as their composition. We add to the structure of PCL, generalizing it for peer-to-peer applications. We also discuss two security issues we discovered with original versions of the proposals and our proposed remedies.

Specifying and managing access control policies is a challenging problem. We propose to develop formal verification techniques for access control policies to improve the current state of the art of policy specification and management. In this paper, we formalize classes of security analysis problems in the context of Role-Based Access Control. We show that in general these problems are PSPACE-complete. We also study the factors that contribute to the computational complexity by considering a lattice of various subcases of the problem with different restrictions. We show that several subcases remain PSPACE-complete, several further restricted subcases are NP-complete, and identify two subcases that are solvable in polynomial time. We also discuss our experiences and findings from experimentations that use existing formal method tools, such as model checking and logic programming, for addressing these problems.

We present a theory for comparing the expressive power of access control models. The theory is based on simulations that preserve security properties. We perceive access control systems as state-transition systems and present two kinds of simulations, reductions and state-matching reductions. In applying the theory, we highlight four new results and discuss these results in the context of other results that can be inferred or are known. One result indicates that the access matrix scheme due to Harrison, Ruzzo and Ullman is limited in its expressive power when compared with a trust-management scheme, thereby formally establishing a conjecture from the literature. A second result is that a particular RBAC (Role-Based Access Control) scheme, ARBAC97, may be limited in its expressive power, thereby countering claims in the literature that RBAC is more expressive than DAC (Discretionary Access Control). A third result demonstrates that the ability to check for the absence of rights (in addition to the presence of rights) can cause a scheme to be more expressive. A fourth result is that a trust-management scheme is at least as expressive as RBAC with a particular administrative scheme (the URA97 component of ARBAC97).

Separation-of-duty (SoD) is widely considered to be a fundamental principle in computer security. A static SoD (SSoD) policy states that in order to have all permissions necessary to complete a sensitive task, the cooperation of at least a certain number of users is required. Role-based access control (RBAC) is today's dominant access-control model. It is widely believed that one of RBAC's main strengths is that it enables the use of constraints to support policies, such as separation-of-duty. In the literature on RBAC, statically mutually exclusive roles (SMER) constraints are used to enforce SSoD policies. In this paper, we formulate and study fundamental computational problems related to the use of SMER constraints to enforce SSoD policies. We show that directly enforcing SSoD policies is intractable (coNP-complete), while checking whether an RBAC state satisfies a set of SMER constraints is efficient; however, verifying whether a given set of SMER constraints enforces an SSoD policy is also intractable (coNP-complete). We discuss the implications of these results. We show also how to generate SMER constraints that are as accurate as possible for enforcing an SSoD policy.

We introduce the notion of resiliency policies in the context of access control systems. Such policies require an access control system to be resilient to the absence of users. An example resiliency policy requires that, upon removal of any s users, there should still exist d disjoint sets of users such that the users in each set together possess certain permissions of interest. Such a policy ensures that even when emergency situations cause some users to be absent, there still exist independent teams of users that have the permissions necessary for carrying out critical tasks. The Resiliency Checking Problem determines whether an access control state satisfies a given resiliency policy. We show that the general case of the problem and several subcases are intractable (NP-hard), and identify two subcases that are solvable in linear time. For the intractable cases, we also identify the complexity class in the polynomial hierarchy to which these problems belong. We discuss the design and evaluation of an algorithm that can efficiently solve instances of nontrivial sizes that belong to the intractable cases of the problem. Finally, we study the consistency problem between resiliency policies and static separation of duty policies.

The administration of large role-based access control (RBAC) systems is a challenging problem. In order to administer such systems, decentralization of administration tasks by the use of delegation is an effective approach. While the use of delegation greatly enhances flexibility and scalability, it may reduce the control that an organization has over its resources, thereby diminishing a major advantage RBAC has over discretionary access control (DAC). We propose to use security analysis techniques to maintain desirable security properties while delegating administrative privileges. We give a precise definition of a family of security analysis problems in RBAC, which is more general than safety analysis that is studied in the literature. We show that two classes of problems in the family can be reduced to similar analysis in the RT[↞∩] role-based trust-management language, thereby establishing an interesting relationship between RBAC and the RT framework. The reduction gives efficient algorithms for answering most kinds of queries in these two classes and establishes the complexity bounds for the intractable cases.

An apparently prevailing myth is that safety is undecidable in discretionary access control (DAC); therefore, one needs to invent new DAC schemes in which safety analysis is decidable. In this paper we dispel this myth. We argue that DAC should not be equated with the Harrison-Ruzzo-Ullman (1976) access matrix scheme, in which safety is undecidable. We present an efficient (running time cubic in its input size) algorithm for deciding safety in the Graham-Denning (1972) DAC scheme, which subsumes the DAC schemes used in the literature on comparing DAC with other access control models. We also counter several claims made in recent work by Solworth and Sloan (2004), in which the authors present a new access control scheme based on labels and relabelling and assert that it can implement the full range of DAC models. We present a precise characterization of their access control scheme and show that it does not adequately capture a relatively simple DAC scheme.

Separation of Duty (SoD) is widely considered to be a fundamental principle in computer security. A Static SoD (SSoD) policy states that in order to have all permissions necessary to complete a sensitive task, the cooperation of at least a certain number of users is required. In Role-Based Access Control (RBAC), Statically Mutually Exclusive Role (SMER) constraints are used to enforce SSoD policies. In this paper, we pose and answer fundamental questions related to the use of SMER constraints to enforce SSoD policies. We show that directly enforcing SSoD policies is intractable (coNP-complete), while checking whether an RBAC state satisfies a set of SMER constraints is efficient. Also, we show that verifying whether a given set of SMER constraints enforces an SSoD policy is intractable (coNP-complete) and discuss why this intractability result should not lead us to conclude that SMER constraints are not an appropriate mechanism for enforcing SSoD policies.

Comparing the expressive power of access control models is recognized as a fundamental problem in computer security. Such comparisons are generally based on simulations between different access control schemes. However, the definitions for simulations that are used in the literature make it impossible to put results and claims about the expressive power of access control models into a single context and to compare such models to one another in a meaningful way.

Delegation is often used in administrative models for Role-Based Access Control (RBAC) systems to decentralize administration tasks. While the use of delegation greatly enhances flexibility and scalability, it may reduce the control that an organization has over its resources, thereby diminishing a major advantage RBAC has over Discretionary Access Control(DAC). We propose to use security analysis techniques to maintain desirable security properties while delegating administrative privileges. We give a precise definition of a family of security analysis problems in RBAC, which is more general than safety analysis that is studied in the literature. We also show that two classes of problems in the family can be reduced to similar analysis in the RT0 trust-management language, thereby establishing an interesting relationship between RBAC and the RT (Role-based Trust-management) framework. The reduction gives efficient algorithms for answering most kinds of queries in these two classes and establishes the complexity bounds for the intractable cases.

Discusses the Address Resolution Protocol (ARP) and the problem of ARP cache poisoning. ARP cache poisoning is the malicious act, by a host in a LAN, of introducing a spurious IP address to MAC (Ethernet) address mapping in another host's ARP cache. We discuss design constraints for a solution: the solution needs to be implemented in middleware, without any access or change to any operating system source code, it needs to be backward-compatible with the existing protocol and to be asynchronous. We present our solution and implementation aspects of it in a Streams-based networking subsystem. Our solution comprises two parts: a "bump in the stack" Streams module, and a separate Stream with a driver and user-level application. We also present the algorithm that is executed in the module and application to prevent ARP cache poisoning where possible, and to detect and raise alarms otherwise. We then discuss some limitations with our approach and present some preliminary performance figures for our implementation.