Certoraチーフ・サイエンティストMooly Sagiv：ブロックチェーンのセキュリティはコードだけではない

2025年が我々に教えてくれたことがあるとすれば、それはソラーナがブレイクアウトの速度を記録し、小売チェーンとしての地位を確立したことだ。毎日、何千人ものユーザーが資金を移動し、取引に署名し、潜在的なリスクを気にすることなく、底知れぬほど複雑なスマートコントラクトに関与している。

もちろん、サービスの根底にはリスクが潜んでいる。

もちろん、サービスの下にもリスクは存在します。しかし、暗号のハッキングや悪用は私たちが望むよりもはるかに一般的ですが、人々は一般的に、最大のリスクは不明瞭なロジックや技術的なコードベースの奥深くに埋もれていると考えています。

ムーリー・サギヴはそう考えていない。

ブロックチェーンセキュリティ企業であるCertoraのチーフサイエンティストによると、ほとんどの損失はコードロジックの欠陥やプログラミングエラーによるものではなく、もっと単純な原因によるものだという。

“Keep an eye on your key… and keep an eye on your phone.”

。

これは単純な警告ですが、暗号セキュリティにとって決定的に重要で、見落とされがちなアプローチをとらえています。そして、モバイル暗号アプリの急増は、変数と潜在的な脆弱性を増やすだけです。

サギブは、このケースを説明するユニークな立場にある。学術仲間の間では、シュムエル (ムーリー) サギブとして知られている Certora のチーフ・サイエンティストは、テルアビブ大学のソフトウェア・システム学科長を約 28 年間務めています。プログラム解析と検証の数十年にわたる研究により、Sagiv は、フォーマル検証をニッチな分野から開発者が継続的に実行できるものへと拡大する Certora&rsquo の推進において、主導的な役割を果たしています。

Breakpoint 2025でSolanaFloorと共に講演したMooly Sagiv氏は、ブロックチェーン・セキュリティの暗い森に明るい光を投げかけました。Certoraのチーフ・サイエンティストは、暗号ユーザーがセキュリティに関して抱いている大きな誤解や、形式的検証の重要性、AIや量子コンピューティングのリスクは誇張されすぎているのかなどを明らかにしました。

暗号セキュリティ最大の誤解：すべてのバグはコードの中にあるブロックチェーンのセキュリティに関する誤解について、サギヴ氏は暗号文化があまりにも甘すぎると主張する。最も危険な誤解は、脆弱性はコードの中だけに存在し、コードが監査されれば、ユーザーは常識を覆すことができるという考えです。

“Everybody feels that all the bug[s] is in the code.そして、それは必ずしもそうとは限りません。もしかしたら、あなたのコードはまったく問題ないかもしれませんが、それがデプロイされる方法の外側に何かがあるかもしれません。

暗号の専門家は、「コードは法律である」というような核心的な哲学的信条を掲げています。しかし、それは真実かもしれませんが、考慮すべき変数はまだ何十もあります。プロトコルが正しくても、鍵の管理が不十分であったり、統合が脆弱であったり、運用環境が危うかったりして、安全でないことがある。アプリは、それを管理する人々のシステムと行動と同じくらい安全です。

Sagivの2つ目の誤解は、ほとんどのユーザーが信じたいと思っているものです。

“It’s never fully safe.より安全にすることはできるが、完全に安全であることはない。

監査は暗号セキュリティの不可欠な要素であることは間違いないが、決して保証にはならない。しかし、DeFiユーザーは基本的なセキュリティの実践を忘れてはなりません。

セキュリティに対するCertoraのハイブリッドアプローチ

サジブは監査を否定しているわけではない。実際、彼は、形式的な検証が人間のレビューに取って代わるという考えに対して明確に反論しています。その代わりに、形式的な検証と人間による監査は、可能な限り多くのカバレッジを提供するために併用されるのが理想的である。

SolanaFloorの取材に応じたSagiv氏は、監査が一般的に既知の攻撃パターンから防御する一方で、形式的検証は未知の未知数への露出を減らすことができることを概説しました。

“When you're doing’re audit, you are review your code [with] your best person against the known attack.形式的な検証を行うことができれば、未知の未知の攻撃に対するある種の[予防]を行うことができます。

暗号は軍拡競争であるため、この違いは重要です。攻撃テクニックは進化し、ハッカーやサイバー犯罪者は、私たちが毎日使っている10億ドル規模のアプリを破るための新しい手法やテクニックを常に見つけています。

新しいクラスのバグが発見されるのは、誰かがどこかで、業界が気付かなかった仮定を破る賢い方法を見つけたからです。形式的検証は、このような「未知の未知」に対するもう1つの防衛手段を提供することを目的としています。

Sagivは、Certoraが繰り返し見てきたパターンを説明しています。チームは、セキュリティに膨大な社内リソースを投入し、精鋭の監査人を雇い、すべてを正しく行うことができます。

“ あなたは最高のセキュリティ研究者に10個の重大な問題を発見させました。あなたはとても満足するでしょう。そして、フォーマル検証を実行する。それはさらに2つ見つけます。

このテーゼは、Certora’社のフォーマル検証チームのリーダーであるPamina Georgiev氏によってさらに強化されました。彼はSolana Breakpointのステージに立ち、FVの重要性と影響を説明しました。

形式的検証が提供するすべての約束と保護にもかかわらず、形式的検証は完璧なシステムにはほど遠いものです。形式的検証は、暗号Twitterのある種の人々が信じさせるかもしれないにもかかわらず、ハッカーを足止めする不可侵の力場とは言い難いのです。

