雙十一喧囂未散，王校長 ig 剛奪冠...
作為中獎絕緣體的小編自以為沒那福分成為錦鯉...
於是乎，默默地逛起論壇，順手把喜歡的文章翻譯整理出來供各位看官把玩...
希望各位看得愉快，各有收穫...
智能合約形式化驗證主要是基於形式化驗證來確認目標合約是否安全並且滿足 SN[T]ARKs 的某些規範，相應的功能類似於傳統互聯網中的 「https」。
1.1 背景
現狀是智能合約的形式化驗證是在每個計算機上執行的，如果某人已經對合約進行形式化驗證，那麼當前用戶是無法在不執行形式化驗證程序的前提下驗證合約。而對智能合約來說，它是無法判定其他合約是否經過形式化驗證的。
LayerX Inc. R& D 團隊（ R & D: Research and Development) 針對上述問題提出了鏈上的解決方案，並且計算成本要低得多。
該解決方案帶來的主要有2個好處：
1）智能合約可以自行判斷即將調用的其他合約是否經過形式化驗證並滿足某些規範要求。
2）移動應用程序等輕量級客戶端可以查看某個合約是否符合某些規格。
換句話說，該協議在區塊鏈中相當於 「https」 ，雖然這不能杜絕黑客攻擊，但會給予某種程度的安全保證。
1.2 協議摘要
在協議中，驗證者合約(verifier contract ) 驗證 SN[T]ARKS 證明，即證明給定的 EVM 位元組碼滿足某些規範。SN[T]ARKS 證明 即 SNARKS 證明及 STARKS 證明，從 zk-SNARKs 到 zk-STARKs 是空間換時間的取捨，雖然都不完美，但在持續進化中。用戶合約或是其他合約可以通過詢問相應的驗證者合約來獲取目標合約是否經過形式化驗證或滿足某些規範。
1.3 案例
以下是 1.1 中所描述的相應示例：
（1） 無代幣的加密抵押系統
在穩定幣或衍生物的一些金融協議中，不僅包括以太幣，還包括其他的基於 ERC20 協議的代幣所涉及的加密資產被用作抵押品，即便這些協議能夠處理代幣價格下跌的情況，但是如果抵押資產所依據的合約有漏洞，比如著名的整數溢出或是重放攻擊，可能會造成「黑天鵝」事件，以及整個系統都將被破壞。
如果基於這些協議的系統合約禁止使用未經形式化驗證的代幣作為抵押品，在一定程度上將減少 「黑天鵝」 事件的發生。
（2）安全錢包應用或 dapp 瀏覽器
錢包應用或 dapp 瀏覽器基於驗證者合約來避免使用不安全的智能合約。這不僅限於檢查溢出漏洞 (overflow)。
Layer2 協議，如 plasma 以及狀態通道在未來會發布相應的標準。L4 以及 Celer 團隊證致力於狀態通道的相關協議研發，這些標準將被編寫為適用於形式化驗證的正式規範。
基於這些協議，錢包應用或是 dapp 瀏覽器可以警告用戶所使用的合約是否符合這些標準。
好了 ，以上都是一些虛的客套話，接下來小編給大家上正菜。
emmmm......祖國的花骨朵表示只想學習，不想吃，端走！
2.方法
2.1 SNARKs 形式化驗證
鑒於證明體量足夠小並且適合區塊鏈，本文使用 SNARK 作為非互動式證明系統。
SNARKs 的證明體量只有 288 位元組，其中 128 位元組用於安全性證明。
STARKs 較 SNARKs 的優勢在於需要可信設置以及證明成本，但加密證明的容量也會大得多 。
下面討論 SNARKs:
copyright @ LayerX Inc. R&D 團隊
驗證者智能合約需要在設置階段預先部署。
圖示中的前端 (Frontend）部分，形式驗證程序在 RAM 中被執行，RAM 是一個通用計算模型，該節點生成 SNARKs 的電路。
而在後端(Backend) 中，生成的電路和 RAM 用於 SNARKs。
設置(Setup)階段主要是作為生成證明密鑰和驗證密鑰的預處理階段。
只有當證明人通過形式化驗證的位元組碼時，從證明人傳遞給驗證者的證明才會被接受
並且通過驗證者合約返回 true ，並通知 dapp 瀏覽器或被其他合約調用。
基於 SNARKs 的驗證過程公式化如下 ：
Pprove(w = bytecode, x = hash(bytecode)) {return proof}
Pverify(proofkey, hash(bytecode)) = True/False
x 是傳遞給鏈上計算的主要輸入，w 是輔助輸入
bytecode 是需要驗證的合約位元組碼
proof_key:形式化驗證結果的證明密鑰
鑒於智能合約位元組碼的體量過於龐大，以致於無法放於鏈上，因此將它作為輔助輸入（也可以稱為私有輸入），只把它的哈希值作為主要輸入（即公有輸入）。
以下是 P_prove 的偽代碼片段：
為了將程序轉換成布爾電路，因此引入了 TinyRAM 等計算模型，並基於這些計算模型實現形式驗證器。
私有輸入變數包含證明，以及除了對位元組碼進行哈希處理之外，如何對其應用推理規則的對象。
當 P_verify 返回值為 true , 驗證後的合約在部署者合約中註冊或是發出事件以將結果通知給鏈下客戶端。
2.3 設置
上述的協議中，驗證者合約需要在合約的可信任列表中事先註冊或是基於該協議的移動應用程序。
這些協議皆是基於 verifier 合約的正確性，即
1）形式化驗證的演算法
2）需驗證的形式化格式
3）表示形式化驗證演算法的電路
4）SN[T]ARKs 驗證程序
3 挑戰&解決方案
3.1 面臨的主要挑戰
實現這一目標的主要困難在於將形式化驗證程序轉換為電路。大多數形式驗證方法採用 Z3 作為 SMT 求解器或是使用 Coq ，Isabelle 等互動式定理證明器。
具體來說，主要存在兩個挑戰：
（1）實現方面的困難
已有的幾個庫，如 Z0Krates ,xJsnark ,以及 Pequin 來幫助將程序編譯為 SNARKs 電路。但是該領域專屬語言(DSL) 無法與 JAVA,PYTHON ,C++等匹敵，因此實現形式驗證器非常困難，沒有足夠的文檔支撐，並且其中的大部分都不是為了生產用途。
（2）電路複雜性
SNARK 的驗證時間和證明體量是恆定的，但隨著程序複雜性的增加，約束的數目也會隨之增加。即生成密鑰的時間和成本。
因此形式化驗證的計算成本是巨大的，如 DIZK 等庫則用於降低電路的複雜性，節約計算成本。
gnosis 團隊預估基於 AWS 和 DIZK ，他們的去中心化交易所的成本為 1200 美元。因此優化工作不僅應在後端進行，前端也應該進行優化。
3.2 解決方案
(1)通用計算
LayerX 團隊計劃基於 LLVM 實現形式化驗證並將其編譯到 RAM 以轉換成電路。TinyRAM 能夠生成複雜度較小的電路，
但因為基於 LLVM 後端實現 TinyRAM 過於困難，因此轉而使用與 TinyRAM 較為類似的後端，其中一個是 RISC-V,它的指令集較為簡單並且數量有限。於是 LayerX 團隊將其作為生成電路的計算機器。
但是因為 RISC-V 的指令集較 TinyRAM 更為龐大，因此在生成電路的效率方面有所不及，並且在計算形式化驗證演算法方面面臨著更大的困難。
(2)計算量更少的形式化驗證演算法
其中一個非常有前景的方法是移除證明搜索部分，因為證明搜索需要大量的計算，以便專註於 給定證明的驗證。
形式化證明軟體在人類的幫助下半自動地找到證明，推理相應的代碼規則。因為由鏈下形式驗證器生成的證明可以作為私有輸入進行傳遞，並且所有的程序都專註於對驗證證明，所以協議中轉換成電路的程序不一定要找到證明。
另一種方法是針對某些漏洞的啟發式方法。
比如 Securify 在表達其 DSL 的目標位元組碼語義中使用模式檢測，通俗來說，違反智能合約的屬性設置其實也違反了更簡單的屬性設置，而這更容易進行審查。與 KEVM 以及互動式定理證明器相比，該演算法更容易轉換為電路。但如果沒有 Z3 等自動定理證明器，證明「無溢出」將是非常困難的。
4.展望未來
針對形式驗證器的電路複雜性研究至關重要，以及包括 STARK 在內的零知識證明系統研究。
LayerX 未來的長期目標包括：
1）通過通用性計算進行 SN[T]ARKs 證明的基礎性開發工作。
2）更加友好的 SN[T]ARKs 形式化驗證開發。
