Team for Research in
Ubiquitous Secure Technology

Citation
"A Logic of Secure Systems and its Application to Trusted Computing". A. Datta, J. Franklin, D. Garg, D. Kaynar (eds.), 30th IEEE Symposium on Security and Privacy, May, 2009.

Abstract
We present a logic for reasoning about properties of secure systems. The logic is built around a concurrent programming language with constructs for modeling machines with shared memory, a simple form of access control on memory, machine resets, cryptographic operations, network communication, and dynamically 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-ADVERSARY). 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.

Electronic downloads

• dfgk-oakland09.pdf · application/pdf · 209 kbytes

• HTML

   <a
  href="http://www.truststc.org/pubs/753.html"
  ><i>A Logic of  Secure Systems and its Application
  to Trusted Computing</i></a>, A. Datta, J.
  Franklin, D. Garg, D. Kaynar (eds.), 30th IEEE Symposium on
  Security and Privacy, May, 2009.

• Plain text

   "A Logic of  Secure Systems and its Application to
  Trusted Computing". A. Datta, J. Franklin, D. Garg, D.
  Kaynar (eds.), 30th IEEE Symposium on Security and Privacy,
  May, 2009.

• BibTeX

  @proceedings{DattaFranklinGargKaynar09_LogicOfSecureSystemsItsApplicationToTrustedComputing,
      title = {A Logic of  Secure Systems and its Application to
                Trusted Computing},
      editor = {A. Datta, J. Franklin, D. Garg, D. Kaynar},
      organization = {30th IEEE Symposium on Security and Privacy},
      month = {May},
      year = {2009},
      abstract = {We present a logic for reasoning about properties
                of secure systems. The logic is built around a
                concurrent programming language with constructs
                for modeling machines with shared memory, a simple
                form of access control on memory, machine resets,
                cryptographic operations, network communication,
                and dynamically 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-ADVERSARY). 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.},
      URL = {http://www.truststc.org/pubs/753.html}
  }
  

Posted by Jessica Gamble on 5 May 2010.
For additional information, see the Publications FAQ or contact webmaster at www truststc org.