Jason Franklin, Ph.D. Student, Computer Science Department, Carnegie Mellon University

Computer Science Department
Carnegie Mellon University
Office: 8124 Wean Hall
5000 Forbes Ave
Pittsburgh, PA 15213

jfr CLICK TO REVEAL @cmu.edu

News

May 14th, 2008: During a formal verification of the SecVisor hypervisor (Seshadri et al. SOSP'07), we identified two serious vulnerabilities in the design of the shadow page table synchronization code. We were able to craft exploits (37 and 15 l.o.c) for the vulnerabilities and launch a successful code-injection attack against a SecVisor-protected Linux kernel. We repaired the vulnerabilities and formally verified the repaired design. A report on our experiences is available below:
Attacking, Repairing, and Verifying SecVisor: A Retrospective on the Security of a Hypervisor
Jason Franklin, Arvind Seshadri, Ning Qu, Sagar Chaki, and Anupam Datta
Under submission to 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08).

Nov. 19th, 2007: We've realized Lipner's 1975 suggestion concerning human-verifiable code execution:
"The covert channels of Lampson are associated with the one system-wide resource, time, that can be observed in at least a coarse way by every user and every program. Each user (presumably) has a wristwatch..." by Lipner in SOSP'75.

PRISM: Enabling Personal Verification of Code Integrity, Untampered Execution, and Trusted I/O or Human-Verifiable Code Execution

August 4th, 2007: Storm worm, the state of security practice in a nutshell

+More

This article is an excellent depiction of the state of the art of security practice. In just a few paragraphs it hits on arms races/evolving threats, social engineering, botnets, spam, economically-motivated malicious activity, VMM detection, and the sad state of our defenses "Keep anti-virus software up to date and be suspicious of any e-mail attachment or link, even from what appears to be a familiar source.".
August 1st, 2007: Security remains benefit of virtualization

+More

The article Security not a benefit of virtualisation incorrectly concludes that our HotOS'07 paper entitled "Compatibility is Not Transparency: VMM Detection Myths and Realities" suggests that security is not a benefit of virtualization. Our paper only suggests that security resulting from the perception of VMM stealth is not a benefit of virtualization. Virtualized systems still accrue security benefits from the VMMs isolation and introspection abilities, among others.

Academic Background

I am currently a 3rd year Ph.D. student in the computer science department at Carnegie Mellon University working on the ToSS project.

I graduated from the University of Wisconsin-Madison in 2004 with majors in computer science and mathematics. As an undergraduate, I worked on the CIPART project under the direction of Professor Mary Vernon, before that I worked with Professor Eric Bach researching cryptographic modes of operation.

Projects

Some projects I've worked on include:

The Theory of Secure Systems (ToSS) Project.
The Emerging Threats (ET) Project.

Research

Under Submission

Attacking, Repairing, and Verifying SecVisor: A Retrospective on the Security of a Hypervisor
Jason Franklin, Arvind Seshadri, Ning Qu, Sagar Chaki, and Anupam Datta
Under submission to 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08).

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.
Towards a Theory of Secure Systems
with Deepak Garg, Dilsun Kaynar, and Anupam Datta
CMU Cylab Technical Report CMU-CyLab-08-003, Feb. 2008.

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

Refereed Papers in Conferences and Workshops

An Inquiry into the Nature and Causes of the Wealth of Internet Miscreants
with Vern Paxson, Adrian Perrig, and Stefan Savage.
Proceedings of 14th ACM CCS, November 2007.
Press:[ arstechnica CMU ComputerWorld Crypto-Gram InfoWeek NewScientist PCPro ScienceDaily Slashdot theregister]

PDF PS Slides (PPT) +Abstract

This paper studies an active underground economy which specializes in the commoditization of activities such as credit card fraud, identity theft, spamming, phishing, online credential theft, and the sale of compromised hosts. Using a seven month trace of logs collected from an active underground market operating on public Internet chat networks, we measure how the shift from ``hacking for fun'' to ``hacking for profit'' has given birth to a societal substrate mature enough to steal wealth into the millions of dollars in less than one year.

