Explainability and transparency of computations, as well as compliance with data-privacy requirements, presuppose an understanding of whether some input plays a non-trivial role in computing an output. However, difficulty in distinguishing between correlation and actual usage in computation, along with possible correlations between inputs, makes determination of such accountability challenging. A flow definition is presented that can make this distinction. The definition enables the construction of accountability evidence to establish how an input is computed based on an output, in terms of the intermediate variables used. Intermediate variables can also serve as mediation points that fully block information flow from an input to an output. A connection between accountability and mediation is established by showing the role of mediation points for constructing accountability evidence.

Hyperproperties generalize ordinary properties by expressing relations among multiple executions of a system. Self-composition has been used to reduce verifying that a system satisfies certain classes of Hyperproperties to verifying that a derived system satisfies an ordinary property. By describing systems and their properties in the temporal logic TLA, we use self-composition to handle a larger class of Hyperproperties that includes those we have seen that express security conditions. TLA tools are used to verify that high-level designs of industrial systems satisfy properties. Now, they can also verify that those systems satisfy these Hyperproperties. No prior knowledge of Hyperproperties or TLA is assumed.

Restrictions that a reactive information flow (RIF) label imposes on a value are determined by the sequence of operations used to derive that value. This allows declassification, endorsement, and other forms of reclassification to be supported in a uniform way. Piecewise noninterference (PWNI) is introduced as a fitting security policy, because noninterference is not suitable. A type system is given for static enforcement of PWNI in programs that associate checkable classes of RIF labels with variables. Two checkable classes of RIF labels are described: RIF automata are general-purpose and based on finite-state automata; κ-labels concern confidentiality in programs that use cryptographic operations.

Flow-sensitive labels used by dynamic enforcement mechanisms might themselves encode sensitive information, which can leak. Metalabels, employed to represent the sensitivity of labels, exhibit the same problem. This paper derives a new family of enforcers-k-Enf, for 2 ≤ k ≤ ∞-that uses label chains, where each label defines the sensitivity of its predecessor. These enforcers satisfy Block-safe Noninterference (BNI), which proscribes leaks from observing variables, label chains, and blocked executions. Theorems in this paper characterize where longer label chains can improve the permissiveness of dynamic enforcement mechanisms that satisfy BNI. These theorems depend on semantic attributes-k-precise, k-varying, and k-dependent-of such mechanisms, as well as on initialization, threat model, and lattice size.

Three integrity measures are introduced: contamination, channel suppression and program suppression. Contamination is a measure of how much untrusted information reaches trusted outputs; it is the dual of leakage, which is a measure of information-flow confidentiality. Channel suppression is a measure of how much information about inputs to a noisy channel is missing from the channel outputs. And program suppression is a measure of how much information about the correct output of a program is lost because of attacker influence and implementation errors. Program and channel suppression do not have interesting confidentiality duals. As a case study, a quantitative relationship between integrity, confidentiality and database privacy is examined.

Paxos, Viewstamped Replication, and Zab are replication protocols for high-availability in asynchronous environments with crash failures. Claims have been made about their similarities and differences. But how does one determine whether two protocols are the same, and if not, how significant are the differences? We address these questions using refinement mappings. Protocols are expressed as succinct specifications that are progressively refined to executable implementations. Doing so enables a principled understanding of the correctness of design decisions for implementing the protocols. Additionally, differences that have a significant impact on performance are surfaced by this exercise.

Theomni-kernelarchitecture is designed around pervasive monitoring and scheduling. Motivated by new requirements in virtualized environments, this architecture ensures that all resource consumption is measured, that resource consumption resulting from a scheduling decision is attributable to an activity, and that scheduling decisions are fine-grained.Vortex, implemented for multi-core x86-64 platforms, instantiates the omni-kernel architecture, providing a wide range of operating system functionality and abstractions. With Vortex, we experimentally demonstrated the efficacy of the omni-kernel architecture to provide accurate scheduler control over resource allocation despite competing workloads. Experiments involving Apache, MySQL, and Hadoop quantify the cost of pervasive monitoring and scheduling in Vortex to be below$6$percent ofcpuconsumption.

No abstract available.

