
기호 실행 도구
이 프로젝트는 더 이상 내부적으로 개발 및 유지보수되지 않습니다.
Manticore는 스마트 계약 및 바이너리 분석을 위한 기호 실행 도구입니다.
Manticore는 다음 유형의 프로그램을 분석할 수 있습니다:
참고: 다른 프로젝트나 패키지와의 충돌을 방지하기 위해 가상 환경에 Manticore를 설치하는 것을 권장합니다.
옵션 1: PyPI에서 설치:
pip install manticore
옵션 2: PyPI에서 설치, 네이티브 바이너리 실행에 필요한 추가 종속성 포함:
pip install "manticore[native]"
옵션 3: nightly 개발 빌드 설치:
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 프로그래밍 인터페이스를 제공합니다.
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() # Manticore에 중지를 지시합니다.
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는 기본적으로 Yices를 사용합니다. 그렇지 않은 경우 Z3 또는 CVC4로 대체됩니다. 사용할 솔버를 수동으로 선택하려면 다음과 같이 할 수 있습니다:
manticore --smt.solver Z3
자세한 내용은 https://cvc4.github.io/를 참조하세요. 그렇지 않으면 바이너리를 가져와서 사용하십시오.