Portrait of Jay Lorch

Jay Lorch

Principal Researcher

About

I'm a Principal Researcher in the Systems Research Group at Microsoft Research. My research focuses broadly on computer systems, with particular emphasis on distributed systems, software verification, trusted computing, privacy, cloud computing, and energy management.

I love projects that involve building systems, and a major interest of mine is achieving fault tolerance in those systems. I've shown how to deal with server failures in SMART and Shroud, trusted-component power failures in TrInc and Memoir, and improperly behaving participants in decentralized systems like GreenUp and FARSITE. I'm an expert in Paxos and its many variants, having used it in several systems; most recently, in the IronFleet project, my team and I produced the first-ever implementation of Paxos with a machine-checked proof of both its safety and liveness.

In much of my work, I leverage the power of trusted computing to solve difficult problems in security and privacy. The TrInc work shows how a simple trusted device could be leveraged for a great variety of purposes, including efficiently tolerating Byzantine faults, preventing Sybil attacks, preventing BitTorrent under-reporting, and allowing untrusted entities to provide trusted services. The Shroud system demonstrates how a server can use secure hardware to hide difficult-to-hide information hackers can otherwise glean from access patterns, such as who's friends with whom and where someone is looking for local information. And, the Ironclad project shows how to use full-system software verification to enable provably justifiable trust in services that run on trusted platforms in the cloud.

Projects

Project Everest – Verified Secure Implementations of the HTTPS Ecosystem

Established: May 31, 2016

Summary Project Everest aims to build and deploy a verified HTTPS stack. The HTTPS ecosystem (HTTPS and TLS protocols, X.509 public key infrastructure, crypto algorithms) is the foundation on which Internet security is built. Unfortunately, this ecosystem is extremely brittle, with headline-grabbing attacks such as FREAK and LogJam and emergency patches many times a year. Project Everest proposes to solve this problem by constructing a high-performance, standards-compliant, and verified implementation of the full HTTPS ecosystem. We…

Blockchains, consensus, and probabilistic proofs

Established: February 3, 2016

Summary Blockchain technology is expected to dramatically transform many common business processes. The fundamental reason is it promises to enable a new form of trustworthy business processes among multiple, mutually distrusting entities by offering the much-needed automation, auditability, transparency, and integrity without requiring enormous trust in the participating entities. However, existing proposals do not fully deliver the promises of blockchain technology. We are investigating new distributed systems and cryptographic techniques to build a secure and efficient blockchain.…

Ironclad

Established: October 2, 2014

An Ironclad App lets a user securely transmit her data to a remote machine with the guarantee that every instruction executed on that machine adheres to a formal abstract specification of the app's behavior. This does more than eliminate implementation vulnerabilities such as buffer overflows, parsing errors, or data leaks; it tells the user exactly how the app will behave at all times. Our specifications, code, proofs, and tools for our projects Ironclad Apps (verifying the…

Zero-Effort Payments

Established: September 16, 2014

Zero-Effort Payments (ZEP) is a seamless mobile computing system designed to accept payments with no effort on the customer’s part beyond a one-time opt-in. With ZEP, customers need not present cards nor operate smartphones to convey their identities. ZEP uses three complementary identification technologies: face recognition, proximate device detection, and human assistance.

Drawbridge

Established: September 19, 2011

Drawbridge is a research prototype of a new form of virtualization for application sandboxing. Drawbridge combines two core technologies: First, a picoprocess, which is a process-based isolation container with a minimal kernel API surface. Second, a library OS, which is a version of Windows enlightened to run efficiently within a picoprocess. Hardware-based Virtual Machines (VMs) have fundamentally changed computing in data centers and enabled the cloud. VMs offer three compelling qualities: Secure Isolation: isolating applications…

GreenUp

Established: June 14, 2011

The GreenUp project provides a comprehensive energy/sleep monitoring and seamless wake up solution for a corporate network environment. Machines can be allowed to aggressively go to sleep safe in the knowledge that they can be seamlessly woken on-demand whenever they are accessed. By allowing machines to sleep more often significant energy savings can be achieved. Energy savings and usage can be readily monitored on the client as well as via a central database. How does…

Dafny: A Language and Program Verifier for Functional Correctness

Established: December 23, 2008

Dafny is a programming language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs. The Dafny programming language is designed to support the static verification of programs. It is imperative, sequential, supports generic classes, dynamic allocation, and inductive datatypes, and builds in specification constructs. The specifications include pre- and postconditions, frame specifications (read and write sets), and termination metrics. To further support specifications, the language also offers…

Publications

2017

Everest: Towards a Verified, Drop-In Replacement of HTTPS
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Beguelin, Jean-Karim Zinzindohoué, in SNAPL 2017, May 2, 2017, View abstract, Download PDF, View external link

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2004

2003

2002

2001

2000

1998

1997

1996

1995

1994

Projects

Downloads

Memoir

April 2011

    Click the icon to access this download

  • Website

TrustSim

April 2011

    Click the icon to access this download

  • Website

Other

  • Program Committee Member for SOSP 2017, IEEE S&P 2016 & 2017, NSDI 2016 & 2017, WWW 2015, FAST 2014, NDSS 2014, HotOS 2013, ICDCS 2013, Eurosys 2011, IPTPS 2008 & 2009, P2P 2012 & 2013, and MMVE 2010 & 2012
  • Treasurer for SOSP 2015
  • Program Committee Chair for P2P 2015
  • Panelist for NSF Expeditions in Computing 2011
  • Registration Chair for SOSP 2009
  • Sponsorships Chair for SOSP 2007