プログラム中の文字列チェック機能の脆弱性を自動修正する技術を世界に先駆けて実現

～専門知識をもたない開発者でも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」と呼ばれ、従来の発見型のレビューやテストによる網羅性を持たない検証の問題点を解決でき、高品質なソフトウェアを効率的に生成できると期待されています。

４．今後の展開

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

発表について

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

タイトル：Repairing DoS Vulnerability of Real-World Regexes

著者：Nariyoshi Chida (NTT Secure Platform Laboratories), Tachio Terauchi (Waseda University)

用語解説

※1　正規表現

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

※2　ReDoS脆弱性

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

※3　実世界の正規表現

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

※4　S&P

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

※5　 Programming by Examples (PBE)メソッド

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

※6　形式検証

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

An international astronomer team has discovered the most distant galaxy candidate to date, named HD1, which is about 13.5 billion light-years away. This discovery implies that bright systems like HD1 existed as early as 300 million years after the Big Bang. This galaxy candidate is one of the targets of the James Webb Space Telescope launched late last year. If observations with the James Webb Space Telescope confirm its exact distance, HD1 will be the most distant galaxy ever recorded.

To understand how and when galaxies formed in the early Universe, astronomers look for distant galaxies. Because of the finite speed of light, it takes time for the light from distant objects to reach Earth. If an object is 1 billion light-years away, it means that the light left that object 1 billion years ago and had to travel for 1 billion years to reach us. Thus studying distant galaxies lets us look back in time.

The current record holder for the most distant galaxy is GN-z11, a galaxy 13.4 billion light-years away discovered by the Hubble Space Telescope. However, this distance is about the limit of Hubble’s detection capabilities.

HD1, a candidate object for the earliest/most-distant galaxy at 13.5 billion light-years away, was discovered from more than 1,200 hours of observation data taken by the Subaru Telescope, VISTA Telescope, UK Infrared Telescope, and Spitzer Space Telescope. “It was very hard work to find HD1 out of more than 700,000 objects,” says Yuichi Harikane, an assistant professor of ICRR, the University of Tokyo, who discovered HD1. “HD1’s red color matched the expected characteristics of a galaxy 13.5 billion light-years away surprisingly well, giving me a little bit of goosebumps when I found it.”

The team conducted follow-up observations using the Atacama Large Millimeter/submillimeter Array (ALMA) to confirm HD1’s distance. Akio Inoue, a professor at Waseda University, who led the ALMA observations, says, “We found a weak signal at the frequency where an oxygen emission line was expected. The significance of the signal is 99.99%. If this signal is real, this is evidence that HD1 exists 13.5 billion light-years away, but we cannot be sure without a significance of 99.9999% or more.”

HD1 is very bright, suggesting that bright objects already existed in the Universe only 300 million years after the Big Bang. HD1 is difficult to explain with current theoretical models of galaxy formation. Observational information on HD1 is limited and its physical properties remain a mystery. It is thought to be a very active star-forming galaxy, but it might be an active black hole. Either possibility makes it a very interesting object. In recognition of its astronomical importance, HD1 was selected as a target for the cycle 1 observations by the James Webb Space Telescope, launched last year. Yuichi Harikane, who is leading these observations, says, “If the spectroscopic observation confirms its exact distance, HD1 will be the most distant galaxy ever recorded, 100 million light-years further away than GN-z11. We are looking forward to seeing the Universe with the James Webb Space Telescope.”

This research will be published in the April 8, 2022 issue of The Astrophysical Journal as Yuichi Harikane, et al. “A Search for H-Dropout Lyman Break Galaxies at z~12-16”. This work was supported by the Japanese Ministry of Education, Culture, Sports, Science and Technology (MEXT), the Japan Society for the Promotion of Science (17H06130, 19J01222, 20K22358, 21K13953), and the NAOJ ALMA Scientific Research Grant (2020-16B).

