如果一個漏洞需要「先呼叫 A 函數、再把 B 變數設定為特定值、最後 C 函數的運算結果剛好等於 0」才會觸發，Slither 這種只看程式碼表面的工具通常會無能為力。這時候，我們就需要請出區塊鏈資安界的重裝武器：基於符號執行 (Symbolic Execution) 的檢測工具——Mythril。

什麼是符號執行 (Symbolic Execution)？
要理解 Mythril 的強大，我們必須先搞懂「符號執行」的運作原理。

想像合約是一個巨大的迷宮。

1. 單元測試 (Unit Test)：就像是你親自走進去，每次只能測試一條你預想好的路線。
2. 靜態分析 (Slither)：像是拿著迷宮的平面圖在看，能找出明顯的死路，但不知道實際走起來會不會遇到機關。
3. 符號執行 (Mythril)：它不會代入具體的數字（例如 x = 5）去跑程式，而是把輸入值當作一個「未知數符號 (Symbol)」。它會利用強大的數學證明引擎（SMT Solver，例如微軟的 Z3），同時窮舉並計算出迷宮中「所有可能」的執行路徑。一旦它發現某條路徑會導致資金被盜，它就會逆向推導出「你需要輸入什麼特定數值」才能走到那裡！

靶機：隱藏在深處的提款後門
讓我們來看一個刻意隱藏邏輯後門的合約。這個後門條件非常嚴苛，一般的隨機測試（甚至人眼）幾乎不可能掃得出來：
'''
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

contract HiddenBackdoor {
mapping(address => uint256) public balances;

function deposit() public payable {
    balances[msg.sender] += msg.value;
}

// 正常的提款函數
function withdraw(uint256 amount) public {
    require(balances[msg.sender] >= amount, "Insufficient balance");
    balances[msg.sender] -= amount;
    payable(msg.sender).transfer(amount);
}

// 隱藏的後門：只有當傳入的兩個數字滿足特定複雜方程式時，才能清空合約！
function secretWithdraw(uint256 a, uint256 b) public {
    // 條件：a 的平方必須等於 b，且 a 必須大於 10000
    require(a > 10000, "Condition 1 failed");
    require(a * a == b, "Condition 2 failed");

    // 觸發後門，把合約裡的錢全轉給駭客
    payable(msg.sender).transfer(address(this).balance);
}

}
'''
如果你用 Slither 掃描這個合約，它大概只會警告你 transfer 沒加防護，但它算不出要怎麼觸發。這時候就輪到 Mythril 上場了。

Mythril 安裝與實戰掃描
Mythril 是由 ConsenSys 開發的工具。最簡單的安裝與執行方式是使用 Docker（這樣就不會弄髒你的本地 Python 環境）。

打開終端機，在你的專案目錄下執行以下指令來分析 HiddenBackdoor.sol：
'''
docker run -v $(pwd):/tmp/app -w /tmp/app mythril/myth analyze src/HiddenBackdoor.sol
'''
Mythril 終端機輸出解析：
因為 Mythril 是在做極度耗費運算資源的數學推演，所以掃描時間會比 Slither 慢上許多（可能需要幾分鐘）。但當它跑完後，它會給你一個令人驚豔的報告：
'''
==== Unprotected Ether Withdrawal ====
SWC ID: 105
Severity: High
Contract: HiddenBackdoor
Function name: secretWithdraw(uint256,uint256)
PC address: 456
Estimated Gas Usage: 6000 - 25000

The contract balance is sent to an arbitrary user.
Any user can withdraw the contract's entire balance by executing this function.

Transaction Sequence to trigger this issue:

1. Call secretWithdraw(uint256,uint256) with:
   a: 10001
   b: 100020001
   '''
   看到了嗎？Mythril 內建的數學引擎不但抓出了 secretWithdraw 是一個不受保護的提款漏洞，它還直接幫你解開了方程式，明確告訴你駭客只要傳入 a = 10001 和 b = 100020001，就能成功突破所有 require 限制，把錢偷走！

兩大工具的黃金組合
在實務的資安稽核中，Slither 和 Mythril 不是競爭關係，而是完美的互補：

1. 開發階段 (CI/CD)：每次 Push 程式碼時，先用極速的 Slither 掃描，抓出忘記加 onlyOwner 或語法寫錯的低級失誤。
2. 上線前夕 (Audit)：在合約準備部署到主網前，將編譯好的 Bytecode 交給 Mythril 跑個幾小時甚至幾天，讓它深入挖掘隱藏的邏輯炸彈。

這次見識到了符號執行強大的數學破壞力，它讓所有隱藏的邏輯後門無所遁形。