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.

翻译：本文提出了一种范畴论框架，用于对可信计算系统与远程证明中的信任关系进行建模。该框架通过将元素、声明、结果和决策形式化为范畴中的对象，并将证明、验证和决策过程视为态射，为理解信任建立机制提供了严谨的数学方法，同时为“可信性”“正当性/取证”等术语提供了明确定义的语义。信任决策空间采用海廷代数进行形式化描述，从而支持超越二元信任/不信任状态的精细化信任等级。我们进一步引入附加结构，特别利用范畴论意义上的指数运算来定义证明操作的组合，并为证明环境的表达能力度量奠定基础。文中给出了多个具体示例，包括启动-运行-关闭序列、邪恶女仆攻击以及基于该模型的证明环境规范。最后，我们探讨了在建模由多重组合构成的动态大规模系统时所面临的挑战。