Vijay K. Garg (UT at Austin) & Neeraj Mittal (UT at Dallas)

A Lattice-Theoretic Approach to Monitoring Distributed Computations

 

Abstract:
Reasoning about distributed programs is hard because the non-deterministic interleaving of concurrent activities in the system dramatically increases the number of possible executions of the program. This non-determinism also makes it difficult to test or verify the correctness of a distributed program before deployment. Continuous monitoring of a running system is a complementary approach for increasing the dependability of a distributed program after deployment.

An execution of a distributed system, also referred to as a distributed computation, can be modeled as a partially ordered set (poset) of events ordered by the happened-before relation. The set of all consistent global states of the computation correspond to the lattice of all down-sets of the poset. The problem of runtime monitoring can be viewed as evaluating a predicate on this lattice. In this tutorial, we will give a survey of algorithms and their limitations for evaluating global predicates in distributed systems. The algorithms exploit lattice-theoretic properties of predicates for efficiency. For example, if the given predicate $B$ is meet-closed and join-closed, then we can compute a subcomputation (called slice) which exactly captures all the consistent global states that satisfy $B$. We will describe centralized and distributed algorithms to compute such a slice. We also show how slices can be used to detect temporal logic predicates in a distributed computation.

 

 

     

David Basin (ETH-Zurich) & Felix Klaedtke (NEC Labs, Europe)

Runtime Monitoring and Enforcement of Security Policies

 

Abstract:
Many kinds of digitally stored data should only be used in restricted ways.  The intended usage may be stipulated by government regulations, corporate privacy policies, preferences of the data owner, etc.  Such policies cover not only who may access which data, but also how the data may or must not be used after access.  An example of such a usage restriction is that "collected data must be deleted after 30 days and not accessed or forwarded to third parties."

In this tutorial, we present different methods and results for monitoring and enforcing such policies along with their underlying foundations. We show how temporal logical can be used not only to formalize such regulations, but to synthesize efficient monitors from specifications. These monitors can then be used either online or offline to check whether the behavior of system agents, i.e., users and processes, is policy compliant.   A particular focus here will be on the use of metric first-order temporal logic as a policy language, its algorithmic realization in the MonPoly tool, and our experience using this tool.

We will also consider the question of when and how can such policies be enforced by execution monitoring.  We will review Schneider's seminal work on policy enforcement as well as its limitations.  We will show how to overcome the limitations of Schneider’s setting by distinguishing between system actions that are controllable by an enforcement mechanism and those actions that are only observable, that is, the enforcement mechanism sees them but cannot prevent their execution. For this refined setting, we give necessary and sufficient conditions on when a security policy is enforceable.   Furthermore for different specification languages, we investigate the problem of deciding whether a given policy is enforceable and synthesizing an enforcement mechanism from an enforceable policy.