Which security policies are enforceable by runtime monitors? A survey

Runtime monitoring is a widely used approach to ensure code safety. Several implementations of formal monitors have been proposed in the literature, and these differ with respect to the set of security policies that they are capable of enforcing. In this survey, we examine the evolution of knowledge regarding the issue of precisely which security policies monitors are capable of enforcing. We identify three stages in this evolution. In the first stage, we discuss initial limits on the set of enforceable properties and various ways in which this set can be extended. The second stage presents studies that identify constraints to the enforcement power of monitors. In the third stage, we present a final series of studies that suggest various alternative definitions of enforcement, which specify both the set of properties the monitors can enforce as well as the manner by which this enforcement is provided.     

Edit automata: enforcement mechanisms for run-time security policies

We analyze the space of security policies that can be enforced by monitoring and modifying programs at run time. Our program monitors, called edit automata, are abstract machines that examine the sequence of application program actions and transform the sequence when it deviates from a specified policy. Edit automata have a rich set of transformational powers: they may terminate an application, thereby truncating the program action stream; they may suppress undesired or dangerous actions without necessarily terminating the program; and they may also insert additional actions into the event stream.After providing a formal definition of edit automata, we develop a rigorous framework for reasoning about them and their cousins: truncation automata (which can only terminate applications), suppression automata (which can terminate applications and suppress individual actions), and insertion automata (which can terminate and insert). We give a set-theoretic characterization of the policies each sort of automaton can enforce, and we provide examples of policies that can be enforced by one sort of automaton but not another.     

The Clara framework for hybrid typestate analysis

A typestate property describes which operations are available on an object or a group of inter-related objects, depending on this object??s or group??s internal state, the typestate. Researchers in the field of static analysis have devised static program analyses to prove the absence of typestate-property violations on all possible executions of a given program under test. Researchers in runtime verification, on the other hand, have developed powerful monitoring approaches that guarantee to capture property violations on actual executions. Although static analysis can greatly benefit runtime monitoring, up until now, most static analyses are incompatible with most monitoring tools. We present Clara, a novel framework that makes these approaches compatible. With Clara, researchers in static analysis can easily implement powerful typestate analyses. Runtime-verification researchers, on the other hand, can use Clara to specialize AspectJ-based runtime monitors to a particular target program. To make aspects compatible to Clara, the monitoring tool annotates them with so-called dependency state machines. Clara uses the static analyses to automatically convert an annotated monitoring aspect into a residual runtime monitor that is triggered by fewer program locations. If the static analysis succeeds on all locations, this proves that the program fulfills the stated typestate properties, making runtime monitoring entirely obsolete. If not, the residual runtime monitor is at least optimized. We instantiated Clara with three static typestate analyses and applied these analyses to monitoring aspects generated from tracematches. In two-thirds of the cases in our experiments, the static analysis succeeds on all locations, proving that the program fulfills the stated properties, and completely obviating the need for runtime monitoring. In the remaining cases, the runtime monitor is often significantly optimized.     

Replay and testing for concurrent programs

Attention is given to the problems that arise during the testing and debugging cycle of concurrent programs because of their nondeterministic execution behavior, whereby multiple executions of a concurrent program with the same input may exercise different synchronization sequences and even produce different results. These problems are solved by using deterministic execution debugging and testing. The purpose of deterministic execution debugging to to replay executions of a concurrent program so that debugging information can be collected. Examples of semaphores and monitors are used to illustrate the approach and the process of designing replay tubes is described. The use of regression testing to see if earlier debugging and testing introduced new errors, is examined     

Formalizing Java-MaC

The Java-MaC framework is a run-time verification system for Java programs that can be used to dynamically test and enforce safety policies. This paper presents a formal model of the Java-MaC safety properties in terms of an operational semantics for Middleweight Java, a realistic subset of full Java. This model is intended to be used as a framework for studying the correctness of Java-MaC program instrumentation, optimizations, and future experimentation with run-time monitor expressiveness. As a preliminary demonstration of this model's applicability for these tasks, the paper sketches a correctness result for a simple program instrumentation scheme.     

