CMU Theory of Secure Systems (ToSS) Project

• ToSS Home
• Related Work

Affiliations

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

Goals of ToSS Project

Our long-term goal is to develop a formal framework for modeling and analysis of secure systems at two levels of abstraction--system architecture 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.

Modeling and Analysis of Secure Systems

Several inherent features of secure systems stand in the way of a formal theory:

1. Secure systems are complex, requiring temporal reasoning about multiple users and access control mechanisms to protect shared resources.


2. Secure systems are frequently networked to form networked and distributed systems. This mandates a theory that is general enough to model this immense variety of systems.


3. The definition of security and adversary model for secure systems are often poorly specified or completely ignored. As a result, developing adversary models for secure systems is a relatively unexplored area of research.

Selected Papers

• 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).




• Towards a Theory of Secure Systems
  Deepak Garg, Jason Franklin, Dilsun Kaynar, and Anupam Datta
  CMU CyLab Technical Report CMU-CyLab-08-003, Feb. 2008.
  PDF +Abstract

  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.