Aufgezeichnet: 21.07.2021 CERIAS Sicherheitsseminar an der Purdue University Ein formaler Verifier für die Diem Blockchain Move Sprache David Dill, Facebook Die Diem-Blockchain, die 2018 von Facebook ins Leben gerufen wurde, umfasst eine neuartige Programmiersprache namens Move zur Implementierung von Smart Contracts. Die Korrektheit von Move-Programmen ist besonders wichtig, da die Blockchain große Mengen an Vermögenswerten hosten wird, diese Vermögenswerte von Smart Contracts verwaltet werden und es in der Vergangenheit große Verluste auf anderen Blockchains aufgrund von Fehlern in Smart Contracts gegeben hat. Die Move-Sprache ist so sicher wie möglich gestaltet und wird von einer formalen Spezifikation und einem automatischen Verifikationstool, dem Move Prover, begleitet. Ein Projekt zur Spezifizierung und formalen Verifizierung so vieler wichtiger Eigenschaften der Move Standardbibliothek ist bereits gut im Gange. Dieser Vortrag wird sich mit den Zielen des Projekts und den interessantesten Erkenntnissen befassen, die wir zum Zeitpunkt der Präsentation gewonnen haben. Die gesamte Blockchain-Implementierung, einschließlich der Move-Sprache, der virtuellen Maschine, des Move Prover und nahezu finaler verschiedener Move-Module, ist auf
http://github.com/libra verfügbar \(Besuchen Sie: www.cerias.purdue.edu\)