libxml2のxmlBuildQNameで、なぜ容量の検査が働かなかったのか？

libxml2のxmlBuildQNameは接頭辞とローカル名からprefix:nameの形の名前（QName）を組み立てる関数です。呼び出し側が渡したバッファに結果が収まるかを確かめ、収まらなければ新しく領域を確保します。¹

CVE-2025-6021はこの確認が働かない入力があるという脆弱性です。接頭辞とローカル名の長さにコロンと終端の2バイトを足した値（必要なバイト数）がintの上限を超えると、100バイトのバッファにも約2GiBの名前を書き込みます。²³ この記事では原因のコードと修正を読み、修正前のlibxml2 2.14.3で実際に確かめます。最後の章では、同じ計算をAdaのサブセットであるSPARKで書いた例として、小村ソフトが実験として公開しているlibxml3の実装を取り上げ、証明できた範囲と証明していない範囲を示します。libxml3はlibxml2の後継ではありません。

実測は2026年11月13日に、Ubuntu 24.04.5 LTS（x86-64）のGCC 13.3.0で行いました。intが32ビット、size_tが64ビットの環境です。32ビットの環境では試していません。

1. 概要

CVE-2025-6021は2025年6月12日に公開された、libxml2のxmlBuildQNameの脆弱性です。CVEの記録は、バッファの大きさの計算で整数オーバーフローが起き、スタック上のバッファの範囲外への書き込みにつながると説明しています。結果として挙げているのはメモリ破壊とサービス妨害（DoS）です。²

libxml2の保守担当者のNick Wellnhoferは報告への返信で、パーサーには名前の長さの検査があるのでパーサーは影響を受けないはずだと述べています。影響を受けうるものとして挙げているのは、長い文字列を渡してxmlBuildQNameを呼ぶ、libxml2を使う側のプロジェクトです。⁸ この記事の実測では、修正前のlibxml2 2.14.3で、ツリーを作るAPIで作った要素を検証の関数の1つであるxmlValidNormalizeAttributeValueに渡した場合にも、同じ大きさの範囲外への書き込みが検出されました。

flowchart TB
        accTitle: CVE-2025-6021で範囲外への書き込みに至るまで
        accDescr: 接頭辞とローカル名から求めた必要なバイト数がintの上限を超えると、容量の検査が働かず、呼び出し側のバッファの外へ書き込み、メモリ破壊やサービス妨害につながる流れを示します。
        A["接頭辞とローカル名を渡す"] --> B{"必要なバイト数がintの上限を超えるか"}
        B -->|"超えない"| C["容量の検査が正しく働く"]
        B -->|"超える"| D["容量の検査が働かない"]
        D --> E["バッファの外へ書き込む"]
        E --> F["メモリ破壊、サービス妨害"]

図1: 必要なバイト数がintの上限を超える入力では、容量の検査が働かなくなります。²³

図の実線は常に成り立つ関係、破線は条件付きの関係です(成立条件は詳細ページの各関係の説明に記載)。関係すべての一覧(全10件、根拠・確度つき)と主要概念の定義は知識マップ詳細ページにまとめています。データ: JSON-LD / Turtle

2. 対象

影響を受けるバージョン

CVEの記録は2.14.4より前のlibxml2を影響ありとしています。⁹ 修正は3つのブランチに入りました。

長さをintの変数に入れてlen < lenn + lenp + 2で容量を確かめる書き方は、この関数が2003年4月に追加されたときからあります。¹⁴

Red Hatは、Red Hat Enterprise Linuxの7（Extended Lifecycle Support）、8、9、10のlibxml2パッケージに修正版を出しています。9では2.9.13-10.el9_6が修正版で、上流の2.14.4より古いバージョン番号のまま修正が入っています。Red Hat Enterprise Linux 6の状態はunknownと記録されています。ここに挙げたのは代表例で、CVEの記録にはRed Hat Enterprise Linuxの延長サポートの各ストリームやRed Hat OpenShift Container Platformなども載っています。⁹

影響を受ける呼び出し方

修正前のコードを読むと、3章で確かめる場合のように呼び出し側のバッファの外へ書き込むには、次の3つが必要です。2つ目の数値はこの記事で修正前のコードから導いたもので、資料に書かれた値ではありません。

1. 接頭辞（NULLではない）とローカル名を渡してxmlBuildQNameを呼ぶ。
2. 2つの長さの合計が2,147,483,646バイト以上である。コロンと終端の2バイトを足すとintの上限の2,147,483,647を超える。
3. 結果を書き込むバッファを呼び出し側が渡している。呼び出し側はアプリケーションのこともlibxml2の内部の関数のこともある。

