標題：Amarna：Cairo程序的靜態分析

我們正在開源Amarna，這是我們用於Cairo 編程語言的新靜態分析器和linter（檢查代碼風格/錯誤的小工具）。 Cairo 是一種編程語言，為擁有數百萬美元資產的多個交易交易所提供支持（例如由StarkWare 驅動的dYdX），並且是StarkNet 合約的編程語言。但是，與其他語言不同，它也有一些奇怪的功能。因此，我們將首先簡要概述該語言、其生態系統以及開發人員應注意的該語言中的一些漏洞。然後，我們將介紹Amarna 並討論它是如何工作的？

為什麼我們需要Cairo？ Cairo以及類似的語言(如Noir和Leo)的目的是編寫“可證明的程序”，其中一方運行程序並創建一個證明，證明它在給定特定輸入時返回特定輸出。

假設我們想將程序的計算外包給某個服務器，並且需要保證結果是正確的。使用Cairo，我們可以獲得程序輸出正確結果的證明；我們只需要驗證證明而不是自己重新計算函數（這將違背外包計算的初衷）。

總之，我們採取了以下步驟：

1.導出我們要計算的函數。

2.使用的具體輸入在工作設備上運行該函數，獲得結果，並生成計算有效性的證明。

3.通過驗證證明來驗證計算。

Cairo編程語言如上所述，Cairo 編程模型涉及兩個關鍵角色：運行程序並創建程序返回特定輸出的證明的驗證程序，以及驗證驗證程序創建的證明的驗證程序。

然而，在實踐中，Cairo 程序員實際上不會自己生成或驗證證明。相反，生態系統包括以下三個部分：

1.SHARed Prover (SHARP) 是一個公共驗證程序，它為用戶發送的程序跟踪生成有效性證明。

2.證明驗證程序合約驗證程序執行的有效性證明。

3.可以查詢事實註冊合約來檢查某個事實是否有效。

事實註冊表是一個數據庫，用於存儲程序事實，或從程序及其輸出的哈希計算的值；創建程序事實是將程序綁定到其輸出的一種方法。

這是Cairo的基本工作流程：

1.用戶編寫程序並將其跟踪提交給SHARP（通過Cairo Playground 或命令cairo-sharp）。

2.SHARP 為程序跟踪創建一個STARK 證明，並將其提交給證明驗證程序合約。

3.證明驗證程序合約驗證證明，如果有效，則將程序事實寫入事實註冊表。

4.任何其他用戶現在都可以查詢事實註冊表合約以檢查該程序事實是否有效。

還有兩件事要記住：

Cairo 的內存是一次性寫入的：一個值寫入內存後，就無法更改。

assert語句assert a=b的行為會根據a是否被初始化而不同：如果a 未初始化，則assert 語句將b 分配給a；如果a 被初始化，assert 語句斷言a 和b 相等。

儘管Cairo 的語法和關鍵字的細節很有趣，但我們不會在這篇文章中討論這些主題。

設置和運行Cairo代碼現在我們已經簡要地概括了Cairo語言，接下來討論如何設置和運行Cairo代碼。考慮以下簡單的Cairo程序。這個函數計算一對數字(input, 1) 的Pedersen 哈希函數，並在控制台中輸出結果：

要設置Cairo 工具，我們使用Python 虛擬環境：

然後，我們編譯程序：

最後，我們運行程序，它將輸出以下值：

這個值就是(4242, 1)的Pedersen hash對應的字段元素。

現在，假設我們將輸入從4242 更改為某個隱藏值，而是為驗證程序提供以下輸出：

為什麼驗證程序會相信我們？好吧，我們可以證明我們知道使程序返回該輸出的隱藏值！

為了生成證明，我們需要計算程序的哈希來生成程序事實。這個哈希值不依賴於輸入值，因為賦值是在一個提示中進行的(這是Cairo的一個奇怪設置，我們將在本文後面討論)：

然後，我們可以通過使用事實註冊表合約並以程序事實作為輸入調用isValid 函數來檢查程序事實的有效性：

