Compositional Security

Compositional security principles are critical for scalable construction and analysis of secure systems. Contemporary systems are built up from smaller components, but even if each component is secure in isolation, a system composed of secure components may not meet its security requirements. Attacks using properties of one component to subvert another have shown up in practice in many different settings, including cryptographic protocols, systems software, application software, web browsers and infrastructure. We develop a general theory of compositional security called Adversary-aware Assume Guarantee. In traditional assume-guarantee reasoning for reasoning about system correctness, system components assume that other components satisfy certain assumptions. These assumptions are discharged by analyzing the code of other components. In contrast, in our security setting, assumptions about adversarial components are enforced using a combination of cryptographic, hardware, and software protection mechanisms and associated program-directed methods for reasoning about them. Significant results include the following:

  • System M: The first program logic that allows proofs of safety for higher-order programs that execute adversary-supplied code without requiring the adversarial code to be available for deep static analysis. It supports reasoning about invariants of adversarial components via interface-confinement (or sandboxing) and code identity checks. System M has been used to verify security properties of models of hypervisors and trusted computing systems. [CSF 2015]. Builds on our prior work on a related logic where adversaries were restricted to only supply data (not code) via system interfaces [MFPS 2010].
  • Logic of Secure Systems: A program logic for reasoning about security properties of systems that employ cryptographic and trusted computing primitives. It was used to construct the first formal analysis of attestation protocols for trusted computing systems, while reasoning about adversary-supplied untrusted code during attestation; identified a previously unknown insecure interaction between two attestation protocols [IEEE S & P 2009].
  • Quantitative Protocol Composition Logic: A program logic that enables proofs of concrete security for a class of cryptographic protocols [Manuscript 2015]
  • Protocol Composition Logic: A program logic for compositional reasoning about security properties of network protocols. [ Project Page at Stanford]
  •  

    Overview

     

    Publications

    • L. Jia, S. Sen, D. Garg, A. Datta, A Logic of Programs with Interface-confined Code, in Proceedings of 28th IEEE Computer Security Foundations Symposium, July 2015. [ Paper]
    • A. Vasudevan, S. Chaki, L. Jia, J. McCune, J. Newsome, A. Datta. Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework, in Proceedings of 34th IEEE Symposium on Security and Privacy, May 2013. [ Paper]
    • J. Franklin, S. Chaki, A. Datta, J. McCune, A. Vasudevan, Parametric Verification of Address Space Separation, in Proceedings of ETAPS Conference on Principles of Security and Trust, March 2012. [ Paper] [Full Version] ETAPS Best Paper Nominee
    • J. Franklin, S. Chaki, A. Datta, A. Seshadri, Scalable Parametric Verification of Secure Systems: How to Verify Reference Monitors without Worrying about Data Structure Size, inProceedings of 31st IEEE Symposium on Security and Privacy, May 2010. [ Paper ]
    • J. McCune, Y. Li, N. Qu, Z. Zhou, A. Datta, V. Gligor, A. Perrig, TrustVisor: Efficient TCB Reduction and Attestation, in Proceedings of 31st IEEE Symposium on Security and Privacy, May 2010. [ Paper ]
    • D. GargJ. FranklinD. KaynarA. Datta, Compositional System Security with Interface-Confined Adversaries, in Proceedings of 26th Annual Conference on Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science, May 2010. [ Paper] [ Full Version ]  Invited Paper
    • A. DattaJ. FranklinD. GargD. Kaynar, A Logic of  Secure Systems and its Application to Trusted Computing, in Proceedings of 30th IEEE Symposium on Security and Privacy, May 2009. [ Paper ] [Full Version]
    • A. RoyA. Datta, A. Derek, J. C. Mitchell, Inductive Trace Properties for Computational Security, in Journal of Computer Security18(6): 1035-1073 (2010). [ Paper]
    • A. RoyA. DattaJ. C. Mitchell, Formal Proofs of Cryptographic Security of Diffie-Hellman based Protocols, in Proceedings of Symposium On Trustworthy Global Computing, November 2007. [ Paper ]
    • A. RoyA. Datta, A. Derek, J. C. Mitchell, Inductive Proofs of Computational Secrecy, in Proceedings of 12th European Symposium On Research In Computer Security , September 2007. [ Paper ]
    • A. Datta, A. Derek, J. C. MitchellA. Roy, Protocol Composition Logic (PCL), in Electronic Notes in Theoretical Computer Science (Gordon D. Plotkin Festschrift), 2007. [ Paper ]   Invited Paper
    • A. RoyA. Datta, A. Derek, J. C. Mitchell, Inductive Trace Properties for Computational Security, in Proceedings of ACM SIGPLAN and IFIP WG 1.7  7th Workshop on Issues in the Theory of Security, March 2007. (Invited to Special Issue of Journal of Computer Security). [ Paper ]    Award Paper
    • A. RoyA. Datta, A. Derek, J. C. Mitchell, J.-P. Seifert, Secrecy Analysis in Protocol Composition Logic, in Proceedings of 11th Annual Asian Computing Science Conference, December 2006. [ Paper ]
    • A. Datta, A. Derek, J. C. MitchellB. Warinschi, Computationally Sound Compositional Logic for Key Exchange Protocols, in Proceedings of 19th IEEE Computer Security Foundations Workshop, pp. 321-334, July 2006. [ Paper ]
    • M. BackesA. Datta, A. Derek, J. C. MitchellM. Turuani, Compositional Analysis of Contract-Signing Protocols, in Theoretical Computer Science, 367(1-2), pp. 33-56, 2006. [ Paper ]
    • C. He, M. Sundararajan, A. Datta, A. Derek, J. C. Mitchell, A Modular Correctness Proof of TLS and IEEE 802.11i, in Proceedings of 12th ACM Conference on Computer and Communications Security, pp. 2-15, November 2005. (Invited to ACM Transactions on Information and System Security, Special Issue of Selected Papers from CCS'05.) [ Paper ]    Award Paper
    • A. Datta, A. Derek, J. C. MitchellV. ShmatikovM. Turuani, Probabilistic Polynomial-time Semantics for a Protocol Security Logic, in Proceedings of 32nd International Colloquium on Automata, Languages and Programming, pp. 16-29, July 2005. [ Paper ]    Invited Paper
    • A. Datta, A. Derek, J. C. MitchellD. Pavlovic, A Derivation System and Compositional Logic for Security Protocols, Journal of Computer Security (Special Issue of Selected Papers from CSFW-16), Vol. 13, pp. 423-482, 2005. [ Paper ]
    • M. BackesA. Datta, A. Derek, J. C. MitchellM. Turuani, Compositional Analysis of Contract-Signing Protocols, in Proceedings of 18th IEEE Computer Security Foundations Workshop, pp. 94-110, June 2005. [ Paper ]
    • A. Datta, A. Derek, J. C. MitchellD. Pavlovic, Abstraction and Refinement in Protocol Derivation, in Proceedings of 17th IEEE Computer Security Foundations Workshop, pp. 30-45, June 2004. [ Paper ]
    • A. Datta, A. Derek, J. C. MitchellD. Pavlovic, Secure Protocol Composition.
      • In Proceedings of 19th Annual Conference on Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science, Vol. 83, 2004. [ Paper ]
      • Extended abstract in Proceedings of ACM  Workshop on Formal Methods in Security Engineering, pp. 11-23, October 2003. [ Paper ]
    • A. Datta, A. Derek, J. C. MitchellD. Pavlovic, A Derivation System for Security Protocols and its Logical Formalization, in Proceedings of 16th IEEE Computer Security Foundations Workshop, pp. 109-125, June 2003. (Invited to Journal of Computer Security, Special Issue of Selected Papers from CSFW-16) Paper ]    Award Paper