Formal verification of smart contracts
Overview
dominik.icon
Survey on smart contract language and the formal verification
by A.Miller, et al. at ISoLA
Classification
Related
Model checking
Uncategorized
Jiao Jiao et al.
補足
クライアントの実装の検証
ACL2 Ethereum Project
Kastrel Instituteによるブロックチェーン関連ソフトウェア開発プロジェクト 公式HP Grant Wave3採択
Kastrel InstituteはStanford Research Parkのコンピューターサイエンスの研究所、DARPAや国防総省など政府系機関から支援を受ける
ALC2はプログラミング言語としてはcommon LISPの変種
APTはKastelが開発している
declarative specificationsから実行可能なプログラムを合成してくれる
First Phase(2018.10月~)では、command-line wallet suitable for cold storage of keys and transaction signingを作る
ハッシュ関数や楕円曲線などの暗号アルゴリズムおよびBIP系のウォレット標準の仕様・実装
今後取り組むらしいこと
ACL2の高保証なEthereumノード開発と、他クライアントの検証への応用
スマートコントラクトコードの検証可能なコンパイラの開発
形式的検証のコミュニティ・エコシステム
Yoichi Hirai(pirapira)さん率いるFomal Verification Team
2016年9月よりEthereum Foundationのプロジェクトとして形式的検証の研究開発を担当 記事 LemによるEVMのセマンティック定義、Isabelleによるコントラクトの形式的検証、独自言語Banbooの開発など
Ethereum Foundationのサポート(Grants program)
Wave 3
Kestrel Institute – $400K. Formal verification of cryptographic primitives
ICE Center at ETH Zurich – $185K. ICE Center research and tooling development
Pyramid – $30K. Smart contract language
Wave 2
Cedille – $50K. Smart contract formal verification R&D.
Wave1
Runtime Verification – Security Grant – $500K. Casper contract formal verification.
VyperのCasperコントラクトの形式的検証が主なスコープらしい
Solium – DevEx Grant – $10K. Solidity static analyzer.
Language Design Community for the EVM(少し古い)