CertiK：AI 更會找漏洞，合約稽核還夠用嗎？

0:00AI 讓攻防變不對稱

0:00大家早安。接下來幾分鐘，我想分享形式化驗證可以怎麼改寫智慧合約開發的安全樣貌。這其實也回應了 Matthew 的問題：我們想修的是「相信你的程式碼是安全的」這個信任問題。我覺得目前還是沒修好。近幾年我們看到，AI agent 進展非常劇烈。Good morning, everyone. In the next few minutes, I want to share with you how formal verification can help to reshape the landscape of security in smart contract development. So that basically also answers the question of Matthew: that we are trying to fix the trust problem of trusting your code is secure. I think it's still not working. So, as we see in recent years, AI agents have made drastic advancements.

0:47大型語言模型找到的漏洞，比我們以前能想像的多得多。這個趨勢還沒停，我們可以預見不久之後，AI agent 還能挖出比現在更深的漏洞。重點是這樣：如果你的程式碼裡有任何 bug，AI agent 一定找得到。這就變成安全工程師、開發者跟攻擊者之間的不對稱戰爭。過去，安全工程的目標是提高攻擊成本。And the large language models find much, much more vulnerabilities than we could ever imagine before. And the trend is still not stopping, as we can foresee that in the near future, AI agents can reveal even much deeper vulnerabilities than we've ever seen. And also, the takeaway is like this. So if your code contains any bugs, an AI agent will definitely find it. So that becomes an asymmetric battle between the security engineers, the developers, and the attackers. So in the past, the goal of security engineering is to increase the cost of the attack.

1:44只要攻擊成本高於利用漏洞能拿到的收益，我們就可以把系統看成安全。但兩邊都有 AI agent 幫忙之後，砝碼就不平衡了。攻擊者只要找到一個 bug，就能利用整個系統。安全研究員跟開發者卻必須找到全部、修掉全部，還得確保補丁沒有引入更多 bug。DeFi 系統彼此還總是連在一起。例如一個 DEX 通常需要預言機或橋才能運作。As long as the cost of the attack is higher than the gain of the exploit, we can consider that the system is secure. However, with the help of AI agents on both sides, the weight is not balanced here. As we can see, the attackers only need to find one bug in order to exploit the entire system. However, the security researchers and the developers need to find all of them and also patch them, and make sure that your patch does not introduce more bugs. Also, for a DeFi system, those systems are always interconnected with each other. For example, a DEX usually needs some oracles or bridges to make it work.

2:34所以攻擊者只要在整個系統層級裡找到最弱的模組，就能發動攻擊。安全研究員跟開發者卻必須把整個系統加固才算安全。結論是：攻擊者與安全研究員、開發者之間的成本效益並不平衡。攻擊者這邊，即使技術沒那麼高的人，只要燒掉一些 token，就能利用 DeFi 智慧合約協議後面跑著的大量資產。防守者則必須燒掉更多 token，才能把所有 bug 排除掉。So the attackers only need to find the weakest module in the entire system hierarchy so that they can just launch the attack. However, the security researchers and the developers need to strengthen the entire system in order to make it secure. So it comes to the conclusion that the cost-effectiveness is not balanced between the attackers and the security researchers and developers. For the attackers, even a less-skilled attacker, they just can burn some of the tokens and they can exploit a huge amount of assets that are running behind the protocol of the DeFi smart contract. But for the defenders, they need to burn more tokens in order to exclude all the bugs.

3:27上線前用形式化驗證消掉漏洞

3:27這場不平衡、不對稱的戰爭，有解法嗎？談解法之前，先把現實寫下來。第一個事實：程式碼裡有 bug，AI 就會找到。第二個事實：防守者找 bug 永遠比攻擊者更貴。第三個事實：防守者有先跑的優勢。我想這是我們相對攻擊者最後的優勢。三個事實寫完，目標就清楚了：必須在合約上線前消掉所有 bug，而且要划算。So, are there any solutions to this unbalanced or asymmetric battle? Before we talk about solutions, let's first write down the realities. The first fact is that if there is a bug in your code, AI will find it. And the second fact is that it always costs the defenders more to find bugs than the attackers. And the third fact is that defenders have a head start. So I guess that is our last advantage over the attackers. So the goal is clear after we write down these three facts. We must eliminate all the bugs before a contract goes online and do it cost-effectively.

