solidity static analysis
Alpha
https://github.com/shaunazzopardi/solidity-cfg-builderおよびhttps://github.com/gordonpace/contractlarvaに基づく堅牢性スマートコントラクトの検証のための静的分析。
このツールは、Solidity Smart Contractsのプロパティを完全に証明しようとします。部分的な成功により、Solidity Smart Contractが証明されていない残留プロパティが返されます。
Solidity Smart Contractのコントロールフロー（Solidity-CFG-Builderとその変動状態に基づく）を過剰に承認することにより、Sathinit Smart Contractのコントロールフローグラフ表現を使用します。
これは、Prepost 2017の議事録、EPCTSシリーズの議事録で提示された作業に部分的に基づいており、Arxivで入手可能です。
各スマートコントラクト関数は、トリプルを含むトリプルでタグ付けされたコントロールフローオートマトン（CFA）として表されます。（i）プログラム変数状態の条件。 （ii）プログラム変数状態を変換するステートメント。 （iii）声明の実行時にアクティブ化されたプロパティイベント。
このような各オートマトンは、プログラムの初期、通話、または終了状態で発生するイベントを可能にする抽象遷移（プロパティイベントのみでタグ付け）で補強されています。これは、副甲状腺内分析の基礎として使用されます。このような各オートマトンは、対応する関数を呼び出すスマートコントラクトのすべての実行を過度に承認します。このオートマトンは、抽象的なコントロールフローオートマトン（ACFA）と呼ばれます。
単純なアサーション伝播アルゴリズムは、CFAの明示的な状態を介して、アサーションに影響を与える可能性のあるステートメントが発生するまで、プログラム変数状態（条件と声明で暗示される）に関するアサーションを伝播します。これは健全です。
プロパティは、次のトリプルでタグ付けされた遷移を使用する動的イベントオートマトン（DEA）として表されます。（i）イベント。 （ii）プロパティ変数状態の警備員。 （iii）プロパティ変数状態に関するアクション。
可変抽象化を備えたACFAは、DEAで構成され、CFAおよびDEA遷移のペアでタグ付けされた遷移、または＃シンボルを含む位置の1つを備えた抽象監視されたシステム（AMS）を生成します。 ＃がCFA遷移の代わりに使用されると、抽象遷移の一致を通知しますが、DEA遷移の代わりにDEA遷移マッチがない場合。
次に、特定のDEAに対してプログラムの各機能に対してAMSが作成されます。
SMTソルバーZ3は、AMSの構築中にオンザフライと呼ばれ、与えられた遷移が実際の実行でその時点でアクティブ化できるかどうかを判断します。 CFA-DEA遷移ペアを考えると、DEAガードがCFA遷移の条件とステートメントで更新されたソース状態の変数抽象化に当てはまることを確認します。 CFA-＃ペアが与えられている間、ソース状態の変数抽象化がCFA遷移の条件で更新され、ステートメントがこの時点で活性化される可能性のあるDEA遷移の統治の否定と矛盾していないことを確認します（同じDEA州からのDEA遷移は、相互に排他的に排他的であることを望んでいることに注意してください）。
各AMSを分析してCFA-DEA遷移ペアを特定し、この方法で使用されるDEA遷移を抽出し、＃プレースホルダーとのDEA遷移の一致を無視します。これらのDEA遷移の結合は、元のDEAの残差を生み出します。これは、残留DEAの構文分析によってさらに減少することがあります。
さらに、AMSSから、DEAトランジションのガードを削除できるか（つまり、 Trueに変更）、つまりAMSで使用できる場合はいつでも使用できる場合はいつでも識別できます。
残留生産に移行がない場合、プロパティが証明されています。
要件：Cabal v2.4。*（例：Haskellプラットフォーム全体をインストール）
編集：ここで指示に従ってください
正しい結果については、Solidity CodeがSolidityコンパイラでコンパイルされることを常に確認してください。
ツールを使用するには、スマートコントラクトソリディティファイルの場所、DEAプロパティファイル、および実行可能ファイルへの出力の優先位置、例：Execute：
./main "./examples/Courierservice.sol" "
このプロジェクトは、Apache 2.0ライセンスの条件に基づいてライセンスされています。
