About

Ethan Cecchetti is an Assistant Professor in the Computer Sciences department at the University of Wisconsin–Madison. His research focuses on areas related to computer security, programming languages, and decentralized systems. He has contributed to the development of programming frameworks for zkSNARKs, smart contracts with secure control flow, and mechanisms for provable integrity protection in decentralized systems. His work spans topics such as nonmalleable information flow control, compositional security for reentrant applications, and robust compilation under universal composability frameworks. Cecchetti's research also addresses challenges in secure remote attestation, oblivious serializable transactions in cloud environments, and authenticated data feeds for smart contracts. Through his publications and technical reports, he has advanced the understanding of secure programming models and cryptographic protocols, often collaborating with other researchers to explore the intersection of security, programming languages, and distributed ledger technologies.

Research topics

• Computer Security
• Computer Science
• Programming language
• Theoretical computer science

Selected publications

• Generating Compilers for Qubit Mapping and Routing

  Proceedings of the ACM on Programming Languages · 2026-01-08 · 1 citations

  articleOpen access

  To evaluate a quantum circuit on a quantum processor, one must find a mapping from circuit qubits to processor qubits and plan the instruction execution while satisfying the processor's constraints. This is known as the qubit mapping and routing (QMR) problem. High-quality QMR solutions are key to maximizing the utility of scarce quantum resources and minimizing the probability of logical errors affecting computation. The challenge is that the landscape of quantum processors is incredibly diverse and fast-evolving. Given this diversity, dozens of papers have addressed the QMR problem for different qubit hardware, connectivity constraints, and quantum error correction schemes by a developing a new algorithm for a particular context. We present an alternative approach: automatically generating qubit mapping and routing compilers for arbitrary quantum processors. Though each QMR problem is different, we identify a common core structure—device state machine—that we use to formulate an abstract QMR problem. Our formulation naturally leads to a compact domain-specific language for specifying QMR problems and a powerful parametric algorithm that can be instantiated for any QMR specification. Our thorough evaluation on case studies of important QMR problems shows that generated compilers are competitive with handwritten, specialized compilers in terms of runtime and solution quality.

  PublisherDOI

• Choreographic Quick Changes: First-Class Location (Set) Polymorphism

  ArXiv.org · 2025-06-12

  preprintOpen accessSenior author

  Choreographic programming is a promising new paradigm for programming concurrent systems where a developer writes a single centralized program that compiles to individual programs for each node. Existing choreographic languages, however, lack critical features integral to modern systems, like the ability of one node to dynamically compute who should perform a computation and send that decision to others. This work addresses this gap with $λ_{QC}$, the first typed choreographic language with \emph{first class process names} and polymorphism over both types and (sets of) locations. $λ_{QC}$ also improves expressive power over previous work by supporting algebraic and recursive data types as well as multiply-located values. We formalize and mechanically verify our results in Rocq, including the standard choreographic guarantee of deadlock freedom.

  PublisherOA PDFDOI

• zkStruDul: Programming zkSNARKs with Structural Duality

  ArXiv.org · 2025-11-13

  preprintOpen accessSenior author

  Non-Interactive Zero Knowledge (NIZK) proofs, such as zkSNARKS, let one prove knowledge of private data without revealing it or interacting with a verifier. While existing tooling focuses on specifying the predicate to be proven, real-world applications optimize predicate definitions to minimize proof generation overhead, but must correspondingly transform predicate inputs. Implementing these two steps separately duplicates logic that must precisely match to avoid catastrophic security flaws. We address this shortcoming with zkStruDul, a language that unifies input transformations and predicate definitions into a single combined abstraction from which a compiler can project both procedures, eliminating duplicate code and problematic mismatches. zkStruDul provides a high-level abstraction to layer on top of existing NIZK technology and supports important features like recursive proofs. We provide a source-level semantics and prove its behavior is identical to the projected semantics, allowing straightforward standard reasoning.

  PublisherOA PDFDOI

