Static Analysis and Synthesis of Layered Attestation Protocols

Trust is a fundamental issue in computer security. Frequently, systems implicitly trust in other

systems, especially if configured by the same administrator. This fallacious reasoning stems from the belief

that systems starting from a known, presumably good, state can be trusted. However, this statement only

holds for boot-time behavior; most non-trivial systems change state over time, and thus runtime behavior is

an important, oft-overlooked aspect of implicit trust in system security.

    To address this, attestation was developed, allowing a system to provide evidence of its runtime behavior to a

verifier. This evidence allows a verifier to make an explicit informed decision about the system’s trustworthiness.

As systems grow more complex, scalable attestation mechanisms become increasingly important. To apply

attestation to non-trivial systems, layered attestation was introduced, allowing attestation of individual

components or layers, combined into a unified report about overall system behavior. This approach enables

more granular trust assessments and facilitates attestation in complex, multi-layered architectures. With the

complexity of layered attestation, discerning whether a given protocol is sufficiently measuring a system, is

executable, or if all measurements are properly reported, becomes increasingly challenging.

    In this work, we will develop a framework for the static analysis and synthesis of layered attestation protocols,

enabling more robust and adaptable attestation mechanisms for dynamic systems. A key focus will be the

static verification of protocol correctness, ensuring the protocol behaves as intended and provides reliable

evidence of the underlying system state. A type system will be added to the Copland layered attestation

protocol description language to allow basic static checks, and extended static analysis techniques will be

developed to verify more complex properties of protocols for a specific target system. Further, protocol

synthesis will be explored, enabling the automatic generation of correct-by-construction protocols tailored to

system requirements.