2022年3月6日、弊社代表取締役 古瀬 淳 が 日本ソフトウェア科学会 第24回プログラミングおよびプログラミング言語ワークショップ(PPL 2022) にて「ブロックチェーンと形式検証 ～ Tezos の場合」という招待講演を行いました。
現時点での Tezos での形式検証活動のそれなりのサーベイになっていると思いますので、概要と使用したスライドを公開します。
Our CEO Jun Furuse was invited to talk “Blockchain and formal verification - cases of Tezos” at PPL 2022, programming and programming language workshop by JSSST. Here are the abstract and the slides in Japanese.
概要
非中央集権分散データベースであるブロックチェーンでは、各サーバノードの運営コストやデータ改竄を防ぐためのインセンティブとして、換金性のあるトークンの導入がどうしても必要になります。結果、ブロックチェーンには巨額の金銭的価値が保持されます。この「お金」との切っても切れない関係、そしてソースコードが全公開されるという性質により、ブロックチェーンシステムに深刻なバグがあった場合、それを突いた巨額のトークン窃盗が起きかねません。このように高い安全性が求められるブロックチェーンではソフトウェアテストだけでは不十分で、数理的にバグがないことを証明する形式検証が非常に強力な安全化手段となります。
Tezosブロックチェーンでは、安全なシステムの構築を目指しその大きな実装単位である経済プロトコル、プロトコルを使ってブロックの検証を行うシェル、そして契約の自動執行を行うアプリケーションであるスマートコントラクト、それぞれの重要部品に対し実際に形式検証を行っています。これらの検証例のいくつかを紹介します。
スライド
画像埋め込みの HTML スライドはこちら。