About

Michael Walfish is a professor in the Computer Science department at the Courant Institute of New York University (NYU), where he has been a faculty member since 2014. Before joining NYU, he served as an assistant professor in the Computer Science department at The University of Texas at Austin starting in 2009. His research interests encompass systems, security, and networking, with a focus on areas such as untrusted peripherals, untrusted computation, untrusted storage, failure detection in distributed systems, naming, network architecture, verifiable auctions, and denial-of-service defense. Throughout his career, Walfish has received several honors including paper awards at SOSP in 2017 and IEEE S&P in 2016, a Sloan Research Fellowship in 2012, an NSF CAREER award in 2011, an Air Force Young Investigator award in 2010, recognition from the Intel Early Career Faculty Honor Program, and a Teaching Excellence Award from the UT College of Natural Sciences. He earned his Bachelor of Arts degree from Harvard University and his Ph.D. in Computer Science from the Massachusetts Institute of Technology (MIT).

Research topics

• Computer Science
• Computer Security
• Programming language
• Algorithm
• Mathematics
• Theoretical computer science
• Philosophy

Selected publications

• Efficient Auditing of Event-driven Web Applications

  2024-04-18

  articleSenior author

  When a deployer of a web application puts that application on a server (on-prem or cloud), how can they be sure that the application is executing as intended? This paper studies how the deployer can efficiently check that the execution is faithful. We seek mechanisms that: (i) work with web applications that are built with modern event-driven web frameworks, (ii) impose tolerable computation and communication overheads on the web server, and (iii) are complete and sound. We exhibit such a mechanism, based on a new record-replay algorithm. We have implemented our algorithm in Karousos, a system that audits Node.js web applications.

  PublisherDOI

• NOPE: Strengthening domain authentication with succinct proofs

  2024-11-04 · 2 citations

  articleOpen accessSenior author

  Server authentication assures users that they are communicating with a server that genuinely represents a claimed domain. Today, server authentication relies on certification authorities (CAs), third parties who sign statements binding public keys to domains. CAs remain a weak spot in Internet security, as any faulty CA can issue a certificate for any domain.

  PublisherOA PDFDOI

• Less is more: refinement proofs for probabilistic proofs

  2022 IEEE Symposium on Security and Privacy (SP) · 2023 · 3 citations

  • Computer Science
  • Computer Science
  • Theoretical computer science

  There has been intense interest over the last decade in implementations of probabilistic proofs (IPs, SNARKs, PCPs, and so on): protocols in which an untrusted party proves to a verifier that a given computation was executed properly, possibly in zero knowledge. Nevertheless, implementations still do not scale beyond small computations. A central source of overhead is the front-end: translating from the abstract computation to a set of equivalent arithmetic constraints. This paper introduces a general-purpose framework, called Distiller, in which a user translates to constraints not the original computation but an abstracted specification of it. Distiller is the first in this area to perform such transformations in a way that is provably safe. Furthermore, by taking the idea of "encode a check in the constraints" to its literal logical extreme, Distiller exposes many new opportunities for constraint reduction, resulting in cost reductions for benchmark computations of 1.3–50×, and in some cases, better asymptotics.

  PublisherDOI

• Zero-Knowledge Middleboxes.

  IACR Cryptology ePrint Archive · 2021 · 6 citations

  Senior authorCorresponding
  • Computer Science
  • Computer Science
  • Algorithm
  Publisher

• Cobra: Making transactional key-value stores verifiably serializable

  Operating Systems Design and Implementation · 2020 · 11 citations

  Senior authorCorresponding
  • Computer Science
  • Computer Science
  • Computer Security
  Publisher

• Detecting Incorrect Behavior of Cloud Databases as an Outsider

  arXiv (Cornell University) · 2019-12-19

  preprintOpen accessSenior author

  Cloud DBs offer strong properties, including serializability, sometimes called the gold standard database correctness property. But cloud DBs are complicated black boxes, running in a different administrative domain from their clients; thus, clients might like to know whether the DBs are meeting their contract. A core difficulty is that the underlying problem here, namely verifying serializability, is NP-complete. Nevertheless, we hypothesize that on real-world workloads, verifying serializability is tractable, and we treat the question as a systems problem, for the first time. We build Cobra, which tames the underlying search problem by blending a new encoding of the problem, hardware acceleration, and a careful choice of a suitable SMT solver. cobra also introduces a technique to address the challenge of garbage collection in this context. cobra improves over natural baselines by at least 10x in the problem size it can handle, while imposing modest overhead on clients.

  PublisherOA PDFDOI