• Nonmalleable Progress Leakage

  2025-06-16

  preprintOpen access1st authorCorresponding

  Information-flow control systems often enforce progress-insensitive noninterference, as it is simple to understand and enforce. Unfortunately, real programs need to declassify results and endorse inputs, which noninterference disallows, while preventing attackers from controlling leakage, including through progress channels, which progress-insensitivity ignores. This work combines ideas for progress-sensitive security with secure downgrading (declassification and endorsement) to identify a notion of securely downgrading progress information. We use hyperproperties to distill the separation between progress-sensitive and progress-insensitive noninterference and combine it with nonmalleable information flow, an existing (progress-insensitive) definition of secure downgrading, to define nonmalleable progress leakage (NMPL). We present the first information-flow type system to allow some progress leakage while enforcing NMPL, and we show how to infer the location of secure progress downgrades. All theorems are verified in Rocq.

  PublisherOA PDFDOI

• Choreographic Quick Changes: First-Class Location (Set) Polymorphism

  Proceedings of the ACM on Programming Languages · 2025-10-09

  articleOpen accessSenior author

  Choreographic programming is a promising new paradigm for programming concurrent systems where a developer writes a single centralized program that compiles to individual programs for each node. Existing choreographic languages, however, lack critical features integral to modern systems, like the ability of one node to dynamically compute who should perform a computation and send that decision to others. This work addresses this gap with λ QC , the first typed choreographic language with first class process names and polymorphism over both types and (sets of) locations. λ QC also improves expressive power over previous work by supporting algebraic and recursive data types as well as multiply-located values. We formalize and mechanically verify our results in Rocq, including the standard choreographic guarantee of deadlock freedom.

  PublisherDOI

• Computationally Bounded Robust Compilation and Universally Composable Security

  arXiv (Cornell University) · 2024-01-26

  preprintOpen accessSenior author

  Universal Composability (UC) is the gold standard for cryptographic security, but mechanizing proofs of UC is notoriously difficult. A recently-discovered connection between UC and Robust Compilation (RC)$\unicode{x2014}$a novel theory of secure compilation$\unicode{x2014}$provides a means to verify UC proofs using tools that mechanize equality results. Unfortunately, the existing methods apply only to perfect UC security, and real-world protocols relying on cryptography are only computationally secure. This paper addresses this gap by lifting the connection between UC and RC to the computational setting, extending techniques from the RC setting to apply to computational UC security. Moreover, it further generalizes the UC$\unicode{x2013}$RC connection beyond computational security to arbitrary equalities, providing a framework to subsume the existing perfect case, and to instantiate future theories with more complex notions of security. This connection allows the use of tools for proofs of computational indistinguishability to properly mechanize proofs of computational UC security. We demonstrate this power by using CryptoVerif to mechanize a proof that parts of the Wireguard protocol are computationally UC secure. Finally, all proofs of the framework itself are verified in Isabelle/HOL.

  PublisherOA PDFDOI

• System-Level Defense against Indirect Prompt Injection Attacks: An Information Flow Control Perspective

  arXiv (Cornell University) · 2024-09-27 · 1 citations

  preprintOpen access

  Large Language Model-based systems (LLM systems) are information and query processing systems that use LLMs to plan operations from natural-language prompts and feed the output of each successive step into the LLM to plan the next. This structure results in powerful tools that can process complex information from diverse sources but raises critical security concerns. Malicious information from any source may be processed by the LLM and can compromise the query processing, resulting in nearly arbitrary misbehavior. To tackle this problem, we present a system-level defense based on the principles of information flow control that we call an f-secure LLM system. An f-secure LLM system disaggregates the components of an LLM system into a context-aware pipeline with dynamically generated structured executable plans, and a security monitor filters out untrusted input into the planning process. This structure prevents compromise while maximizing flexibility. We provide formal models for both existing LLM systems and our f-secure LLM system, allowing analysis of critical security guarantees. We further evaluate case studies and benchmarks showing that f-secure LLM systems provide robust security while preserving functionality and efficiency. Our code is released at https://github.com/fzwark/Secure_LLM_System.

  PublisherOA PDFDOI

