Search

Security policy-makers (influencers) in an organization set security policies that embody intended behaviours for employees (as decision-makers) to follow. Decision-makers then face choices, where this is not simply a binary decision of whether to comply or not, but also how to approach compliance and secure working alongside other workplace pressures, and limited resources for identifying optimal security-related choices. Conflict arises because of information asymmetries present in the relationship, where influencers and decision-makers both consider costs, gains, and losses in ways which are not necessarily aligned. With the need to promote good enough' decisions about security-related behaviours under such constraints, we hypothesize that actions to resolve this misalignment can benefit from constructs from both traditional economics and behavioural economics. Here we demonstrate how current approaches to security behaviour provisioning in organizations mirror rational-agent economics, even where behavioural economics is embodied in the promotion of individual security behaviours. We develop and present a framework to accommodate bounded security decision-making, within an ongoing programme of behaviours which must be provisioned for and supported. Our four stage plan to Capture, Adapt, Realign, and Enable behaviour choices provides guidance for security managers, focusing on a more effective response to the uncertainty associated with security behaviour in organizations.

Conventional security policies for software applications are adequate for managing concerns on the level of access control. But standard abstraction mechanisms of mainstream programming languages are not sufficient to express how information is allowed to flow between resources once access to them has been obtained. In practice we believe that such control - information flow control - is needed to manage the end-to-end security properties of applications. In this paper we present Paragon, a Java-based language with first-class support for static checking of information flow control policies. Paragon policies are specified in a logic-based policy language. By virtue of their explicitly stateful nature, these policies appear to be more expressive and flexible than those used in previous languages with information-flow support. Our contribution is to present the design and implementation of Paragon, which smoothly integrates the policy language with Java's object-oriented setting, and reaps the benefits of the marriage with a fully fledged programming language.

A computerized workflow management system may enforce a security policy, specified in terms of authorized actions and constraints, thereby restricting which users can perform particular steps in a workflow. The existence of a security policy may mean that a workflow is unsatisfiable, in the sense that it is impossible to find a valid plan (an assignment of steps to authorized users such that all constraints are satisfied). Work in the literature focuses on the workflow satisfiability problem, a decision problem that outputs a valid plan if the instance is satisfiable (and a negative result otherwise). In this paper, we introduce the Bi-Objective Workflow Satisfiability Problem (BO-WSP), which enables us to solve optimization problems related to workflows and security policies. In particular, we are able to compute a “least bad” plan when some components of the security policy may be violated. In general, BO-WSP is intractable from both the classical and parameterized complexity point of view (where the parameter is the number of steps). We prove that computing a Pareto front for BO-WSP is fixed-parameter tractable (FPT) if we restrict our attention to user-independent constraints. This result has important practical consequences, since most constraints of practical interest in the literature are user-independent. Our proof is constructive and defines an algorithm, the implementation of which we describe and evaluate. We also present a second algorithm to compute a Pareto front which solves multiples instances of a related problem using mixed integer programming (MIP). We compare the performance of both our algorithms on synthetic instances, and show that the FPT algorithm outperforms the MIP-based one by several orders of magnitude on most instances. Finally, we study the important question of workflow resiliency and prove new results establishing that known decision problems are fixed-parameter tractable when restricted to user-independent constraints. We then propose a new way of modeling the availability of users and demonstrate that many questions related to resiliency in the context of this new model may be reduced to instances of BO-WSP.

Adaptive systems improve their efficiency by modifying their behaviour to respond to changes in their operational environment. Also, security must adapt to these changes and policy enforcement becomes dependent on the dynamic contexts. We study these issues within MLCoDa, (the core of) an adaptive declarative language proposed recently. A main characteristic of MLCoDa is to have two components: a logical one for handling the context and a functional one for computing. We extend this language with security policies that are expressed in logical terms. They are of two different kinds: context and application policies. The first, unknown ap riorito an application, protect the context from unwanted changes. The others protect the applications from malicious actions of the context, can be nested and can be activated and deactivated according to their scope. An execution step can only occur if all the policies in force hold, under the control of an execution monitor. Beneficial to this is a type and effect system, which safely approximates the behaviour of an application, and a further static analysis, based on the computed effect. The last analysis can only be carried on at load time, when the execution context is known, and it enables us to efficiently enforce the security policies on the code execution, by instrumenting applications. The monitor is thus implemented within MLCoDa, and it is only activated on those policies that may be infringed, and switched off otherwise.

