Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs

要約

ブロックチェーン システムがトラストレスであると言われるとき、これが実際に意味するのは、すべての信頼がソフトウェアに置かれているということです。
したがって、ブロックチェーン ソフトウェアが正しいことを確認するための強力なインセンティブが存在します。ここでの脆弱性は数百万ドルの損失をもたらし、ビジネスを破壊します。
ソフトウェアの正確性を確立する最も強力な方法の 1 つは、形式的な方法を使用することです。
ただし、正式な手法に基づくアプローチでは、それらをうまく採用するために必要な時間と専門知識の点で、多大なオーバーヘッドが生じます。
私たちの研究では、形式モデル (ソフトウェア システムの数学的抽象化) の作成を自動化することで、この重大な欠点に対処しています。形式モデルは、形式手法を採用する際の中心的なタスクとなることがよくあります。
モデル合成は 3 つのフェーズで実行されます。最初にコードをモデル スタブにトランスパイルします。
次に、大規模言語モデル (LLM) を使用して「空白を埋めます」。
最後に、生成されたモデルを構文レベルと意味レベルの両方で繰り返し修復します。
このようにして、正式なモデルの作成に必要な時間を大幅に短縮し、それらに依存する貴重なソフトウェア検証手法のアクセシビリティを高めます。
私たちの仕事の実際的な背景は、スマート コントラクトの正当性監査に正式なモデルを使用することで価値が得られるまでの時間を短縮することでした。

要約(オリジナル)

When blockchain systems are said to be trustless, what this really means is that all the trust is put into software. Thus, there are strong incentives to ensure blockchain software is correct — vulnerabilities here cost millions and break businesses. One of the most powerful ways of establishing software correctness is by using formal methods. Approaches based on formal methods, however, induce a significant overhead in terms of time and expertise required to successfully employ them. Our work addresses this critical disadvantage by automating the creation of a formal model — a mathematical abstraction of the software system — which is often a core task when employing formal methods. We perform model synthesis in three phases: we first transpile the code into model stubs; then we ‘fill in the blanks’ using a large language model (LLM); finally, we iteratively repair the generated model, on both syntactical and semantical level. In this way, we significantly reduce the amount of time necessary to create formal models and increase accessibility of valuable software verification methods that rely on them. The practical context of our work was reducing the time-to-value of using formal models for correctness audits of smart contracts.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google