4:12來看我們的工具箱。測試、fuzzing、專家審查，這些都是在搜漏洞，不是在消漏洞。它們是好方法，大概不是我們要找的答案。這種情況我們可能得出盒子外面。不能只搜 bug，要找另一種解法。我們能不能寫下一條規則，而這條規則永遠不會被打破？答案是：如果我們能確保這個合約能接受的所有情況、所有場景，都只被我們寫下的模型允許。So let's look into our toolbox. What we have, for example, testing, fuzzing, or having an expert review. All of them are trying to search for bugs, not to eliminate them. So they are good solutions, probably not the answers that we are searching for. And in this case, we probably need to jump out of the box. We need to not just search for the bugs. We need to find another solution. So can we just write a rule, and can this rule ever be broken? And the answer is that if we can make sure all the cases, all the scenarios this contract can accept, all of them are only allowed by the model that we have written.

5:07那樣我們就能確定程式碼真的安全，而且已經消掉所有 bug。這種做法通常叫做形式化驗證。什麼是形式化驗證？基本上可以拆成三步。第一步，把程式碼變成嚴謹的數學模型，好在那個模型裡真正推理程式碼的執行。第二步是規格。規格幫我們把對程式碼的意圖或期望，翻譯成數學公式。So in that case, we can make sure that our code is actually secure and it has eliminated all the bugs. So this way is usually called formal verification. So what is formal verification? It basically can be split into three steps. The first step is to turn our code into a rigorous mathematical model, so that in that model we can really reason about the execution of the code. And the second step is about specification. Specification helps us to translate our intention or our expectation to the code into some mathematical-based formulas.

5:55第三步，真正寫下機器可檢查的證明：對任何情況，如果程式執行把狀態從 S 轉到 S'，那 S 跟 S' 都滿足形式規格。形式化驗證看起來很簡單，也很強大，但為什麼多數公司現在還沒在用？做了幾十年形式化驗證之後，我們找出兩道擋住它被廣泛使用的障礙。And the third step is to really write down the machine-checkable proof that shows that, for any cases, if our code execution transits the states from S to S prime, then S and S prime satisfy the formal specification. So formal verification seems very simple, and it is very powerful, but why do most of the companies not already use it right now? So, after decades of working on formal verification, we have identified two obstacles to prevent this from being widely used.

6:44AI 原生證明器與 SMT

6:44第一道障礙是怎麼寫證明。回想高中幾何或大學微積分，你就知道寫數學證明要花很多力氣。更別說要證明整個程式庫安全，每個函式都得寫證明。第二道障礙比第一道更難：形式規格該寫什麼？我們該證明什麼？這種情況你不只得知道程式碼打算做什麼、背景是什麼。The first barrier is how to write the proof. If you can recall your high school geometry lessons or your college calculus lessons, you know that when you want to write a mathematical proof, it really needs a lot of effort to put in. Let alone if you want to prove your entire codebase is safe, you have to write the proof for each of the functions. And the second barrier is even harder than the first one. That is, how to... What should be written as a formal specification? What should we prove? In that case, you have to not only know what your code intends to do and what is the background of the code.

7:34你還得知道常見攻擊場景，而且必須是安全專家，才能寫出有意義的規格。我們在智慧合約形式化驗證上做了幾年之後，會看到這件事快要改變，因為這兩道障礙我們基本上已經處理掉。為了處理第一道，我們做了一個新的 prover。它本質上是 AI 原生的 prover，用它寫證明，可以像跟 AI agent 講話一樣容易。You also need to know the common attack scenarios, and you must be a security expert in order to write meaningful specifications. So, after several years that we put into formal verification on the smart contract, we will see that this will be about to change, because we have developed, we have basically tackled these two barriers. So, to tackle the first barrier, we have developed a new prover. That prover is essentially an AI-native prover, and with that prover, you can just write the proof as easy as just talking with an AI agent.

