manticore
Manticore 0.3.7
이 프로젝트는 더 이상 내부적으로 개발 및 유지 관리되지 않습니다. 그러나 우리는 커뮤니티의 작고 잘 작성된 끌어오기 요청을 검토하고 수락하게 되어 기쁘게 생각합니다. 우리는 버그 수정과 사소한 개선 사항만 고려할 것입니다.
새롭거나 현재 열려 있는 문제와 토론은 커뮤니티에서 답변하고 지원해야 합니다.
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를 사용할 수 있습니다.
개발 설치에 대해서는 위키를 참조하세요.
Manticore에는 바이너리 또는 스마트 계약의 기본 기호 분석을 수행할 수 있는 명령줄 인터페이스가 있습니다. 분석 결과는 mcore_ 로 시작하는 작업공간 디렉토리에 배치됩니다. 작업공간에 대한 자세한 내용은 위키를 참조하세요.
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 프로그래밍 인터페이스를 제공합니다.
이더리움 스마트 계약의 경우 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가 지원되며 명령줄 또는 구성 설정을 통해 선택할 수 있습니다. Yice를 사용할 수 있는 경우 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 슬랙 채널에 들러 주시기 바랍니다.
문서는 여러 위치에서 사용할 수 있습니다.
위키에는 Manticore를 시작하고 기여하는 방법에 대한 정보가 포함되어 있습니다.
API 참조에는 API에 대한 더 철저하고 심층적인 문서가 있습니다.
예제 디렉토리에는 API 기능을 보여주는 몇 가지 작은 예제가 있습니다.
manticore-examples 저장소에는 실제 CTF 문제를 포함하여 좀 더 관련된 예제가 있습니다.
버그 보고서를 제출하거나 기능을 요청하려면 문제 페이지를 사용하세요.
질문이나 설명이 필요한 경우 토론 페이지를 방문하세요.
Manticore는 AGPLv3 라이센스에 따라 라이센스가 부여되고 배포됩니다. 약관에 대한 예외를 찾고 있는 경우 당사에 문의하세요.
학술 작업에 Manticore를 사용하는 경우 Crytic $10,000 연구상 신청을 고려해보세요.
