web3開発インフラ「Bunzz」のR&Dチームに、京大・末永幸平准教授が技術アドバイザとして参画！計算機科学によるスマートコントラクトの脆弱性、収益機会の研究を開始

このたびBunzz pte ltd（シンガポール、代表：圷 健太、 以下「Bunzz」）は、京都大学で計算機科学を研究する末永幸平准教授を技術アドバイザとして迎え入れ、Formal Verification（形式検証）、及びFuzzing等の計算機科学的なアプローチにより、スマートコントラクトの脆弱性や収益機会を検知する取り組みを開始したことをお知らせいたします。

研究開発の経緯

Bunzzはブロックチェーン領域におけるスマートコントラクトのセキュリティ監査の業界課題を解決すべく「Bunzz Audit」を提供しております。業界課題の根本原因である人間によるマニュアル監査を、脆弱性データベースをLLMで総当りする当社独自の手法によって機械化し、約90%のコストカットと48時間という短納期を実現しました。

BunzzのR&Dチームは、こうした機械的なアプローチが「スマートコントラクトの想定外の動作」を検知するのに有効であり、同時に監査以外の分野にも利用可能だと考えています。具体的にはDeFiにおけるトレード手法の開発等です。
一方でLLMとデータベースの活用のみでは限界があり、Formal VerificationやFuzzingなど、計算機科学のアプローチからコントラクトの動作を形式的にプログラム意味論の手法を用いて定義し、エッジを発見することで技術的なブレークスルーを生み出せると考え、ブロックチェーン分野における計算機科学、特に形式検証手法の適用において第一線で活躍されている京都大学・末永幸平准教授を技術アドバイザとしてお迎えすることを決定いたしました。

ブロックチェーン×LLM×計算機科学の可能性

末永准教授のブロックチェーン領域における実績

DAppの開発者にとってフレンドリーな環境を提供するブロックチェーン、Tezosにおいて、静的検証ツール「Helmholtz」の開発に加わり、Tezosエコシステムのセキュリティに貢献されたほか、Helmholtzの派生として、複数コントラクト間のインタラクションやデプロイ前のコントラクトの振る舞いも計算可能な「iCon」の開発メンバーでもあるなど、当該分野でグローバルレベルの実績を残されています。

BunzzR&Dチームとのシナジー

Bunzzは2019年からブロックチェーン関連プロダクトの開発を行い、スマートコントラクトに関する知見を深め、2022年からはLLMをコントラクトの解析・監査に適用や、脆弱性データベースの構築等、ノウハウを蓄積してまいりました。ブロックチェーン、LLM、計算機科学を組み合わせブレークスルーを生み出すためには、それぞれの専門性を横断した高度な研究開発が求められます。BunzzはブロックチェーンとLLMに関する技術、そして実装力を惜しみなく注ぎ、業界にとって意義のあるプロダクトの開発を目指してまいります。

Bunzz CEO 圷 健太より

ブロックチェーン上のアプリケーションは、「スマートコントラクト」によって自律分散的に振る舞います。基本的にこのコントラクトを介しP2Pでデジタルアセットのやり取りを行うため、プログラムの正当性やセキュリティも客観的な評価が求められます。そのような背景から、数学的にコントラクトの動作を検証できるFormal VerificationやFuzzing等の応用が進み、注目が集まってきています。
末永准教授はこの分野において世界でもトップレベルの知見と経験をお持ちの研究者です。当社のR&Dチームにジョインいただけることを嬉しく思っています。Bunzzチームは、これまでに培ったLLMの技術ノウハウやDeFiマーケットのビジネスロジック等の知見を提供し、先生とのコラボレーションから価値のあるプロダクトの開発を目指してまいります。

末永准教授より

このたび、技術アドバイザとして加わることとなりました。私の専門は、ソフトウェアを数理的手法に基づいて検証する手法である formal verification と呼ばれる手法です。この手法は、通常のソフトウェアはもちろんですが、スマートコントラクトのような、扱うアセットの価値が大きく、欠陥がその毀損につながる可能性の大きいソフトウェアにおいて、その真価を発揮すると考えています。価値のある仕事ができるようにがんばります！