Domain-based policies group subjects and objects that share the same access control characteristics into protection domains, with authorization rules formulated in terms of these domains. This policy model is used in operating systems such as SEAndroid. Recent work by Zhang and Fong addresses the mining of domain-based policies from noise-free but incomplete access logs using MaxSAT solving. Due to the computational intensity of MaxSAT, their approach is limited to policy mining instances of moderate size.

Continuous authentication helps mitigate the risk of session hijacking, insider attack, and privilege abuse. Applying zero trust principles, this paper proposes a family of four formally specified access control models to account for the use of continuous authentication to monitor user access patterns in user-facing software applications, each model providing increasingly expressive user modeling capabilities. We name these models Zero Trust Continuous Authentication (ZTCA). Deploying a ZTCA model requires the authoring of policies. To ease the challenge of developing ZTCA policies, we studied the problem of automatically generating ZTCA policies from declarative usability and security requirements. We devised a novel SAT encoding for the automated policy formulation problem, so that policy formulation can be performed by state-of-the-art SAT solvers. Empirical experiments demonstrate that our novel encoding approach runs significantly faster than a competing encoding approach previously published in the literature.

Protection domains are one of the most enduring concepts in Access Control. Entities with identical access control characteristics are grouped under the same protection domain, and domain-based policies assign access privileges to the protection domain as a whole. With the advent of the Internet of Things (IoT), devices play the roles of both subjects and objects. Domain-based policies are particularly suited to support this symmetry of roles. This paper studies the mining of domain-based policies from incomplete access logs. We began by building a theory of domain-based policies, resulting in a polynomial-time algorithm that constructs the optimal domain-based policy out of a given access control matrix. We then showed that the problem of domain-based policy mining (DBPM) and the related problem of mining policies for domain and type enforcement (DTEPM) are both NP-complete. Next, we looked at the practical problem of using a MaxSAT solver to solve DBPM. We devised sophisticated encodings for this purpose, and empirically evaluated their relative performance. This paper thus lays the groundwork for future study of DBPM.

Online event hosting platforms, such as Zoom Meetings and Twitch Streams, have revolutionized the way we socialize with one another. These platforms offer a rich set of interactive features such as live chat and gestures, enabling dynamic and engaging social events. In public events, however, participants are not well-known entities originating from the same institution, and thus traditional access control fails to provide means for maintaining order without disrupting interactivity. Zoombombing and cyberbullying in Twitch Streams are symptoms of this dilemma. The design of the aforementioned event hosting systems thus resort to social control mechanisms that allow moderators to monitor the social interactions of the participants and respond to disorderly behavior in real time. The designer of an event hosting system needs to make sure that social control mechanisms preserve interactivity expectations. In this paper, we introduce HIPE (Highly Interactive Public Event), a framework for modelling social control mechanisms, articulating interactivity expectations, as well as verifying if social control interferes with interactivity. We catalogued 4 classes of social control mechanisms that can be reused in the design of event hosting systems, including sanction, remedy, containment, and retaliation. Additionally, we formulated a 2-safety hyperproperty known as ( a , p )-interactivity, for expressing the degree of interactivity expected of an event hosting system. Furthermore, we designed a model checking algorithm for verifying ( a , p )-interactivity. An empirical case study has been conducted to illustrate the interplay between social control and interactivity, as well as to evaluate the performance of our model checking algorithm. To the best of our knowledge this is the first work to formally study the balancing of social control and interactivity in public events.

Cyberphysical systems involve connected devices that are physically embedded. These devices enter into transient relationships with one another and with the environment. We propose an access control model, HO(T)-ReBAC, for facilitating access control in such dynamic environments. Specifically, HO(T)-ReBAC bases its authorization decisions on the history of relationship changes. We demonstrate the usefulness of this model in a case study on a Medical Internet-of-Things application. We extend a recently proposed graph matching algorithm to handle temporality in our model, thereby yielding an efficient authorization mechanism, the performance of which has been evaluated empirically. This model is the first instantiation of a general idea, Higher-Order Relationship-Based Access Control, that we have been developing.

Controlled sharing is fundamental to distributed systems. We consider a capability-based distributed authorization system where a client receives capabilities (access tokens) from an authorization server to access the resources of resource servers. Capability-based authorization systems have been widely used on the Web, in mobile applications and other distributed systems.