Sagivは、なぜそのような枠組みが危険なのかを率直に語っている。

形式的検証は、コードがある絶対的な意味で安全であることを証明するものではありません。コードが一連のプロパティを満たすことを証明します。もし間違ったプロパティを選んでしまうと、非常に信頼できそうなものができあがってしまいますが、水密性からはほど遠いものになってしまいます。

CI、自動化、そしてループに人間を入れないこと

ブレイクポイントにおけるサギブの最も明確な指摘のひとつは、セキュリティは一過性のものではないということだ。あるアプリケーションが数年前に監査を受けたからといって、それが現在も安全であるとは限りません。このことは、プロトコルや攻撃手法が絶えず繰り返され、1行のコードの変更がスタックの他の部分に影響を及ぼしかねない暗号において特に当てはまります。

“It completely changes, one change of one line can break the whole code.”

“It completely changes, one change of one line can break the whole code.”

それが、Certoraが検証を開発者のワークフローに押し込む理由です。Sagiv氏によると、CertoraはCIパイプラインに統合されるため、新しいコミットごとに検証チェックが自動的に開始され、1回限りのマイルストーンではなく、継続的なガードレールが確立されます。

“コードを変更してコミットするたびに、フォーマル検証を実行します。それが私たちのツールの優れた点です。

私たちのツールは自動的です。

Certoraは、Rustで書かれたSolanaスマートコントラクトを検証するために設計された“Certora Solana Prover&rdquoで、Solanaプログラムの形式的検証のための専用ドキュメントを維持しています。

サイファーパンクとアカデミア

サイファーパンクや反体制的な倫理観に根ざした多くの暗号の起源物語とは異なり、サギヴはこの業界に必要なアカデミックな気風をもたらしている。彼は学界からの転身を、知的挑戦と現実世界の利害の衝突と表現している。

“Crypto is the only domain where you have small code carrying a lot of value”

従来のセーフティクリティカルなソフトウェアでは、コードは巨大かもしれませんが、古くて安定していることが多く、暗号の迅速な反復とは完全に対極にあります。これは、Certoraのお気に入りのキャッチフレーズの1つである「Move fast and break nothing”（速く動いて、何も壊さない）

」の根拠となったかもしれない。

。

Sagiv氏は、暗号の多くが本質的に数学的なものであるため、暗号は形式的手法に完璧に適合するとしている。

“I give academic lectures still.暗号が嫌いな人もいます。私は技術的な面で彼らのモチベーションを高めようとしています。私は技術的なことに立ち返り、何が挑戦的なのかを伝えています。

たとえ彼の学究的な同僚が暗号に懐疑的であったとしても、サギヴは暗号が新進の開発者にとってコンピュータサイエンスのより刺激的でやる気を起こさせる分野の1つであることを強調しています。

ソラーナの「やる気」

Certoraは決してSolana専属のセキュリティ企業ではありませんが、だからといって同社がSolanaのDeFiシーンに深く関わっていないわけではありません。Sagivは、Solanaの最大かつ最も影響力のあるアプリケーションのいくつかと仕事をしてきたことで、トップチームと肩を並べることでしか得られないレベルの業務上の尊敬をエコシステムに与えています。

Certoraが最初にSolanaに関わったのは、Sagivが「素晴らしい」と評価するSquadsでした。

そこからCertoraはSolana Foundationと協力し、SPLプログラムのプロパティを検証しました。

最も際立っているのは、他の環境との比較である。Sagic 氏は、Solidity Developers での経験に触れながら、チームが変更に抵抗することがあると指摘しました。

“Solidity では、ときどきコードの変更を依頼すると、非常に嫌がります。ここ（Solana）では、人々はもっと「できる」という態度を持っています。コードを変更するように頼むと、彼らはとても素直なんだ。

2026年の安全保障上の脅威

2026年に人々が認識する必要がある最大の脅威について尋ねられたとき、Sagiv氏は再び、人々はコードの脆弱性に過剰な指標を当てるべきではないと強調しました。優れた運用セキュリティは多面的なものであり、平均的な暗号保有者は、DeFiエクスプロイトで資金を失うよりも、ソーシャル・エンジニアリングや保管ミスの犠牲者になる可能性の方がはるかに高い。

“We are seeing all kinds of things happening, it's not just the code.”

“We are seeing all kinds of things happening, it's not just the code.

彼は間違っていない。Chainalysis’ 2025 Crypto Crime Reportによると、詐欺師は2025年の間に140億ドル以上を盗み、またもや過去最高を記録した。

彼は間違っていない。

。

Sagivはまた、AIの脅威が誇張されているかもしれないと考えています。セキュリティの専門家であるCertoraのチーフ・サイエンティストは、AIを悪意のある脅威ではなく、ツールであると考えています。確かに、AIは攻撃者にとって増長要因となり得ますが、防御者やセキュリティ企業にとっても活用できるものです。

“The bad guys could use AI.善人もAIを使うことができる

“The bad guys could use AI.

AIが脆弱性の発見に役立つなら、プロパティの証明や、より強力な仕様の生成、検証問題の解決にも役立ちます。

暗号が完全に安全になることはありません。しかし、進むべき道は、暗号セキュリティ101に忠実であることに変わりはありません。鍵管理を強化し、常識を用い、セキュリティを一度宣言して忘れるものではなく、継続的に証明するものとして扱うのです。

ソラナフロアについてもっと読む

唯一の確実性は不確実性である

。

中加貿易協議、円インフレ、そしてまたもや政府閉鎖が暗号市場を怯えさせる

SolanaFloor Sits Down with Certora’s Mooly Sagiv