調用isValid 函數檢查程序事實有效性的結果。

概括地說，我們運行了程序，SHARP創建了一個可以在事實註冊表中查詢的證明，以檢查其有效性，證明我們確實知道將導致程序輸出該值的輸入。

現在，我實際上可以告訴你，我使用的輸入是71938042130017，你可以繼續檢查結果是否匹配。

Cairo功能Cairo有幾個奇怪功能，新的Cairo程序員可能還使不習慣。我們將描述三個容易被濫用並導致安全問題的Cairo 習慣：Cairo 提示、遞歸和欠約束結構之間的相互作用以及非確定性跳轉。

提示

提示是特殊的Cairo 語句，基本上使驗證程序能夠編寫任意Python 代碼。是的，以Cairo 提示編寫的Python 代碼實際上是被執行的！

提示寫在%{ %} 中。我們已經在第一個示例中使用它們給輸入變量賦值：

因為Cairo 可以在提示中執行任意Python 代碼，所以你不應該在自己的設備上運行任意Cairo 代碼，這樣做可以將你的設備的完全控制權授予編寫代碼的人。

提示通常用於編寫僅由驗證程序執行的代碼。證明驗證程序甚至不知道提示的存在，因為提示不會改變程序哈希。下面來自Cairo playground的函數計算一個正整數n的平方根：

該程序通過使用提示中的Python數學庫計算n的平方根。但是在驗證時，這段代碼不會運行，驗證程序需要檢查結果是否真的是平方根。因此，在函數返回結果之前，函數包含一個檢查，以驗證n是否等於res * res。

Underconstrained結構Cairo 缺乏對while 和for 循環的支持，程序員只能使用原有的舊遞歸進行迭代。讓我們考慮一下Cairo的“動態分配”挑戰。挑戰要求我們編寫一個函數，給定一個元素列表，將這些元素平方，並返回一個包含這些平方元素的新列表：

運行此代碼將按預期輸出數字1、4、9和16。

但是，如果發生錯誤（或錯誤的錯誤）並導致以零長度調用sqr_array 函數會發生什麼？

基本上，會發生以下情況：

sqr_array 函數將分配res_array 並調用_inner_sqr_array(array, res_array, 0)。

_inner_sqr_array 會將長度與0 進行比較並立即返回。

sqr_array 將返回已分配（但從未寫入）的res_array。

那麼當你在new_array 的第一個元素上調用serialize_word 時會發生什麼？

按原樣運行代碼將導致錯誤，因為new_array的值是未知的：

按原樣運行上述代碼後出現的錯誤。

但是，請記住，通常你不會運行代碼。你將驗證程序輸出某些值的證據。而且我實際上可以向你證明該程序可以輸出你想要的任何四個值！

下面的事實將該程序與輸出[1,3,3,7]綁定：

根據事實註冊合同，這一事實是有效的：

事實註冊表對程序事實的驗證。

可以看到，由於返回的數組只是分配的，從不寫入（因為它的長度為0，所以遞歸一開始就停止），驗證程序可以在提示中寫入數組，提示代碼不會影響程序的哈希！

惡意的sqr_array 函數實際上如下：

簡而言之，如果有一些錯誤使數組的長度為0，惡意驗證程序可以創建他想要的任意結果。

你可能會有疑問，惡意驗證程序不能簡單地在程序末尾添加一個提示來以他希望的任何方式更改輸出。好吧，他可以，只要之前沒有寫過那個內存；這是因為Cairo 的內存是一次性寫入的，所以每個內存單元只能寫入一個值。

由於Cairo中內存的工作方式，這種創建最終結果數組的模式是必要的，但它也存在安全問題的風險：跟踪該數組長度的一個簡單的錯誤可能允許惡意驗證程序任意控制數組內存。

非確定性跳躍對於第一次閱讀Cairo的程序員來說，非確定性跳躍是另一種看起來不自然的代碼模式。它們結合提示和條件跳躍來重定向帶有某個值的程序控制流。驗證程序可以不知道這個值，因為驗證程序可以在提示中設置它。