This paper presents the design and implementation of NetQuery, a knowledge plane for federated networks such as the Internet. In such networks, not all administrative domains will generate information that an application can trust and many administrative domains may have restrictive policies on disclosing network information. Thus, both the trustworthiness and accessibility of network information pose obstacles to effective reasoning. NetQuery employs trustworthy computing techniques to facilitate reasoning about the trustworthiness of information contained in the knowledge plane while preserving confidentiality guarantees for operator data. By characterizing information disclosure between operators, NetQuery enables remote verification of advertised claims and contractual stipulations; this enables new applications because network guarantees can span administrative boundaries. We have implemented NetQuery, built several NetQuery-enabled devices, and deployed applications for cloud datacenters, enterprise networks, and the Internet. Simulations, testbed experiments, and a deployment on a departmental network indicate NetQuery can support hundreds of thousands of operations per second and can thus scale to large ISPs.

This paper describes the design and implementation of a new operating system authorization architecture to support trustworthy computing. Called logical attestation, this architecture provides a sound framework for reasoning about run time behavior of applications. Logical attestation is based on attributable, unforgeable statements about program properties, expressed in a logic. These statements are suitable for mechanical processing, proof construction, and verification; they can serve as credentials, support authorization based on expressive authorization policies, and enable remote principals to trust software components without restricting the local user's choice of binary implementations.

Nexus Authorization Logic (NAL) provides a principled basis for specifying and reasoning about credentials and authorization policies. It extends prior access control logics that are based on “says” and “speaks for” operators. NAL enables authorization of access requests to depend on (i) the source or pedigree of the requester, (ii) the outcome of any mechanized analysis of the requester, or (iii) the use of trusted software to encapsulate or modify the requester. To illustrate the convenience and expressive power of this approach to authorization, a suite of document-viewer applications was implemented to run on the Nexus operating system. One of the viewers enforces policies that concern the integrity of excerpts that a document contains; another viewer enforces confidentiality policies specified by labels tagging blocks of text.

Two kinds of integrity measures-contamination and suppression-are introduced. Contamination measures how much untrusted information reaches trusted outputs; it is the dual of information-flow confidentiality. Suppression measures how much information is lost from outputs; it does not have a confidentiality dual. Two forms of suppression are considered: programs and channels. Program suppression measures how much information about the correct output of a program is lost because of attacker influence and implementation errors. Channel suppression measures how much information about inputs to a noisy channel is missing from channel outputs. The relationship between quantitative integrity, confidentiality, and database privacy is examined.

Cyber-security today is focused largely on defending against known attacks. We learn about the latest attack and find a hack to defend against it. So our defenses improve only after they have been successfully penetrated. This is a recipe to ensure some attackers succeed---not a recipe for achieving system trustworthiness.

Trace properties, which have long been used for reasoning about systems, are sets of execution traces. Hyperproperties, introduced here, are sets of trace properties. Hyperproperties can express security policies, such as secure information flow and service level agreements, that trace properties c annot. Safety and liveness are generalized to hyperproperties, and every hyperproperty is shown to be the intersection of a safety hyperproperty and a liveness hyperproperty. A verification technique for safety hyperproperties is given and is shown to generalize prior techniques for verifying secure information flow. Refinement is shown to be applicable with safety hyperproperties. A topological characterization of hyperproperties is given.

A set of replicas is diverse to the extent that they implement the same functionality but differ in their implementation details. Diverse replicas are less likely to succumb to the same attacks, when attacks depend on memory layout and/or other implementation details. Recent work advocates using mechanical means, such as program rewriting, to create such diversity. A correspondence between the specific transformations being employed and the attacks they defend against is often provided, but little has been said about the overall effectiveness of diversity per se in defending against attacks. With this broader goal in mind, this paper gives a precise characterization of attacks, applicable to viewing diversity as a defense, and also shows how mechanically-generated diversity compares to a well-understood defense: type checking.

Proactive obfuscation is a new method for creating server replicas that are likely to have fewer shared vulnerabilities. It uses semantics-preserving code transformations to generate diverse executables, periodically restarting servers with these fresh versions. The periodic restarts help bound the number of compromised replicas that a service ever concurrently runs, and therefore proactive obfuscation makes an adversary's job harder. Proactive obfuscation was used in implementing two prototypes: a distributed firewall based on state-machine replication and a distributed storage service based on quorum systems. Costs intrinsic to supporting proactive obfuscation in replicated systems were evaluated by measuring the performance of these prototypes. The results show that employing proactive obfuscation adds little to the cost of replica-management protocols.

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 in

Properties, which have long been used for reasoning about systems, are sets of traces. Hyperproperties, introduced here, are sets of properties. Hyperproperties can express security policies, such as secure information flow, that properties cannot. Safety and liveness are generalized to hyperproperties, and every hyperproperty is shown to be the intersection of a safety hyperproperty and a liveness hyperproperty. A verification technique for safety hyperproperties is given and is shown to generalize prior techniques for verifying secure information flow. Refinement is shown to be valid for safety hyperproperties. A topological characterization of hyperproperties is given.