Neo4j is a popular graph database that offers two versions: an enterprise edition and a community edition . The enterprise edition offers customizable Role-based Access Control features through custom developed procedures , while the community edition does not offer any access control support. Being a graph database, Neo4j appears to be a natural application for Relationship-Based Access Control (ReBAC), an access control paradigm where authorization decisions are based on relationships between subjects and resources in the system (i.e., an authorization graph). In this article, we present AReBAC, an attribute-supporting ReBAC model for Neo4j that provides finer-grained access control by operating over resources instead of procedures. AReBAC employs Nano-Cypher, a declarative policy language based on Neo4j’s Cypher query language, the result of which allows us to weave database queries with access control policies and evaluate both simultaneously. Evaluating the combined query and policy produces a result that (i) matches the search criteria, and (ii) the requesting subject is authorized to access. AReBAC is accompanied by the algorithms and their implementation required for the realization of the presented ideas, including GP-Eval, a query evaluation algorithm. We also introduce Live-End Backjumping (LBJ), a backtracking scheme that provides a significant performance boost over conflict-directed backjumping for evaluating queries. As demonstrated in our previous work, the original version of GP-Eval already performs significantly faster than the Neo4j’s Cypher evaluation engine. The optimized version of GP-Eval , which employs LBJ, further improves the performance significantly, thereby demonstrating the capabilities of the technique.

First proposed by Wang and Li in 2007, workflow resiliency is a policy analysis for ensuring that, even when an adversarial environment removes a subset of workers from service, a workflow can still be instantiated to satisfy all the security constraints. Wang and Li proposed three notions of workflow resiliency: static, decremental, and dynamic resiliency. While decremental and dynamic resiliency are both PSPACE-complete, Wang and Li did not provide a matching lower and upper bound for the complexity of static resiliency. The present work begins with proving that static resiliency is $¶i^p_2$-complete, thereby bridging a long-standing complexity gap in the literature. In addition, a fourth notion of workflow resiliency, one-shot resiliency, is proposed and shown to remain in the third level of the polynomial hierarchy. This shows that sophisticated notions of workflow resiliency need not be PSPACE-complete. Lastly, we demonstrate how to reduce static and one-shot resiliency to Answer Set Programming (ASP), a modern constraint-solving technology that can be used for solving reasoning tasks in the lower levels of the polynomial hierarchy. In summary, this work demonstrates the value of focusing on notions of workflow resiliency that reside in the lower levels of the polynomial hierarchy.

Event-based systems lie at the heart of many cloud-based Internet-of-Things (IoT) platforms. This combination of the Broker architectural style and the Publisher-Subscriber design pattern provides a way for smart devices to communicate and coordinate with one another. The present design of these cloud-based IoT frameworks lacks measures to (i) protect devices against malicious cloud disconnections, (ii) impose information flow control among communicating parties, and (iii) enforce coordination protocols in the presence of compromised devices. In this work, we propose to extend the modular event-based system architecture of Fiege et al., to incorporate brokering policies and execution monitors, in order to address the three protection challenges mentioned above. We formalized the operational semantics of our protection scheme, explored how the scheme can be used to enforce BLP-style information flow control and RBAC-style protection domains, implemented the proposal in an open-source MQTT broker, and evaluated the performance impact of the protection mechanisms.

Neo4j is a popular graph database that offers two versions; a paid enterprise edition and a free community edition. The enterprise edition offers customizable Role-Based Access Control (RBAC) features through custom developed procedures, while the community edition does not offer any access control support. Being a graph database, Neo4j is a natural application for Relationship-Based Access Control (ReBAC), an access control paradigm where authorization decisions are based on relationships between subjects and resources in the system. In this paper we present AReBAC, an attribute-supporting ReBAC model for Neo4j (applicable to both editions) that provides finer grained access control. AReBAC employs Nano-Cypher, a declarative policy language based on Neo4j»s Cypher query language, the result of which allows us to weave database queries with access control policies and evaluate both simultaneously. Evaluating the combined query and policy produces a result that i) matches the search criteria, and ii) the requesting subject has access to. Our experiments show that our evaluation algorithm performs faster than Neo4j»s query evaluation engine when evaluating queries that are expressible using Nano-Cypher.