This paper presents a formal framework for run-time enforcement mechanisms, or monitors, based on probabilistic input/output automata [3,4], which allows for the modeling of complex and interactive systems. We associate with each trace of a monitored system (i.e., a monitor interposed between a system and an environment) a probability and a real number that represents the cost that the actions appearing on the trace incur on the monitored system. This allows us to calculate the probabilistic (expected) cost of the monitor and the monitored system, which we use to classify monitors, not only in the typical sense, e.g., as sound and transparent [17], but also at a more fine-grained level, e.g., as cost-optimal or cost-efficient. We show how a cost-optimal monitor can be built using information about cost and the probabilistic future behavior of the system and the environment, showing how deeper knowledge of a system can lead to construction of more efficient security mechanisms.

Providing restrictive and secure access to resources is a challenging and socially important problem. Among the many formal security models, Role Based Access Control (RBAC) has become the norm in many of today's organizations for enforcing security. For every model, it is necessary to analyze and prove that the corresponding system is secure. Such analysis helps understand the implications of security policies and helps organizations gain confidence on the control they have on resources while providing access, and devise and maintain policies.In this paper, we consider security analysis for the Temporal RBAC (TRBAC), one of the extensions of RBAC. The TRBAC considered in this paper allows temporal restrictions on roles themselves, user-permission assignments (UA), permission-role assignments (PA), as well as role hierarchies (RH). Towards this end, we first propose a suitable administrative model that governs changes to temporal policies. Then we propose our security analysis strategy, that essentially decomposes the temporal security analysis problem into smaller and more manageable RBAC security analysis sub-problems for which the existing RBAC security analysis tools can be employed. We then evaluate them from a practical perspective by evaluating their performance using simulated data sets.

This paper explores the idea of knowledge-based security policies, which are used to decide whether to answer queries over secret data based on an estimation of the querier's possibly increased knowledge given the results. Limiting knowledge is the goal of existing information release policies that employ mechanisms such as noising, anonymization, and redaction. Knowledge-based policies are more general: they increase flexibility by not fixing the means to restrict information flow. We enforce a knowledge-based policy by explicitly tracking a model of a querier's belief about secret data, represented as a probability distribution, and denying any query that could increase knowledge above a given threshold. We implement query analysis and belief tracking via abstract interpretation, which allows us to trade off precision and performance through the use of abstraction. We have developed an approach to augment standard abstract domains to include probabilities, and thus define distributions. We focus on developing probabilistic polyhedra in particular, to support numeric programs. While probabilistic abstract interpretation has been considered before, our domain is the first whose design supports sound conditioning, which is required to ensure that estimates of a querier's knowledge are accurate. Experiments with our implementation show that several useful queries can be handled efficiently, particularly compared to exact i.e., sound inference involving sampling. We also show that, for our benchmarks, restricting constraints to octagons or intervals, rather than full polyhedra, can dramatically improve performance while incurring little to no loss in precision.

Runtime enforcement is a common mechanism for ensuring that program executions adhere to constraints specified by a security policy. It is based on two simple ideas: the enforcement mechanism should leave good executions without changes transparency and make sure that the bad ones got amended soundness. From the theory side, a number of papers Hamlen et al., Ligatti et al., Talhi et al. provide the precise characterization of good executions that can be captured by a security policy and thus enforced by mechanisms like security automata or edit automata.Unfortunately, transparency and soundness do not distinguish what happens when an execution is actually bad the practical case. They only tell that the outcome of enforcement mechanism should be “good” but not how far the bad execution should be changed. So we cannot formally distinguish between an enforcement mechanism that makes a small change and one that drops the whole execution.In this paper we explore a set of policies called iterative properties that revises the notion of good executions in terms of repeated iterations. We propose an enforcement mechanism that can deal with bad executions and not only the good ones in a more predictable way by eliminating bad iterations.

