The Community for Technology Leaders
2009 30th IEEE Symposium on Security and Privacy (2009)
Oakland, California
May 17, 2009 to May 20, 2009
ISSN: 1081-6011
ISBN: 978-0-7695-3633-0
pp: 221-236
ABSTRACT
We present a logic for reasoning about properties of securesystems. The logic is built around a concurrent programminglanguage with constructs for modeling machines with sharedmemory, a simple form of access control on memory, machineresets, cryptographic operations, network communication, anddynamically loading and executing unknown(and potentially untrusted) code. The adversary's capabilities are constrained by the system interface as defined in the programming model (leading to the name csi). We develop a sound proof system for reasoning about programs without explicitly reasoning about adversary actions. We use the logic to characterize trusted computing primitives and prove code integrity and execution integrity properties of two remote attestation protocols. The proofs make precise assumptions needed for the security of these protocols and reveal an insecure interaction between the two protocols.
INDEX TERMS
Trusted Computing, Remote Attestation, Logic of Secure Systems, Formal Reasoning
CITATION

D. Garg, D. Kaynar, A. Datta and J. Franklin, "A Logic of Secure Systems and its Application to Trusted Computing," 2009 30th IEEE Symposium on Security and Privacy(SP), Oakland, California, 2009, pp. 221-236.
doi:10.1109/SP.2009.16
88 ms
(Ver 3.3 (11022016))