Journal: The Astrophysical Journal
Title: “A Search for H-Dropout Lyman Break Galaxies at z~12-16”
Authors: Yuichi Harikane, Akio K. Inoue, Ken Mawatari, Takuya Hashimoto, Satoshi, Yamanaka, Yoshinobu Fudamoto, Hiroshi Matsuo, Yoichi Tamura, Pratika Dayal, L. Y. Aaron Yung, Anne Hutter, Fabio Pacucci, Yuma Sugahara, and Anton M. Koekemoer
DOI：10.3847/1538-4357/ac53a9
URL：https://iopscience.iop.org/article/10.3847/1538-4357/ac53a9
https://ui.adsabs.harvard.edu/abs/2021arXiv211209141H/abstract

135億光年かなたの最遠方銀河の候補を発見

1．発表者

播金　優一（東京大学宇宙線研究所　宇宙基礎物理学研究部門　助教）
井上　昭雄（早稲田大学　理工学術院先進理工学部　教授）

2．発表のポイント

• 135億光年かなたの宇宙に明るく輝く銀河の候補を発見しました。現在見つかっている銀河の中で最遠方の候補です。
• 発見された銀河は非常に明るく、これまでの銀河形成モデルでは予想されていなかったような天体です。
• 銀河候補はジェイムズ・ウェッブ宇宙望遠鏡の第1期観測ターゲットになっており、今後の観測でこの時代の宇宙について、大きく理解が進むことが期待されます。

3．発表概要

東京大学宇宙線研究所の播金優一助教、早稲田大学理工学術院先進理工学部の井上昭雄教授を中心とする国際研究チームは、135億光年かなたの宇宙に存在する明るい銀河の候補、HD1を発見しました。この発見はHD1のような明るい天体が、ビッグバン後わずか3億年の宇宙に既に存在していたことを示唆しています。この銀河候補は昨年末に打ち上げられたジェイムズ・ウェッブ宇宙望遠鏡の第1期観測のターゲットになっており、分光観測により正確な距離が確認されれば、これまでの記録を塗り替える最遠方の銀河になります （注）。

本成果を記した論文は、2022年4月8日に米国の天文学誌『アストロフィジカル・ジャーナル』（The Astrophysical Journal） の電子版に掲載されました。

論文名：A Search for H-Dropout Lyman Break Galaxies at z~12-16

4．発表内容

① 研究の背景・先行研究における問題点

最遠方銀河の観測は、単に人類の知の地平線を広げるだけでなく、天文学的には宇宙で最初に誕生した初代銀河の形成を知る上でも重要です。初期宇宙において銀河がいつどのように生まれたのかを理解するために、天文学者たちはより昔、つまりより遠方の銀河を探してきました。これまで見つかった銀河の中で最も遠方のものは、ハッブル宇宙望遠鏡が発見した134億光年かなたの銀河、GN-z11でした。しかしさらに遠方の135億光年かなたの銀河は、これまで候補すら見つかっていませんでした。これは135億光年かなたの銀河からの光の波長は宇宙の膨張のために1.7マイクロメートルよりも伸びてしまうため、ハッブル宇宙望遠鏡のカバーする1.7マイクロメートルまでの波長では観測が難しかったためです。

② 研究内容

そこで播金優一助教らは、ハッブル宇宙望遠鏡よりも長い波長をカバーしている地上望遠鏡の観測データを用いて、GN-z11よりも遠方の宇宙に存在する銀河を探査しました。研究チームをリードした播金優一助教はこう語ります。「135億光年かなたの銀河を探すには現状では長い波長をカバーしている地上望遠鏡の画像を使う必要があるのですが、このような試みはこれまで行われてきませんでした。これは地上望遠鏡はハッブル宇宙望遠鏡に比べて感度が悪く、普通は暗いと考えられている遠方銀河の探査には不向きだと思われていたためです。しかし我々は最近の複数の研究結果から明るい遠方銀河も実は存在するのではないか、と仮説を立て、地上望遠鏡の画像データを使って135億光年かなたの銀河を探し始めました。」

すばる望遠鏡、VISTA望遠鏡、UK赤外線望遠鏡、スピッツァー宇宙望遠鏡の合計1200時間以上の観測によって得られた70万個以上の天体データから、135億光年かなたの最遠方銀河の候補天体、HD1が発見されました。「70万個以上の天体からHD1を見つけるのはとても大変な作業でした。」実際にHD1を発見した播金優一助教は話します。「銀河の探索条件を変えながら何度も画像データを調べ上げて、数ヶ月かけてやっとHD1に出会うことができました。HD1の色は赤く、135億年前の銀河の予想される特徴と驚くほどよく一致しており、見つけた時には少し鳥肌が立ちました。銀河のスペクトルモデルを使った詳細な解析を経て、私たちはHD1は135億年前の銀河だという解釈が最も妥当だと結論づけました。しかし確証を得るためには、正確な距離を測ることのできる分光観測が必要です。」

