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.
Conference DayMon 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:45 - 19:30
|Extracting Smart Contracts Tested and Verified in Coq|
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 UniversityPre-print Media Attached File Attached
|Formal Verification of Authenticated, Append-Only Skip Lists in Agda|
Victor Cacciari MiraldoDFINITY Foundation, Harold CarrOracle Labs, USA, Mark MoirOracle Labs, New Zealand, Lisandra SilvaUniversity of Minho, Guy L. Steele Jr.Oracle LabsPre-print Media Attached
|Towards formally verified compilation of tag-based policy enforcement|
CHR ChhakPortland State University, Andrew TolmachPortland State University, Sean AndersonPortland State UniversityPre-print Media Attached