Specification and static enforcement of scheduler-independent noninterference in a middleweight Java

We introduce a new timing covert channel that arises from the interplay between multithreading and object orientation. This example motivates us to explore the root of the problem and to devise a mechanism for preventing such errors. In doing so, we first add multithreading constructs to Middleweight Java, a subset of the Java programming language with a fairly rich set of features. A noninterference property is then presented which basically demands program executions be equivalent in the view of whom observing final public values in environments using the so-called high-independent schedulers. It is scheduler-independent in the sense that no matter which scheduler is employed, the executions of the program satisfying the property do not lead to illegal information flows in the form of explicit, implicit, or timing channels. We also give a provably sound type-based static mechanism to enforce the proposed property.     

Provably correct runtime monitoring

Runtime monitoring is an established technique to enforce a wide range of program safety and security properties. We present a formalization of monitoring and monitor inlining, for the Java Virtual Machine. Monitors are security automata given in a special-purpose monitor specification language, ConSpec. The automata operate on finite or infinite strings of calls to a fixed API, allowing local dependencies on parameter values and heap content. We use a two-level class file annotation scheme to characterize two key properties: (i) that the program is correct with respect to the monitor as a constraint on allowed program behavior, and (ii) that the program has a copy of the given monitor embedded into it. As the main application of these results we sketch a simple inlining algorithm and show how the two-level annotations can be completed to produce a fully annotated program which is valid in the standard sense of Floyd/Hoare logic. This establishes the mediation property that inlined programs are guaranteed to adhere to the intended policy. Furthermore, validity can be checked efficiently using a weakest precondition based annotation checker, thus preparing the ground for on-device checking of policy adherence in a proof-carrying code setting.     

Runtime enforcement monitors: composition,synthesis, and enforcement abilities

Runtime enforcement is a powerful technique to ensure that a program will respect a given set of properties. We extend previous work on this topic in several directions. Firstly, we propose a generic notion of enforcement monitors based on a memory device and finite sets of control states and enforcement operations. Moreover, we specify their enforcement abilities w.r.t. the general Safety-Progress classification of properties. Furthermore, we propose a systematic technique to produce a monitor from the automaton recognizing a given safety, guarantee, obligation or response property. Finally, we show that this notion of enforcement monitors is more amenable to implementation and encompasses previous runtime enforcement mechanisms.     

Infrastructural Support for Enforcing and Managing Distributed Application-Level Policies

State-of-the-art security mechanisms are often enforced in isolation from each other, which limits the kinds of policies that can be enforced in distributed and heterogeneous settings. More specifically, it is hard to enforce application-level policies that affect, or use information from multiple distributed components. This paper proposes the concept of a Security Service Bus (SSB), which is a dedicated communication channel between the applications and the different security mechanisms. The SSB treats the security mechanisms as reusable, stand-alone security services that can be bound to the applications and it allows the enforcement of advanced policies by providing uniform access to application-level information. This leads to a security infrastructure that is more flexible and more manageable and that can enforce more expressive policies.     

Do you really mean what you actually enforced?

In their works on the theoretical side of Polymer, Ligatti and his co-authors have identified a new class of enforcement mechanisms based on the notion of edit automata that can transform sequences and enforce more than simple safety properties. We show that there is a gap between the edit automata that one can possibly write (e.g., by Ligatti et?al in their IJIS running example) and the edit automata that are actually constructed according the theorems from Ligatti??s IJIS paper or from Talhi et?al. ??Ligatti??s automata?? are just a particular kind of edit automata. Thus, we re-open a question which seemed to have received a definitive answer: you have written your security enforcement mechanism (aka your edit automata); does it really enforce the security policy you wanted?     

Java系统安全性的实现与分析

首先归纳了通过ＷＷＷ从Ｉｎｔｅｒｎｅｔ上下载一段不可信任的可执行代码在本地机器上运行时可能造成的各种危害，接着重点介绍了Ｊａｖａ系统防止这些危害的机制及实现方法，随后分析陈春效果，最后讨论了进一步的改进方法。     

