Formal Verification of Authenticated, Append-Only Skip Lists in Agda
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 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:45 - 19:30
|Extracting Smart Contracts Tested and Verified in Coq|
Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University, Jakob Botsch Nielsen Concordium Blockchain Research Center, Aarhus University, Bas Spitters Concordium Blockchain Research Center, Aarhus UniversityPre-print Media Attached File Attached
|Formal Verification of Authenticated, Append-Only Skip Lists in Agda|
Victor Cacciari Miraldo DFINITY Foundation, Harold Carr Oracle Labs, USA, Mark Moir Oracle Labs, New Zealand, Lisandra Silva University of Minho, Guy L. Steele Jr. Oracle LabsPre-print Media Attached
|Towards formally verified compilation of tag-based policy enforcement|
CHR Chhak Portland State University, Andrew Tolmach Portland State University, Sean Anderson Portland State UniversityPre-print Media Attached