Jason Franklin Ph.D.

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

Get my email address

Get my CV

News

• May 2nd: Read my thesis: Abstractions for Model Checking System Security


• March 26th: Parametric Verification of Address Space Separation received Best Paper Nomination (Top 12 paper of 600 submissions, 100+ accepts) at ETAPS 2012


• March 2nd: Successfully defended my thesis!


• Jan 2012: An overly dramatic Wired article about FAWN.


• June 2011: A Chronicle of Higher Education article about information piracy with some of my sage advice.


• June 2011: FAWN Communications of the ACM (CACM) paper.


• More News
  

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:

• Best Paper Nomination at ETAPS 2012 (Top 12 paper of 600+ submissions)
• Best Paper Award at SOSP 2009
• Best Paper Award at USENIX Security 2005

And the following fellowships and scholarships:

• NSF Graduate Research Fellowship
• Department of Homeland Security Fellowship
• Department of Homeland Security Scholarship

Projects

• Theory of Secure Systems (ToSS)
• FAWN: A Fast Array of Wimpy Nodes
• Emerging Threats (ET)

Research

Invited Articles

• FAWN: A Fast Array of Wimpy Nodes
  David Andersen, Jason Franklin, Michael Kaminsky, Amar Phanishayee, Lawrence Tan, and Vijay Vasudevan.
  In Communications of the ACM (CACM), 2011.
  


• On Adversary Models and Compositional Security
  Anupam Datta, Jason Franklin, Deepak Garg, Limin Jia, and Dilsun Kaynar.
  IEEE Security & Privacy, Volume 9, Issue 3, May 2011.
  

  PDF

  We outline a theory of compositional security, addressing a recognized scientific challenge. Contemporary systems are built up from smaller components. However, even if each component is secure in isolation, the composed system may not achieve the desired security property: an adversary may exploit complex interactions between components to compromise security. The goal of a theory of compositional security is to identify relationships among systems, adversaries and properties such that precisely defined composition operations over systems and adversaries preserve security properties. In presenting our theory, we describe our model for general classes of systems, adversaries and security properties. We then present composition results (relationships) in this model. We also discuss how our theory explains a number of specific attacks found in the wild and how it can serve as the basis for predicting whether security properties of systems will be preserved as adversaries come up with new attacks.

  
  
• Energy-efficient Cluster Computing with FAWN: Workloads and Implications
  Vijay Vasudevan, David Andersen, Michael Kaminsky, Lawrence Tan, Jason Franklin, and Iulian Moraru.
  Proceedings of 1st International Conference on Energy-Efficient Computing and Networking (e-Energy 2010), April 2010.
  PDF Slides

Under Submission

• Havoc Improves Scalability of Software Model Checking Security Properties of Secure Systems
  Jason Franklin, Sagar Chaki, Anupam Datta, Jonathan M. McCune, and Amit Vasudevan.
  Under submission, email me for a copy.
  

Refereed Papers in Conferences and Workshops

• Parametric Verification of Address Space Separation - Best Paper Nomination (Top 12 of 600 submissions)
  Jason Franklin, Sagar Chaki, Anupam Datta, Jonathan M. McCune, and Amit Vasudevan.
  To appear in Principles of Security and Trust (POST), 2012.
  PDF Full Version


• Compositional System Security with Interface-Confined Adversaries
  Deepak Garg, Jason Franklin, Dilsun Kaynar, and Anupam Datta.
  Proc. of 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 Slides

  The security of systems such as operating systems, hypervisors, and web browsers depend critically on reference monitors to correctly enforce their desired security policy in the presence of adversaries. Recent progress in developing reference monitors with small code size and narrow interfaces has made automated formal verification of reference monitors a more tractable goal. However, a significant remaining factor for the complexity of automated verification is the size of the data structures (e.g., access control matrices) over which the programs operate. This paper develops a parametric verification technique that scales even when reference monitors and adversaries operate over unbounded, but finite data structures. Specifically, we develop a parametric guarded command language for modeling reference monitors and adversaries. We also present a parametric temporal specification logic for expressing security policies that the monitor is expected to enforce. The central technical results of the paper are a set of small model theorems. These theorems state that in order to verify that a policy is enforced by a reference monitor with an arbitrarily large data structure, it is sufficient to model check the monitor with just one entry in its data structure. We apply our methodology to verify the designs of two hypervisors, SecVisor and the sHype mandatory-access-control extension to Xen. Our approach is able to prove that sHype and a variant of the original SecVisor design correctly enforces the expected security properties in the presence of powerful adversaries.



