Jason Franklin, Ph.D. Student

Technical Reports

• FAWN: A Fast Array of Wimpy Nodes
  David Andersen, Jason Franklin, Amar Phanishayee, Lawrence Tan, and Vijay Vasudevan
  Carnegie Mellon University PDL Technical Report CMU-PDL-08-108, May 2008.

  PDF +Abstract

  This paper introduces the FAWN---Fast Array of Wimpy Nodes---cluster architecture for providing fast, scalable, and power-efficient key-value storage. A FAWN links together a large number of tiny nodes built using embedded processors and small amounts (2--16GB) of flash memory into an ensemble capable of handling 700 queries per second per node, while consuming fewer than 6 watts of power per node. We have designed and implemented a clustered key-value storage system, FAWN-DHT, that runs atop these node. Nodes in FAWN-DHT use a specialized log-like back-end hash-based database to ensure that the system can absorb the large write workload imposed by frequent node arrivals and departures. FAWN uses a two-level cache hierarchy to ensure that imbalanced workloads cannot create hot-spots on one or a few wimpy nodes that impair the system's ability to service queries at its guaranteed rate.
  
  Our evaluation of a small-scale FAWN cluster and several candidate FAWN node systems suggest that FAWN can be a practical approach to building large-scale storage for seek-intensive workloads. Our further analysis indicates that a FAWN cluster is cost-competitive with other approaches (e.g., DRAM, multitudes of magnetic disks, solid-state disk) to providing high query rates, while consuming 3-10x less power.

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

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

Talks and Posters

• Towards High-Assurance Hypervisors
  CMU CyLab Student Seminar Series, Pittsburgh, PA, Oct. 2008.
  PPT
  
  
• Towards End-to-End Security Analysis of Networked Systems (5 Minute Talk)
  Symposium on Computer Security Foundations (CSF), Pittsburgh, PA, June 2008.
  PPT
  
  
• Modeling and Analysis of Networked Secure Systems with Application to Trusted Computing
  CMU CyLab Student Seminar Series, Pittsburgh, PA, May 2008.
  PPT
  
  
• An Inquiry into the Nature and Causes of the Wealth of Internet Miscreants
  ACM CCS'07, Alexandria, VA, Nov. 2007.
  Warning: Slides presented on Oct. 31st with cartoonish Halloween theme.
  PPT
  
  
• Using Economics to Quantify the Security of the Internet
  CMU Hot Topics in Networking Class, CMU, Pittsburgh, PA, May 2007.
  PPT
  
  
• A Discussion of the Insider Threat
  SECMU Group Meeting, CMU, Pittsburgh, PA, Sept. 2006.
  PPT
  
  
• Understanding Botnets: How Massive Internet Break-ins Fuel an Underground Economy
  Poster session, Lawrence Berkeley National Laboratory, Berkeley, CA, July 2006.
  PPT
  
  
• Securely Using Untrusted Terminals and Compromised Computers with Human-Verifiable Code Execution
  Stanford Security Seminar, Stanford University, Palo Alto, CA, July 2006.
  PPT Abstract
  
  
• Remote Virtual Machine Monitor Detection
  ARO-DARPA-DHS Special Workshop on Botnets, Arlington, VA, June 2006.
  PPT
  
  
• Mapping Internet Sensors with Probe Response Attacks
  UC-Davis Security Seminar, Davis, California, July 2005.
  PDF (Extended version of the USENIX Security 2005 slides.)
  
  
• Mapping Internet Sensors with Probe Response Attacks: Protecting Internet Sensor Anonymity
  Department of Homeland Security R&D Conference, Boston, Massachusetts, April 2005.
  PDF (High level overview of USENIX Security 2005 slides.)
  
  
• On the Benefits of Security Log Sharing
  Workshop on Critical Infrastructure Protection, University of Central Florida, Orlando, FL, May 2004.
  PS
  
  

Old (but still interesting) News...

• Oct. 16th, 2008: In April, Slate magazine ran an article on underground markets for sensitive data. They reference our wealth of miscreants paper from CCS and get their facts right. It's one of the best short articles on the topic that I've seen. Nice job Mr. Leibenluft.


• May 21st, 2008: A report on the FAWN: A Fast Array of Wimpy Nodes architecture for fast, scalable, and power-efficient key-value storage is now available. A FAWN links together a large number of tiny nodes built using embedded processors and small amounts (2--16GB) of flash memory into an ensemble capable of handling 700 queries per second per node, while consuming fewer than 4 watts of power per node.


• May 18th, 2008: Our paper "A Logic for Reasoning about Networked Secure Systems" was accepted for presentation at FCS-ARSPA-WITS.


• May 14th, 2008: During a 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 verified the repaired design. More information: Attacking, Repairing, and Verifying SecVisor: A Retrospective on the Security of a Hypervisor.


• Nov. 19th, 2007: We've developed a human-verifiable code execution system based upon Lipner's insight:

  +More

  "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..." [Lipner SOSP'75].
  

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

Fellowships and Scholarships

I am currently supported by the NSF Graduate Research Fellowship. From 2005 to 2008, I was funded by the Department of Homeland Security Fellowship. As an undergraduate I was fortunate to be supported by the Department of Homeland Security Scholarship.