David Dill, Novi Research
Blockchain-Forschung Seminarreihe
Zusammenfassung: Die 2018 von Facebook initiierte Libra-Blockchain 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, die durch Smart Contracts verwaltet werden, und weil 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 Verifikation so vieler wichtiger Eigenschaften der Move-Standardbibliothek ist bereits gut vorangeschritten.
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.