Managing the configuration of heterogeneous enterprise security mechanisms is a complex task. The effectiveness of a configuration may be constrained by poor understanding and/or management of the overall security policy requirements, which may, in turn, unnecessarily expose the enterprise to known threats. This paper proposes a threat management based approach, whereby knowledge about the effectiveness of mitigating countermeasures is used to guide the autonomic configuration of security mechanisms. This knowledge is modeled in terms of Semantic Threat Graphs, a variation of the traditional Threat/Attack Tree, extended in order to relate semantic information about security configuration with threats, vulnerabilities and countermeasures. An ontology-based approach to representing and reasoning over this knowledge is taken. A case study based on Network Access Controls demonstrates how threats can be analysed and how automated configuration recommendations can be made based on catalogues of countermeasures. These countermeasures are drawn from best-practice standards, including NIST, IETF and PCI-DSS recommendations for firewall configuration.

We introduce TG/MC, a Monte Carlo approach for evaluating the impact of uncertainty about vulnerabilities upon forecasts of security for a real-world system modeled by a protection graph. A TG/MC model defines a vulnerability as a potential change to an otherwise safe initial protection graph that, if exploited, leads to an unauthorized state, a violation of the system's security policy through the application of TG rules. TG/MC captures uncertainties about vulnerabilities as probability distributions and forecasts the probability of a specific security violation. TG/MC extends beyond the rigid yes/no analysis of safety in a TG protection graph to consider uncertainty in questions of security for real-world systems.

Inline reference monitoring is a powerful technique to enforce security policies on untrusted programs. The security-by-contract paradigm proposed by the EU FP6 S3MS project uses policies, monitoring, and monitor inlining to secure third-party applications running on mobile devices. The focus of this paper is on multi-threaded Java bytecode. An important consideration is that inlining should interfere with the client program only when mandated by the security policy. In a multi-threaded setting, however, this requirement turns out to be problematic. Generally, inliners use locks to control access to shared resources such as an embedded monitor state. This will interfere with application program non-determinism due to Java's relaxed memory consistency model, and rule out the transparency property, that all policy-adherent behaviour of an application program is preserved under inlining. In its place we propose a notion of strong conservativity, to formalise the property that the inliner can terminate the client program only when the policy is about to be violated. An example inlining algorithm is given and proved to be strongly conservative. Finally, benchmarks are given for four example applications studied in the S3MS project. ispartof: Journal of Computer Security vol:18 issue:1 pages:37-59 status: published

To reason about information flow, a new model is developed that describes how attacker beliefs change due to the attacker’s observation of the execution of a probabilistic (or deterministic) program. The model enables compositional reasoning about information flow from attacks involving sequences of interactions. The model also supports a new metric for quantitative information flow that measures accuracy of an attacker’s beliefs. Applying this new metric reveals inadequacies of traditional information flow metrics, which are based on reduction of uncertainty. However, the new metric is sufficiently general that it can be instantiated to measure either accuracy or uncertainty. The new metric can also be used to reason about misinformation; deterministic programs are shown to be incapable of producing misinformation. Additionally, programs in which nondeterministic choices are made by insiders, who collude with attackers, can be analyzed.

In the last decade, mobile communication has enjoyed unprecedented growth all over the world. The recent advances in mobile communication technologies including Global Positioning System (GPS) and Radio Frequency Identification (RFID) have propelled the growth of a number of mobile services. Typically, these require maintaining the mobile objects’ location and profile information and efficiently serving access requests on the past, present and future status of the moving objects. This creates inherent security and privacy challenges. One solution to this is to specify security policies to ensure controlled access. However, this significantly degrades system performance. To alleviate this, Atluri and Guo have proposed an unified index structure, S TPR-tree, to organize both the moving objects and authorizations specified over them. A significant limitation of this approach is that it is unable to store past location information of objects and is therefore not capable of supporting security policies based on tracking of mobile users. In this paper, we propose a new unified index structure, called the S PPF -tree, which maintains past, present and future positions of the moving objects along with authorizations by employing partial persistent storage. Besides demonstrating how the S PPF -tree can be constructed and maintained, we provide algorithms to process queries where either the subject or the object or both are mobile. We provide a comprehensive experimental evaluation to establish the scalability and performance of our approach.

