第10回ステアラボソフトウェア技術セミナー 西田雄気 様：スマートコントラクトアプリケーションの形式検証 The 10th STAIR Lab ST Seminar: Dr. Yuki Nishida
2026.06.01
どなたでも無料でご参加いただけます。オンライン形式のため特に定員数は設けておりませんので皆様奮ってご参加ください。
【日時】2026 年 6 月 30 日 (火) 13:00〜14:00
【講演形態】オンライン
【講演者】東北大学 西田雄気 様
【講演タイトル】スマートコントラクトアプリケーションの形式検証
【講演概要】
「ブロックチェーン」という言葉を聞いた時に真っ先に思い浮かぶのは日々のニュースなどで目にする暗号通貨でしょうか？イーサリアム以降，多くのブロックチェーンプラットフォームでは通貨の送受金といった組み込みの処理に加えてユーザーの書いた自由なプログラムをチェーン上に登録し実行するという機能が備わっています．こうしたプログラムのことを「スマートコントラクト」と呼びますが，取り扱うデータの資産価値の高さ・プログラムの公開性・顕在的な管理者の不在といった特有の事情から事前に検証することが重要なものとなっています．
本講演ではブロックチェーンシステムの軽い紹介から始め，ソフトウェア検証という視点から見た特徴的なシステムの側面を紹介したのち，ICBC2024で発表された”iCon: Automated Verification of Inter-Transaction Properties in Tezos Smart Contracts with Unknowns”を元にスマートコントラクトアプリケーションに対する形式検証アプローチの一つを紹介します．当検証で扱う性質はいわゆる安全性であり，より具体的には明示的に与えた不変条件の検証を行いますが，技術的な困難の一つとして検証者のあずかり知らぬ外部のスマートコントラクトとのインタラクションをどう扱うかという点があります．講演の後半ではこうした部分について関連研究との比較も交えつつ検証手法の形式化の紹介を行います．