Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Mon 18 Jan 2021 19:00 - 19:15 at CPP - Security, Blockchains, and Smart Contracts Chair(s): Andreas Lochbihler

Authenticated Append-Only Skiplists (AAOSLs) enable maintenance and querying of an authenticated log (such as a blockchain) without requiring any single party to store or verify the entire log, or to trust another party regarding its contents. AAOSLs can help to enable efficient dynamic participation (e.g., in consensus) and reduce storage overhead.

In this paper, we formalize an AAOSL originally described by Maniatis and Baker, and prove its key correctness properties. Our model and proofs are machine checked in Agda. Our proofs apply to a generalization of the original construction and provide confidence that instances of this generalization can be used in practice. Our formalization effort has also yielded some simplifications and optimizations.

Mon 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:45 - 19:30: Security, Blockchains, and Smart ContractsCPP at CPP
Chair(s): Andreas LochbihlerDigital Asset

Streamed session: https://youtu.be/Qak5mK92etU?t=2832

18:45 - 19:00
Talk
Extracting Smart Contracts Tested and Verified in Coq
CPP
Danil AnnenkovConcordium Blockchain Research Center, Aarhus University, Mikkel MiloConcordium Blockchain Research Center, Aarhus University, Jakob Botsch NielsenConcordium Blockchain Research Center, Aarhus University, Bas SpittersConcordium Blockchain Research Center, Aarhus University
Pre-print Media Attached File Attached
19:00 - 19:15
Talk
Formal Verification of Authenticated, Append-Only Skip Lists in Agda
CPP
Victor Cacciari MiraldoDFINITY Foundation, Harold CarrOracle Labs, USA, Mark MoirOracle Labs, New Zealand, Lisandra SilvaUniversity of Minho, Guy L. Steele Jr.Oracle Labs
Pre-print Media Attached
19:15 - 19:30
Talk
Towards formally verified compilation of tag-based policy enforcement
CPP
CHR ChhakPortland State University, Andrew TolmachPortland State University, Sean AndersonPortland State University
Pre-print Media Attached