trailofbits/manticore기호 실행 도구
이 프로젝트는 더 이상 내부적으로 개발 및 유지보수되지 않습니다.
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/를 참조하세요. 그렇지 않으면 바이너리를 가져와서 사용하십시오.
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에 지원하는 것을 고려하세요.