Permissions are highly sensitive in Internet-of-Things (IoT) applications, as IoT devices collect our personal data and control the safety of our environment. Rather than simply granting permissions, further constraints shall be imposed on permission usage so as to realize the Principle of Least Privilege. Since IoT devices are physically embedded, they are often accessed in a particular sequence based on their relative physical positions. Monitoring if such sequencing constraints are honoured when IoT devices are accessed provides a means to fence off malicious accesses. This paper proposes a history-based capability system, HCAP, for enforcing permission sequencing constraints in a distributed authorization environment. We formally establish the security guarantees of HCAP, and empirically evaluate its performance.

Social Network Systems (SNSs) allow third-party extensions to access user profiles by providing an Application Programming Interface (API). It has been demonstrated in the literature that this API can be exploited by malicious extensions to infer users' sensitive information from the information that is accessible through the API. To prevent this type of privacy violation, we propose a view-based protection model, in which a sanitizing transformation, called a view, is applied to the user profile when it is queried by a third-party extension. We demonstrate empirically that such a protection mechanism effectively reduces the statistical correlation between sensitive and accessible information. We also propose an optimization in which the materialization of views is performed lazily: rather than sanitizing the entire profile during a query, only the parts of the profile that are visible to the query are transformed. We demonstrate empirically that this optimization offers visible performance advantage, and propose a programming language-independent, probabilistic automata model for encoding such transformations.

Modern social computing platforms (e.g., Facebook) are extensible. Third-party developers deploy extensions (e.g., Facebook applications) that augment the functionalities of the underlying platforms. Previous work demonstrated that permission-based protection mechanisms, adopted to control access to users' personal information, fail to control inference - the inference of private information from public information. We envision an alternative protection model in which user profiles undergo sanitizing transformations before being released to third-party applications. Each transformation specifies an alternative view of the user profile. Unlike permission-based protection, this framework addresses the need for inference control. This work lays the theoretical foundation for view-based protection in three ways. First, existing work in privacy- preserving data publishing focuses on structured data (e.g., tables), but user profiles are semi-structured (e.g., trees). In information-theoretic terms, we define privacy and utility goals that can be applied to semi-structured data. Our notions of privacy and utility are highly targeted, mirroring the set up of social computing platforms, in which users specify their privacy preferences and third-party applications focus their accesses on selected components of the user profile. Second, we define an algebra of trees in which sanitizing transformations previously designed for structured data (e.g., generalization, noise introduction, etc) are now formulated for semi-structured data in terms of tree operations. Third, we evaluate the usefulness of our model by illustrating how the privacy enhancement and utility preservation effects of a view (a sanitizing transformation) can be formally and quantitatively assessed in our model. To the best of our knowledge, ours is the first work to articulate precise privacy and utility goals of inference control mechanisms for third-party applications in social computing platforms.

The collaborative nature of content development has given rise to the novel problem of multiple ownership in access control, such that a shared resource is administrated simultaneously by co-owners who may have conflicting privacy preferences and/or sharing needs. Prior work has focused on the design of unsupervised conflict resolution mechanisms.

Abstract We present GSUVis, a visualization tool designed to provide better understanding of location‐based social network (LBSN) data. LBSN data is one of the most important sources of information for transportation, marketing, health, and public safety. LBSN data consumers are interested in accessing and analysing data that is as complete and as accurate as possible. However, LBSN data contains sensitive information about individuals. Consequently, data anonymization is of critical importance if this data is to be made available to consumers. However, anonymization commonly reduces the utility of information available. Working with privacy experts, we designed GSUVis a visual analytic tool to help experts better understand the effects of anonymization techniques on LBSN data utility. One of GSUVis's primary goals is to make it possible for people to use LBSN data, without requiring them to gain deep knowledge about data anonymization. To inform the design of GSUVis, we interviewed privacy experts, and collected their tasks and system requirements. Based on this understanding, we designed and implemented GSUVis. It applies two anonymization algorithms for social and location trajectory data to a real‐world LBSN dataset and visualizes the data both before and after anonymization. Through feedback from domain experts, we reflect on the effectiveness of GSUVis and the impact of anonymization using visualization.