Liveness-enforcing supervision of bounded ordinary Petri nets usingpartial order methods

This paper combines and refines recent results into a systematic way to verify and enforce the liveness of bounded ordinary Petri nets. The approach we propose is based on a partial-order method called network unfolding. Network unfolding maps the original Petri net to an acyclic occurrence net. A finite prefix of the occurrence net is defined to give a compact representation of the original net reachability graph while preserving the causality between net transitions. A set of transition invariants denoted as base configurations is identified in the finite prefix. These base configurations capture all of the fundamental executions of the net system, thereby providing a modular way to verify and synthesize supervisory net systems. This paper proves necessary and sufficient conditions that characterize the original net liveness and the existence of maximally permissive supervisory policies that enforce liveness     

Supporting reconfigurable security policies for mobile programs

Programming models that support code migration have gained prominence, mainly due to a widespread shift from stand-alone to distributed applications. Although appealing in terms of system design and extensibility, mobile programs are a security risk and require strong access control. Further, the mobile code environment is fluid, i.e. the programs and resources located on a host may change rapidly, necessitating an extensible security model. In this paper, we present the design and implementation of a security infrastructure. The model is built around an event/response mechanism, in which a response is executed when a security-related event occurs. We support a fine-grained, conditional access control language, and enforce policies by instrumenting the bytecode of protected classes. This method enhances efficiency and promotes separation of concerns between security policy and program specification. This infrastructure also allows security policies to change at runtime, adapting to varying system state, intrusion, and other events.     

An approach for modeling and analysis of security system architectures

Security system architecture governs the composition of components in security systems and interactions between them. It plays a central role in the design of software security systems that ensure secure access to distributed resources in networked environment. In particular, the composition of the systems must consistently assure security policies that it is supposed to enforce. However, there is currently no rigorous and systematic way to predict and assure such critical properties in security system design. A systematic approach is introduced to address the problem. We present a methodology for modeling security system architecture and for verifying whether required security constraints are assured by the composition of the components. We introduce the concept of security constraint patterns, which formally specify the generic form of security policies that all implementations of the system architecture must enforce. The analysis of the architecture is driven by the propagation of the global security constraints onto the components in an incremental process. We show that our methodology is both flexible and scalable. It is argued that such a methodology not only ensures the integrity of critical early design decisions, but also provides a framework to guide correct implementations of the design. We demonstrate the methodology through a case study in which we model and analyze the architecture of the Resource Access Decision (RAD) Facility, an OMG standard for application-level authorization service.     

Grid Scheduling with Makespan and Energy-Based Goals

The need for better energy efficiency in grid computing is significant given the massive amount of energy dissipated by large grids. We approximate the optimal allocation of compute nodes to a job stream, with each job consisting of multiple tasks, and while considering both the computing requirements and a desired balance of shorter makespans and lower energy consumption. The approach is widely applicable to many grid scenarios and does not require the scheduler to have administrative rights to change the workers’ DVFS or hibernation state. A discrete particle swarm optimisation (PSO) determines the worker assignments based on estimations of the tasks’ service times and energy consumption using an online learning process, and taking into account pending task executions from prior jobs. The performance of the proposed system is then evaluated through extensive Monte Carlo simulations using traces of real multi-threaded program executions on representative computer hardware. The results demonstrate the latent energy savings that are possible in grid computing through an energy-aware task scheduling.     

RBAC模型中角色的继承与互斥问题的研究

RBAC (Role-Based Access Control)maps naturally to an organization's structure and facilitates safety administration by separating logically users and permissions via roles as well as constructing role hierarchies, and therefore RBAC offers a powerful means of specifying access control decisions and is attracting increasing attention. In role hierarchies of RBAC,superroles inherit all properties and permissions of subroles. This paper classifies role inheritance into two types : generalization inheritance and supervision inheritance . Furthermore, it outlines two problems in relation to role inheritance :one is how to maintain data integrity,another is how to reduce the effect of absent roles on the normal running of the system. At last ,this paper discusses solutions to them 。RBAC is attracting increasing attention as a security mechanism .Separation of duty is an important safety requirement which is implemented by means of mutual exclusion of roles in RBAC. This paper presents a basic RBAC model,then explores some properties of mutual exclusion of roles,which helps enforcing security policies efficiently. At last ,this paper describes how mutual exclusion of roles affects role hierarchies.     