例如，我們可以編寫一個程序，檢查兩個元素x和y是否相等，方法如下：

運行此程序將返回預期結果（0 表示不同的值，1 表示相等的值）：

然而，這個函數實際上很容易受到惡意驗證程序的攻擊。注意跳躍指令如何僅依賴於提示中的值：

而且我們知道提示完全可以由驗證程序控制！這意味著驗證程序可以在該提示中編寫任何其他代碼。事實上，不能保證驗證程序確實檢查了x 和y 是否相等，甚至不能保證x 和y 以任何方式使用過。由於沒有其他檢查，該函數可以返回驗證程序想要的任何內容。

正如我們之前看到的，程序哈希不考慮提示中的代碼；因此，驗證程序無法知道是否執行了正確的提示。惡意驗證程序可以通過更改提示代碼並將每個證明提交到SHARP。

那麼我們如何解決這個問題呢？每當我們看到非確定性跳轉時，我們需要確保跳轉是有效的，並且驗證程序需要驗證每個標籤中的跳轉：

在本例中，該函數足夠簡單，代碼只需要一個if語句：

在審核Cairo代碼時，我們注意到除了VScode中的語法高亮顯示外，基本上沒有任何形式的語言支持。然後，當我們在代碼中發現問題時，我們希望確保類似的模式不會出現在代碼庫的其他地方。

我們決定為Cairo 構建Amarna，一個靜態分析器，這樣就能夠創建自己的規則並蒐索我們感興趣的代碼模式，不過不一定是安全漏洞，但任何安全敏感操作都需要分析或檢查代碼時需要更多的關注。

Amarna 將其靜態分析結果導出為SARIF 格式，使我們能夠使用VSCode 的SARIF Viewer 擴展輕鬆地將它們集成到VSCode 中，並查看代碼中帶下劃線的警告：

帶有下劃線的dead store（左）和顯示來自Amarna 的結果的SARIF Viewer 擴展的Cairo 代碼（右）。

Amarna是如何工作的？ Cairo 編譯器是用Python 編寫的，它使用解析工具包lark 來定義語法並構建其語法樹。使用Lark 庫，可以直接為程序的抽象語法樹構建訪問者。從這裡開始，編寫規則就是對要在樹中找到的內容進行編碼。

我們編寫的第一條規則是強調算術運算+、-、* 和/的所有用途。當然，並非所有除法的使用都是不安全的，但是在這些操作下劃線後，開發人員會被提醒Cairo算術在有限域上工作，並且除法不是整數除法，就像在其他編程語言中那樣。字段算術下溢和溢出是開發人員需要注意的其他問題。通過突出顯示所有算術表達式，Amarna 幫助開發人員和審查人員快速放大代碼庫中在這方面可能存在問題的位置。

檢測所有分區的規則很簡單：它基本上只是創建帶有文件位置的結果對象並將其添加到分析結果中：

當我們尋找更複雜的代碼模式時，我們開發了三類規則：

1.本地規則獨立分析每個文件。上述用於查找文件中所有算術運算的規則是本地規則的一個示例。

2.收集規則獨立地分析每個文件，並收集供後處理規則使用的數據。例如，我們有收集所有聲明函數和所有調用函數的規則。

3.在分析所有文件並使用收集規則收集的數據之後，將運行後處理規則。例如，在收集規則找到文件中所有聲明的函數和所有調用的函數之後，後處理規則可以通過標識聲明但從未調用的函數來找到所有未使用的函數。

到目前為止，我們已經實施了10 條規則，其影響範圍從幫助我們審核代碼的信息性規則（標記為Info）到可能對安全敏感的代碼模式（標記為警告）：

雖然這些規則中的大多數屬於信息類別，但它們肯定具有安全含義：例如，未能檢查函數的返回碼可能會非常嚴重（想像一下，如果函數是簽名驗證）；錯誤代碼規則將找到其中一些實例。

未使用的參數規則可以找到函數中沒有使用的參數，這是通用編程語言linter 中的常見模式；這通常表明存在使用該參數的某種意圖，但從未實際使用過，這也可能具有安全隱患。