この3つは必要な条件で、そろえば必ず外へ書き込むわけではありません。長さがintに収まらないほど大きいと、lennやlenpには実際の長さと違う値が入り、結果はその値で変わります。また、バッファを渡さない呼び出しでも、長さの組み合わせによっては確保した領域の外へ書き込みえます。たとえば2つの長さがどちらもINT_MAXのとき、必要なバイト数が32ビットで0に折り返すと仮定すると、0バイトの確保が成功すれば、そのあとにmemcpyが続きます。この段落の内容は修正前のコードを読んで導いたもので、動かして確かめてはいません。

XML文書をパースさせるだけでは、2つ目の条件を満たさないはずです。libxml2 2.14.3のパーサーは名前の長さを既定で50,000バイトに制限しており、XML_PARSE_HUGEを指定したときの上限も10,000,000バイトです。¹⁵ libxml2の内部にも50バイトのバッファを渡してこの関数を呼ぶ箇所がありますが、そこへ渡る名前がパーサーの読んだものなら、この上限に収まります。¹⁶ これは保守担当者の説明と上限の定義からの判断で、パーサーからxmlBuildQNameまでのすべての経路を調べたわけではありません。

この上限がかかるのはパーサーが読んだ名前だけです。ツリーを作るAPIのxmlNewNodeは、プログラムが渡した名前を、パーサーのような長さの上限をかけずに要素にコピーします。コピーできるのは長さがintに収まる名前までです。¹⁷ そうして作った要素をxmlValidNormalizeAttributeValueのような検証の関数に渡すと、xmlBuildQNameを直接呼ばなくても、50バイトのバッファを使う内部の呼び出しに長い名前が渡ります。この経路は3章で実測します。

flowchart TB
        accTitle: ツリーを作るAPIに渡した名前が内部の呼び出しに渡る経路
        accDescr: xmlNewNodeに渡した名前はパーサーのような長さの上限なしで要素にコピーされ、その要素を検証の関数に渡すと、関数が50バイトのバッファでxmlBuildQNameを呼ぶことを示します。
        A["xmlNewNodeに長い名前を渡す"] --> B["パーサーの上限なしで要素にコピーされる"]
        B --> C["要素を検証の関数に渡す"]
        C --> D["50バイトのバッファでxmlBuildQNameを呼ぶ"]

図2: ツリーを作るAPIに渡した名前は、パーサーの上限がかからないまま内部の呼び出しへ渡ります。¹⁷¹⁶

保守担当者は、この関数を使うオープンソースのプロジェクトはとても少ないようだと書き、見つかった例としてswift-corelibs-foundationとPHPのSOAP拡張を挙げています。報告者はWineも多く使っていると返信しています。¹⁸ これらのプロジェクトが実際に影響を受けるかは、この記事では確かめていません。

flowchart TB
        accTitle: xmlBuildQNameへ長い名前が渡る経路
        accDescr: パーサーが読んだ名前は長さの上限で止まり、パーサーを通らない文字列がxmlBuildQNameに渡る経路では、長さの合計が2,147,483,646バイト以上のときに範囲外への書き込みが起きうることを示します。
        A["XML文書の名前"] --> B["パーサーの長さの上限"]
        B --> C["最大でも10,000,000バイト"]
        D["パーサーを通らない文字列"] --> E["xmlBuildQNameに渡る"]
        E --> F{"長さの合計が2,147,483,646バイト以上か"}
        F -->|"はい"| G["範囲外への書き込みが起きうる"]
        F -->|"いいえ"| H["この条件は満たさない"]

図3: パーサーを通った名前は上限で止まるので、条件を満たしうるのはパーサーを通らない文字列がxmlBuildQNameに渡る経路です。⁸¹⁵

3. 詳細

xmlBuildQNameの動作

xmlBuildQNameは4つの引数を受け取ります。ローカル名のncname、接頭辞のprefix、呼び出し側が用意したバッファのmemory、その大きさのlenです。prefixがNULLならncnameをそのまま返します。NULLでなければ、結果に必要なバイト数を2つの長さとコロン、終端のNULの合計として求めます。memoryがNULLでなくlenが必要なバイト数以上ならmemoryに書き、そうでなければ新しい領域を確保して書きます。¹