Inspired by the access control models of social network systems, Relationship-Based Access Control (ReBAC) was recently proposed as a general-purpose access control paradigm for application domains in which authorization must take into account the relationship between the access requestor and the resource owner. The healthcare domain is envisioned to be an archetypical application domain in which ReBAC is sorely needed: e.g., my patient record should be accessible only by my family doctor, but not by all doctors.

Nowadays, a user may belong to multiple social computing systems (SCSs) in order to benefit from a variety of services that each SCS may provide. To facilitate the sharing of contents across the system boundary, some SCSs provide a mechanism by which a user may "connect" his accounts on two SCSs. The effect is that contents from one SCS can now be shared to another SCS. Although such a connection feature delivers clear usability advantages for users, it also generates a host of privacy challenges. A notable challenge is that the access control policy of the SCS from which the content originates may not be honoured by the SCS to which the content migrates, because the latter fails to faithfully replicate the protection model of the former.

In social computing, multiple users may have privacy stakes in a content (e.g., a tagged photo). They may all want to have a say on the choice of access control policy for protecting that content. The study of protection schemes for multiple stakeholders in social computing has captured the imagination of researchers, and general-purpose schemes for reconciling the differences of privacy stakeholders have been proposed. A challenge of existing multiple-stakeholder schemes is that they can be very complex. In this work, we consider the possibility of simplification in special cases. If we focus on specific instances of multiple stakeholders, are there simpler design of access control schemes? We identify two design patterns for handling a significant family of multiple-stakeholder scenarios. We discuss efficient implementation techniques that solely rely on standard SQL technology. We also identify scenarios in which general-purpose multiple-stakeholder schemes are necessary. We believe that future work on multiple stakeholders should focus on these scenarios.

A Geo-Social Computing System (GSCS) allows users to declare their current locations, and uses these declared locations to make authorization decisions. Recent years have seen the emergence of a new generation of social computing systems that are GSCSs. This paper proposes a protection model for GSCSs. The protection system tracks the current locations of users and a knowledge base of primitive spatial relations between locations. Access control policies can be formulated by the composition of primitive spatial relations. The model is extended to account for Geo-Social Network Systems (GSNSs), which track both a spatial knowledge base and a social network. A policy language for GSNSs is proposed for specifying policies that combine both social and spatial constraints.

Abstract We introduce Papilio, a new visualization technique for visualizing permissions of real‐world Android applications. We explore the development of layouts that exploit the directed acyclic nature of Android application permission data to develop a new explicit layout technique that incorporates aspects of set membership, node‐link diagrams and matrix layouts. By grouping applications based on sets of requested permissions, a structure can be formed with partially ordered relations. The Papilio layout shows sets of applications centrally, the relations among applications on one side and application permissions, as the reason behind the existence of the partial order, on the other side. Using Papilio to explore a set of Android applications as a case study has led to new security findings regarding permission usage by Android applications.

Purpose is a key concept in privacy policies. Although some models have been proposed for enforcing purpose-based privacy policies , little has been done in defining formal semantics for purpose, and therefore an effective enforcement mechanism for such policies has remained a challenge. We have developed a framework for expressing and enforcing such policies by giving a formal definition of purpose and proposing a modal-logic language for formally expressing purpose constraints. The semantics of this language are defined over an abstract model of workflows . Based on this formal framework, we discuss some properties of purpose, show how common forms of purpose constraints can be formalized, how purpose-based constraints can be connected to more general access control policies, and how they can be enforced in a workflow-based information system by extending common access control technologies.

Social Network Systems (SNSs) providers allow third-party extensions to access users' information through an Application Programming Interface (API). Once an extension has been authorized by a user to access data in a user's profile, there is no more control on how that extension uses the data. This raises serious concerns about user privacy because a malicious extension may infer some private information based on the legitimately accessible information. This information leakage is called an inference attack. In addition, inference attacks are not only a privacy violation, they could also be used as the building blocks for more dangerous security attacks, such as identity theft. In this work, we conduct a comprehensive empirical study to assess the feasibility and accuracy of inference attacks that are launched from the extension API of SNSs. We also discuss an attack scenario in which inference attacks are employed as building blocks. The significance of this work is in thoroughly discussing how inference attacks could happen in practice via the extension API of SNSs, and highlighting the clear and present danger of even the naively crafted inference attacks.

