manticore
Manticore 0.3.7
このプロジェクトは社内で開発および保守されなくなりました。ただし、コミュニティからの小さくてよく書かれたプル リクエストを喜んでレビューし、受け入れます。バグ修正と軽微な機能強化のみを考慮します。
新しい問題や現在未解決の問題や議論にはコミュニティが回答し、サポートするものとします。
Manticore は、スマート コントラクトとバイナリを分析するためのシンボリック実行ツールです。
マンティコアは次の種類のプログラムを分析できます。
注: 他のプロジェクトやパッケージとの競合を防ぐために、仮想環境に Manticore をインストールすることをお勧めします。
オプション 1: PyPI からインストール:
pip install manticoreオプション 2: PyPI からインストールします。ネイティブ バイナリの実行には追加の依存関係が必要です。
pip install " manticore[native] "オプション 3: 夜間の開発ビルドをインストールする:
pip install --pre " manticore[native] "オプション 4: masterブランチからのインストール:
git clone https://github.com/trailofbits/manticore.git
cd manticore
pip install -e " .[native] "オプション 5: Docker 経由でインストール:
docker pull trailofbits/manticoreインストールすると、 manticore CLI ツールと Python API が使用できるようになります。
開発用インストールについては、Wiki を参照してください。
Manticore には、バイナリまたはスマート コントラクトの基本的なシンボリック分析を実行できるコマンド ライン インターフェイスがあります。分析結果は、 mcore_で始まるワークスペース ディレクトリに配置されます。ワークスペースについては、wiki を参照してください。
Manticore CLI は、(たとえば) コントラクトに.solまたは.vy拡張子が付いている場合、コントラクトをテストしようとしていることを自動的に検出します。デモをご覧ください。
$ manticore examples/evm/umd_example.sol
[9921] m.main:INFO: Registered plugins: DetectUninitializedMemory, DetectReentrancySimple, DetectExternalCallAndLeak, ...
[9921] m.e.manticore:INFO: Starting symbolic create contract
[9921] m.e.manticore:INFO: Starting symbolic transaction: 0
[9921] m.e.manticore:INFO: 4 alive states, 6 terminated states
[9921] m.e.manticore:INFO: Starting symbolic transaction: 1
[9921] m.e.manticore:INFO: 16 alive states, 22 terminated states
[13761] m.c.manticore:INFO: Generated testcase No. 0 - STOP(3 txs)
[13754] m.c.manticore:INFO: Generated testcase No. 1 - STOP(3 txs)
...
[13743] m.c.manticore:INFO: Generated testcase No. 36 - THROW(3 txs)
[13740] m.c.manticore:INFO: Generated testcase No. 37 - THROW(3 txs)
[9921] m.c.manticore:INFO: Results in ~ /manticore/mcore_gsncmlgx代替の CLI ツールが提供されており、コントラクトのテストを簡素化し、コントラクトで使用されているのと同じ高級言語でプロパティ メソッドを作成できます。 manticore-verifier のドキュメントをチェックしてください。デモを見る
$ manticore examples/linux/basic
[9507] m.n.manticore:INFO: Loading program examples/linux/basic
[9507] m.c.manticore:INFO: Generated testcase No. 0 - Program finished with exit status: 0
[9507] m.c.manticore:INFO: Generated testcase No. 1 - Program finished with exit status: 0
[9507] m.c.manticore:INFO: Results in ~ /manticore/mcore_7u7hgfay
[9507] m.n.manticore:INFO: Total time: 2.8029580116271973Manticore は、強力なカスタム分析を実装するために使用できる Python プログラミング インターフェイスを提供します。
Ethereum スマート コントラクトの場合、API を使用して任意のコントラクト プロパティを詳細に検証できます。ユーザーは開始条件を設定し、シンボリック トランザクションを実行し、検出された状態を確認してコントラクトを保持するための不変条件を確認できます。
from manticore . ethereum import ManticoreEVM
contract_src = """
contract Adder {
function incremented(uint value) public returns (uint){
if (value == 1)
revert();
return value + 1;
}
}
"""
m = ManticoreEVM ()
user_account = m . create_account ( balance = 10000000 )
contract_account = m . solidity_create_contract ( contract_src ,
owner = user_account ,
balance = 0 )
value = m . make_symbolic_value ()
contract_account . incremented ( value )
for state in m . ready_states :
print ( "can value be 1? {}" . format ( state . can_be_true ( value == 1 )))
print ( "can value be 200? {}" . format ( state . can_be_true ( value == 200 )))API を使用して、Linux バイナリ用のカスタム分析ツールを作成することもできます。初期状態を調整すると、CLI の使用時によく発生する状態爆発の問題を回避できます。
# example Manticore script
from manticore . native import Manticore
m = Manticore . linux ( './example' )
@ m . hook ( 0x400ca0 )
def hook ( state ):
cpu = state . cpu
print ( 'eax' , cpu . EAX )
print ( cpu . read_int ( cpu . ESP ))
m . kill () # tell Manticore to stop
m . run ()Manticore は、プロパティの検証や一般的な分析のために、シンボリック入力に対して WebAssembly 関数を評価することもできます。
from manticore . wasm import ManticoreWASM
m = ManticoreWASM ( "collatz.wasm" )
def arg_gen ( state ):
# Generate a symbolic argument to pass to the collatz function.
# Possible values: 4, 6, 8
arg = state . new_symbolic_value ( 32 , "collatz_arg" )
state . constrain ( arg > 3 )
state . constrain ( arg < 9 )
state . constrain ( arg % 2 == 0 )
return [ arg ]
# Run the collatz function with the given argument generator.
m . collatz ( arg_gen )
# Manually collect return values
# Prints 2, 3, 8
for idx , val_list in enumerate ( m . collect_returns ()):
print ( "State" , idx , "::" , val_list [ 0 ])ulimit -s 100000を実行するか、 --ulimit stack=100000000:100000000をdocker runに渡します。$PATHにsolcプログラムが必要です。crytic-compile直接実行することを検討してください。マンティコアは、smtlib2 をサポートする外部ソルバーに依存しています。現在、Z3、Yices、および CVC4 がサポートされており、コマンドラインまたは構成設定を通じて選択できます。 Yices が利用可能な場合、Manticore はデフォルトでそれを使用します。そうでない場合は、Z3 または CVC4 に戻ります。使用するソルバーを手動で選択したい場合は、次のように行うことができます: manticore --smt.solver Z3
詳細については、https://cvc4.github.io/ を参照してください。それ以外の場合は、バイナリを取得して使用してください。
sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
sudo chmod +x /usr/bin/cvc4
イースは信じられないほど速いです。詳細はこちら https://yices.csl.sri.com/
sudo add-apt-repository ppa:sri-csl/formal-methods
sudo apt-get update
sudo apt-get install yices2
マンティコアの使用または拡張に関するヘルプが必要な場合は、Empire Hacking の #manticore スラック チャンネルにお気軽にお立ち寄りください。
ドキュメントはいくつかの場所で入手できます。
Wiki には、Manticore の使用開始と貢献に関する情報が含まれています。
API リファレンスには、API に関するより徹底的かつ詳細なドキュメントが含まれています。
サンプル ディレクトリには、API 機能を紹介する小さなサンプルがいくつかあります。
manticore-examples リポジトリには、実際の CTF 問題など、さらに複雑な例がいくつかあります。
バグレポートや機能リクエストを提出したい場合は、問題ページをご利用ください。
質問や説明については、ディスカッション ページをご覧ください。
Manticore は、AGPLv3 ライセンスに基づいてライセンス供与され、配布されています。規約の例外をご希望の場合は、お問い合わせください。
学術研究でマンティコアを使用している場合は、Crytic の 10,000 ドル研究賞への応募を検討してください。