• FAWN: A Fast Array of Wimpy Nodes - Best Paper Award
  David Andersen, Jason Franklin, Michael Kaminsky, Amar Phanishayee, Lawrence Tan, and Vijay Vasudevan.
  Proceedings of ACM Symposium on Operating System Principles (SOSP), Oct. 2009.
  

  PDF PDF-Web

  This paper presents a new cluster architecture for low-power data-intensive computing. FAWN couples low-power embedded CPUs to small amounts of local flash storage, and balances computation and I/O capabilities to enable efficient, massively parallel access to data.
  The key contributions of this paper are the principles of the FAWN architecture and the design and implementation of FAWN-KV---a consistent, replicated, highly available, and high-performance key-value storage system built on a FAWN prototype. Our design centers around purely log-structured datastores that provide the basis for high performance on flash storage, as well as for replication and consistency obtained using chain replication on a consistent hashing ring. Our evaluation demonstrates that FAWN clusters can handle roughly 350 key-value queries per Joule of energy---two orders of magnitude more than a disk-based system.



• FAWNdamentally Power-efficient Clusters
  Vijay Vasudevan, Jason Franklin, David Andersen, Amar Phanishayee, Lawrence Tan, Michael Kaminsky, and Iulian Moraru.
  Proceedings of HotOS XII, May 2009.
  

  PDF

  Power is becoming an increasingly large financial and scaling burden for computing and society. The costs of running large data centers are becoming dominated by power and cooling to the degree that companies such as Microsoft and Google have built new data centers close to large and cost-efficient hydroelectric power sources. Studies have projected that by 2012, 3-year data center energy costs will be double that of server equipment expenditures. Power consumption and related cooling costs have become a primary design constraint at all levels, limiting the achievable density of data centers and large systems, and pushing processor manufacturers towards alternative architectures. While power constraints have pushed the processor industry toward multi-core architectures, power-efficient alternatives to traditional disk and DRAM-based cluster architectures have been slow to emerge.
  As a power-efficient alternative for data-intensive computing, we propose a cluster architecture called a Fast Array of Wimpy Nodes, or FAWN. A FAWN consists of a large number of slower but efficient nodes that each draw only a few watts of power, coupled with low-power storage---our prototype FAWN nodes are built from 500MHz embedded devices with CompactFlash storage that are typically used as wireless routers, Internet gateways, or thin clients.
  Through our preliminary evaluation, we demonstrate that a FAWN can be up to six times more efficient than traditional systems with Flash storage in terms of \textit{queries per joule} for seek-bound applications and between two to eight times more efficient for I/O throughput-bound applications...



• 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 PS-Full Slides

  We present a logic for reasoning about properties of secure systems. The logic is built around a concurrent programming language with constructs for modeling machines with shared memory, a simple form of access control on memory, machine resets, cryptographic operations, network communication, and dynamically loading and executing unknown (and potentially untrusted) code. The adversary's capabilities are constrained by the system interface as defined in the programming model (leading to the name CSI-ADVERSARY). We develop a sound proof system for reasoning about programs without explicitly reasoning about adversary actions. We use the logic to characterize trusted computing primitives and prove code integrity and execution integrity properties of two remote attestation protocols. The proofsmake precise assumptions needed for the security of these protocols and reveal an insecure interaction between the two protocols.



• A Logic for Reasoning about Networked Secure Systems
  Deepak Garg, Jason Franklin, Dilsun Kaynar, and Anupam Datta
  In FCS-ARSPA-WITS, June 2008.
  Extends Technical Report CMU-CyLab-08-003, Feb. 2008.
  

  PDF PDF-Full Slides

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



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

  PDF PS Slides

  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
  
  
• Remote Detection of Virtual Machine Monitors with Fuzzy Benchmarking
  Jason Franklin, Mark Luk, Jonathan M. McCune, Arvind Seshadri, Adrian Perrig, and Leendert van Doorn.
  In ACM SIGOPS OS Review (Special Issue on Computer Forensics), April 2008.
  Extends CMU Cylab Technical Report CMU-CyLab-07-001, January 2007.
  

  PDF PS

  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.



• 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

  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 Slides Abstract