Users of an online community are willing to share resources because they can expect reasonable behaviour from other members of the community. Such expectations are known as social contracts. In this work, we study the specification and enforcement of social contracts in a computer mediated collaboration environment. Specifically, we examine social contracts that contain both relationship- and history-based elements. A series of policy languages, all based on modal and temporal logics, with increasing expressiveness, have been proposed to express social contracts. Reference monitors are designed to correctly and efficiently enforce the specified policies. A technique called "relational abstraction" is employed to reduce the reference monitor into a purely relationship-based protection system, that is, what is commonly known as a social network system.

In policy composition frameworks, such as XACML, composite policies can be formed by the application of policy composition algorithms (PCAs), which combine authorization decisions of component policies. Understanding the behaviour of composite policies is a non-trivial endeavour, but instrumental in the engineering of correct access control policies. Existing policy analyses take a black-box approach, in which the global behaviour of the composite policy is assessed. A black-box approach is useful for detecting the presence of erroneous behaviour, but not particularly useful for locating the source of the error. In this work, we propose a white-box policy analysis, known as Decision in Context (DIC), that assesses the behaviour of component policies situated in a composite policy. We show that the DIC query can be applied to facilitate policy change impact analysis, break-glass reduction analysis, dead policy identification, as well as the pruning of redundant subpolicies. For generality, the DIC query is defined in an XACML-style policy composition framework that is agnostic of the underlying access control model. The DIC query is implemented via a reduction to either propositional satisfiability (SAT) or pseudo boolean satisfiability (PBS) instances, after which standard solvers can be invoked to complete the evaluation. Empirical analyses have been conducted to compare the relative efficiency of the SAT and PBS encodings. The latter is found to be a more effective encoding, especially for composite policies containing majority-voting PCAs.

An extensible software system must protect its resources from being abused by untrusted software extensions. The access control policies of such systems are traditionally enforced by reference monitors. Recent study of access control policies advocates the use of obligation policies, which impose behavioural constraints to the future actions of the accessor after the access is granted. It is argued that obligation policies provide continuous protection to the system.

Access control policy is typically defined in terms of attributes, but in many applications it is more natural to define permissions in terms of relationships that resources, systems, and contexts may enjoy. The paradigm of relationship-based access control has been proposed to address this issue, and modal logic has been used as a technical foundation.

Social Network Systems pioneer a paradigm of access control that is distinct from traditional approaches to access control. Gates coined the term Relationship-Based Access Control (ReBAC) to refer to this paradigm. ReBAC is characterized by the explicit tracking of interpersonal relationships between users, and the expression of access control policies in terms of these relationships. This work explores what it takes to widen the applicability of ReBAC to application domains other than social computing. To this end, we formulate an archetypical ReBAC model to capture the essence of the paradigm, that is, authorization decisions are based on the relationship between the resource owner and the resource accessor in a social network maintained by the protection system. A novelty of the model is that it captures the contextual nature of relationships. We devise a policy language, based on modal logic, for composing access control policies that support delegation of trust. We use a case study in the domain of Electronic Health Records to demonstrate the utility of our model and its policy language. This work provides initial evidence to the feasibility and utility of ReBAC as a general-purpose paradigm of access control.

We define a semantic model for purpose, based on which purpose-based privacy policies can be meaningfully expressed and enforced in a business system. The model is based on the intuition that the purpose of an action is determined by its situation among other inter-related actions. Actions and their relationships can be modeled in the form of an action graph which is based on the business processes in a system. Accordingly, a modal logic and the corresponding model checking algorithm are developed for formal expression of purpose-based policies and verifying whether a particular system complies with them. It is also shown through various examples, how various typical purpose-based policies as well as some new policy types can be expressed and checked using our model.