バッファを渡すと、結果が収まる場合は領域を確保せずに済みます。この関数を追加したコミットのメッセージには、QNameを組み立てるコードから余分な確保を取り除くとあります。¹⁴ libxml2の内部では、50バイトの配列をスタックに置いて渡す呼び出しが検証の処理などにあります。¹⁶

flowchart TB
        accTitle: xmlBuildQNameが書き込み先を決める手順
        accDescr: prefixがNULLならncnameを返し、そうでなければ必要なバイト数を求め、memoryがありlenが足りればmemoryへ、足りなければ新しく確保した領域へ書くことを示します。
        A{"prefixがNULLか"} -->|"はい"| B["ncnameをそのまま返す"]
        A -->|"いいえ"| C["必要なバイト数を求める"]
        C --> D{"memoryがありlenが足りるか"}
        D -->|"はい"| E["memoryに書く"]
        D -->|"いいえ"| F["新しく確保して書く"]

図4: 書き込み先は必要なバイト数とlenの比較で決まります。¹

修正前のコード

libxml2 2.14.3のxmlBuildQNameは次のとおりです。ファジング用のビルドでだけ有効になる数行は省きました。¹

xmlChar *
xmlBuildQName(const xmlChar *ncname, const xmlChar *prefix,
	      xmlChar *memory, int len) {
    int lenn, lenp;
    xmlChar *ret;

    if (ncname == NULL) return(NULL);
    if (prefix == NULL) return((xmlChar *) ncname);

    lenn = strlen((char *) ncname);
    lenp = strlen((char *) prefix);

    if ((memory == NULL) || (len < lenn + lenp + 2)) {
	ret = xmlMalloc(lenn + lenp + 2);
	if (ret == NULL)
	    return(NULL);
    } else {
	ret = memory;
    }
    memcpy(&ret[0], prefix, lenp);
    ret[lenp] = ':';
    memcpy(&ret[lenp + 1], ncname, lenn);
    ret[lenn + lenp + 1] = 0;
    return(ret);
}

strlenが返すのはsize_tの値ですが、代入先のlennとlenpはintです。容量を確かめるlen < lenn + lenp + 2の右辺もintどうしの足し算なので、結果もintで求まります。報告はこの2点を原因に挙げています。³

必要なバイト数がintの上限を超える入力での計算

報告にある値で計算を追います。接頭辞が10バイト、ローカル名がINT_MAX - 10バイト、呼び出し側のバッファが100バイトです。³

必要なバイト数はintの上限を2だけ超えます。Cの規格は、式の結果がその型で表せる範囲に収まらないときの動作を未定義としており、整数のオーバーフローを未定義の動作の例に挙げています。¹⁹ 表の5行目は、結果が2の補数の32ビットで折り返すと仮定した記事の計算値です。規格が折り返しを決めているわけではありません。

折り返した値は負なので、100はそれより小さくありません。検査は「バッファが足りない」と判定せず、関数は呼び出し側のバッファを書き込み先に選びます。報告もこの場合を、合計が小さな正の値か負の値に折り返して検査の条件が偽になる場合として説明しています。³

flowchart TB
        accTitle: 容量の検査が偽になるまでの計算
        accDescr: strlenの結果をintに代入し、lenn + lenp + 2をintで計算するとintの上限を超えて負の値になり、len < 負の値が偽になって呼び出し側のバッファが選ばれることを示します。
        A["strlenの結果をintに代入"] --> B["lenn + lenp + 2をintで計算"]
        B --> C["2,147,483,649はintの上限を超える"]
        C --> D["折り返すと負の値になる"]
        D --> E["100 < 負の値 は偽"]
        E --> F["呼び出し側のバッファに書く"]

図5: 検査の式の値がintの上限を超え、足りないバッファが足りると判定されます。³

書き込み先が決まると、関数は接頭辞の10バイト、コロンの1バイト、ローカル名の2,147,483,637バイトの順に書きます。100バイトのバッファに収まるのはローカル名の先頭の89バイトまでで、残りの2,147,483,548バイトはバッファの外に書かれます。この2つの数値は記事の計算値です。

flowchart TB
        accTitle: 100バイトのバッファへの書き込みの内訳
        accDescr: 接頭辞10バイト、コロン1バイト、ローカル名の先頭89バイトまでがバッファに収まり、残りの2,147,483,548バイトがバッファの外に書かれることを示します。
        A["接頭辞10バイト"] --> B["コロン1バイト"]
        B --> C["ローカル名の先頭89バイト"]
        C --> D["ここで100バイトのバッファが終わる"]
        D --> E["残り2,147,483,548バイトは外へ"]

