Static analysis tools for smart contracts
Analysis tools for pre-defined bugs.
Developed by Bernhard Mueller(b-mueller)
Oyente
2016年からあり、セキュリティチェックツール系ではもっとも(?)古い
melonport自体は分散型投資ファンド的なプロジェクト
paperではEVMのサブセット("EtherLite")でシンボリック実行エンジンを構築しているとしていた(最新のリポジトリ中その名前はないが)
検証項目
(a) mishandled exceptions, (b) transaction-ordering dependence, (c) timestamp dependence and (d) reentrancy
課題
Securifyのpaperのintroで言われてたやつ
violationを全て漏らさず検知できるとも限らない(under-approximationのため)
偽陽性(false positive)
現実的な制約のもとではコードのカバレッジが小さい(OyenteのParity Walletのやつだと20%くらい)
使ってみた
CLIがない、oyente.pyを実行する
dockerはsolidityのバージョンが古くてconstructor() がコンパイルされず Manticore
シンボリック実行系
セキュリティ会社trailofbits Inc.が開発
EVMバイトコードだけではなく、Linux向けのコードもチェックできる
使ってみた
pip install manticore の途中でunicornのインストールがこける
unicorn自体がmac OSだと入らない？
yudetamago.icon >
workaround
unicornはPython2系しか対応してないっぽいので、2系の環境に入れるかこのオプションが必要？ capstoneもインストール出来なかったのでこれが必要 Mythiril, Manticore, Oyenteの比較
2018年5月時点での、consensys dilligenceによるMythiril, Manticore, Oyenteの比較結果 割と得意不得意が分かれている
Slither
trailofbitsが開発、2018年10月にリリースされたので比較的新しい
パターン検出系
脆弱性チェックの他にビジュアライズなどもできる
Suicaidal, Reentrancy, etherのロック、その他静的解析
yudetamago.icon >
SolidityからSlithIRという中間言語に翻訳してその解析を行う Maian
良いpaper
OyenteのNUSチームが2018年に開発、ラストオーサー二人はOyenteのpaperと同じでAquinas Hobor氏とPrateek Saxena氏
Aquinas Hobor氏はScillaのpaperでもラストオーサーとして登場
Scilla作っているIlya Sergey氏も入っている
Parityマルチシグウォレットの事件を背景に開発されている
検証項目
Suicidal contracts (can be killed by anyone, like the Parity Wallet Library contract)
Prodigal contracts (can send Ether to anyone)
Greedy contracts (nobody can get out Ether)
このクラスの脆弱性のことを"trace vulnerabilities"と呼んでいる
悪用可能性が、特定のアカウントのステートに依存し、攻撃には連続的なコントラクトのコールが必要な脆弱性
仕組み
Symbolicに事前に決められたプロパティを充足するか調査し、Concreteに具体的な値を入れてみてfalse positiveなケースを除く
Oyenteと同じくシンボリック実行にはEtherLiteを使っている
Concrete Validation
実際のブロックチェーンの最新のステートを使う(maianはgethを使う模様)
そして、Z3がviolation conditionを充足すると提出した値を入れて見る
実験
Ethereumブロックチェーン上のデータを使って実証実験
https://gyazo.com/1da390400bf547ff8770092d6b72dd9b
使ってみた
yudetamago.icon >
そのままだとインストール出来なかったのでいくつかworkaroundが必要
最新のweb3.pyへの対応
古いバージョンのpyrlpへの対応
ETHRACER
Aashish Kolluri∗, Ivica Nikolic´∗, Ilya Sergey †, Aquinas Hobor‡, Prateek Saxena
∗NUS, ‡Yale-NUS College, †University College London
Event-ordering (or EO) bugs due to dynamic ordering of calls of its functions on the blockchain
Dynamic symboric execution, fuzzing, etc.
Securify
ChainSecurityはICE(ETH Zurichの学際的R&Dセンター)発のスタートアップ
ICEはGrant Wave3に採択された
仕組み
https://gyazo.com/68d55f573b15fa1918f9214e8be2efdf
(1)EVMバイトコードをスタックなしのrepresentationにdecompileする
SSA(Single Static Assignment)
ローカル変数(上図だとaなど)を導入してスタックを除く
decompile後に、メモリ・ストレージのoffsetを解決する
(2)セマンティックを推論する
(3)セキュリティパターンを検出する
DSLで記述されたcompliance/violationのパターンを検出する
検証方法・検証項目
DSLでpropertyを記述する
https://gyazo.com/97b6ae65c83976a676113532e718e4ef
このDSLで(本来は)ユーザーが自身のpropertyを書ける(現状のツールだとできない)
https://gyazo.com/8e1d1f48a8c3c64c73b35228e006a6df
Complianceパターンとviolationパターンを定義し、それ以外は全てwarningにする
"domains-specific properties"
本来検証したい項目に対して、その項目が違反される時同時に違反されがちな少し緩めた項目を検証する
例: Reentrancy→No writes after call
コントラクトコールの後にストレージ変更が伴わないか
それぞれpaperでは形式的にも書いてある
No writes after callの例
https://gyazo.com/c1bf1871055a469550de3d423028850b
課題
数値計算に関する検証はできない(オーバーフローなど)
reachabilityに関する推論は行わない、全てのinstructionは到達可能とする
コントラクト次第な部分もpropertyに含まれてしまっている。
例えば、Restricted writeに関して、全員が書き込めて然るべきフィールドなどがある
VerX
Anton Permenev, Dimitar Dimitrov Petar Tsankov, Dana Drachsler-Cohen, Martin Vechev
ChainSecurity AG, ETH Zurich
S&P 2020
SmartCheck
パーサジェネレーターANTLRでSolidityのパーサを構築
ZEUS
IBM Research
abstract interpretation & symbolic model checking
XACMLスタイルのテンプレートにspecを書く
コントラクトコードとspecをLLVMのbitcodeに変換(assertとして入る？)
SMTソルバを使う
sound(false negativesなし)、検証速度速いらしい
限定された項目のみ検証
参考
Verisol
Microsoft
関連: solhydra
BlockChainCompany
MythrilやOyenteなど複数のツールの解析をいっぺんに実行してくれる
Quantstamp
ICO色が強い
開発が止まっているようだが、独自でセキュリティチェックツールを開発
GitHubアカウントではmythrilやOyente, solhydraをforkしている
Quantstamp自体はもっと広いaudit networkを構築することを目指している
auto-auditに加え、SAT solverの並列化やsolverの計算資源提供のインセンティブ設計, bug bountyなど
CertiK
ICO色が強い
ファウンダーは清華大→イェール大→現コロンビア大助教の中国人
形式的検証専門で、CertiKOSという形式的に検証されたOSカーネルを開発した
paperでは2018 FebにPrivate Sale実施となっている(クラウドセールはなし?)
リポジトリ見当たらず
仕組み
コメントの中に検証したい条件を書く
https://gyazo.com/eb1fc791d9a81fcfdc0977772c67425c
Quantstamp同様、SMTソルバの計算資源をP2Pで提供するプロトコルを検討しているよう
layered-basedなアプローチでSMTソルバの状態爆発をなんとかすると言っているが詳細は書かれていない
Synthetic Minds
Yコンビネータ卒業生、シードで$5.5M調達(Khosla Ventures, Pantera Capital)
形式的検証だけではなく、プログラム合成を行う
コードやpaperはまだない(?)が、創業者のSaurabh Srivastava氏(UCBerkeley)のPh.D以降の研究成果に基づく模様
BIRなる中間表現にコンパイルしてシンボリック実行
a shared-memory, non-object, explicit Blockchain-state Intermediate Representation (BIR)
参考
Solidity built-in SMT Checker
pragma experimental SMTChecker; すれば使える
(EVMバイトコードではなく)Solidityコードのシンボリック実行
assertの中に指定した条件のviolationがありうるかチェックしてくれる
sound but not complete
false positveの原因は複雑な型、複雑な関数、外部コントラクトの抽象化、状態変数の不変条件を推論しないこと
参考
実装: solidityのlibsolidityの中にc++で書かれている Pact(for Kadena) built-in SMT Checker
Lispライク but 非チューリング完全な言語
Recursion in Pact is detected and causes an immediate failure at module load. Looping is only supported using map and fold on finite list structures.
Z3を使う
KadenaではコントラクトはPactのコードが直接ブロックチェーンに記録される
読みやすくして検証しやすくするためらしい
Pact自体他にも色々な特徴がある(型安全性やSQLの影響, gasがない)
unbounded integer !?