Cornell Systems Lunch

CS 7490 Spring 2016
Friday 12PM, Gates 114

Emin Gun Sirer and Robbert van Renesse

Sponsored by Microsoft

The Systems Lunch is a seminar for discussing recent, interesting papers in the systems area, broadly defined to span operating systems, distributed systems, networking, architecture, databases, and programming languages. The goal is to foster technical discussions among the Cornell systems research community. We meet once a week on Fridays at noon in Gates 114.

The systems lunch is open to all Cornell Ph.D. students interested in systems. First-year graduate students are especially welcome. Non-Ph.D. students have to obtain permission from the instructor. Student participants are expected to sign up for CS 7490, Systems Research Seminar, for one credit.

To join the systems lunch mailing list please send an empty message to with the subject line "join". More detailed instructions can be found here.

Links to papers and abstracts below are unlikely to work outside the Cornell CS firewall. If you have trouble viewing them, this is the likely cause.

Date Paper Presenter
January 29 IronFleet: Proving Practical Distributed Systems Correct
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jay Lorch, Bryan Parno, Michael Roberts, Srinath Setty, Brian Zill (Microsoft Research)

Distributed systems are notorious for harboring subtle bugs. Verification can, in principle, eliminate these bugs a priori, but verification has historically been difficult to apply at full-program scale, much less distributed-system scale. This talk will describe IronFleet, our methodology for building practical and provably correct distributed systems based on a unique blend of TLA-style state-machine refinement and Hoare-logic verification. We demonstrate this methodology on a complex implementation of a Paxos-based replicated state machine library and a lease-based sharded key-value store. We prove that each obeys a concise safety specification, as well as desirable liveness requirements. Each implementation achieves performance competitive with a reference system. With our methodology and lessons learned, we aim to raise the standard for distributed systems from "tested" to "correct." The talk will also briefly discuss the broader Ironclad project, of which IronFleet is part, including its past successes and future plans. The goal of the Ironclad project is to realize the power of automated software verification to build verifiable, secure, and practical system software. We have open-sourced our code, and made it available at, to encourage other researchers to further extend the state of the art in systems verification.

BIO: Jay Lorch is a Senior Researcher at Microsoft Research in Redmond, WA. Before joining Microsoft, he received his Ph.D. in Computer Science from UC Berkeley in 2001 under the supervision of Alan Jay Smith. His research focuses broadly on computer systems, with particular emphasis on distributed systems, security, cloud computing, and energy management. In recent work, he has developed TrInc (NSDI 2009), a simple piece of trusted hardware useful in securing a variety of distributed systems; Memoir (IEEE S&P 2011), a framework for building stateful, crash-resilient trusted modules; GreenUp (NSDI 2012), a decentralized system for maintaining the availability of machines while letting them save energy by sleeping; and Ironclad (OSDI 2014), a system for verifying that every instruction a server executes conforms to a high-level specification.

Jay Lorch (Microsoft)
February 5 Information Centric Networking: Addressing Information at the Network Level
Antonio Carzaniga (Università della Svizzera Italiana)

Imagine a network in which you address information. Literally, packet-level addressing of information rather than hosts. For example, you may request the front page of The New York Times with a request packet addressed to "the front page of the New York Times"! (Sort of.) Then the network forwards the request to some server that can produce the right data (possibly cached) and then delivers that data back to you. You do not have to figure out where that information is; the network does that for you. Or you may announce a talk ("push") with a packet addressed to whomever is interested in the topics of the talk. You do not have to keep track of who might be interested, nor you have to send many copies of your announcement. An information centric networking would do all of that for you. An information centric network would offer a rich service, ideal for many applications. But would that scale? Would it even work? How? In this talk I will present some basic ideas on how to architect a rich and expressive information centric network. I will focus primarily on routing and forwarding.