8:19這個 prover 根本上建立在兩個引擎上。左邊是自動化 prover。它架在 SMT solver 上，能處理所有基本證明，並確保證明是健全且確定性的。右邊是 AI harness。它可以跟這個以 SMT 為後盾的 prover 互動，把承擔的任務翻譯成基本證明條件，好自動檢查。兩個引擎一起把那些難證明拆成非常小步的證明，並確保每一步都過。And this prover is fundamentally built on top of two engines. The engine on the left side is the automated prover. On top of an SMT solver, this prover can handle all the basic proofs and make sure all the proofs are sound and deterministic. And on the right side, that is the AI harness. It can just interact with the SMT-backed prover to make sure that all the undertaking tasks can be translated into the basic proof conditions so that it can be automatically checked. And these two engines will work together to break down all of those hard proofs into very, very small-step proofs, and to make sure all the small-step proofs pass.

9:13這些小步合在一起，就能構成我們想證明的整個目標。給一個具體例子：我們最近從零驗證了一個高度最佳化的 Solidity 指數函式。這個函式有大約一半程式碼是 inline assembly。整個證明從頭到尾只花一天，包含 AI 寫證明加上人工審查。證明生成與檢查大概只要七分鐘。整份證明腳本大約 2,000 行。跟基於 Lean 4 的證明比，大概只要十分之一的證明腳本就能完整生成證明。And all of them can construct the entire goal that we want to prove. To give you a concrete example, we recently have verified a highly optimized Solidity exponential function from scratch. So this function is optimized. It has like half of the code written by inline assembly. And the entire proof from scratch to the end of the proof only takes one day. That includes the AI writing the proof plus the human review of the proof. And the entire proof generation and the checking only takes like seven minutes. And the entire proof script is about 2,000 lines of code. Compared to the Lean 4-based proof, it basically takes only one-tenth of the proof script to fully generate the proof.

10:08從稽核走到可重用規格

10:08這不是簡單的證明。它用了大量證明技術，需要數學家等級的專業才能構造，例如泰勒展開、區間求值等等。為了處理第二道障礙，我們累積了一套方法，幫忙知道程式碼哪裡是高風險區，以及怎麼把直覺翻成期望的安全性質、再變成形式規格。我們叫它 audit-to-proof。你可以想像：寫好一份不錯的智慧合約，上鏈部署之前，大概會做一次安全稽核，不管是內部還是外部。And it is not just a trivial proof. It basically uses tons of proof technologies, requires a mathematician's expertise to construct the proof, for example, Taylor expansion, interval evaluation, and so on. And to tackle the second barrier, we have accumulated a methodology to help to know which part of the code is a high-risk area, and to know how we translate our intuition into the expected security properties and turn them into the formal specifications. So we call it audit-to-proof. So audit-to-proof, you can imagine that after you write a very nice smart contract, and before you release, deploy it on-chain, you probably will do an audit on your code, a security audit on your code, either internally or externally.

11:10稽核之後你可能會找到一些發現，再把它們變成修復、變成補丁。多數團隊就停在這裡。我們再往前一步：把那些補丁轉成下一輪工作，叫做形式化驗證。之後我們可以產出幾行包住你函式的規格。這些規格可以看成能力的轉移，或把安全能力去中心化交給你。之後你可以把規格接到 DevOps 或持續整合流程裡。After that audit, you may find some findings, and you will turn those findings into fixes, into patches. And that is where most teams just end there. But we just take one step forward. We turn all those patches into a new engagement that is called formal verification. And afterwards, we can produce several lines of specs surrounding your functions. And those specs, you can view it as the transfer of the capabilities, or decentralization of the security capabilities that we transfer to you. And afterwards, you can integrate that specification into your DevOps operations or continuous integration process.

12:00這份規格你可以隨時、隨地、跑任意多次。只要你想最佳化或改程式碼，都可以用規格檢查程式碼到底安不安全。它基本上就是把稽核者、形式化驗證專家、開發者的專業，收進一份可以重用的規格。動手看一個真實世界的例子。在 RWA，我們把所有東西代幣化，轉成代幣之後要交易。為了交易，我們想把代幣換成某種常用代幣。And you can run that spec at any time, anywhere, any number of times. As long as you want to optimize or change your code, you can always use the spec to check if your code is actually safe or not. So it basically just leverages the auditors' and the formal verification experts' and the developers' expertise into one specification that you can reuse. So to give you a hands-on, let's look into a real-world example. So in RWA, we tokenize everything, and after we convert everything into tokens, we want to trade them. So in order to trade them, we want to swap our tokens into some commonly used token.