The successful design and implementation of secure systems must include security concerns from the beginning. A component that processes data at multiple security levels is critical and must go through additional evaluation to ensure the processing is secure. It is common practice to isolate and separate the processing of data at different levels into different components. In this paper we present policy-based architectural refinement techniques for the design of multi-level secure (MLS) systems. In addition, a policy refinement language is proposed to specify the rules of refinement patterns, and the hierarchy of the refinement patterns is presented. We discuss which security policies must be satisfied through the refinement process, including when separation works and when it does not. The process oriented approach will lead to verified engineering techniques for the design of MLS systems, which should greatly reduce the cost of certification of those systems.

The security of complex infrastructures depends on many technical and organizational issues that need to be properly addressed by a security policy. For purpose of our discussion, we define a security policy as a document that states what is and what is not allowed in a system during normal operation; it consists of a set of rules that could be expressed in formal, semi-formal or very informal language. In many contexts, a system can be considered secure and trustworthy if the policy enforced by its security administrator is trustworthy too; from this standpoint it is possible to evaluate the system security by evaluating its policy. In this paper we present a policy-based methodology to formalize and compare policies, and a Security Metric to evaluate the security level that a system is able to grant. All the steps of the methodology will be illustrated with an operative approach, by directly applying it to a real case study: the semi-automated Cross Certification among Public Key Infrastructures.

Prior works in communication security policy have focused on general-purpose policy languages and evaluation algorithms. However, because the supporting frameworks often defer enforcement, the correctness of a realization of these policies in software is limited by the quality of domain-specific implementations. This paper introduces the Antigone communication security policy enforcement framework. The Antigone framework fills the gap between representations and enforcement by implementing and integrating the diverse security services needed by policy. Policy is enforced by the run-time composition, configuration, and regulation of security services. We present the Antigone architecture, and demonstrate non-trivial applications and policies. A profile of policy enforcement performance is developed, and key architectural enhancements identified. We also consider the advantages and disadvantages of alternative software architectures appropriate for policy enforcement.

Noninterference requires that there is no information flow from sensitive to public data in a given system. However, many systems release sensitive information as part of their intended function and therefore violate noninterference. To control information flow while permitting information release, some systems have a downgrading or declassification mechanism, but this creates the danger that it may cause unintentional information release. This paper shows that a robustness property can be used to characterize programs in which declassification mechanisms cannot be controlled by attackers to release more information than intended. It describes a simple way to provably enforce this robustness property through a type-based compile-time program analysis. The paper also presents a generalization of robustness that supports upgrading (endorsing) data integrity.

Software developers rely on sophisticated programming language protection models and APIs to manifest security policies for Internet applications. These tools do not provide suitable expressiveness for fine-grained, configurable policies. Nor do they ensure the consistency of a given policy implementation across objects in a heterogeneous environment. Programmable access control provides syntactic and semantic constructs in programming languages for systematically embedding security functionality within applications. Secure interoperability is of utmost importance in a distributed heterogeneous environment This paper introduces a methodology for programmable security by language extension, as well as a prototype model and implementation of JPAC, a programmable access control extension to Java. A coor-. dination language is also presented to support secure interoperability within the framework.

Software systems are becoming heterogeneous: instead of a small number of large programs from well-established sources, a user's desktop may now consist of many smaller components that interact in intricate ways. Some components will be downloaded from the network from sources that are only partially trusted. A user would like to know that a number of security properties hold, e.g., that personal data is not leaked to the net, but it is typically infeasible to verify that such components are well-behaved. Instead, they must be executed in a secure environment that provides fine-grain control of the allowable interactions between them, and between components and other system resources.In this paper, we consider the problem of assembling concurrent software systems from untrusted or partially trusted off-the-shelf components, using wrapper programs to encapsulate components and enforce security policies. We introduce a model programming language, the box-π calculus, that supports composition of software components and the enforcement of information flow security policies. Several example wrappers are expressed using the calculus; we explore the delicate security properties they guarantee. We present a novel causal type system that statically captures the allowed flows between wrapped possibly-badly-typed components; we use it to prove that an example ordered pipeline wrapper enforces a causal flow property.

