trailofbits/manticoreシンボリック実行ツール
このプロジェクトは、もはや内部で開発・保守されていません。
Manticoreは、スマートコントラクトとバイナリの解析のためのシンボリック実行ツールです。
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.8029580116271973
Manticoreは強力なカスタム解析を実装するために使用できるPythonプログラミングインターフェースを提供します。
イーサリアムスマートコントラクトの場合、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を実行するか、docker runに--ulimit stack=100000000:100000000を渡すことで行えます。$PATHにsolcプログラムが必要です。crytic-compileを直接実行して問題を特定しやすくすることを検討してください。Manticoreは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
Yicesは非常に高速です。詳細は https://yices.csl.sri.com/ をご覧ください。
sudo add-apt-repository ppa:sri-csl/formal-methods
sudo apt-get update
sudo apt-get install yices2
Manticoreの使用や拡張に関するヘルプについては、Empire Hacking の #manticore Slackチャンネルにお立ち寄りください。
ドキュメントはいくつかの場所で入手できます：
Wiki には、Manticoreを使い始めたり貢献したりするための情報が含まれています
APIリファレンス には、APIに関するより詳細で深いドキュメントがあります
examples ディレクトリには、APIの機能を示す小さな例がいくつかあります
manticore-examples リポジトリには、実際のCTF問題を含む、より複雑な例があります
バグレポートや機能リクエストを提出する場合は、issues ページをご利用ください。
質問や確認については、discussion ページをご覧ください。
ManticoreはAGPLv3ライセンスの下でライセンスされ、配布されています。条件の例外をお探しの場合は、こちらまでお問い合わせください。
学術研究でManticoreを使用している場合は、Crytic $10k Research Prize への応募をご検討ください。
