CMU Theory of Secure Systems (ToSS) Project

• ToSS Home
• Related Work

ToSS Project

The Theory of Secure Systems Project (ToSS) is affiliated with the computer science department and CyLab at Carnegie Mellon University.

The primary goal of the ToSS project is to develop a formal framework for modeling and analysis of secure systems at two levels of abstraction--system architecture (specification) and system implementation. A specific issue that we plan to address in developing and using this framework is to provide rigorous definitions of security and adversary models, a relatively unexplored area in systems security. In addition, we hope to identify design principles for secure systems, as well as a core set of basic building blocks from which complex systems can be constructed via secure composition.

Selected Papers

• Compositional System Security with Interface-Confined Adversaries
  Deepak Garg, Jason Franklin, Dilsun Kaynar, and Anupam Datta.
  To appear in the Mathematical Foundations of Programming Semantics (MFPS) Conference, 2010.
  PDF Full Version


• Scalable Parametric Verification of Secure Systems: How to Verify Reference Monitors without Worrying about Data Structure Size
  Jason Franklin, Sagar Chaki, Anupam Datta, and Arvind Seshadri.
  Proceedings of IEEE Symposium on Security and Privacy (Oakland '10), May 2010.
  PDF Full Version


• ASPIER: An Automated Framework for Verifying Security Protocol Implementations
  Sagar Chaki and Anupam Datta
  Proceedings of 22nd IEEE Computer Security Foundations Symposium, July 2009.
  PDF


• A Logic of Secure Systems and its Application to Trusted Computing
  Anupam Datta, Jason Franklin, Deepak Garg, and Dilsun Kaynar.
  Proceedings of IEEE Symposium on Security and Privacy (Oakland '09), May 2009.
  PDF PS PDF (Full Version) PS (Full Version)


• Attacking, Repairing, and Verifying SecVisor: A Retrospective on the Security of a Hypervisor
  Jason Franklin, Arvind Seshadri, Ning Qu, Sagar Chaki, and Anupam Datta
  CMU Cylab Technical Report CMU-CyLab-08-008, June 2008.
  PDF +Abstract

  SecVisor is a hypervisor designed to guarantee that only code approved by the user of a system executes at the privilege level of the OS kernel [Seshadri07]. We employ a model checker to verify the design properties of SecVisor and identify two design-level attacks that violate SecVisor's security requirements. Despite SecVisor's narrow interface and tiny code size, our attacks were overlooked in both SecVisor's design and implementation. Our attacks exploit weaknesses in SecVisor's memory protections. We demonstrate that our attacks are realistic by crafting exploits for an implementation of SecVisor and successfully performing two attacks against a SecVisor-protected Linux kernel. To repair SecVisor, we design and implement an efficient and secure memory protection scheme. We formally verify the security of our scheme. We demonstrate that the performance impact of our proposed defense is negligible and that our exploits are no longer effective against the repaired implementation. Based on this case study, we identify facets of secure system design that aid the verification process.



• A Logic for Reasoning about Networked Secure Systems
  Deepak Garg, Jason Franklin, Dilsun Kaynar, and Anupam Datta
  In Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis, and Issues in the Theory of Security, June 2008.
  PDF (Short Version) PDF (Full Version) +Abstract

  We initiate a program to model and analyze end-to-end security properties of contemporary secure systems that rely on network protocols and memory protection. Specifically, this paper introduces the Logic of Secure Systems (LS^2). LS^2 extends an existing logic for security protocols by incorporating shared memory, time and limited forms of access control. The proof system for LS^2 supports high-level reasoning about secure systems in the presence of adversaries on the network and the local machine. We prove a soundness theorem for the proof system and illustrate its use by proving a relevant security property of a protocol inspired by the Transport Layer Protocol of the Secure Shell (SSH).