The Relationship-Based Access Control (ReBAC) model was recently proposed as a general-purpose access control model. It supports the natural expression of parameterized roles, the composition of policies, and the delegation of trust. Fong proposed a policy language that is based on Modal Logic for expressing and composing ReBAC policies. A natural question is whether such a language is representationally complete, that is, whether the language is capable of expressing all ReBAC policies that one is interested in expressing. In this work, we argue that the extensive use of what we call Relational Policies is what distinguishes ReBAC from traditional access control models. We show that Fong’s policy language is representationally incomplete in that certain previously studied Relational Policies are not expressible in the language. We introduce two extensions to the policy language of Fong, and prove that the extended policy language is representationally complete with respect to a well-defined subclass of Relational Policies.

In Face book-style Social Network Systems (FSNSs), which are a generalization of the access control model of Face book, an access control policy specifies a graph-theoretic relationship between the resource owner and resource access or that must hold in the social graph in order for access to be granted. Pseudonymous identities may collude to alter the topology of the social graph and gain access that would otherwise be forbidden. We formalize Denning's Principle of Privilege Attenuation (POPA) as a run-time property, and demonstrate that it is a necessary and sufficient condition for preventing the above form of Sybil attacks. A static policy analysis is then devised for verifying that an FSNS is POPA compliant (and thus Sybil free). The static analysis is proven to be both sound and complete. We also extend our analysis to cover a peculiar feature of FSNS, namely, what Fong et al. dubbed as Stage-I Authorization. We discuss the anomalies resulted from this extension, and point out the need to redesign Stage-I Authorization to support a rational POPA-compliance analysis.

Inlined Reference Monitor (IRM) is an established enforcement mechanism for history-based access control policies. IRM enforcement injects monitoring code into the binary of an untrusted program in order to track its execution history. The injected code denies access when execution deviates from the policy. The viability of IRM enforcement is predicated on the ability of the binary rewriting element to optimize away redundant monitoring code without compromising security.

Recent years have seen unprecedented growth in the popularity of social network systems, with Facebook being an archetypical example. The access control paradigm behind the privacy preservation mechanism of Facebook is distinctly different from such existing access control paradigms as Discretionary Access Control, Role-Based Access Control, Capability Systems, and Trust Management Systems. This work takes a first step in deepening the understanding of this access control paradigm, by proposing an access control model that formalizes and generalizes the privacy preservation mechanism of Facebook. The model can be instantiated into a family of Facebook-style social network systems, each with a recognizably different access control mechanism, so that Facebook is but one instantiation of the model. We also demonstrate that the model can be instantiated to express policies that are not currently supported by Facebook but possess rich and natural social significance. This work thus delineates the design space of privacy preservation mechanisms for Facebook-style social network systems, and lays out a formal framework for policy analysis in these systems.

With the recent advent of dynamically extensible software systems, in which software extensions may be dynamically loaded into the address space of a core application to augment its capabilities, there is a growing interest in protection mechanisms that can isolate untrusted software components from a host application. Existing language-based environments such as the JVM and the CLI achieves software isolation by an interposition mechanism known as stack inspection. Expressive as it is, stack inspection is known to lack declarative characterization and is brittle in the face of evolving software configurations. A run-time module system, ISOMOD, is proposed for the Java platform to facilitate software isolation. A core application may create namespaces dynamically and impose arbitrary name visibility policies to control whether a name is visible, to whom it is visible, and in what way it can be accessed. Because ISOMOD exercises name visibility control at load time, loaded code runs at full speed. Furthermore, because ISOMOD access control policies are maintained separately, they evolve independently from core application code. In addition, the ISOMOD policy language provides a declarative means for expressing a very general form of visibility constraints. Not only can the ISOMOD policy language simulate a sizable subset of permissions in the Java 2 security architecture, it does so with policies that are robust to changes in software configurations. The ISOMOD policy language is also expressive enough to completely encode a capability type system known as Discretionary Capability Confinement. In spite of its expressiveness, the ISOMOD policy language admits an efficient implementation strategy. In short, ISOMOD avoids the technical difficulties of interposition by trading off an acceptable level of expressiveness. Name visibility control in the style of ISOMOD is therefore a lightweight alternative to interposition.