Antonio Carzaniga (USI)
February 12 Inference Attacks on Property-Preserving Encrypted Databases
Muhammad Naveed, Seny Kamara, and Charles V. Wright
ACM Conference on Computer and Communications Security (CCS), 2015
Muhammad Naveed
February 19 Minimizing Faulty Executions of Distributed Systems
Colin Scott (Berkeley), Aurojit Panda (Berkeley), Vjekoslav Brajkovic (ICSI), George Necula (Berkeley), Arvind Krishnamurthy (UW), and Scott Shenker (Berkeley, ICSI)

When a bug is found in a long-running distributed system, developers typically start by identifying (i) which events in the execution caused their system to arrive at the unsafe state, and (ii) which events are irrelevant. This process of troubleshooting can be highly time-consuming, as developers spend hours poring over multigigabyte traces containing thousands of events.

I will present a tool that reduces effort spent on troubleshooting distributed systems, by automatically eliminating events from a given buggy execution that are not causally related to the bug at hand. The developer is left with a `minimal causal sequence' of triggering events, each of which is necessary for triggering the bug. We claim that the greatly reduced size of the trace makes it easier for the developer to figure out which code path contains the underlying bug, allowing them to focus their effort on the task of fixing the problematic code itself.

In the talk I formally define the execution minimization problem, the algorithms we have developed to solve it, and the system we have built to apply our techniques in practice. The examples I present are drawn from real bugs we have found and minimized in Raft and Spark.

Colin Scott (Berkeley)
February 26 The Evolution of Advanced Caching in the Facebook CDN
Qi Huang et al. (Facebook)

Facebook users access media content (photos, videos) billions of times per day, posing unique technical challenges at large scale. Over the past several years, researchers and engineers at Facebook have redesigned and evolved our infrastructure to serve such content more efficiently, including evolving our own CDN (Content Delivery Network), storage, and revamping our media processing engine. In this talk, I will focus on the development happened in the CDN domain, which was actually driven by a research collaborations with Cornell starting from 2012. Particularly, I will walk through three iterations of caching solutions we built and deployed inside Facebook CDN: McDipper, BlockCache, and RIPQ, and illustrated how we evolved an in-production system stack at different times due to changing workload, hardware specs, and new research discoveries.

Qi Huang (Facebook)
March 4 Blindly Signed Contracts: Anonymous On-Blockchain and Off-Blockchain Bitcoin Transactions
Ethan Heilman (BU)

Although Bitcoin is often perceived to be an anonymous currency, research has shown that a user’s Bitcoin transactions can be linked to compromise the user’s anonymity. We present solutions to the anonymity problem for both transactions on Bitcoin’s blockchain and off the blockchain (in so called micropayment channel networks). We use an untrusted third party to issue anonymous vouchers which users redeem for Bitcoin. Blind signatures and Bitcoin transaction contracts (aka smart contracts) ensure the anonymity and fairness during the bitcoin ↔ voucher exchange. Our schemes are practical, secure and anonymous.

Ethan Heilman (BU)
March 11 The Design and Implementation of the Warp Transactional Filesystem
Robert Escriva and Emin Gun Sirer
NSDI 2016
Robert Escriva
Bitcoin-NG: A Scalable Blockchain Protocol
Ittay Eyal, Efe Gencer, Emin Gun Sirer, and Robbert van Renesse
NSDI 2016
Ittay Eyal
March 18 Shielding Applications from an Untrusted Cloud with Haven
Andrew Baumann, Marcus Peinado, and Galen Hunt, Microsoft Research
OSDI 2014
Zhiming Shen
March 25 A fast and scalable payment network with bitcoin duplex micropayment channels
C. Decker and R. Wattenhofer
In Stabilization, Safety, and Security of Distributed Systems, pages 3–18. Springer, 2015
Efe Gencer
April 1 Spring Break, no meeting.
April 8 ACSU Luncheon—no systems lunch, no meeting.
April 15 All Your Queries Are Belong to Us: The Power of File-Injection Attacks on Searchable Encryption

The goal of searchable encryption (SE) is to enable a client to execute searches over encrypted files stored on an untrusted server while ensuring some measure of privacy for both the encrypted files and the search queries. Research has focused on developing efficient SE schemes at the expense of allowing some small, well-characterized “(information) leakage” to the server about the files and/or the queries. The practical impact of this leakage, however, remains unclear.

We thoroughly study file-injection attacks—in which the server sends files to the client that the client then encrypts and stores—on the query privacy of single-keyword and conjunctive SE schemes. We show such attacks can reveal the client’s queries in their entirety using very few injected files, even for SE schemes having low leakage. We also demonstrate that natural countermeasures for preventing file-injection attacks can be easily circumvented. Our attacks outperform prior work significantly in terms of their effectiveness as well as in terms of their assumptions about the attacker’s prior knowledge.

Yupeng Zhang (UMD)
April 22 Lattice Priority Scheduling: Low-Overhead Timing-Channel Protection for a Shared Memory Controller
Andrew Ferraiuolo, Yao Wang, Danfeng Zhang, Andrew C. Myers, and G. Edward Suh
HPCA 2016
Andrew Ferraiuolo
April 29 Physical Side Channel Attacks on PCs and Mobile Devices
Daniel Genkin

Can secret information be extracted from PCs and mobile devices by measuring their physical properties from the outside? What would it take to extract whole keys from such fast and complex devices? We present myriad ways to do so, including: * Acoustic key extraction, using microphones to record the high-pitched noise caused by vibration of electronic circuit components during decryption. * Electric key extraction exploiting fluctuations in the "ground" electric potential of computers. An attacker can measure this signal by touching the computer's chassis, or the shield on the remote end of Ethernet, VGA or USB cables. * Electromagnetic key extraction, using a cheap radios to non-intrusively attack computers and mobile devices. The talk will discuss the cryptanalytic, physical and signal-processing principles of the attacks, and include live demonstrations. The talk is based on joint works with Lev Pachmanov, Itamar Pipman, Adi Shamir Eran Tromer and Yuval Yarom.

BIO: Daniel Genkin is a Ph.D student at the Computer Science Department, Technion and a Research Assistant at the School of Computer Science, Tel Aviv University. Daniel's research focuses on practical and theoretical aspects of cryptography, including side channel attacks and secure multiparty computation.

Daniel Genkin (Technion)
May 6 Programming Line-Rate Routers
Anirudh Sivaraman

Historically, the evolution of network routers and switches has been driven primarily by performance. Recently, thanks in part to the emergence of large data centers, the need for better control over network operations, and the desire for new features, programmability of switches has become as important as performance. In response, researchers and practitioners have developed reconfigurable switching chips that are performance-competitive with line-rate fixed-function switching chips. These chips provide some programmability through restricted hardware primitives that can be configured with software directives.

This talk will focus on two abstractions for programming such chips. The first abstraction, packet transactions, lets programmers express packet processing in an imperative language under the illusion that the switch processes exactly one packet at a time. A compiler then translates this sequential programmer view into a pipelined implementation on a switching chip that processes multiple packets concurrently. The second abstraction, a push-in first-out queue, allows programmers to program new scheduling algorithms using a priority queue coupled with a program to compute each packet's priority in the priority queue. For the first time, these two abstractions allow us to program several packet-processing functions at line rate. These packet-processing functions include in-network congestion control, active queue management, data-plane load balancing, network measurement, and packet scheduling.

This talk includes joint work with collaborators at MIT, Barefoot Networks, Cisco Systems, Microsoft Research, Stanford, and University of Washington. Preprints describing the work in further detail are available at: and


Anirudh Sivaraman is a graduate student in MIT’s Computer Science and Artificial Intelligence Laboratory. He is broadly interested in computer networking and his recent research work focuses on software abstractions and hardware primitives for programmable line-rate routers.

Anirudh Sivaraman (MIT)