はじめに
第4回目です。スマートコントラクトのセキュリティの回です！
Title
Securify: Practical Security Analysis of Smart Contracts
2018/6/4
https://arxiv.org/pdf/1806.01143.pdf
Abstruct
ブロックチェーンにより第三者を信頼することなく任意のプログラム（スマートコントラクト）とトラストレスにやりとりできるようになった。しかし、実際には数十億ドル規模のセキュリティ問題が発生しています。
そこでこの問題を対処するために我々は、EthereumスマートコントラクトのセキュリティアナライザであるSecurifyを紹介します。これは、スケーラブルで完全に自動化され、特定のプロパティをもとに、マートコントラクトの振る舞いが安全かどうか証明します。
Securifyの分析は2つのステップで構成されています。
まず、コントラクトの依存グラフを象徴的に分析して、コードから正確な意味情報を抽出します。次に、プロパティが保持されているかどうかを証明するのに十分な条件を取得するコンプライアンスパターンと違反パターンをチェックします。
また、拡張性を考慮して、すべてのパターンは指定されたドメイン固有の言語で指定されます。 Securifyは公表されており、ユーザーは約22,000人で、定期的にセキュリティ監査を実施しています。我々は、世の中のEthereunmスマートコントラクトを評価するSecurifyを提案し、Securifyはスマートコントラクトの安全性を効果的に証明し、重大な違反を発見できることを実証しました。
Conclusion
我々は、Ethereumスマートコントラクトのための新しい軽量でスケーラブルな検証ツールであるSecurifyを紹介しました。
Securifyはいくつかの重要な利点を享受しています。
- すべての契約行動を分析する。
- アラームが正しいものか誤ったものかを分類する際のユーザーの労力を軽減する。
- ユーザーが新しい脆弱性パターンを出現したときに報告できる。
- バイトコードの逆コンパイル、最適化、パターンチェックまでの分析パイプラインは、スケーラブルで既製のDatalogソルバーを使用して完全に自動化されています。