Modelling Trust and Trusted Systems: A Category Theoretic Approach

TL;DR

This work introduces a category-theoretic framework (Category TRUST) for modeling trust in trusted computation and remote attestation, treating Elements $E$, Claims $C$, Results $R$, and Decisions $D$ as objects and Attest/Verify/Decide as morphisms within a topos. The decision space $D$ is formalized as a Heyting algebra, enabling nuanced, intuitionistic trust levels beyond binary judgments, with exponentials used to model attestation mechanisms, context, and policies. The framework is instantiated through detailed constructions (pullbacks for claims, contextual information $\Xi$, and a commutative attestation pipeline $\mathcal{A}$) and illustrated via dynamic scenarios (boot/run/shutdown), Evil Maid attacks, and a concrete attestation server design (Jane). The approach provides a rigorous semantic backbone for trust, enable-forensic reasoning, and cross-domain specification of attestation environments, while acknowledging limitations in dynamics and pointing to future work in higher-category formalisms and Kan extensions for policy evolution and complex compositions.

Abstract

We introduces a category-theoretic framework for modelling trust as applied to trusted computation systems and remote attestation. By formalizing elements, claims, results, and decisions as objects within a category, and the processes of attestation, verification, and decision-making as morphisms, the framework provides a rigorous approach to understanding trust establishment and provides a well-defined semantics for terms such as `trustworthiness' and 'justification'/forensics. The trust decision space is formalized using a Heyting Algebra, allowing nuanced trust levels that extend beyond binary trusted/untrusted states. We then present additional structures and in particular utilise exponentiation in a category theoretic sense to define compositions of attestation operations and provide the basis of a measurement for the expressibility of an attestation environment. We present a number of worked examples including boot-run-shutdown sequences, Evil Maid attacks and the specification of an attestation environment based upon this model. We then address challenges in modelling dynamic and larger systems made of multiple compositions.

Figures (11)

• Figure 1: Objects and Morphisms
• Figure 2: A Pullback showing $T$ are 'trusted' parts of $E$
• Figure 3: Pullback of Claims
• Figure 4: Attest and Verify Diagram
• Figure 5: Mapping to Decisions

Theorems & Definitions (8)

• proof
• proof
• proof
• proof
• proof
• proof
• proof
• proof