• Doubly-Efficient zkSNARKs Without Trusted Setup

  2018-05-01 · 247 citations

  articleSenior author

  We present a zero-knowledge argument for NP with low communication complexity, low concrete cost for both the prover and the verifier, and no trusted setup, based on standard cryptographic assumptions. Communication is proportional to d log G (for d the depth and G the width of the verifying circuit) plus the square root of the witness size. When applied to batched or data-parallel statements, the prover's runtime is linear and the verifier's is sub-linear in the verifying circuit size, both with good constants. In addition, witness-related communication can be reduced, at the cost of increased verifier runtime, by leveraging a new commitment scheme for multilinear polynomials, which may be of independent interest. These properties represent a new point in the tradeoffs among setup, complexity assumptions, proof size, and computational cost. We apply the Fiat-Shamir heuristic to this argument to produce a zero-knowledge succinct non-interactive argument of knowledge (zkSNARK) in the random oracle model, based on the discrete log assumption, which we call Hyrax. We implement Hyrax and evaluate it against five state-of-the-art baseline systems. Our evaluation shows that, even for modest problem sizes, Hyrax gives smaller proofs than all but the most computationally costly baseline, and that its prover and verifier are each faster than three of the five baselines.

  PublisherDOI

• Doubly-efficient zkSNARKs without trusted setup.

  2017-01-01 · 1 citations

  preprintSenior author

  We present a zero-knowledge argument for NP with low communication complexity, low concrete cost for both the prover and the verifier, and no trusted setup, based on standard cryptographic assumptions. Communication is proportional to d log G (for d the depth and G the width of the verifying circuit) plus the square root of the witness size. When applied to batched or data-parallel statements, the prover's runtime is linear and the verifier's is sub-linear in the verifying circuit size, both with good constants. In addition, witness-related communication can be reduced, at the cost of increased verifier runtime, by leveraging a new commitment scheme for multilinear polynomials, which may be of independent interest. These properties represent a new point in the tradeoffs among setup, complexity assumptions, proof size, and computational cost. We apply the Fiat-Shamir heuristic to this argument to produce a zero-knowledge succinct non-interactive argument of knowledge (zkSNARK) in the random oracle model, based on the discrete log assumption, which we call Hyrax. We implement Hyrax and evaluate it against five state-of-the-art baseline systems. Our evaluation shows that, even for modest problem sizes, Hyrax gives smaller proofs than all but the most computationally costly baseline, and that its prover and verifier are each faster than three of the five baselines.

• Full accounting for verifiable outsourcing.

  IACR Cryptology ePrint Archive · 2017-01-01

  preprint

  Systems for verifiable outsourcing incur costs for a prover, a verifier, and precomputation; outsourcing makes sense when the combination of these costs is cheaper than not outsourcing. Yet, when prior works impose quantitative thresholds to analyze whether outsourcing is justified, they generally ignore prover costs. Verifiable ASICs (VA)---in which the prover is a custom chip---is the other way around: its cost calculations ignore precomputation. This paper describes a new VA system, called Giraffe; charges Giraffe for all three costs; and identifies regimes where outsourcing is worthwhile. Giraffe's base is an interactive proof geared to data-parallel computation. Giraffe makes this protocol asymptotically optimal for the prover and improves the verifier's main bottleneck by almost 3x, both of which are of independent interest. Giraffe also develops a design template that produces hardware designs automatically for a wide range of parameters, introduces hardware primitives molded to the protocol's data flows, and incorporates program analyses that expand applicability. Giraffe wins even when outsourcing several tens of sub-computations, scales to 500x larger computations than prior work, and can profitably outsource parts of programs that are not worthwhile to outsource in full.

  Publisher

• The Efficient Server Audit Problem, Deduplicated Re-execution, and the Web

  2017-10-12 · 22 citations

  preprintOpen accessSenior author

  You put a program on a concurrent server, but you don't trust the server; later, you get a trace of the actual requests that the server received from its clients and the responses that it delivered. You separately get logs from the server; these are untrusted. How can you use the logs to efficiently _verify_ that the responses were derived from running the program on the requests? This is the _Efficient Server Audit Problem_, and it abstracts real-world scenarios, including running a web application on an untrusted provider. We give a solution based on several new techniques, including simultaneous replay and efficient verification of concurrent executions. We implement the solution for PHP web applications. For several applications, our verifier achieves 5.6--10.9x speedup versus simply re-executing, with less than 10 percent overhead for the server.

  PublisherOA PDFDOI

Recent grants

• FIA: Collaborative Research: NEBULA: A Future Internet That Supports Trustworthy Cloud Computing

  NSF · $664k · 2010–2014

• TWC: Small: Accelerating Cryptographic Protocols with Reconfigurable Hardware

  NSF · $498k · 2014–2019

• CiC: FRCC: Cloud Storage with Minimal Trust

  NSF · $370k · 2011–2014

• TWC: Medium: Scaling proof-based verifiable computation

  NSF · $1.2M · 2015–2021

• CAREER: Practical verification of outsourced computations

  NSF · $450k · 2011–2017

Frequent coauthors

• Andrew J. Blumberg

  Herbert Irving Comprehensive Cancer Center

  20 shared

• Srinath Setty

  16 shared

• Scott Shenker

  University of California, Berkeley

  16 shared

• Riad S. Wahby

  Carnegie Mellon University

  12 shared

• David Mazières

  Stanford University

  10 shared

• Joshua B. Leners

  Two Sigma Investments (United States)

  10 shared

• Hari Balakrishnan

  IIT@MIT

  10 shared

• Marcos K. Aguilera

  8 shared

Labs

• NYU Computer SciencePI

Education

• B.S.

  Harvard University

• Ph.D., Computer Science

  MIT