In computing systems, trust is an expectation on the dynamic behavior of an agent; static analysis is a collection of techniques for establishing static bounds on the dynamic behavior of an agent. We study the relationship
between code identity, static analysis and trust in open distributed systems. Our primary result is a robust safety theorem
expressed in terms of a distributed higher-order pi-calculus with code identity and a primitive for remote attestation; types
in the language make use of a rich specification language for access control policies.
Keywords Trusted Computing - Remote Attestation - Access Control - Authorization Logic - Compound Principals - Higher-Order Pi Calculus - Typing