了解Marlowe成為安全智能合約開發平台的原因
免責聲明： 馬洛安全公司這篇文章中的內容是"按原樣"提供的，沒有任何形式的保證。本文件中的任何內容都無意成為專業建議，包括但不限於金融、投資、法律或稅務建議。Input Output Global對你使用或依賴本文件中的任何信息不負責任。
介紹
在大多數區塊鏈中，智能合約是一個計算機程序，一旦滿足某些預定義的條件就會自動執行。在Cardano中，情況有些不同，因為智能合約的執行發生在外部提交給Cardano節點的交易中。但是，無論它在引擎蓋下如何工作，智能合約對許多行業都很有用：金融、房地產、商業和其他許多行業。
使用智能合約的交易可能涉及大量價值的移動和轉移，這可能是不良行為者的一個重要目標。同樣，由於編碼中的缺陷或漏洞，這種價值可能被鎖定，或完全丟失。
要避免任何不受歡迎的結果，需要實施一個強大的安全框架，這涉及到開發人員、交易所和任何其他處理智能合約的各方的設計原則、審計和最佳實踐的結合。
Marlowe是一個由Input Output Global（IOG）創建的工具和語言的生態系統，使Cardano區塊鏈上的金融和交易智能合約的開發得以實現，它增加了整個Cardano技術社區不斷增長的資源。
Marlowe套件的設計和開發都是以安全為中心的。例如，Marlowe的創造者已經建立了功能限制，確保合約是有限的，並且總是終止的。Marlowe還避免了某些編程結構，以防止不希望出現的結果，例如遞歸和循環。第三方Tweag在Marlowe部署到主網上之前進行了靜態和動態審計。所有這些安全特性的結果，以及其他許多特性，是一個安全的智能合約創建和開發平台。
本文深入探討了Marlowe的安全性，解釋了安全審計的發現，以及團隊如何應對這些發現，內置的功能限制，部署中包含的安全分析工具，以及使用Marlowe時必須采取的一些預防措施和注意事項。
文件架構
本文件分為六個明確界定的部分：
- 智能合約審計
- 基於智能合約的攻擊
- Tweag審計
- Marlowe中內置的安全增強功能限制
- 交易驗證
- 貨幣政策
作為一個整體，本文打算全面了解智能合約審計的重要性，以及目前存在的基於智能合約的不同類型的攻擊，然後再具體深入探討Marlowe工具套件如何利用審計和強大的安全原則來維護安全的智能合約開發環境。
智能合約審計
概覽
智能合約固有的自主性和某些交易中涉及的相對高風險意味著確保一致性和安全性是最重要的。這需要準確了解智能合約在執行時的行為，以便發現和解決任何潛在的缺陷或故意的惡意代碼。從安全角度對智能合約進行審計是防止後續失敗或損害的最佳方式。審計在部署前徹底檢查智能合約的代碼和條件，以確保合約的行為符合預期。
審計方式
雖然智能合約審計的方法可能不同，而且因項目而異，但智能合約可以使用人工或自動方法進行分析。通常情況下，大多數項目采用兩者的組合。
檔案搜集
在審計過程開始之前，審計人員可能會花一些時間收集任何與項目有關的文件。這可能包括技術文件、白皮書、代碼庫，以及任何其他可能與審計過程有關和有幫助的材料。
人工審計
這種形式的智能合約審計涉及一群人分析每一行代碼、合約邏輯、合約架構和任何內置的安全措施，以確保高效的設計和正確性。除了揭示編碼錯誤外，人工審計還可能發現設計缺陷。人工審計往往被認為是一種非常徹底和準確的方法。
自動化審計
與人工審計不同，自動審計通常采取以軟件為中心的測試方法。專有的或現成的軟件審計工具可能有助於發現錯誤，但某些漏洞可能不會變得明顯。
由於這些方法的互補性，最佳的審計實踐涉及手動和自動審計的結合，以確保所有潛在的缺陷、錯誤和漏洞被發現和糾正。
審計後的行動
一旦審計過程完成，審計師將提出一份報告，詳細說明他們的發現。這些報告可能包括按嚴重程度進行的錯誤分類和一系列的建議。
合約錯誤可分為：
– 重大型：這種類型的缺陷很可能會阻止合同和/或協議的安全運行。
– 大型：編碼或邏輯中的某些錯誤可能會導致資金損失，或出現不受控制的協議狀態。
– 中型：雖然資金可能沒有風險，但這些類型的錯誤可能會影響合約的執行或可靠性。
– 小型：這種分類通常包括對安全影響很小或沒有影響的低效代碼。
（補充資訊：通常指的是編碼風格或最佳實踐問題。）
智能合約審計的優點
雖然審計對任何應用程序都很重要，但對於在區塊鏈上運行的智能合約和去中心化應用程序（DApps）來說尤其關鍵，因為這些去中心化的賬本具有不可更改的性質。
智能合約審計的優勢包括主動識別風險，避免潛在的高成本錯誤，整體上有一個更好的開發環境，以及獲得關於漏洞的洞察力，以及如何消除它們。
主動識別分險
部署未經審計的智能合約是一場賭博，任何開發者或公司都不應該這樣做。一些智能合約可能涉及大量資金，如果丟失或受損，可能導致更大的責任。通過積極主動地補救這些風險，發生嚴重錯誤的可能性會大大降低。
避免潛在需大量花費的錯誤
由於編碼/邏輯錯誤或由於合同中的惡意幹擾，資金被永遠鎖定，這是任何客戶或開發者都不願意經歷的。經濟損失只是其中的一個方面。也可能有嚴重的法律後果。
一個整體更好的開發環境
對軟件進行審計不僅是推薦的，而且是一項要求。保證一個應用程序或一套應用程序的安全，並遵循最佳實踐，可以加強提供的服務，創造一個更健康的開發環境。
獲得關於脆弱性的見解，以及如何消除它們
在軟件開發中，預防要比修補好。而當涉及到智能合約時，由於區塊鏈的不可篡改性，沒有機會進行修補。徹底的審計將產生許多關於代碼、合約的邏輯、架構和許多其他參數的信息，使開發人員能夠完善並產生盡可能好的合約。
基於智能合約的攻擊
重複進入的攻擊
在這種攻擊中，一個智能合約函數通過調用第二個合約暫時放棄了對交易的控制，而第二個合約則開始對第一個合約進行遞歸提款調用，在第一個合約更新其狀態之前耗盡其資金。這些類型的攻擊之所以成為可能，是因為智能合約編碼中存在的漏洞。2016年的DAO事件涉及到一個重入式攻擊。
Cardano區塊鏈的設計使重入攻擊不可能發生。因為Cardano使用EUTXO模型，智能合約是原子性的，不會互相調用，這使得重入成為不可能。
前端入侵
一些區塊鏈設計允許智能合約和交易在被鏈上確認之前有一段時間是可以公開查看的。這些待定交易在整個網絡的內存池中共享，這使對手能夠看到合同的預期結果。這樣一個能看到待定交易的對手可以引入一個新的交易，因為他知道這樣做會在待定交易的基礎上獲得利潤，而犧牲其他用戶的利潤。從本質上講，對手操縱交易的執行順序對他們自己有利。
雖然這種類型的事件在其他區塊鏈上是一個大問題，但沒有證據表明Cardano（以及延伸到Marlowe）會受到前面運行的入侵。
預言機操控
預言機將區塊鏈與外部系統連接起來，智能合約可能會根據從預言機收到的數據執行。這種對外部系統的依賴性意味著，如果預言機收到的輸入在輸入到預言機之前被操縱了，智能合約執行的安全性和完整性可能會受到影響。
其他常見的基於智能合約的安全漏洞包括算術錯誤、整數溢出和下溢、智能合約可見性設置和時間戳操縱。
Tweag 審計
本節重點介紹Tweag安全審計的結果，Marlowe團隊的回應，以及Marlowe設計中的安全原則。
特威格安全審計的主要結果和內部回應
特威格對Marlowe語言進行了手動和自動審計，發現了幾個問題。
高嚴重度的發現包括負數存款的處理，防止 “雙重滿足”，狀態不變性的執行，正式規範與Plutus實現之間的實施差異，以及貨幣保存定理的證明。
負數存款處理
存款收入的計算方法是將存款輸入相加，不管它們是否為負數，而語義學認為它們是零存款。再加上沒有對結束的馬洛狀態進行余額檢查，這使得結束的余額與支付給馬洛驗證人的價值不同。這可以被一個允許負數存款的Marlowe合同所利用。
內部回應
這個問題已經通過在Marlowe語義驗證器中添加一個針對負數存款的防護措施來解決。該防護措施確保驗證器對負數存款的語義與Marlowe的Isabelle語義一致。具體來說，一個負數的存款被視為零的存款。因此，一個負的存款不會減少Plutus數據中的任何賬戶余額，而且內部餘額的總和將與UTXO中持有的Marlowe語義腳本地址的值相匹配。
預防雙重滿足
盡管Marlowe驗證器防止了在同一交易中運行的多個Marlowe驗證器腳本副本之間的雙重滿足，但在同一交易中Marlowe驗證器與另一個Plutus驗證器同時運行的情況下，它並沒有防止。
內部回應
現在，通過強制要求Marlowe驗證器是唯一在交易中運行的Plutus腳本，以防止雙重滿足。這允許Marlowe合約與其他Plutus腳本協調，但只在不可能有雙重滿足的情況下。添加了一些基於屬性的測試來檢查這個緩解措施的正確性。
狀態不變性的強制執行
最初，Marlowe驗證器對自己的正確操作做了樂觀的假設，並且沒有檢查某些不變量，以減少Plutus的執行成本。
內部回應
Marlowe語義驗證器現在嚴格執行初始和最終狀態的不變性，確保正數帳戶、不重覆的狀態條目（賬戶、選擇和約束值）以及總的內部值與腳本UTXO的值相匹配這三個狀態不變性。
正式規範與Plutus實施之間的實施差異
審計揭示了正式規範和實際的Plutus實現之間的一些差異。具體來說，是關於Isabelle、Haskell和Plutus Tx的語言差異和效率考慮。
形式化的規範是用Isabelle編寫的，這是一種形式化方法的語言，而實際的Marlowe實現是用Haskell和Plutus Tx編寫的。Marlowe團隊盡可能地遵循Isabelle的規範，但是由於語言的不同，一些偏差是不可避免的。例如，Marlowe實現的某些方面在Isabelle中是低效的，所以必須進行修改以獲得更高效的Haskell實現。
內部回應
這個問題通過代碼分析和基於屬性的測試得到了緩解
貨幣保全定理的證明
貨幣保全定理只考慮了資產的數量，而沒有考慮其類型。這意味著該證明不會考慮這樣一種情況：例如，一個合同可以收到20阿達和15傑德，並償還20傑德和15阿達。
內部回應
對Isabelle代碼的修訂彌補了這個問題。具體來說，增加了一個新的MultiAssets類型，並重構了Isabelle代碼（沒有修改解釋器），以證明資產被保留下來。
Marlowe的內置安全增強功能限制
Marlowe具有幾個限制，以確保某些安全風險無法發生。
– 合約是有限的
– 合約會終止
– 合約有明確的有效期
– 合約結束時沒有資產被保留
– 價值是保存的
除了這些限制外，為了確保安全，Marlowe中沒有一些編程語言結構：
– 不允許遞歸
– 不支持循環
– 不允許定義函數
– 超時必須是數字常數
– 只有Case continuations可以被merkleized。Faustus編程語言放寬了上面的一些限制，但它可以編譯成安全的Marlowe。
安全分析工具
Marlowe團隊設計的marlow-cli運行分析工具檢查Marlowe合約與Cardano賬本規則的兼容性。
Cardano帳本有內置的限制，可能會阻止Marlowe合約在鏈上運行，即使合約本身對Marlowe語言來說是有效的。例如，帳本對角色和代幣名稱的長度進行了限制，還限制了Plutus的執行成本。任何違反這些規則的合約都不會在鏈上運行，即使該合同可能是正確構建的。同樣，雖然合約可能在Playground上運行，但如果合同違反了分類帳的限制，它們也不會在鏈上運行。了解更多關於內置分類賬設計限制的信息。
主要啟發： Playground是關於語言的，而Runtime是關於在Cardano區塊鏈上具體實現Marlowe合約的。如果有人在其他區塊鏈上實現Marlowe，你仍然可以使用Playground，但你不能在其他區塊鏈上使用Runtime。
注意： 如果數據點不適合在鏈上，合同會被鎖定，但Marlowe套件包括評估這種風險的工具。這些工具應該在部署合約之前使用。
交易驗證
有兩種Plutus驗證器腳本參與驗證UTXO支出：
– 語義驗證器
– 支付驗證器
安全實踐表明，除非交易的內容和影響已經被審查並被充分理解，否則不應該簽署交易。在Marlowe環境中，這意味著驗證Marlowe合同，它的輸入和它的狀態。這也意味著要確保所使用的角色鑄幣策略（如果有的話）和Marlowe驗證器是正確的。
下面的安全考慮適用於兩種驗證器腳本類型。
語義驗證器
在簽署Marlowe交易之前，應充分了解以下概念：
- 該交易是否操作Marlowe合約？
- 它的鑄幣政策中的角色是什麽（如果有的話）？
- 角色代幣是如何分配的（如果有的話）？
- 當前的合約和它的狀態是什麽？
- 哪些輸入正被應用於該合約？
- 該交易中還發生了什麽？
該交易是否操作Marlowe合約？
Plutus驗證器腳本是所有指定版本的Marlowe合約的通用解釋器，這意味著一個Marlowe合約的UTXO駐留在一個腳本哈希中。驗證一個交易從一個將Marlowe腳本哈希值作為其支付部分的地址支出，就可以確認真正的Marlowe驗證器將運行以驗證該特定UTXO的支出。通過編譯驗證器並計算其哈希值，可以從第一原理上計算出Marlowe驗證器的腳本哈希值，前提是這個存儲庫中的Marlowe腳本源代碼可以被信任。
它的鑄幣政策中的角色是什麽（如果有的話）？
鑄幣政策是創建特定代幣類型的代幣的規則集，由其鑄幣政策的哈希值識別。這被稱為造幣政策ID。鑄幣政策決定了是否可以創建新的代幣，或者已經創建的代幣是否就是全部。
例如，Marlowe合同的各方，如貸款人和借款人，可以用兩種方式表示：
- 通過地址：每一個地址類型的當事人都對應於一對公鑰和私鑰的實例，這對公鑰和私鑰大概由其中一個當事人的錢包持有。使用地址來代表各方比使用角色更簡單、更便宜。為了認證自己，由地址代表的各方只需要簽署需要他們認證的交易（即那些為該方執行存款或選擇）。
- 通過角色令牌：每一個角色類型的當事人都對應著一個存儲在鏈上的令牌。對於一個合同使用角色令牌作為認證，該合同需要聲明其角色令牌的鑄幣政策ID是它想作為角色令牌的鑄幣政策ID。在這種情況下，由鑄幣政策ID識別的令牌的每個資產名稱都代表不同的一方。為了驗證交易，角色令牌所有者只需要將其作為需要驗證角色令牌所有者的交易的一部分。有可能存在不止一個具有相同資產名稱的令牌，所以從技術上講，你並不擁有一個角色方，除非你擁有具有該方資產名稱的角色令牌的所有實例。
角色代幣是如何分配的（如果有的話）？
如果一個合約只使用地址來代表各方，那麽角色的鑄幣政策就不是一個問題。地址的缺點是它們不能被證明地轉移，所以一旦知道了地址的私鑰，你就不能表明你已經忘記了它並刪除它。從地址接收者的角度來看，地址始終是不安全的。擁有安全地址的唯一方法是自己生成。
優點或作用是，因為代幣被視為鏈上的原生資產，它們可以像ada或任何其他資產一樣被轉讓。但是，任何擁有具有正確鑄幣政策ID和資產名稱的代幣的人都可以作為它所代表的一方，所以你需要確保你是唯一擁有這種代幣的人，否則你就不能真正控制這一方。
當然，你可以通過自己鑄造角色代幣來確保你是唯一擁有該代幣的人（Marlowe Runtime會在合同創建過程中安全地完成這一過程）。如果有其他人鑄造了角色代幣或創建了合約，你需要確保：
- 你擁有所有現有的控制方的代幣
- 不能再創建此類代幣（因為鑄幣政策不允許）
當前的合約和它的狀態是什麽？
合約的交易前狀態是在與正在從Marlowe腳本地址花費的UTXO相關的Plutus數據中定義的。這個數據集必須在交易中提供，並且必須包含以下內容：
- 合約內部賬戶的餘額
- 在合約執行過程中，到此為止的選擇歷史
- 合約中綁定的變量的當前值
- 合約中尚待執行的部分
數據可以從無符號的交易主體中提取，並使用函數Plutus.V2.Ledger.Api.fromData將其反序列化為Language.Marlowe.Core.V1.Semantics.MarloweData。
或者是：
- 命令行工具
marlowe log --show contract將顯示合約的鏈上歷史。 - 這個在線工具還可以查看合約和鏈上狀態。
- REST API提供了通過
marlowe log --show獲得的相同信息。
哪些輸入正被應用於該合約？
與從Marlowe腳本地址花費UTXO相關的Plutus贖回者定義了被應用於合同的輸入，以及在交易主體中指定的交易的槽有效期。輸入是一個由零個或多個存款、選擇和通知組成的序列。使用像Marlowe Playground或marlow-cli run prepare這樣的工具，可以分析將這個輸入應用到合約中的後果。
贖回者可以從未簽名的交易主體中提取，並使用函數Plutus.V2.Ledger.Api.fromData將其反序列化為Language.Marlowe.Scripts.MarloweInput。命令行工具marowe-cli util slotting將計算出有效性間隔中提到的槽與合同中的POSIX時間之間的關系。
該交易中還發生了什麽？
未簽署的交易可能包含了Marlowe合約規定之外的其他支出和付款。這可以用工具cardano-cli transaction view來檢查。
貨幣政策
通常情況下，應該使用貨幣政策（如Marlowe Runtime支持的貨幣政策），強制執行單一的造幣事件和每個角色的單一代幣。這些政策確保角色代幣是真正的不可偽造的代幣（NFT），所以角色代幣持有者是可以驗證的唯一可以作為合同中的當事人的人。
鑄造多份特定角色代幣的貨幣政策，或具有開放鑄造政策的政策，支持非標準的用例。例如，鑄造每個角色代幣的兩個副本，並將其分配給同一方，如果包含 "熱 "角色代幣的錢包無法訪問，該方可以將一個代幣放入冷庫作為備份。一些新穎的眾包合同可能涉及到將角色（通過相同的角色代幣，甚至在合同開始後也可能被鑄造）分配給許多參與者。最後，Plutus合約對角色代幣的鑄造政策可以與一個或多個Marlowe合約的運作相協調。
角色代幣
角色令牌可以授權Marlowe交易中的存款和選擇。授權使用角色代幣比用公鑰授權更靈活，因為角色代幣（以及因此參與Marlowe合約）可以在錢包之間轉移或轉移給其他人。
Marlowe驗證器腳本不對角色令牌執行任何特定的貨幣政策，以實現新的使用案例。然而，在基於角色的Marlowe合同中，授權的安全性確實嚴重依賴於角色代幣的貨幣政策。這意味著貨幣政策和代幣的鏈上支付都應該在參與Marlowe合約之前進行仔細的審查。驗證一個簡單腳本的貨幣政策需要從區塊鏈上檢索腳本並研究它。驗證Plutus腳本的貨幣政策包括獲取和研究該腳本的Plutus源代碼，並對源代碼進行哈希運算以檢查貨幣政策ID。
特別感謝：Joseph Fajen、Brian Bush和Omer Husain都對本文做出了寶貴的貢獻。