数学的な証明にも限界
この技術はまだ試作段階にある。需要は高いものの、顧客がこの技術にどれほどの費用を支払う意思があるのか、また、どのようなかたちで導入したいと考えているのかは不透明だ。形式的検証では、コンピューターの動作やユーザーの操作について、あらかじめ想定した条件をもとに検証する。このことから、ユーザーの操作ミスやハードウェアの故障に起因する不具合まで検出できるのかと疑問を抱く専門家もいる。
AIを活用したバグ検出ソフトウェアを開発するスタートアップ、Antithesisを率いるウィル・ウィルソンは、形式的検証について、自分のような数学好きが陥りやすい「わな」だと語る。Antithesisは自社のサイバーセキュリティ対策の一部について形式的検証を実施するために、数百万ドルを費やした。そして、その作業は「とんでもなく面倒だった」と、ウィルソンは語る。
それでも同社は、自社のツールを使って、それまで見つかっていなかった不具合を発見している。さらに、すでに形式的検証が済んでいた複数の顧客企業のソフトウェアからもバグを見つけることができた。「形式的検証によってある程度の安心感は得られます。しかし、それが本当に確かなものかを証明するには、徹底的で網羅的なテストが必要です」とウィルソンは話す。
暗号資産イーサリアムの生みの親として知られる開発者ヴィタリック・ブテリンも、今年5月に投稿したブログ記事で「形式的検証は万能ではありません」と指摘している。それでもブテリンをはじめとする形式的検証の支持者たちは、AIシステムがサイバー攻撃を仕掛け、深刻な被害をもたらすのを防ぐうえで、この技術が重要な防御手段になると考えている。
セキュリティを支える技術
各社が公表している情報によると、ボーイングの航空機、アマゾンのサーバー、現在使用されている25億台を超えるアップル製デバイスでは、ソフトウェアの一部で形式的検証が実施されている。脆弱性を悪用された場合、深刻な被害につながる恐れがあることから、主にセキュリティ関連のコードが形式的検証の対象となっている。
Amazon Web Services（AWS）のバイスプレジデント兼研究者のバイロン・クックによると、形式的検証はクラウドのセキュリティに対する顧客の懸念を和らげるだけでなく、重大なバグを早い段階で解消できることから、社内チームがより早く開発を進めることにも役立っているという。
一方、中規模のテック企業数社は『WIRED』の取材に対し、形式的検証を実施している場合でも、通常は製品の主要機能に限られると説明する。その理由としては、形式的検証を担当できる技術者の不足や、不具合によるリスクに比べて検証費用が高いことが挙げられる。そして、特に懸念されているのは、コードの形式的検証に数週間もかかることで、イノベーションの妨げになりかねないという点だ。
アップルのセキュリティチームは今年初め、暗号化に使用するライブラリー「corecrypto」で形式的検証を実施し、そこで発見した問題の一部は、ほかの方法では見つけられなかったと説明していた。ただし、新しいコードをcorecryptoに追加する際には、検証作業が追いつけるよう「慎重に」進める必要があるとも付け加えている。
これまでコードの形式的検証を実施してこなかった大企業のサイバーセキュリティ担当幹部2人は、検証作業が自動化されても、自社で形式的検証を導入する価値があるかどうかはわからないと話す。一方で、大手AI企業が形式的検証を済ませたAI生成コードを提供するのであれば、購入を検討する余地はあるという。両名とも公の場で発言する権限がないため、匿名を条件に取材に応じた。