A set of replicas is diverse to the extent that all implement the same functionality but differ in their implementation details. Diverse replicas are less prone to having vulnerabilities in common, because attacks typically depend on memory layout and/or instruction-sequence specifics. Recent work advocates using mechanical means, such as program rewriting, to create such diversity. A correspondence between the specific transformations being employed and the attacks they defend against is often provided, but little has been said about the overall effectiveness of diversity per se in defending against attacks. With this broader goal in mind, we here give a precise characterization of attacks, applicable to viewing diversity as a defense, and also show how mechanically-generated diversity compares to a well-understood defense: strong typing

A precise characterization of those security policies enforceable by program rewriting is given. This also exposes and rectifies problems in prior work, yielding a better characterization of those security policies enforceable by execution monitors as well as a taxonomy of enforceable security policies. Some but not all classes can be identified with known classes from computational complexity theory.

Information leakage traditionally has been defined to occur when uncertainty about secret data is reduced. This uncertainty-based approach is inadequate for measuring information flow when an attacker is making assumptions about secret inputs and these assumptions might be incorrect; such attacker beliefs are an unavoidable aspect of any satisfactory definition of leakage. To reason about information flow based on beliefs, a 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 leads to a new metric for quantitative information flow that measures accuracy rather than uncertainty of beliefs.

A protocol is given to take an ElGamal ciphertext encrypted under the key of one distributed service and produce the corresponding ciphertext encrypted under the key of another distributed service, but without the plaintext ever becoming available. Each distributed service comprises a set of servers and employs threshold cryptography to maintain its service private key. Unlike prior work, the protocol requires no assumptions about execution speeds or message delivery delays. The protocol also imposes fewer constraints on where and when various steps are performed, which can bring improvements in end-to-end performance for some applications (e.g., a trusted publish/subscribe infrastructure.) Two new building blocks employed — a distributed blinding protocol and verifiable dual encryption proofs — could have uses beyond re-encryption protocols.

Tamper-proof coprocessors for secure computing are poised to become a standard hardware feature on future computers. Such hardware provides the primitives necessary to support trustworthy computing applications, that is, applications that can provide strong guarantees about their run time behavior.

APSS, a proactive secret sharing (PSS) protocol for asynchronous systems, is explained and proved correct. The protocol enables a set of secret shares to be periodically refreshed with a new, independent set, thereby thwarting mobile-adversary attacks. Protocols for asynchronous systems are inherently less vulnerable to denial-of-service attacks, which slow processor execution or delay message delivery. So APSS tolerates certain attacks that PSS protocols for synchronous systems cannot.

CODEX (COrnell Data Exchange) stores secrets for subsequent access by authorized clients. It also is a vehicle for exploring the generality of a relatively new approach to building distributed services that are both fault-tolerant and attack-tolerant. Elements of that approach include: embracing the asynchronous (rather than synchronous) model of computation, use of Byzantine quorum systems for storing state, and employing proactive secret sharing with threshold cryptography for implementing confidentiality and authentication of service responses. Besides explaining the CODEX protocols, experiments to measure their performance are discussed.

Abstract For seven years, the TACOMA project has investigated the design and implementation of software support for mobile agents. A series of prototypes has been developed, with experiences in distributed applications driving the effort. This paper describes the evolution of these TACOMA prototypes, what primitives each supports, and how the primitives are used in building distributed applications. Copyright © 2002 John Wiley & Sons, Ltd.

COCA is a fault-tolerant and secure online certification authority that has been built and deployed both in a local area network and in the Internet. Extremely weak assumptions characterize environments in which COCA's protocols execute correctly: no assumption is made about execution speed and message delivery delays; channels are expected to exhibit only intermittent reliability; and with 3t+ 1 COCA servers up totmay be faulty or compromised. COCA is the first system to integrate a Byzantine quorum system (used to achieve availability) with proactive recovery (used to defend against mobile adversaries which attack, compromise, and control one replica for a limited period of time before moving on to another). In addition to tackling problems associated with combining fault-tolerance and security, new proactive recovery protocols had to be developed. Experimental results give a quantitative evaluation for the cost and effectiveness of the protocols.