A Negotiation Scheme for Access Rights Establishment in Autonomic Communication

Autonomic computing and communication has become a new paradigm for dynamic service integration and resource sharing in today's ambient networks. Devices and systems need to dynamically collaborate and federate with little known or even unknown parties in order to perform everyday tasks. Those devices and systems act as independent nodes that autonomously manage and enforce their own security policies. Thus in autonomic pervasive communications clients may not know a priori what access rights they need in order to execute a service nor service providers know a priori what credentials and privacy requirements clients have so that they can take appropriate access decisions. To solve this problem we propose a negotiation scheme that protects security and privacy interests with respect to information disclosure while still providing effective access control to services. The scheme proposes a negotiation protocol that allows entities in a network to mutually establish sufficient access rights needed to grant a service.

---

     

A cubic-wise balance approach for privacy preservation in data cubes

A data warehouse stores current and historical records consolidated from multiple transactional systems. Securing data warehouses is of ever-increasing interest, especially considering areas where data are sold in pieces to third parties for data mining practices. In this case, existing data warehouse security techniques, such as data access control, may not be easy to enforce and can be ineffective. Instead, this paper proposes a data perturbation based approach, called the cubic-wise balance method, to provide privacy preserving range queries on data cubes in a data warehouse. This approach is motivated by the following observation: analysts are usually interested in summary data rather than individual data values. Indeed, our approach can provide a closely estimated summary data for range queries without providing access to actual individual data values. As demonstrated by our experimental results on APB benchmark data set from the OLAP council, the cubic-wise balance method can achieve both better privacy preservation and better range query accuracy than random data perturbation alternatives.     

Predicting program execution times by analyzing static and dynamic program paths

This paper describes a method to predict guaranteed and tight deterministic execution time bounds of a sequential program. The basic prediction technique is a static analysis based on simple timing schema for source-level language constructs, which gives accurate predictions in many cases. Using powerful user-provided information, dynamic path analysis refines looser predictions by eliminating infeasible paths and decomposing the possible execution behaviors in a pathwise manner. Overall prediction cost is scalable with respect to desired precision, controlling the amount of information provided. We introduce a formal path model for dynamic path analysis, where user execution information is represented by a set of program paths. With a well-defined practical high-level interface language, user information can be used in an easy and efficient way. We also introduce a method to verify given user information with known program verification techniques. Initial experiments with a timing tool show that safe and tight predictions are possible for a wide range of programs. The tool can also provide predictions for interesting subsets of program executions.This research was supported in part by the Office of Naval Research under grant number N00014-89-J-1040.     

Developing secure data warehouses with a UML extension

Data Warehouses (DWs), Multidimensional (MD) Databases, and On-Line Analytical Processing Applications are used as a very powerful mechanism for discovering crucial business information. Considering the extreme importance of the information managed by these kinds of applications, it is essential to specify security measures from the early stages of the DW design in the MD modeling process, and enforce them. In the past years, some proposals for representing main MD modeling properties at the conceptual level have been stated. Nevertheless, none of these proposals considers security issues as an important element in its model, so they do not allow us to specify confidentiality constraints to be enforced by the applications that will use these MD models. In this paper, we will discuss the specific confidentiality problems regarding DWs as well as present an extension of the Unified Modeling Language for specifying security constraints in the conceptual MD modeling, thereby allowing us to design secure DWs. One key advantage of our approach is that we accomplish the conceptual modeling of secure DWs independently of the target platform where the DW has to be implemented, allowing the implementation of the corresponding DWs on any secure commercial database management system. Finally, we will present a case study to show how a conceptual model designed with our approach can be directly implemented on top of Oracle 10g.