接著，我們談一談目前的難點以及影響ZK證明投入實踐的主要障礙。大多數傳統的ZK協議要求底層語句必須首先用布林電路（Boolean circuit）或無迴圈的運算電路（即組合電路）來表示。對於布林電路，可以用AND門、NOT門和XOR門，而對於運算電路，可以用ADD門和MULT門可以想象，要想把一個要證明的語句轉換成這樣的電路並不容易，如果還沒有簡潔的數學公式，更是難上加難。例如，如果一個程式包含迴圈行為，那麼在電路生成之前，必須先把它展開，而當程式包含資料依賴型迴圈時，那就無法展開了。
另外，電路尺寸也會影響到ZK協議的效率。一般情況下，驗證時間與電路尺寸至少呈線性關係（通常，各個門的開銷通常很大且恆定）。因此，在漏洞披露時，ZK證明需要底層漏洞能被尺寸合適的電路捕捉到。
證明可利用性
由於ZK證明一般會接收寫成布林電路的語句，因此，這裡的難點在於需要布林電路僅在漏洞利用成功時返回“true”，以此表示存在漏洞利用。
我們希望當驗證人向程式中匯入會造成漏洞利用的輸入時，電路能夠接收（accept），例如：能夠讓攻擊者取得程式執行許可權的緩衝區溢位（buffer overflow）。由於大多數二進位制漏洞利用針對的是二進位制（binary）和特定的處理器，因此，我們的電路必須準確地對程式的目標編譯架構進行建模。最後，當程式成功執行時，以及當漏洞利用在執行過程中被觸發時，我們需要一個電路來接收。
初級的方法是開發一個電路來代表目標建模處理器的“一步”（one step）。接著，我們根據要執行的程式，將容納該程式的記憶體初始化；按照程式的啟動時間，設定程式計數器；驗證人使程式執行在自己的惡意輸入上——重複處理器電路，直至程式結束，檢查每一步是否均滿足了漏洞利用條件。也就是說檢查程式計數器是否被設定成了一個已知的“惡意”（bad）值，或被寫入了一個有許可權的記憶體地址。關於此策略的重要注意事項：在每一步均需要完整執行整個處理器電路（即便實際上只有一條指令在執行），因為單獨列出一項功能會洩露相關的跟蹤資訊。
不幸的是，這種方法會導致電路過大，因為程式執行的每一步都需要有一個電路對核心處理器邏輯及整個RAM進行建模。即便我們把RAM限制成50 MB，對於一次漏洞利用，如果其跟蹤使用了100條指令，那麼產生一條相應的ZK語句會導致電路至少達到5GB。這種方法效率太低，無法用於有意義的程式。關鍵問題在於電路尺寸與跟蹤長度和RAM大小成線性關係。為了解決這個問題，我們採用了SNARKs for C的方法，即把程式執行證明分為兩部分，一部分為核心邏輯，另一部分為記憶體正確性。
要證明邏輯有效性，必須將處理器電路應用於程式跟蹤中連續的每一對指令（sequential pair of instructions）。該電路可以驗證一個暫存器狀態能否合法地跟隨另一暫存器狀態。如果每一對狀態均有效，則電路接收。不過要注意，這裡的前提是記憶體操作是正確的。如果轉移函式電路中存在一個儲存器檢查器，則會產生開銷，此開銷與所使用的RAM大小成比例。
讓驗證人也輸入一個記憶體排序的執行跟蹤，就能進行記憶體驗證。如果第一個記憶體地址訪問了一個低於第二個記憶體地址的記憶體地址（破壞了時間戳（timestamp）關係），那麼這個跟蹤就會在另一個跟蹤之前放置一條跟蹤記錄。這個跟蹤能讓我們線性地掃描記憶體排序指令，確保記憶體訪問的一致性。此方法無需根據RAM大小建立相應尺寸的電路。不過，該電路與跟蹤尺寸呈線性關係，並且僅能執行基礎的相等性檢查（equality check），不能明確地記錄每一步下的完整RAM。
最後一個要解決的問題是，驗證人不受阻撓地使用與最初情況不符並且無法建立假證明的記憶體排序跟蹤。要解決此問題，我們必須新增一個“排列檢查器”（permutation checker）電路來驗證我們是否確實根據記憶體位置對程式跟蹤進行了排序。欲進一步瞭解相關討論，請參見SNARKs for C論文。
建模x86
知道了如何證明ZK中存在漏洞利用，接下來我們需要把相關的處理器架構建模成布林電路。此前已經有人對TinyRAM進行了建模，這是一種RISC架構，其目標是在ZK環境中高效執行。不幸的是，TinyRAM並未商用，而且由於漏洞利用大多依賴特定於架構的行為，因此TinyRAM不能為現實程式提供ZK可利用性證明。
我們接下來將透過建模一種相對簡單且應用廣泛的微處理器——MSP430進行建模，以開發ZK可利用性證明，這種簡單的晶片被廣泛應用於各種嵌入式系統。另外，Microcorruption CTF系統也是基於MSP430執行。我們的首要目標是針對Microcorruption受到的每一次挑戰提供ZK證明。在完成此“可行性演示”後，我們會轉向x86。
從簡單的RISC架構過渡到複雜的CISC架構，隨之而來的是各種複雜問題。對於RISC處理器的電路模型，每週期的時鐘門為1至10k。另一方面，如果我們的x86處理器達到10萬門級別，那麼對於需要10000條指令才能完成的漏洞利用，ZK證明會達到48 GB。由於x86比MSP430複雜了幾個數量級，因此即便把邏輯證明和儲存器正確性證明分開，也無法天真地將其功能實現為布林電路。
我們的解決方案基於一個顯而易見的事實，即沒有程式能完全用盡x86。一個程式在理論上能用到x86所支援的全部3000條指令，但實際上，大多程式只用到了幾百條。我們會使用程式分析技術來判斷特定二進位制所需的x86最小子集，並動態地生成能夠驗證其正確執行能力的處理器模型。
當然，我們無法支援部分x86指令，因為這些指令實現了資料依賴型迴圈。例如，repz會重複後續指令，直至rcx為0。對於這樣的指令，只有在執行時才能確定其實際行為，而我們的處理器電路必須是組合電路，因此無法支援此類指令。為了處理這些指令，我們會把一個靜態二進位制轉換器（binary translator）從普通x86轉成特定於我們程式的x86子集。這樣的話，我們就能夠處理最複雜的x86指令，而無需將其硬編碼到我們的處理器電路中。
新型的bug披露模式
能夠與約翰斯·霍普金斯大學以及DARPA SIEVE專案的同仁共同啟動這項工作，我們倍感興奮。我們希望得到能夠從根本上顛覆漏洞披露方式的工具，以便企業能夠明確其bug懸賞範圍，漏洞研究人員可以安全地提交能明確證明其掌握了漏洞利用情況的證明。而且，我們還希望ZK漏洞披露能成為消費者的保護傘。研究人員可以在不公佈相關漏洞的情況下，警告使用者特定裝置存在潛在危險，這麼做是在向企業施壓，逼迫他們解決本不願解決的問題。
更廣泛地說，我們想把ZK證明從學術界帶入產業界，使其更貼近當今的軟體、更實際。關於此技術，若您有特定用途且未在本文中未提及，我們歡迎您來函。關於ZK證明方案與電路編譯器的複雜生態系統，我們積累了相應的專業知識，可為您提供幫助！
*在此我們要特別感謝Colleen Swanson和Marcella Hastings，感謝他們的校對工作，以及他們關於本文的寶貴反饋。
