Towards a Theory of Secure Systems (CMU-CyLab-08-003)

We initiate a program to develop a principled theory of secure systems. Our main technical result is a formal logic for reasoning about a network of shared memory, multi-user systems. The logic is inspired by an existing logic for security protocols. It extends the attacker model and adds shared memory, time, and limited forms of access control. We prove soundness for the proof system in the presence of an attacker who controls the network and has partial control over shared memory on individual machines. We illustrate the use of the logic by proving a relevant security property of a part of the Trusted Computing Group’s remote attestation protocol