Two implementations are given for Java's stack inspection access-control policy. Each implementation is obtained by generating an inlined reference monitor (IRM) for a different formulation of the policy. Performance of the implementations is evaluated, and one is found to be competitive with Java's less flexible, JVM-resident implementation. The exercise illustrates the power of the IRM approach for enforcing security policies.

Although open-source software development has virtues, there is reason to believe that the approach would not have a significant effect on the security of today's systems. The lion's share of vulnerabilities caused by software bugs is easily dealt with by means other than source code inspections. The tenets of open-source development are inhospitable to business models whose success depends on promoting secure systems.

A precise characterization is given for the class of security policies enforceable with mechanisms that work by monitoring system execution, and automata are introduced for specifying exactly that class of security policies. Techniques to enforce security policies specified by such automata are also discussed.

One use of mobile agents is support for itinerant computation (D. Chess et al., 1995). An itinerant computation is a program that moves from host to host in a network. Which hosts the program visits is determined by the program. The program can have a pre-defined itinerary or can dynamically compute the next host to visit as it visits each successive host; it can visit the same host repeatedly or it can even create multiple concurrent copies of itself on a single host. Itinerant computations are susceptible to processor failures, communications failures, and crashes due to program bugs. NAP is a protocol for supporting fault tolerance in itinerant computations. It employs a form of failure detection and recovery, and it generalizes the primary backup approach to a new computational model. The guarantees offered by NAP as well as an implementation for NAP in TACOMA are discussed.

SASI enforces security policies by modifying object code for a target system before that system is executed. The approach has been prototyped for two rather dieren t machine architectures: Intel x86 and Java JVML. Details of these prototypes and some generalizations about the SASI approach are discussed.

Sound and complete modal propositional logic C is presented, in which □P has the interpretation ‘P is true in all states’. This interpretation is already known as the Camapian extension of S5. The new axiomatization for C provides two insights. First, introducing an inference rule textual substitution allows integration of the propositional and modal parts of the logic in a way that gives a more practical system for writing formal proofs. Second, the two following approaches to axiomatizing a logic are shown to be not equivalent: (i) give axiom schemes that denote an infinite number of axioms and (ii) write a finite number of axioms in terms of propositional variables and introduce a substitution inference rule.

Protocols to implement a fault-tolerant computing system are described. These protocols augment the hypervisor of a virtual-machine manager and coordinate a primary virtual machine with its backup. No modifications to the hardware, operating system, or application programs are required. A prototype system was constructed for HP's PA-RISC instruction-set architecture. Even though the prototype was not carefully tuned, it ran programs about a factor of 2 slower than a bare machine would.

The TACOMA project is concerned with implementing operating system support for agents, processes that migrate through a network. Two TACOMA prototypes have been completed; this paper outlines our experiences in building and using them. A mechanism for exchanging electronic cash was explored, as well as agent-based schemes for scheduling and fault-tolerance.

No abstract available.

Protocols to implement a fault-tolerant computing system are described.These protocols augment the hypervisor of a virtttalmachine manager and coordinate a primary virtual machine with its backup.The result is a fault-tolerant computing system.No modification to hardware, operating system, or application programs is required.A prototype system was constructed for HP's PA-RISC instruction-set architecture.The prototype was able to run programs about a factor of 2 slower than a bare machine would.

We formalize equational propositional logic, prove that it is sound and complete, and compare the equational-proof style with the more traditional Hubert style.

We give an operational model of causally-ordered message-passing primitives. Based on this model, we formulate a Hoare-style proof system for causally-ordered delivery. To illustrate the use of this proof system and to demonstrate the feasibility of applying invariant-based verification techniques to algorithms that depend on causally-ordered delivery, we verify an asynchronous variant of the distributed termination detection algorithm of Dijkstra, Feijen, and van Gasteren.

We consider incomplete trace-based network proof systems for safety properties, identifying extensions that are necessary and sufficient to achieve relative completeness. We investigate the expressiveness required of any trace logic to encode these extensions.

An approach to proving temporal properties of concurrent programs that does not use temporal logic as an inference system is presented. The approach is based on using Buchi automata to specify properties. To show that a program satisfies a given property, proof obligations are derived from the Buchi automata specifying that property. These obligations are discharged by devising suitable invariant assertions and variant functions for the program. The approach is shown to be sound and relatively complete. A mutual exclusion protocol illustrates its application.

Abstract. Most trace-based proof systems for networks of processes are known to be incomplete. Extensions to achieve completeness are generally complicated and cumbersome. In this paper, a simple trace logic is defined and two examples are presented to show its inherent incompleteness. Surprisingly, both examples consist of only one process, indicating that network composition is not a cause of incompleteness. Axioms necessary and sufficient for the relative completeness of a trace logic are then presented.

