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.

Cryptographic protocols are useful for trust engineering in Web transactions. The Cryptographic Protocol Programming Language (CPPL) provides a model wherein trust management annotations are attached to protocol actions, and are used to constrain the behavior of a protocol participant to be compatible with its own trust policy.

In this paper, we present a systematic way to determine the information flow security goals achieved by systems running a secure O/S, specifically systems running Security-Enhanced Linux. A formalization of the access control mechanism of the SELinux

Turner popularized a technique of Wadsworth in which a cyclic graph rewriting rule is used to implement reduction of the fixed point combinator Y . We examine the theoretical foundation of this approach. Previous work has concentrated on proving that graph methods are, in a certain sense, sound and complete implementations of term methods. This work is inapplicable to the cyclic Y rule, which is unsound in this sense since graph normal forms can exist without corresponding term normal forms. We define and prove the correctness of combinator head reduction using the cyclic Y rule; the correctness of normal reduction is an immediate consequence. Our proof avoids the use of infinite trees to explain cyclic graphs. Instead, we show how to consider reduction with cycles as an optimization of reduction without cycles.