Through the design and implementation of a JVM that supports Pluggable Verification Modules (PVMs), the idea of an extensible protection mechanism is entertained. Link-time bytecode verification becomes a pluggable service that can be readily replaced, reconfigured and augmented. Application-specific verification services can be safely introduced into the dynamic linking process of the JVM. This feature is enabled by the adoption of a previously proposed modular verification architecture, Proof Linking [23, 24], which decouples bytecode verification from the dynamic linking process, rendering the verifier a replaceable module. The PVM mechanism has been implemented in an open source JVM, the Aegis VM [21]. To evaluate the software engineering and security engineering benefits of this extensible protection mechanism, an augmented type system JAC (Java Access Control) [37] has been successfully implemented as a PVM.

Software execution environments like operating systems, mobile code platforms and scriptable applications must protect themselves against potential damages caused by malicious code. Monitoring the execution history of the latter provides an effective means for controlling the access pattern of system services. Several authors have recently proposed increasingly general automata models for characterizing various classes of security policies enforceable by execution monitoring. An open question raised by Bauer, Ligatti and Walker is whether one can further classify the space of security policies by constraining the capabilities of the execution monitor. This paper presents a novel information-based approach to address the research problem. Specifically, security policies are characterized by the information consumed by an enforcing execution monitor. By restricting the execution monitor to track only a shallow history of previously granted access events, a precise characterization of a class of security policies enforceable by restricted access to information is identified. Although provably less expressive than the general class of policies enforceable by execution monitoring, this class does contain naturally occurring policies including Chinese Wall policy, low-water-mark policy, one-out-of-k authorization, assured pipelines, etc. Encouraged by this success, the technique is generalized to produce a lattice of policy classes. Within the lattice, policy classes are ordered by the information required for enforcing member policies. Such a fine-grained policy classification lays the semantic foundation for future studies on special-purpose policy languages.

Although mobile code systems typically employ link-time code verifiers to protect host computers from potentially malicious code, implementation flaws in the verifiers may still leave the host system vulnerable to attack. Compounding the inherent complexity of the verification algorithms themselves, the need to support lazy, dynamic linking in mobile code systems typically leads to architectures that exhibit strong interdependencies between the loader, the verifier, and the linker. To simplify verifier construction and provide improved assurances of verifier integrity, we propose a modular architecture based on the concept of proof linking. This architecture encapsulates the verification process and removes dependencies between the loader, the verifier, and the linker. We also formally model the process of proof linking and establish properties to which correct implementations must conform. As an example, we instantiate our architecture for the problem of Java bytecode verification and assess the correctness of this instantiation. Finally, we briefly discuss alternative mobile code verification architectures enabled by the proof-linking concept.

How do we decide if it is safe to run a given piece of software on our machine? Software used to arrive in shrink-wrapped packages from known vendors. But increasingly, software of unknown provenance arrives over the internet as applets or agents. Running such software risks serious harm to the hosting machine. Risks include serious damage to the system and loss of private information. Decisions about hosting such software are preferably made with good knowledge of the software product itself, and of the software process used to build it. We use the term Trusted Software Engineering to describe tools and techniques for constructing safe software artifacts in a manner designed to inspire trust in potential hosts. Existing approaches have considered issues such as schedule, cost and efficiency; we argue that the traditionally software engineering issues of configuration management and intellectual property protection are also of vital concern. Existing approaches (e.g., Java) to this problem have used static type checking, run-time environments, formal proofs and/or cryptographic signatures; we propose the use of trusted hardware in combination with a key management infrastructure as an additional, complementary technique for trusted software engineering, which offers some attractive features.

Security flaws are routinely discovered in commercial implementations of mobile code systems such as the Java Virtual Machine (JVM). Typical architectures for such systems exhibit complex interdependencies between the loader, the verifier, and the linker, making them difficult to craft, validate, and maintain. This reveals a software engineering challenge that is common to all mobile code systems in which a static verification phase is introduced before dynamic linking. In such systems, one has to articulate how loading, verification, and linking interact with each other, and how the three processes should be organized to address various security issues.We propose a standard architecture for crafting mobile code verifiers, based on the concept of proof linking. This architecture modularizes the verification process and isolates the dependencies among the loader, verifier, and linker. We also formalize the process of proof linking and establish properties to which correct implementations must conform. As an example, we instantiate our architecture for the problem of Java bytecode verification and assess the correctness of this instantiation. Finally, we briefly discuss alternative mobile code verification architectures enabled by our modularization.