図6: バッファに収まるのは先頭の100バイトだけで、ローカル名の残りは外に書かれます。

報告はもう1つの場合も挙げています。strlenの結果がintに収まらず、代入したlennが負になる場合です。報告の例ではlennが−1、lenpが4、lenが100で、検査は100 < 5となって偽になり、memcpyには−1をsize_tに直した大きさが渡ります。³ この場合は試していません。

修正前のlibxml2 2.14.3での実測

タグv2.14.3とv2.14.4のlibxml2をそれぞれ静的ライブラリとしてビルドし、同じ確認用のプログラムをリンクして動かしました。コンパイルのオプションは-g -O1 -fno-omit-frame-pointer -fsanitize=address,undefinedです。このオプションで有効になるAddressSanitizerは範囲外へのアクセスを、UndefinedBehaviorSanitizerは符号付き整数のオーバーフローを実行時に検出します。²⁰ 確認用のプログラムは次のとおりで、報告と同じ値でxmlBuildQNameを1回呼び、戻り値がどれに当たるかを表示します。

/* xmlBuildQName を、必要なバイト数が INT_MAX を超える入力で呼ぶ確認用プログラム。
   入力の値は libxml2 の Issue #926 の報告と同じ（prefix 10 バイト、
   ncname INT_MAX - 10 バイト、呼び出し側のバッファ 100 バイト）。 */
#include <limits.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <libxml/tree.h>
#include <libxml/xmlerror.h>
#include <libxml/xmlmemory.h>

int main(void) {
    const xmlChar *prefix = (const xmlChar *)"1234567890";
    size_t name_length = (size_t)INT_MAX - 10;
    xmlChar *name = malloc(name_length + 1);
    xmlChar buffer[100];
    xmlChar *result;

    if (name == NULL) {
        fprintf(stderr, "allocation failed\n");
        return 2;
    }
    memset(name, 'A', name_length);
    name[name_length] = '\0';
    memset(buffer, 'B', sizeof(buffer));

    result = xmlBuildQName(name, prefix, buffer, (int)sizeof(buffer));
    if (result == buffer) {
        printf("result: caller buffer\n");
    } else if (result != NULL) {
        printf("result: new allocation, length %zu\n", strlen((const char *)result));
        xmlFree(result);
    } else {
        const xmlError *error = xmlGetLastError();
        printf("result: NULL, last error code %d\n", error != NULL ? error->code : 0);
    }
    free(name);
    return 0;
}

libxml2 2.14.3では次の出力で止まりました。抜粋で、パスは短くしてあります。

tree.c:186:34: runtime error: signed integer overflow: 2147483647 + 1 cannot be represented in type 'int'
==2418==ERROR: AddressSanitizer: stack-buffer-overflow on address 0x7f9606300094
WRITE of size 2147483637 at 0x7f9606300094 thread T0
    #2 0x5570f5ea564a in xmlBuildQName tree.c:195
    #3 0x5570f5e81ff6 in main buildqname_probe.c:27
  This frame has 1 object(s):
    [48, 148) 'buffer' (line 16) <== Memory access at offset 148 overflows this variable

186行目は容量を確かめるifの行、195行目はローカル名をコピーするmemcpyの行です。¹ 書き込みの大きさの2,147,483,637はローカル名の長さと一致します。bufferはフレームの48バイト目から148バイト目の手前までを占めており、検出された位置の148はその直後です。1行目のメッセージの式は2147483647 + 1で、ソースのlenn + lenp + 2とは形が違います。GCC 13.3.0の出力をそのまま載せています。

libxml2 2.14.4では、同じプログラムがエラーなしで終わりました。

result: new allocation, length 2147483648

容量の検査が「足りない」と判定し、関数は新しい領域を確保してそこへ書いています。長さの2,147,483,648は接頭辞の10、コロンの1、ローカル名の2,147,483,637の合計です。

ツリーを作るAPIで作った要素を検証の関数に渡した場合の実測

xmlBuildQNameを直接呼ばない経路も同じ2つのビルドで試しました。確認用のプログラムは同じ長さの名前と接頭辞を持つ要素をxmlNewNodeで作り、xmlValidNormalizeAttributeValueに渡します。この関数は公開のヘッダーにありますが、非推奨の指定が付いており、説明のコメントには内部用の関数で使わないようにとあります。¹⁶ 次はプログラムの抜粋です。

