In distributed systems, trust decisions are made on the basis of integrity evidence generated via remote attestation. Examples of the kinds of evidence that might be collected are boot time image hash values; fingerprints of initialization files for userspace applications; and a comprehensive measurement of a running kernel. In layered attestations, evidence is typically composed of measurements of key subcomponents taken from different trust boundaries within a target system. Discrete measurement evidence is bundled together for appraisal by the components that collectively perform the attestation.

In distributed systems, trust decisions are often based on remote attestations in which evidence is gathered about the integrity of subcomponents. Layered attestations leverage hierarchical dependencies among the subcomponents to bolster the trustworthiness of evidence. Copland is a declarative, domain-specific language for specifying complex layered attestations. How phrases are composed bears directly on the trustworthiness of the evidence they produce, and complex phrases become quite difficult to analyze by hand. We introduce an automated method for analyzing executions of attestations specified by Copland phrases in an adversarial setting. We develop a general theory of executions with adversarial corruption and repair events. Our approach is to enrich the Copland semantics according to this theory. Using the model finder Chase, we characterize all executions consistent with a set of initial assumptions. From this set of models, an analyst can discover all ways an active adversary can corrupt subcomponents without being detected by the attestation. These efforts afford trust policymakers the ability to compare attestations expressed as Copland phrases against trust policy in a way that encompasses both static and runtime concerns.

Remote attestation consists of generating evidence of a system’s integrity via measurements and reporting the evidence to a remote party for appraisal in a form that can be trusted. The parties that exchange information must agree on formats and protocols. We assert there is a large variety of patterns of interactions among appraisers and attesters of interest. Therefore, it is important to standardize on flexible mechanisms for remote attestation. We make our case by describing scenarios that require the exchange of evidence among multiple parties using a variety of message passing patterns. We show cases in which changes in the order of evidence collection result in important differences to what can be inferred by an appraiser. We argue that adding the ability to negotiate the appropriate kind of attestation allows for remote attestations that better adapt to a dynamically changing environment. Finally, we suggest a language-based solution to taming the complexity of specifying and negotiating attestation procedures.

The increasing number of persistent attacks on computing systems has inspired considerable research in cyber resilience solutions. Resilient system designers seek objective approaches to aid in the comparison and selection of effective solutions. Decision theoretic techniques such as Markov decision processes can be leveraged for such comparisons and design decisions. Markov decision processes facilitate examination of uncertainty in system dynamics, diversity of responses, and optimization for operational objectives. This paper proposes a system design approach based in decision theory to achieve effective cyber resilience solutions. The prototypical example of a system with network intrusion detection and host reconstitution is used to illustrate this approach and highlight difficulties designers face due to the non-trivial coupling that may arise between response mechanisms.

We view a distributed system as a graph of active locations with unidirectional channels between them, through which they pass messages. In this context, the graph structure of a system constrains the propagation of information through it. Suppose a set of channels is a cut set between an information source and a potential sink. We prove that, if there is no disclosure from the source to the cut set, then there can be no disclosure to the sink. We introduce a new formalization of partial disclosure, called blur operators, and show that the same cut property is preserved for disclosure to within a blur operator. A related compositional principle ensures limited disclosure for a class of systems that differ only beyond the cut.

When collaborating agents share sensitive information to achieve a common goal it would be helpful to them to decide whether doing so will lead to an unwanted release of confidential data. These decisions are based on which other agents are involved, what those agents can do in the given context, and the individual confidentiality preferences of each agent. In this paper we consider a model of collaboration in which each agent has an explicit confidentiality policy. We offer three ways to interpret policy compliance (system compliance, plan compliance and weak plan compliance) corresponding to different levels of trust among the agents. We show it is EXPSPACE-complete to determine whether a given system is compliant and whether the agents can collaboratively reach a given common goal. On the other hand, we show it is undecidable to determine whether a given system has either a compliant plan or a weakly compliant plan leading to a common goal. The undecidability results are, in part, a consequence of the flexibility of the model, which allows interpretations of policy compliance that depend on current configurations.

Collaboration among organizations or individuals is common. While these participants are often unwilling to share all their information with each other, some information sharing is unavoidable when achieving a common goal. The need to share information and the desire to keep it private/ secret are two competing notions which affect the outcome of a collaboration. This paper proposes a formal model of collaboration which addresses privacy/secrecy concerns. We draw on the notion of a plan which originates in the AI literature. We consider transition systems in which actions have pre- and post-conditions of the same size. We show it is PSPACE-complete to decide whether a given such system protects the privacy/secrecy of its participants and whether it contains a plan leading from a given initial state to a desired goal state.