#Cardano 創設者チャールズ・ホスキンソンは、Liquidネットワークのフェデレーション・ウォレットから4,000ビットコインが盗まれたと伝えられたことに反応した。
Liquidは昨日、Xへの投稿でこの件を確認し、ハッカーがフェデレーション・ウォレットから約4,000ビットコイン相当（3億2,000万ドル）を吸い上げたと述べた。ネットワークによれば、攻撃者はSideSwapのPeg-out Authorization Key（PAK）サービスを通じて資金を移動させた。
しかしLiquidとSideSwapはいずれも、PAK自体は侵害されていなかったことを示した。代わりにSideSwapは、取引に使われたL-BTCは、Liquidのサイドチェーンを動かすビットコイン派生のソフトウェアであるElementsの脆弱性に由来すると述べた。
この件を受けてLiquidはブリッジノードを無効化し、連携（フェデレーション）のメンバーが侵害を調査している間ネットワーク活動を停止した。その一方で、取引所には通知が届き、L-BTCの入出金を停止する、あるいは停止に備える動きが始まった。
その取引には、攻撃者が「ホワイトハット」を名乗り、オンチェーンでの連絡を求めた旨のOP_RETURNメッセージも含まれていた。
ホスキンソン、AI主導のサイバーセキュリティ上のリスクを警告
この件を受けてホスキンソンは、人工知能から来るサイバーセキュリティ上の脅威が高まっているという自身の見方を強調するために、その侵害を取り上げた。
彼は、形式手法が、ますます能力を高めるAI主導型の攻撃に対する最も強力な防御の一つになり得ると主張した。AIシステムがソースコードの解析に長けるほど、脆弱性の特定や高度な攻撃の自動化が可能になる一方で、ブロックチェーン開発者が「ソフトウェアの弱点が発見されてから悪用されるまで」の猶予は、ますます狭まっていく。
AIはすでに、攻撃者が潜在的な標的を特定し、複雑なコードを分析し、フィッシングやソーシャルエンジニアリングのキャンペーンを自動化することで、暗号資産のセキュリティ環境を変え始めている。総額1億3,000万ドル相当のビットコインが盗まれたとされるコールドカードのハックの報道も、先進的なAIツールが難しい脆弱性をより見つけやすくし、悪用もしやすくするのではないかという懸念をさらに強めた。
こうした背景のもと、ホスキンソンは、従来のテストだけではもはや十分な防御になり得ないと主張している。代わりに、数学的仕様と証明を用いて、ソフトウェアが意図された設計どおりに動作するかどうかを検証する形式手法を指摘している。
カルダノの形式的検証の重視
ホスキンソンの警告は、カルダノが長年にわたり、数学的に厳密なブロックチェーン開発を重視してきた点とも一致している。
カルダノの開発思想には、セキュリティ戦略の重要な構成要素として、学術研究、査読、形式的検証が組み込まれている。たとえば、そのオウロボロスのコンセンサス・プロトコルは、形式的な学術研究から生まれた。一方で、より広いエコシステムでは、実験的なテストのみに頼るのではなく、プロトコルやソフトウェアの重要な性質を「証明すること」が重視されてきた。
このアプローチはホスキンソンの主張を支持する。なぜなら形式的検証は、指定された性質が成り立つことを数学的に示すことを目的としているからだ。その結果、開発者はコードを本番環境に投入する前に、脆弱性の「まるごとした」種類（クラス）を潜在的に特定できる可能性がある。
カルダノも、ハスケルやプルートゥスのような関数型プログラミング技術に依存している。強力な型システムと数学的な基盤は、開発プロセスの早い段階で開発者が特定の種類のプログラミングエラーを検出するのに役立つ。
注目すべき点として、カルダノのアプローチは、テストや従来のセキュリティ手法のみに頼るのではなく、脆弱性が本番環境に到達する前にそれを防ぐことを目指している。