A verified algebraic representation of Cairo program execution (CPP 2022)

Sun 16 - Fri 28 January 2022 Philadelphia, Pennsylvania, United States

Who

Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman

Track

CPP 2022

Time Zone

The program is currently displayed in (GMT-05:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Mon 17 Jan 2022 15:55 - 16:20 at Salon III - Security and Distributed Systems Chair(s): Alwyn Goodloe

Abstract

Cryptographic interactive proof systems provide an efficient and scalable means of verifying the results of computation on blockchain. A prover constructs a proof, off-chain, that the execution of a program on a given input terminates with a certain result. The prover then publishes a certificate that can be verified efficiently and reliably modulo commonly accepted cryptographic assumptions. The method relies on an algebraic encoding of execution traces of programs. Here we report on a verification of the correctness of such an encoding of the Cairo model of computation with respect to the STARK interactive proof system, using the Lean 3 proof assistant.

Link to Preprint

https://arxiv.org/abs/2109.14534

Jeremy Avigad

Carnegie Mellon University, USA

Lior Goldberg

Starkware Industries Ltd.

David Levit

Starkware Industries Ltd.

Yoav Seginer

cdl-lang.org, Netherlands

Alon Titelman

Starkware Industries Ltd.

Time Zone

The program is currently displayed in (GMT-05:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

Mon 17 Jan
Displayed time zone: Eastern Time (US & Canada) change

15:30 - 17:10	Security and Distributed SystemsCPP at Salon III Chair(s): Alwyn Goodloe NASA Langley Research Center

15:30 25m Talk		Reflection, Rewinding, and Coin-Toss in EasyCryptRemote CPP Denis Firsov Tallinn University of Technology, Dominique Unruh University of Tartu Pre-print Media Attached
15:55 25m Talk		A verified algebraic representation of Cairo program executionRemote CPP Jeremy Avigad Carnegie Mellon University, USA, Lior Goldberg Starkware Industries Ltd., David Levit Starkware Industries Ltd., Yoav Seginer cdl-lang.org, Netherlands, Alon Titelman Starkware Industries Ltd. Pre-print
16:20 25m Talk		Formal Verification of a Distributed Dynamic Reconfiguration ProtocolInPerson CPP William Schultz Northeastern University, Ian Dardik Northeastern University, Stavros Tripakis Northeastern University Pre-print
16:45 25m Talk		Forward build systems, formallyInPerson CPP Sarah Spall Indiana University, Neil Mitchell Meta, Sam Tobin-Hochstadt Indiana University Link to publication