そこで研究チームは酸素輝線を検出するために、ALMA望遠鏡を用いて分光観測を行いました。分光観測をリードした井上昭雄教授はこう語ります。「我々は酸素輝線が予想される周波数に弱いシグナルを見つけました。シグナルの有意度は99.99%です。もしこのシグナルが本物なら、HD1は135億光年かなたに存在していることの証拠になりますが、99.9999%の有意度がないと確証は持てません。一方でシグナルが弱いことは酸素が少ないこと、つまりHD1はできたての初代銀河のような性質を持つことを示しているのかもしれません。」

HD1は非常に明るく、これはHD1のような明るい天体がビッグバン後わずか3億年の宇宙に既に存在していたことを示唆しています。HD1の存在は、これまでの銀河形成の理論モデルでは予言されていませんでした。HD1に関する観測的な情報は限られており、物理的な性質は謎に包まれています。非常に活発な星形成をしている銀河だと考えられますが、一方で活動的なブラックホールだという説もあります。どちらの説でも非常に興味深い天体です。

③ 社会的意義・今後の予定

HD1はその天文学的な重要性が認められて、去年に打ち上げられたジェイムズ・ウェッブ宇宙望遠鏡の第1期観測のターゲットになっています。播金優一助教はこの宇宙望遠鏡による観測も主導しています。「HD1はジェイムズ・ウェッブ宇宙望遠鏡の分光器の1つ、NIRSpecにより観測が行われる予定です。もし分光観測により正確な距離が確認されれば、GN-z11より1億光年遠い、これまでの記録を塗り替える最遠方の銀河になります。ジェイムズ・ウェッブ宇宙望遠鏡では他にもワクワクするような観測がたくさん予定されており、今から観測が非常に待ち遠しいです。」

※今回の研究は、科学研究補助金 （番号 17H06130, 19J01222, 20K22358, 21K13953） 、国立天文台ALMA共同科学研究事業2020-16Bによるサポートを受けています。

5．発表雑誌

雑誌名：The Astrophysical Journal （2022年4月8日掲載）
論文タイトル：A Search for H-Dropout Lyman Break Galaxies at z~12-16
著者： Yuichi Harikane, Akio K. Inoue, Ken Mawatari, Takuya Hashimoto, Satoshi, Yamanaka, Yoshinobu Fudamoto, Hiroshi Matsuo, Yoichi Tamura, Pratika Dayal, L. Y. Aaron Yung, Anne Hutter, Fabio Pacucci, Yuma Sugahara, and Anton M. Koekemoer
DOI番号：10.3847/1538-4357/ac53a9
URL：https://iopscience.iop.org/article/10.3847/1538-4357/ac53a9
https://ui.adsabs.harvard.edu/abs/2021arXiv211209141H/abstract

注記

（注） 今回見つかった銀河候補HD1の推定赤方偏移はz=13.3でした。赤方偏移は宇宙論的距離を表す際に使われる指標です。Planck 観測機チームが2015年に公表した宇宙論パラメータ (Planck Collaboration 2016, “Planck 2015 results. XIII.Cosmological parameters”, “TT,TE,EE+lowP+lensing+ext” in Table 4; H0 =67.74 km/s/Mpc, Ωm=0.3089, ΩΛ=0.6911) を用いて赤方偏移から距離を計算すると134.8億光年となり、HD1は134.8億年前に存在していたことになります。一方で宇宙は膨張していますので、現在の宇宙では我々とこの銀河候補の距離は134.8億光年以上になります。参考としてGN-z11は赤方偏移がz=11.0で、133.8億光年かなたの宇宙に存在しています。また今回の研究ではHD1の他に、134.4億光年かなた （赤方偏移z=12.3）に存在する銀河の候補、HD2も見つかっており、こちらもジェイムズ・ウェッブ宇宙望遠鏡による観測が行われる予定です。