本研究深研形式化靜態程式分析技術，在核心技術上開發邏輯式字串限制解法工具，結合程式流分析技術與形式化執行技術，分析軟體應用程式的性質與弱點。在實務上，將分析技術落實於手機應用程式的弱點檢驗以及區塊鏈與智能合約的弱點檢驗。實驗揭露線上應用程式（包含蘋果官方網站與以太坊智能合約）不為人知的資安漏洞。

本研究的關鍵技術涵蓋：二元碼控制流程分析，高效能字串分析與性質驗證技術。已開發Binflow工具，成功分析1000多個Apple官網的行動應用程式，防範隱私資料竊取。另發展針對以太坊的智能合約靜態分析工具，基於控制流程圖對智能合約做出gas分析、攻擊的偵測。

產學合作 「零知識證明技術結合智能合約的模擬驗證」NT 600,000 資策會
2018.3.1-2018.11.30

技術移轉  [數位資產應用智能合約靜態分析技術執行碼] NT98,000 資策會 2018.12-2019.5