形式検証分野の最難関国際会議CAV2026にNTTから論文採択

2026年7月26日～7月29日にポルトガルのリスボンにて開催される、形式検証分野の最難関国際会議38th International Conference on Computer Aided Verification（CAV 2026）に、NTT研究所から論文が本会議に採択されました。CAVでは、モデル検査、定理証明、静的解析、プログラム検証など、ハードウェアやソフトウェアが設計どおり正しく安全に動作することを、数学的・自動的に確認する技術に関する最先端の研究成果が発表されます。またCAV 2026の論文採択率は約26％（投稿数311件）と、難関国際会議として知られています。

Repairing Regex-Dependent String-Manipulation Programs

千田忠賢（特別研究員）（NTT社会情報研究所）、寺内多智弘（早稲田大学）

背景

生成AIの登場により、脆弱性の発見・悪用が高速化し、これまで以上に迅速な対応が求められています（※1）。生成AIによる自動修正は有効な手段ですが、意図しない修正が行われる可能性があり、修正結果の品質をどのように確保するかが課題です。そのため、開発者の意図に沿って、脆弱性の原因特定から修正までを迅速に行う技術が求められています。

研究の成果

本成果では、情報漏洩などにつながる文字列処理の誤りを対象に、原因特定から修正までを自動化する技術を確立しました。従来の自動修正技術では、修正作業の約46.3%を占める原因特定（※2）の自動化が課題でした。本技術では、入力された文字列をどのように処理し、出力すべきかという開発者の意図を、「由来」と呼ぶ仕様として簡潔に記述できるようにしました。例えば、「入力されたパスワードを出力に含めない」と記述することで、通常のテストケースだけでは表しにくい処理上の要件を明確に示すことができます。本技術は、脆弱性が発見された際に、この仕様に基づいて問題の原因となる処理を特定し、開発者の意図に沿った修正案を自動的に生成します。このような一連の処理によって、文字列処理に起因する脆弱性の原因特定から修正までを自動化し、迅速な対応と修正品質の確保を両立します。