This paper presents an approach enabling a smart card issuer to verify that a new applet securely interacts with already downloaded applets. A security policy has been defined that associates levels to applet attributes and methods and defines authorized flows between levels. We propose a technique based on model checking to verify that actual information flows between applets are authorized. We illustrate our approach on applets involved in an electronic purse running on Java enabled smart cards.

Securing application resources or defining finer-gained access control for system resources using the Java security architecture requires manual changes to source code. This is error-prone and cannot be done if only compiled code is present. We show how behavioural reflection can be used to enforce security policies on compiled code. Other authors have implemented code rewriting toolkits that achieve the same effect but they either require policies to be expressed in terms of low level abstractions or require the use of new high level policy languages. Our approach allows reuseable policies to be implemented as metaobjects in a high level objecl oriented language (Java), and then bound to application objects at loadtime. The binding between metaobjects and objects is implemented through bytecode rewriting under the control of a declarative binding specification. We have implemented this approach using Kava which is a portable reflective Java implementation. Kava allows customisation of a rich range of runtime behaviour. and provides a non-bypassable meta level suitable for implementing security enforcement. We discuss how we have used Kava to show how to secure a third-party application, how we prevent Kava being bypassed, and compare its performance with non-reflective security enforcement.

We present two generic formal security models for operating systems of multiapplicative smart cards. The models formalize the main security aspects of secrecy, integrity, secure communication between applications and secure downloading of new applications. The first model is as abstract as possible, whereas the second extends the first by adding practically relevant issues such as a structured file system. The models satisfy a common security policy consisting of authentication and intransitive noninterference. The policy extends the classical security policy of Bell/LaPadula and Biba models, but avoids the need for trusted processes that are allowed to circumvent the security policy. Instead trusted processes are incorporated directly in the model itself and are subject to the security policy. The security policy has been formally proven to be correct for both models.

Questions of information flow are in many ways more important than questions of access control, because the goal of many security policies is to thwart the unauthorized release of information, not merely the illicit obtaining of access rights to that information. The Take-Grant Protection Model is an excellent theoretical tool for examining such issues because conditions necessary and sufficient for information to flow between two objects, and for rights to objects to be obtained or stolen, are known. In this paper we extend these results by examining the question of information flow from an object the owner of which is unwilling to release that information. Necessary and sufficient conditions for such “theft of information” to occur are derived. To emphasize the usefulness of these results, the security policies of complete isolation, transfer of rights with the cooperation of an owner, and transfer of information (but not rights) with the cooperation of the owner are presented; the last is used to model a subject guarding a resource.

We outline an alternative approach to modeling noninterference-style security policies using a state-based model (as opposed to an event-based or i/o-based model). We believe that this approach provides a richer, more intuitive formalism for security modeling than the event-based approach and provides a link to other current research in specification and verification of concurrent and distributed systems. We describe the state-based approach for deterministic and non-deterministic systems with both transitive and intransitive security policies. >

This paper describes the architecture of a prototype multilevel secure windowing system based on the X Window System. The prototype, known as TX, is designed to meet the class B3 architectural requirements of the Trusted Computer System Evaluation Criteria (TCSEC). The architecture and prototype described here demonstrate that high assurance windowing technology is feasible.The TX architecture is based on the encapsulation of untrusted functionality, such as that contained in an ordinary X server, using a relatively small amount of trusted applications code. The untrusted functionality is then polyinstantiated or replicated once for each active sensitivity level. This leads to a combination of high assurance and complex functionality while reducing the evaluation effort to a tractable level. The architecture of TX is described, and its information flow and visible labeling security policies are discussed. The trade-offs that were made to maintain assurance while achieving other software engineering goals are considered. TX is compared with several other trusted windowing systems.