12:47這通常叫做清算。我們通常用 DEX 或 AMM 來做。這次真實世界的攻擊，實際損失大約 9,400 萬美元。根因其實很單純。DEX 或 AMM 通常用流動性池來交換代幣。例如交易者想用代幣 B 換代幣 A，會先把 B 給 DEX 或流動性池，池子再用公式算出要回給交易者多少 A。So that is usually called liquidation. And we usually use a DEX or AMM to do that. And this real-world exploit actually cost like $94 million. So the root cause of this exploit is simple. So usually, the DEX or AMM, they will just use a liquidity pool to swap for tokens. For example, if a trader wants to trade token B for token A, it will first give the token B to the DEX or liquidity pool, and the liquidity pool will use a formula to calculate how much of token A will return to the trader.

13:33AMM 精度漏洞怎麼寫規格

13:33流動性池需要維持這個函式：D'，也就是交換後 A 跟 B 的合併準備，跟交換前的合併，必須相等。現在我們只讓它近似相等，因為有精度損失。這次攻擊就是攻擊者在利用這個精度損失。有一個地方，計算結果應該無條件進位，實際程式碼卻無條件捨去。So the liquidity pool needs to maintain this function, that is D prime, that is the exchanged reserve, combined reserve of A and B, to the combination before, they must be equal. And right now, we just make it approximately equal. That is because of precision loss. So this exploit actually makes the attacker leverage this precision loss. In one place, the calculation should round the result up, but the actual code just rounds the result down.

14:22怎麼排除這個 bug？可以在微觀層做。直接把規格寫到程式碼上。你在函式上面看到的那些註解，就是形式規格。可以看到，它們跟 Solidity 長得很像。看第 10 行，它基本上說結果必須永遠無條件進位。第 11 行說無條件進位要有一個邊界，落在精度跟實際結果之間。So how to rule out this bug? We can do it at the microscopic level. So we can just write directly the specification onto our code, saying that, so what you see above the function, those annotation comments about the function, they are formal specifications. As you can see, they are very close to what the Solidity code looks like. So if you look at line 10, it basically says that the result should make sure the rounding is always rounding up. And line 11 says that rounding up should have a boundary that is between the precision and the actual result.

15:08你可能會說，我怎麼知道哪個函式該無條件捨去、哪個該無條件進位？沒關係，可以在設計者層做。對設計者來說，你永遠想維持一個不變量：A 跟 B 的曲線組合，永遠要比函式執行前、swap 發生前的曲線更大。這樣你就永遠知道，不管發生多少次 swap，你的準備價值不會下降。我們甚至可以在更高層、經濟層來做。But you may say that, how do I know which function I should round down or round up? So that's fine. We can do it at the designer's level. So for a designer, you always want to maintain an invariant saying that the combination, the curve of A and B, should be always larger than the curve of A and B before the function executes, before the swap even happens. So with that, you can always know that no matter how many swaps happen, your value, your reserve value, will not decrease. And we can even do it at a very high level, at economy level.

15:53在經濟層，我們可以看到：如果我對同一種代幣先買再賣，客戶或使用者永遠會拿到比他付出的略少一點的代幣。這樣 AMM 或 DEX 就永遠不會虧錢。形式規格基本上可以寫在任何層級。只要有一條規格被違反，違反的意思是 prover 找到反例，如下面所示，找到一個它無法為你的程式碼相對形式規格構造出證明的例子，那你就找到 bug，可以用它來除錯並把證明做完。So at economy level, we can see that if I do a buy and then do a sell of the same token, the client or the user can always receive a little bit less token than he paid. So in that sense, the AMM or DEX will never lose the money. So you can basically write the formal specification at any level, and as long as one specification is found to be violated, violated means that the prover finds a counterexample, as shown below, finds that one example that the prover cannot construct the formal proof for your code against the formal specification, then you find a bug and you can use this to help you to debug and finish the proof.

16:49把規格嵌進開發流程

16:49收到形式規格之後，我們希望你能把它嵌進整個開發流程。開發的每個週期都可以用它，確保程式碼一直被安全檢查。謝謝各位。AI 降低了攻擊門檻。我們用形式化驗證，把保護程式碼的門檻也降下來。我很樂意。So after you receive the formal specification, what we want is that after you receive the specification, you can integrate it into the entire development process. So you can use it in every cycle of your development to make sure your code is always securely checked. So thank you for your attention. So AI lowers the barrier to the attack. Let's lower the barrier to secure our code with formal verification. So I'm happy to.