プログラム中の文字列チェック機能の脆弱性を自動修正する技術を世界に先駆けて実現
～専門知識をもたない開発者でもReDoS脆弱性の修正が容易に～

日本電信電話株式会社（本社：東京都千代田区、代表取締役社長：澤田　純、以下「NTT」）と学校法人早稲田大学（本部：東京都新宿区　理事長：田中愛治　以下、「早稲田大学」）は、文字列のチェック機能の処理時間を長期化させコンピュータの負荷を大幅に増大させる攻撃を引き起こす脆弱性に対する実用的な自動修正技術を世界に先駆けて実現いたしました。文字列のパターンマッチに用いられる正規表現（※1）とは、特定の文字の並び（文字列）をルールに基づき簡略化して表現する方法で、Webサービスなどにおいてユーザの入力値が期待したものであるかの検証など幅広い場面で利用されています。難解な正規表現の仕組みやルールを深く理解し、検証すべき文字列を厳密に定義できていないと脆弱性になってしまうため、近年グローバルで大きな脅威となっています。この技術によって、専門知識をもたない開発者でもこうした正規表現の脆弱性の修正が可能となり、安全なサービスの実現が期待できます。

1．背景

ソフトウェアの脆弱性を悪用するサイバー攻撃は後を絶たず、世界中で大きな被害が報告されています。脆弱性とは、プログラムの不具合や設計上のミスなどが原因となって発生するセキュリティ上の欠陥であり、なかでも正規表現を用いた文字列のパターンマッチを行う機能に対して、処理時間が長くなる入力を与えることで計算リソースを消費しサービス運用妨害を引き起こす脆弱性をReDoS脆弱性（※2）と言います。
　正規表現は、ほとんどのプログラミング言語に組み込まれて利用されており、入力文字列が意図されたパターンと一致するか否か（例えば、メールアドレスや電話番号の形式チェック）を判断するエンジン等として、さまざまなソフトウェア／サービスで幅広く利用されています。このReDoS脆弱性が原因で商用のサービスが停止するようなインシデントは、この数年の間にたびたび発生しており、グローバルで大きな脅威として注目を集めています。

2．研究の成果

正規表現は形式言語理論に端を発していますが、パターンマッチの発展・応用に伴って利用可能な演算子が拡張され、実際のソフトウェアで利用される実世界の正規表現（※3）は従来の理論では扱うのが難しいことが知られています。これまで、実世界の正規表現のReDoS脆弱性を自動的に修正する技術は存在しませんでした。
　本成果では、実世界の正規表現を対象にReDoS脆弱性および脆弱性のないことを保証する条件を厳密に定義してReDoS脆弱性の修正問題を形式化し、その修正問題を解くアルゴリズムを考案し、理論的な保証付きのReDoS脆弱性自動修正技術を世界に先駆けて実現しました。
　NTTは、実世界の正規表現におけるReDoS脆弱性の定義や修正問題の定義、修正アルゴリズムを考案し、早稲田大学理工学術院の寺内多智弘教授はNTTが考案した手法の理論的な正確さの検証を行いました。
　本成果は、セキュリティとプライバシー分野の最難関国際会議IEEE S&P 2022（43rd IEEE Symposium on Security and Privacy）（※4）に採録されました。S&Pは、1980年から続くセキュリティ・プライバシー分野のトップレベルの国際会議であり、採択率12％程度の狭き門であることが知られています。

3．技術のポイント

本技術のポイントは、①従来の理論では扱いづらかった実世界の正規表現を対象に「ReDoS脆弱性」「ReDoS脆弱性がないことを保証する条件」「ReDoS脆弱性の修正問題」の3点を論理モデルとして明確に定義したこと、②論理モデルに基づいて定義された脆弱性がないことを保証する性質と、プログラムが満たすべき入出力の例をもとに自動でプログラムを生成する「Programming by Examples （PBE）」メソッド（※5）を用い、修正対象となる正規表現および利用者が望む正規表現に対するポジティブな例（受理される文字列）とネガティブな例（拒否される文字列）を与えると、それらの例を正しく分類し、ReDoS脆弱性がないことを保証した正規表現を出力するアルゴリズムを考案したことです。
　このアルゴリズムではReDoS脆弱性がないことを保証するために、正規表現の書き方から曖昧さを排除し、任意の文字列に対してパターンマッチの方法を一意に定める条件を定義し、それに合う修正正規表現を出力させることにより、出力結果に理論的にReDoS脆弱性がないことを保証しています。
　このように、プログラムがある性質を満たすことを論理的に検証し、特定の不具合が存在しないことを保証する手法は「形式検証（※6）」と呼ばれ、従来の発見型のレビューやテストによる網羅性を持たない検証の問題点を解決でき、高品質なソフトウェアを効率的に生成できると期待されています。

4．今後の展開

本技術は、世界中で幅広く使われている正規表現の脆弱性を自動的に修正する技術であり、安全なソフトウェアの創出を可能にするものと期待されます。

発表について

本成果は、2022年5月22～26日に開催されるセキュリティとプライバシー分野の最難関国際会議IEEE S&P 2022（43rd IEEE Symposium on Security and Privacy）にて、下記のタイトル及び著者で発表されます。（所属組織名は投稿時のもの）

用語解説

^※1正規表現・・・コンピュータで特定の文字の並び（文字列）をルールに基づき簡略化して表現する方法の1つで、特定の文字列のパターンを検索・抽出・置換するときに用いられる。

^※2ReDoS脆弱性・・・ReDoSとはRegular Expression Denial of Serviceの略で、正規表現のパターンマッチにかかる処理時間を長期化させて計算リソースを消費し、サービス停止を引き起こすような正規表現の脆弱性のことを表す。

^※3実世界の正規表現・・・形式言語理論において正規言語を表すために導入された純粋正規表現とは異なる性質を持つ、実際のソフトウェアで利用されている拡張された正規表現のことを表す。具体的には、純粋正規表現にはない演算子（後方参照、先読み）を利用可能な正規表現を示している。

^※4S&P・・・IEEEが主催するセキュリティとプライバシー分野のトップ会議 IEEE Symposium on Security and Privacyであり、最先端のセキュリティ対策技術が発表される。

^※5Programming by Examples （PBE）メソッド・・・プログラミングの知識を持たないエンドユーザでもプログラムを生成できるようにする手法の1つで、プログラムが満たすべき入出力の例を与えると、それを実現するプログラムを自動で生成する技術。

^※6形式検証・・・プログラムの状態をモデル化し、ある性質を満たしていることを論理的に検証する高信頼なソフトウェアを設計・開発する手法。