Compatibility is Not Transparency: VMM Detection Myths and Realities
Tal Garfinkel, Keith Adams, Andrew Warfield, and Jason Franklin
Proceedings of HotOS XI, May 2007.
Press:[CNet Slashdot]
PDF PS
Replayer: Automatic Protocol Replay by Binary Analysis
James Newsome, David Brumley, Jason Franklin, and Dawn Song.
Proceedings of 13th ACM CCS, November 2006.
PDF PS
Passive Data Link Layer 802.11 Wireless Device Driver Fingerprinting
Jason Franklin, Damon McCoy, Parisa Tabriz, Vicentiu Neagoe, Jamie Van Randwyk, and Douglas Sicker.
Proceedings of the 15th USENIX Security Symposium, August 2006.
Press:[Slashdot Sandia Labs] Video: [CNBC (12.8MB)]

PDF PS Slides: PPT +Abstract

Motivated by the proliferation of wireless-enabled devices and the suspect nature of device driver code, we develop a passive fingerprinting technique that identifies the wireless device driver running on an IEEE 802.11 compliant device. This technique is valuable to an attacker wishing to conduct reconnaissance against a potential target so that he may launch a driver-specific exploit.

In particular, we develop a unique fingerprinting technique that accurately and efficiently identifies the wireless driver without modification to or cooperation from a wireless device. We perform an evaluation of this fingerprinting technique that shows it both quickly and accurately fingerprints wireless device drivers in real world wireless network conditions. Finally, we discuss ways to prevent fingerprinting that will aid in improving the security of wireless communication for devices that employ 802.11 networking.

Mapping Internet Sensors with Probe Response Attacks
Best Paper Award.
John Bethencourt, Jason Franklin, Mary Vernon.
Proceedings of the 14th USENIX Security Symposium, August 2005.
Press:[CNET InformationWeek NewScientist Slashdot ZDnet]
PDF PS HTML Abstract Slides: PDF

Journal Articles

Remote Detection of Virtual Machine Monitors with Fuzzy Benchmarking
Jason Franklin, Mark Luk, Jonathan M. McCune, Arvind Seshadri, Adrian Perrig, and Leendert van Doorn.
To appear in ACM SIGOPS Operating System Review (Special Issue on Computer Forensics), April 2008.
Extends CMU Cylab Technical Report CMU-CyLab-07-001, January 2007.

PDF PS +Abstract

We study the remote detection of virtual machine monitors (VMMs) across the Internet, and devise fuzzy benchmarking as an approach that can successfully detect the presence or absence of a VMM on a remote system. Fuzzy benchmarking works by making timing measurements of the execution time of particular code sequences executing on the remote system. The fuzziness comes from heuristics which we employ to learn characteristics of the remote system's hardware and VMM configuration. Our techniques are successful despite uncertainty about the remote machine's hardware configuration.

Book Chapters

Towards Sound Detection of Virtual Machines
Jason Franklin, Mark Luk, Jonathan M. McCune, Arvind Seshadri, Adrian Perrig, Leendert van Doorn.
In Advances in Information Security, Botnet Detection: Countering the Largest Security Threat

PDF PS +Abstract

We design, implement, and evaluate a practical timing-based approach to detect virtual machine monitors (VMMs) without relying on VMM implementation details. The algorithms developed in this paper are based on fundamental properties of virtual machine monitors rather than easily modified software artifacts. We evaluate our approach against two common VMM implementations on machines with and without hardware support for virtualization in a number of remote and local experiments. We successfully distinguish between virtual and real machines in all cases even with incomplete information regarding the VMM implementation and hardware configuration of the targeted machine.

Technical Reports

Towards a Theory of Secure Systems
with Deepak Garg, Dilsun Kaynar, and Anupam Datta
CMU Cylab Technical Report CMU-CyLab-08-003, Feb. 2008.

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

More information is available at the TOSS project webpage.

PRISM: Enabling Personal Verification of Code Integrity, Untampered Execution, and Trusted I/O or Human-Verifiable Code Execution
with Mark Luk, Arvind Seshadri, and Adrian Perrig.
CMU Cylab Technical Report CMU-CyLab-07-010, Feburary 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.

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

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.