• Universal Composability Is Robust Compilation

  ACM Transactions on Programming Languages and Systems · 2024-10-10

  articleOpen accessSenior author

  This article discusses the relationship between two frameworks: universal composability ( \(\mathsf{UC}\) ) and robust compilation ( RC ). In cryptography, \(\mathsf{UC}\) is a framework for the specification and analysis of cryptographic protocols with a strong compositionality guarantee: \(\mathsf{UC}\) protocols remain secure even when composed with other protocols. In programming language security, RC is a novel framework for determining secure compilation by proving whether compiled programs are as secure as their source-level counterparts no matter what target-level code they interact with. Presently, these disciplines are studied in isolation, though we argue that there is a deep connection between them and exploring this connection will benefit both research fields. This article formally proves the connection between \(\mathsf{UC}\) and RC and then it explores the benefits of this connection (focussing on perfect, rather than computational \(\mathsf{UC}\) ). For this, this article first identifies which conditions must programming languages fulfil in order to possibly attain \(\mathsf{UC}\) -like composition. Then, it proves \(\mathsf{UC}\) of both an existing and a new commitment protocol as a corollary of the related compilers attaining RC . Finally, it mechanises these proofs in DEEPSEC, obtaining symbolic guarantees that the protocol is indeed \(\mathsf{UC}\) . Our connection lays the groundwork towards a better and deeper understanding of both \(\mathsf{UC}\) and RC , and the benefits we showcase from this connection provide evidence of scalable mechanised proofs for \(\mathsf{UC}\) .

  PublisherOA PDFDOI

• Computationally Bounded Robust Compilation and Universally Composable Security

  2024-07-08 · 1 citations

  articleOpen accessSenior author

  Universal Composability (UC) is the gold standard for cryptographic security, but mechanizing proofs of UC is notoriously difficult. A recently-discovered connection between UC and Robust Compilation (RC)-a novel theory of secure compilation-provides a means to verify UC proofs using tools that mechanize equality results. Unfortunately, the existing methods apply only to perfect UC security, and real-world protocols relying on cryptography are only computationally secure. This paper addresses this gap by lifting the connection between UC and RC to the computational setting, extending techniques from the RC setting to apply to computational UC security. Moreover, it further generalizes the UC-RC connection beyond computational security to arbitrary equalities, providing a framework to subsume the existing perfect case, and to instantiate future theories with more complex notions of security. This connection allows the use of tools for proofs of computational indistinguishability to properly mechanize proofs of computational UC security. We demonstrate this power by using CRYPTOVERIF to mechanize a proof that parts of the Wireguard protocol are computationally UC secure. Finally, all proofs of the framework itself are verified in Isabelle/HOL.

  PublisherOA PDFDOI

• Compositional Security for Reentrant Applications

  2021-05-01 · 1 citations

  preprintOpen access1st authorCorresponding

  The disastrous vulnerabilities in smart contracts sharply remind us of our ignorance: we do not know how to write code that is secure in composition with malicious code. Information flow control has long been proposed as a way to achieve compositional security, offering strong guarantees even when combining software from different trust domains. Unfortunately, this appealing story breaks down in the presence of reentrancy attacks. We formalize a general definition of reentrancy and introduce a security condition that allows software modules like smart contracts to protect their key invariants while retaining the expressive power of safe forms of reentrancy. We present a security type system that provably enforces secure information flow; in conjunction with run-time mechanisms, it enforces secure reentrancy even in the presence of unknown code; and it helps locate and correct recent high-profile vulnerabilities.

  PublisherOA PDFDOI

Frequent coauthors

• Ari Juels

  9 shared

• Andrew C. Myers

  7 shared

• Elaine Shi

  4 shared

• Fan Zhang

  Yale University

  4 shared

• Haobin Ni

  4 shared

• Natacha Crooks

  University of California, Berkeley

  4 shared

• Siqiu Yao

  4 shared

• Owen Arden

  4 shared

Labs

• Ethan Cecchetti LabPI

  Research in programming languages, software engineering, and distributed systems

Education

• PhD, Computer Science

  Cornell University

  2021

• Master of Science, Computer Science

  Cornell University

  2019

• Bachelor of Science, Mathematics - Computer Science

  Brown University

  2012

Awards & honors

• 2017 NDSEG Fellowship