ns = xmlNewNs(NULL, (const xmlChar *)"urn:example", (const xmlChar *)"1234567890");
element = xmlNewNode(ns, name);
/* 中略 */
normalized = xmlValidNormalizeAttributeValue(doc, element,
                                             (const xmlChar *)"a",
                                             (const xmlChar *)"v");

libxml2 2.14.3では、同じ大きさの書き込みが検証の関数の中にある50バイトのバッファで検出されました。次は出力の抜粋です。

WRITE of size 2147483637 at 0x7fe236e00052 thread T0
    #2 0x55a1a12e0b4e in xmlBuildQName tree.c:195
    #3 0x55a1a133ec30 in xmlValidNormalizeAttributeValue valid.c:3938
    #4 0x55a1a12c3f9f in main tree_api_probe.c:35
  This frame has 1 object(s):
    [32, 82) 'fn' (line 3935) <== Memory access at offset 82 overflows this variable

libxml2 2.14.4ではサニタイザーの報告は出ず、プログラムは最後まで動きました。関数の戻り値はNULLでしたが、これは属性の宣言が見つからないときの通常の戻り値で、入力を拒んだわけではありません。試したのはこの関数だけで、50バイトのバッファを渡すほかの内部の呼び出しは試していません。

修正の内容

修正のコミットはtree.cの5行を足し、3行を消しています。次はその差分の抜粋です。¹⁰

-    int lenn, lenp;
+    size_t lenn, lenp;
     xmlChar *ret;
 
-    if (ncname == NULL) return(NULL);
+    if ((ncname == NULL) || (len < 0)) return(NULL);
     if (prefix == NULL) return((xmlChar *) ncname);
@@
     lenn = strlen((char *) ncname);
     lenp = strlen((char *) prefix);
+    if (lenn >= SIZE_MAX - lenp - 1)
+        return(NULL);
 
