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 將可用。
對於開發安裝，請參閱我們的 wiki。
Manticore 有一個命令列介面，可以對二進位或智慧合約執行基本的符號分析。分析結果將被放置到以mcore_開頭的工作空間目錄。有關工作區的信息，請參閱 wiki。
如果（例如）合約具有.sol或.vy擴展名，Manticore CLI 會自動偵測您正在嘗試測試合約。查看示範。
$ 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或將--ulimit stack=100000000:100000000傳遞給docker run來完成$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
請隨時造訪 Empire Hacking 中的#manticore slack 頻道，尋求使用或擴展 Manticore 的協助。
文件可以在幾個地方找到：
該 wiki 包含有關 Manticore 入門和貢獻的信息
API 參考對我們的 API 提供了更全面、更深入的文檔
範例目錄中有一些展示 API 功能的小範例
manticore-examples 儲存庫有一些更複雜的範例，包括一些真正的 CTF 問題
如果您想提交錯誤報告或功能請求，請使用我們的問題頁面。
如有疑問和澄清，請訪問討論頁面。
Manticore 根據 AGPLv3 許可證進行許可和分發。如果您正在尋找條款的例外情況，請與我們聯絡。
如果您在學術工作中使用 Manticore，請考慮申請 Crytic 10k 美元研究獎。
