Jason Franklin Ph.D.


Computer Science Department
Carnegie Mellon University
5000 Forbes Ave
Pittsburgh, PA 15213

Get my email address

Get my CV


Academic Background

I received my Ph.D. in 2012 from the computer science department at Carnegie Mellon University. My thesis advisor was Anupam Datta. I was a TA for Garth Gibson's "Advanced Operating Systems and Distributed Systems" and Greg Kesden's "Introduction to Computer Systems". I graduated from the University of Wisconsin-Madison in 2004 with a B.S. in computer science, a B.S. in mathematics and a minor in business with a focus on economics. As an undergraduate, I worked on the CIPART project under the direction of Mary Vernon and with Eric Bach researching cryptographic modes of operation.

Awards and Fellowships

I've received the following paper awards:

And the following fellowships and scholarships:



Invited Articles

Under Submission

Refereed Papers in Conferences and Workshops

Book Chapters

Technical Reports and Unpublished Works

  • Towards Simple and Scalable Analysis of Secure Systems
    Jason Franklin, Deepak Garg, Dilsun Kaynar, and Anupam Datta.
    Unpublished, March 2009.
    PDF PS

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

  • On the (Im)possibility of Timed Tamper-Evident Software in (A)synchronous Systems
    Jason Franklin and Michael Carl Tschantz.
    Unpublished, Aug. 2007.

    PDF PS +Abstract

    Tamper-evident software has the property that a verifier can detect a violation of program integrity during execution. In this paper, we study programs that through their own execution provide sufficient information in the form of responses and timing to detect tampering. We refer to such programs as timed tamper-evident programs.

    We formalize the notation of a timed tamper-evident program, model a micro-controller under this formalization, and prove the existence of a timed tamper-evident program for this model when used with synchronous communication. We develop timed tamper-evident programs which verify both control and data integrity. We discuss the existence of timed tamper-evident functions in an asynchronous system.

  • PRISM: Enabling Personal Verification of Code Integrity, Untampered Execution, and Trusted I/O or Human-Verifiable Code Execution
    Jason Franklin, Mark Luk, Arvind Seshadri, and Adrian Perrig.
    CMU Cylab Technical Report CMU-CyLab-07-010, February 2007.

    PDF +Abstract

    Today's computer users receive few assurances that their software executes as expected. The problem is that legacy devices do not enable personal verification of code execution. In addition, legacy devices lack trusted paths for secure user I/O making it difficult to ensure the privacy of data.

    We present PRISM, a software-only human-verifiable code execution system that temporally separates a legacy computer system into a trusted component and an untrusted component. PRISM enables a user to securely interact with applications by establishing a trusted path and enables personal verification of untampered application execution.

    PRISM enables the development of a new class of applications which we term personally verifiable applications (PVAs). PVAs have the property that a user can both securely interact with and execute these applications even in the face of a kernel-level compromise. We develop a personally verifiable digital signature application that assures the user that the password-protected private key is not misused and that neither the private key nor the password are disclosed to malware on the device. We describe an implementation of this application on a personal device, and evaluate the usability of our approach with a user study.

Talks and Posters

Old (but still interesting) News...