-    if ((memory == NULL) || (len < lenn + lenp + 2)) {
+    if ((memory == NULL) || ((size_t) len < lenn + lenp + 2)) {

変更は3つあります。1つ目は長さをstrlenの戻り値と同じsize_tで持つことです。2つ目は2つの長さを足す前に、足した結果がsize_tに収まるかを確かめることです。保守担当者は、strlenが返す理論上の最大値はSIZE_MAX - 1なのでSIZE_MAX - lenp - 1はオーバーフローしないと説明しています。²¹ 3つ目は負のlenには先にNULLを返し、比較をsize_tどうしで行うことです。

flowchart TB
        accTitle: 修正後のxmlBuildQNameの検査の順序
        accDescr: 修正後は負のlenにNULLを返し、長さをsize_tで求め、足した結果がsize_tに収まらなければNULLを返し、そのあとでsize_tどうしで容量を比較することを示します。
        A{"lenが負か"} -->|"はい"| B["NULLを返す"]
        A -->|"いいえ"| C["長さをsize_tで求める"]
        C --> D{"必要なバイト数がsize_tに収まるか"}
        D -->|"収まらない"| B
        D -->|"収まる"| E["size_tどうしで容量を比較"]

図7: 修正後は足す前に結果が型に収まることを確かめてから容量を比較します。¹⁰

4. 影響

直接の結果は呼び出し側のバッファの外への書き込みです。CVEの記録はメモリ破壊かサービス妨害になりうるとしています。² Red HatのCVSS 3.1の評価は可用性への影響だけを「高」とし、機密性と完全性への影響を「なし」としています。⁴

報告者は影響の節で、あふれるバッファがヒープにあり、攻撃者が制御できるデータを書き込めるなら、任意のコードの実行につながる可能性があると書いています。³ これは報告者の見解で、CVEの記録の説明には任意のコードの実行は含まれていません。² 外に書かれるのはローカル名のバイト列なので、ローカル名を攻撃者が決められるなら、書かれる内容も攻撃者が決めることになります。サニタイザーなしのビルドで書き込みがどこまで進むかは、この記事では試していません。

この書き込みが起きるには、合計で約2GiBの文字列がこの関数に渡される必要があります。保守担当者はこの問題を、修正の簡単な小さな問題とみています。⁸ 一方でCVSSの基本値は7.5です。CVSS 3.1の仕様は基本値を、導入されるさまざまな環境に共通して、合理的に考えられる最悪の影響を仮定した値と説明しています。²² 自分のシステムでこの関数に約2GiBの文字列が渡されるかは、基本値とは別に確かめることになります。

flowchart TB
        accTitle: 自分のシステムへの影響の確かめ方
        accDescr: パーサーを通らない名前がxmlBuildQNameに渡るか、そこへ約2GiBの文字列が渡されるかを順に確かめ、どちらも当てはまるときに範囲外への書き込みが起きうることを示します。
        A{"パーサーを通らない名前が渡るか"} -->|"渡らない"| B["パーサーの上限で止まる"]
        A -->|"渡る"| C{"約2GiBの文字列が渡されるか"}
        C -->|"渡されない"| D["条件を満たさない"]
        C -->|"渡される"| E["範囲外への書き込みが起きうる"]

図8: 基本値とは別に、自分のシステムで2つの条件が成り立つかを確かめます。⁸

CISAの既知悪用脆弱性カタログの2026年11月10日版に、CVE-2025-6021はありません。⁷

5. 対策

libxml2の更新

上流のlibxml2を使っているなら、2.14.4以降か、2.13系の2.13.9以降に更新します。2.15.0以降は最初から修正を含みます。⁵⁶¹¹ 修正の内容は3章の「修正の内容」に書いたとおりです。

ディストリビューションのパッケージは上流のバージョン番号では判断できません。Red Hat Enterprise Linux 9の修正版は2.9.13-10.el9_6で、8の修正版は2.9.7-21.el8_10.1です。⁹ 入っているパッケージのバージョンをrpm -q libxml2などで調べ、ディストリビューションの告知にある修正版と比べます。

Red Hatは、使いやすさや適用できる範囲などの自社の基準を満たす緩和策はないとして、修正の適用を強く勧めています。²³

libxml2を静的にリンクした製品や、ライブラリを同梱した製品は、OSのパッケージを更新しても直りません。その製品の更新を待つか、自分でビルドし直します。

xmlBuildQNameに名前を渡すコードの確認

自分のコードにxmlBuildQNameの呼び出しがあれば、渡す2つの文字列の長さに上限があるかを確かめます。上限がなく、すぐにはlibxml2を更新できない場合は、呼び出しの前で長さを制限します。ツリーを作るAPIに、外から受け取った文字列を名前として渡している場合も同じです。

修正後もlenに実際のバッファより大きい値を渡せば範囲外に書き込みます。保守担当者は負のlenを検査する提案への返信で、この関数は固定のバッファと一緒に呼ぶものなのでlenは実際上いつも整数の定数になり、libxml2のAPIはすべての引数の検証を保証してきたわけではないと述べています。²⁴

同じ種類の誤りを探す警告

保守担当者は、同じような問題がコードベースにまだ多く見つかるだろうと書き、探す手段としてclangの-Wshorten-64-to-32を挙げています。Michael Catanzaroは-Wint-conversionも役に立つと返信しています。²⁵ どちらも報告のやり取りに出てくる提案で、この記事では試していません。

flowchart TB
        accTitle: CVE-2025-6021への対策の進め方
        accDescr: libxml2が修正版かを確かめて更新し、xmlBuildQNameに名前を渡すコードでは長さの上限を確かめ、警告のオプションで同じ種類の誤りを探す流れを示します。
        A{"libxml2は修正版か"} -->|"いいえ"| B["修正版に更新する"]
        A -->|"はい"| C["名前を渡すコードを探す"]
        B --> C
        C --> D["渡す長さの上限を確かめる"]
        D --> E["警告で同じ種類の誤りを探す"]

図9: 更新のあとで、xmlBuildQNameに名前を渡すコードを確かめ、同じ種類の誤りを警告で探します。²⁵

6. 教訓

容量の検査の式で起きたオーバーフロー

修正前のコードにも容量の検査はありました。働かなかったのは、検査の式を計算する型が確かめたい値を表せなかったためです。必要なバイト数の2,147,483,649はintで表せず、比較の前に別の値になっていました。

修正は、足し算の結果が型に収まることを足す前に確かめています。容量を計算するコードでは、容量の比較より前に、計算の途中の値が型に収まるかを確かめる必要があります。

同じ式をAdaで書いた場合

修正前と同じ形の判定をAdaのIntegerでそのまま書いてみます。Naturalは0以上のIntegerです。

package QName_Size with SPARK_Mode is
   function Fits
     (Capacity, Name_Length, Prefix_Length : Natural) return Boolean
   is (Capacity >= Name_Length + Prefix_Length + 2);
end QName_Size;

GNATproveで解析すると、足し算のオーバーフローの可能性が2件報告されました。次はそのうちの1件で、ソースの位置を示す行は省いてあります。

qname_size.ads:4:48: high: overflow check might fail, cannot prove upper bound for Name_Length + Prefix_Length + 2
  e.g. when Name_Length = Natural'Last-1
        and Prefix_Length = 0
  reason for check: result of addition must fit in a 32-bits machine integer
  possible fix: add precondition (Name_Length + Prefix_Length <= Integer'Last - 2) to subprogram at line 2

証明せずにコンパイルして、報告と同じ値（容量100、名前の長さInteger'Last - 10、接頭辞の長さ10）で呼ぶと、プログラムは次の例外で止まりました。コンパイラーはAlire 2.1.1で入れたgnat_native 14.2.1で、オプションは-gnat2022 -O1です。

raised CONSTRAINT_ERROR : qname_size.ads:4 overflow check failed

Adaの規格は、符号付き整数型の演算が基本範囲の外になるために正しい結果を返せないとき、Constraint_Errorを送出すると定めています。²⁶ 判定は偽にも真にもならず、書き込みには進みません。例外を処理しなければプログラムは止まるので、サービス妨害の余地は残ります。pragma Suppressでこの検査を外した場合は、この限りではありません。Adaの規格は、検査を外した状態でその検査が失敗する状況が起きると、実行は誤り（erroneous）になると定めています。²⁷

flowchart TB
        accTitle: 同じ式をCとAdaとSPARKで書いたときの違い
        accDescr: 結果が型の上限を超える足し算は、Cでは未定義の動作になり、Adaでは実行時にConstraint_Errorで止まり、SPARKではGNATproveが実行の前に報告することを示します。
        A["結果が型の上限を超える足し算"] --> B["C：未定義の動作"]
        A --> C["Ada：実行時に例外で止まる"]
        A --> D["SPARK：実行の前に報告される"]
        B --> E["検査が偽になり書き込みへ進んだ"]

図10: 同じ足し算でも、言語とツールによって誤りが分かる時点が違います。¹⁹²⁶

libxml3での長さの求め方

libxml3は小村ソフトが公開している実験的なプロジェクトで、Ada/SPARKで書いたXMLの処理と、libxml2に似たCのAPIの一部を提供します。libxml2.so.2と同じABIや、libxml2との完全な互換性は提供しません。²⁸ xmlBuildQNameに当たる処理はXML3_Text.QNames.Buildにあります。²⁹

XML3_Text.Buffers.Measure (Name, Name_Length, Measured, Last => Limit - 2);
if not Measured then
   return;
end if;
XML3_Text.Buffers.Measure
  (Prefix, Prefix_Length, Measured, Last => Limit - Name_Length - 2);
if not Measured then
   return;
end if;
Needed := Name_Length + Prefix_Length + 2;
Use_Buffer := Buffer /= System.Null_Address and then Capacity >= Needed;

Limitは必要なバイト数の上限で、既定値はInteger'Last - 16です。先に上限からコロンと終端の2バイトを引き、その範囲で名前の長さを測ります。接頭辞は名前の長さを引いた残りの範囲で測ります。Measureは、測った長さがLast以下であることを事後条件に書いています。²⁹ このためNeededは必ずLimit以下になり、足し算はIntegerの範囲に収まります。

GNATproveはBuildの18件の検査をすべて証明しました。Neededを求める行のオーバーフローの検査2件と範囲の検査1件は、この18件に含まれます。コミット13d2fafのソースを、Alire 2.1.1で入れたgnatprove 14.1.1で、--level=2 --timeout=120 --memlimit=4096を指定して解析した結果です。libxml3の証明の記録にも同じ18件が書かれています。³⁰

3章と同じ確認用のプログラムをlibxml3のヘッダーとライブラリでビルドして動かすと、次の結果になりました。

result: NULL, last error code 115

名前の長さが測る範囲の上限を超えたので、Buildは何も書かずに戻っています。115はXML_ERR_ARGUMENTです。libxml2 2.14.4は新しい領域を確保して返したので、結果は同じではありません。libxml3は必要なバイト数が上限を超える入力にはNULLを返します。³¹

flowchart TB
        accTitle: libxml3のBuildが長さを求める順序
        accDescr: 上限から2バイトを引いた範囲で名前を測り、残りの範囲で接頭辞を測るので、必要なバイト数が必ず上限以下になり、そのあとで容量と比較することを示します。
        A["上限から2バイトを引く"] --> B["その範囲で名前を測る"]
        B --> C["残りの範囲で接頭辞を測る"]
        C --> D["必要なバイト数は上限以下"]
        D --> E["容量と比較する"]

図11: 足す前に測る範囲を狭めておくので、足し算が型の範囲を超えません。²⁹

証明していない範囲

証明したのは、長さの計算が型の範囲に収まることと、Buildが返す状態と結果のポインターの関係（状態がBuiltのときだけ結果がNULLでない）です。²⁹ バイトの読み書きはSPARKの外にある部分が行い、ポインターが指す領域の実際の大きさは証明の対象に入っていません。libxml3の文書も、ポインターの有効性と範囲、確保と解放、実際のバイトの書き込み、CのABIを証明の外としています。³⁰ 呼び出し側がCapacityに実際より大きい値を渡せば、libxml3でもバッファの外に書き込みます。この点は修正後のlibxml2と同じです。

libxml3は実験的なプロジェクトで、libxml2の置き換えとして勧めるものではありません。ここで取り上げたのは長さの計算の書き方を比べるためです。

flowchart TB
        accTitle: libxml3のBuildで証明した範囲と証明していない範囲
        accDescr: 長さの計算が型の範囲に収まることと状態と結果の関係は証明し、ポインターが指す領域の実際の大きさとバイトの読み書きは証明の外にあることを示します。
        A["XML3_Text.QNames.Build"] --> B["証明した範囲"]
        A --> C["証明していない範囲"]
        B --> D["長さの計算が型に収まる"]
        B --> E["状態と結果の関係"]
        C --> F["領域の実際の大きさ"]
        C --> G["バイトの読み書き"]

図12: 証明したのは長さの計算と、状態と結果の関係で、渡された領域の実際の大きさは証明の対象に入っていません。³⁰

関連記事

• SPARKによる形式検証入門
• AIが書いたコードをSPARKで証明する
• 画像処理の境界外アクセスをSPARKで証明する
• Ada と Rust の安全性の考え方の違い
• Ada と C / C# をつなぐ

参考リンク

関連する記事

同じタグを共有する最新の記事です。さらに近い話題で知識を深められます。

関連トピック

このテーマと近いトピックページです。記事を起点に、関連するサービスや他の記事へ進めます。

このテーマがつながるサービス

この記事は次のサービスページにつながります。近い入口からご覧ください。

よくある質問

この記事のテーマについて、相談時によくある質問をまとめています。

XML文書をlibxml2でパースしているだけでも、CVE-2025-6021の影響を受けますか？

libxml2の保守担当者は、パーサーには名前の長さの検査があるので、パーサーは影響を受けないはずだと述べています。libxml2 2.14.3のパーサーは名前を既定で50,000バイト、XML_PARSE_HUGEを指定しても10,000,000バイトに制限しています。影響を受けうるのは、パーサーを通らない長い文字列がxmlBuildQNameに渡るプログラムです。

参考情報

• libxml2 Issue #926（This shouldn't affect the parser）
• libxml2 2.14.3 parserInternals.h（XML_MAX_NAME_LENGTH、XML_MAX_TEXT_LENGTH）

どのバージョンのlibxml2で直っていますか？

上流では2.14.4（2025年6月16日）と2.13.9（2025年9月8日）で直り、2.15.0以降は最初から修正を含みます。ディストリビューションは古いバージョンに修正を取り込んでいることがあるので、上流のバージョン番号だけでは判断できません。たとえばRed Hat Enterprise Linux 9では2.9.13-10.el9_6が修正版です。

参考情報

• libxml2 2.14.4 NEWS（Security）
• CVE-2025-6021の記録（affected）

AdaやSPARKで書けば、この種類の誤りは起きませんか？

同じ式をAdaのIntegerで書くと、オーバーフローの検査を外していなければ、実行時にConstraint_Errorになり、メモリの外への書き込みには進みません。SPARKではGNATproveが実行の前にオーバーフローの可能性を報告します。ただし小村ソフトの実験的な実装であるlibxml3で証明したのは長さの計算と、状態と結果の関係までで、呼び出し側が渡したバッファの実際の大きさは証明の外に残ります。

著者プロフィール

記事の著者プロフィールページです。

小村 豪

合同会社小村ソフト 代表

Windows ソフト開発、技術相談、不具合調査を中心に、既存資産が残る案件や原因が見えにくい障害調査に強みがあります。