Abstract: Similarity is introduced as a model-independent characterization of symmetry. It can be used to decide when a concurrent system has a solution to the selection problem. It can also be used to compare different models of parallel computation, including differences in scheduling policy and instruction set, and the consequences of using randomization. 1.

An Inexact Agreement protocol alows processors that each have a value approximating $\hat{\nu}$ to compute new values that are closer to each other and close to $\hat{\nu}$. Two fault-tolerant protocols for Inexact Agreement are described. As long as fewer than 1/3 of the processors are faulty, the protocols give the required convergence; they also permit iteration and thus convergence to any desired precision. When between 1/3 and 2/3 of the processors are faulty, the protocols may not converge. However, then processors either detect that too many faults have occurred or the new values computed by processors remain close to each other and to $\hat{\nu}$. In this case, the divergence is bounded. Use of the protocols for clock synchronization in a distributed system is explained.

A constraint is a relation among program variables that is maintained throughout execution. Type declarations and a very general form of aliasing can be expressed as constraints. A proof system based upon the interpretation of Hoare triples as temporal logic formulas is given for reasoning about programs with constraints. The proof system is shown to be sound and relatively complete, and example program proofs are given.

A fail-stop processor halts instead of performing an erroneous state transformation that might be visible to other processors, can detect whether another fail-stop processor has halted (due to a failure), and has a predefined portion of its storage that will remain unaffected by failures and accessible to any other fail-stop processor.Fail-stop processors can simplify the construction of fault-tolerant computing systems.In this paper, the problem of approximating fail-stop processors is discussed.Use of fail-stop processors is compared with the state machine approach, another general paradigm for constructing fault-tolerant systems.

Interactive systems, such as editors and program development environments, should explicitly support facilities that permit a user to reverse the effects of past actions and to restore an object to a prior state.A model for interactive systems that allows such recovery facilities to be defined precisely and user and system responsibilities to be delineated is presented.Various techniques for implementing recovery are described.Application of a general recovery facility to support reverse execution is discussed.A program development system (called COPE} with extensive recovery facilities, including reverse execution, is described.

Generalized Hoare Logic is a formal logical system for deriving invariance properties of programs.It provides a uniform way to describe a variety of methods for reasoning about concurrent programs, including noninterference, satisfaction, and cooperation proofs.We describe a simple recta-rule of the Generalized Hoare Logic--the Decomposition Principle--and show how all these methods can be derived using it.

Inference rules are derived for proving partial correctness of concurrent programs that use message passing.These rules extend the notion of a satisfaction proof, first proposed for proving correctness of programs that use synchronous message-passing, to asynchronous message-passing, rendezvous, and remote procedures.Two types of asynchronous message-passing are considered: unreliable datagrams and reliable virtual circuits.The proof rules show how interference can arise and be controlled.

Fault-

Message passing provides a way for concurrently executing processes to communicate and synchronize. In this paper, we develop proof rules for asynchronous message-passing primitives (i.e. “send no-wait”). Two benefits accrue from this. The obvious one is that partial correctness proofs can be written for concurrent programs that use such primitives. This allows programs to be understood as predicate transformers, instead of by contemplating all possible execution interleavings. The second benefit is that the proof rules and their derivation shed light on how interference arises when message-passing operations are used and on how this interference can be controlled. This provides insight into programming techniques to eliminate interference in programs that involve asynchronous activity. Three safe uses of asynchronous message passing are described here: the transfer of values, the transfer of monotonic predicates, and the use of acknowledgments.

A technique for solving synchronization problems in distributed programs is described.Use of this technique in environments in which processes may fail is discussed.The technique can be used to solve synchronization problems directly, to implement new synchronization mechanisms (which are presumably well suited for use in distributed programs), and to construct distributed versions of existing synchronization mechanisms.Use of the technique is illustrated with implementations of distributed semaphores and a conditional message-passing facility.

Four methods for generating and distributing shared group encryption keys in a cryptographic system are described. All four methods can be used to implement secure broadcasts among groups of users in computer networks. Two methods use n secret keys to construct a master key for 2n -1 keys.

Synchronous and asynchronous operation of software systems are defined. It is argued that certifying the correct operation of a system in the synchronous mode is significantly simpler than in the asynchronous mode. A series of compile-time and run-time restrictions for systems constructed in Concuirent Pascal are presented which assure equivalent operation in the synchronous and asynchronous modes.