BitVisor Advent Calendar 3日目

の記事です．

@y_oyama です．
筑波大学でシステムプログラムとかシステムプログラミング序論とか全学計算機システムとかをやっています．

BitVisorのレポジトリ

BitVisorのレポジトリは
https://bitbucket.org/bitvisor/bitvisor
にあります．コミットログは
https://bitbucket.org/bitvisor/bitvisor/commits/all
から見ることができます．EIRAKUさんのコミット回数が突出しています．2017年には他にKoomsinさんがコミットしています．

さてここで，BitVisorを乗っ取る手がかりを得るた...，いや，ハイパバイザの開発での注意点について学ぶために，キーワード "bug" でコミットログを検索してみます．
たとえば，こんなコミットが引っかかります．

pci: fix range check bug in pci_driver_option_get_int() function
https://bitbucket.org/bitvisor/bitvisor/commits/4c04d1c07431b436f4046506d7971aa152f87196

 int
 pci_driver_option_get_int (char *option, char **e, int base)
 {
    char *p;
    long int ret;

    ret = strtol (option, &p, base);
    if (p == option)
        panic ("pci_driver_option_get_int: invalid value %s",
               option);
-   if (ret < -0x80000000)
-       ret = -0x80000000;
+   /* -0x7FFFFFFF - 1 is signed, -0x80000000 is unsigned */
+   if (ret < -0x7FFFFFFF - 1)
+       ret = -0x7FFFFFFF - 1;
    if (ret > 0x7FFFFFFF)
        ret = 0x7FFFFFFF;
    if (e)
        *e = p;
    else if (*p != '\0')
        panic ("pci_driver_option_get_int: invalid value %s",
               option);
    return ret;
 }

-0x80000000 を -0x7FFFFFFF - 1に直しています．
コメントから，符号付き整数や整数オーバフローに関係していそうなバグであることがわかります．
なぜこの2つの整数は異なるのか？ -0x7FFFFFFF - 1がsignedなのはいいとして，なぜ-0x80000000がunsignedなのか？

C言語の整数の符号やオーバフローや昇格についての仕様は最高の娯楽です．たとえば以下のプログラム

#include <stdio.h>

#define f(expr) { a = (expr); printf("%42s -> %16lx (%ld)\n", (#expr), a, a); }

int main(void)
{
  long int a;

  printf("sizeof(int)      = %ld\n", sizeof(int));
  printf("sizeof(long int) = %ld\n", sizeof(long int));

  printf("\n");

  printf("======== very large numbers ========\n");

  f(0x7fffffff);
  f(0x7fffffff + 1);
  f(((long int)0x7fffffff) + 1);
  f(0x80000000);
  f(0x80000000 > 0);
  f((int)0x80000000);
  f((int)0x80000000 > 0);
  f(0x80000000 + 1);
  f(0x80000001);

  printf("\n");

  printf("======== very small numbers ========\n");

  f(-0x7fffffff);
  f(-0x7fffffff - 1);
  f(-0x7fffffff - 2);
  f(-0x80000000);
  f(-(0x80000000));
  f(-0x80000000 > 0);
  f(-0x0000000080000000);
  f(-0x0000000080000000 > 0);
  f(-0x80000000L);
  f(-0x80000000L > 0);

  f(-((int)0x80000000));
  f(-((unsigned int)0x80000000));
  f(-((long int)0x80000000));
  f(-((long long int)0x80000000));
  f(-2147483647);
  f(-2147483647 - 1);
  f(-2147483647 - 2);
  f(-((long int)2147483647) - 2);
  f(-2147483648);
  f(-2147483648 - 1);
  f(-2147483648 - 2);
  f(-2147483649);

  printf("\n");

  return 0;
}

を私の環境（gcc 4.4.7 on CentOS 6.9 on x86_64）で実行した結果は

sizeof(int)      = 4
sizeof(long int) = 8

======== very large numbers ========
                                0x7fffffff ->         7fffffff (2147483647)
                            0x7fffffff + 1 -> ffffffff80000000 (-2147483648)
                ((long int)0x7fffffff) + 1 ->         80000000 (2147483648)
                                0x80000000 ->         80000000 (2147483648)
                            0x80000000 > 0 ->                1 (1)
                           (int)0x80000000 -> ffffffff80000000 (-2147483648)
                       (int)0x80000000 > 0 ->                0 (0)
                            0x80000000 + 1 ->         80000001 (2147483649)
                                0x80000001 ->         80000001 (2147483649)

======== very small numbers ========
                               -0x7fffffff -> ffffffff80000001 (-2147483647)
                           -0x7fffffff - 1 -> ffffffff80000000 (-2147483648)
                           -0x7fffffff - 2 ->         7fffffff (2147483647)
                               -0x80000000 ->         80000000 (2147483648)
                             -(0x80000000) ->         80000000 (2147483648)
                           -0x80000000 > 0 ->                1 (1)
                       -0x0000000080000000 ->         80000000 (2147483648)
                   -0x0000000080000000 > 0 ->                1 (1)
                              -0x80000000L -> ffffffff80000000 (-2147483648)
                          -0x80000000L > 0 ->                0 (0)
                        -((int)0x80000000) -> ffffffff80000000 (-2147483648)
               -((unsigned int)0x80000000) ->         80000000 (2147483648)
                   -((long int)0x80000000) -> ffffffff80000000 (-2147483648)
              -((long long int)0x80000000) -> ffffffff80000000 (-2147483648)
                               -2147483647 -> ffffffff80000001 (-2147483647)
                           -2147483647 - 1 -> ffffffff80000000 (-2147483648)
                           -2147483647 - 2 ->         7fffffff (2147483647)
               -((long int)2147483647) - 2 -> ffffffff7fffffff (-2147483649)
                               -2147483648 -> ffffffff80000000 (-2147483648)
                           -2147483648 - 1 -> ffffffff7fffffff (-2147483649)
                           -2147483648 - 2 -> ffffffff7ffffffe (-2147483650)
                               -2147483649 -> ffffffff7fffffff (-2147483649)

です（生半可なCプログラマには予測不能！）．
ちなみにコンパイラが整数オーバフローの警告を発するのは

0x7fffffff + 1;
-0x7fffffff - 2;
-((int)0x80000000);
-2147483647 - 2;

の4つのみです．残りは，暗黙の型変換によってオーバフロー無しで処理されたり，そもそもビット幅が足りていてオーバフローしていなかったりします．

long int a = -0x80000000;

の理解については，@raccy さんの

C言語の整数リテラルの謎【解説編】
https://qiita.com/raccy/items/e793f67f7e0ab98ef0d9

という記事に詳しい説明があります．

また，

long int a = -0x7FFFFFFF - 1;

の解釈は，
1. 0x7FFFFFFFは（32 bitの）int型データ幅に収まる範囲の整数である．よって0x7FFFFFFFはint型のデータになる．符号は正であり，10進数で書くと2147483647．
2. それがオペランドとして単項マイナスオペレータに渡される．オペランドはもともとint型なので，演算前の暗黙の整数拡張は行われない．算術演算に伴う型変換も行われない．算術演算でオーバフローは起こらない．結果はint型の負の整数であり，値は-2147483647．
3. 二項マイナスオペレータによる減算が行われる．2つのオペランドはどちらももともとint型なので，演算前の暗黙の整数拡張は行われない．算術演算に伴う型変換も行われない．算術演算でオーバフローは起こらない．結果はint型の負の整数であり，値は-2147483648．
4. それがオペランドとして代入オペレータに渡される．int型がlong int型に型変換されてaに代入される．でも，符号も値も変化しない．
となると思っています．

C言語の整数の仕様おそるべしです．
BitVisorもこの仕様に起因するバグを含んでいた時期があったことが，コミットログからわかりました．

関連資料

@a4lg さんがすばらしい記事を書いて下さっています．
@raccy さんもすばらしい記事を書いて下さっています．
- C言語の整数リテラルの謎
- C言語の整数リテラルの謎【解説編】
CERT C コーディングスタンダードは味わい深く，非常に勉強になります．
- INT02-C. 整数変換のルールを理解する
- INT32-C. 符号付き整数演算がオーバーフローを引き起こさないことを保証する
C99の仕様書（PDFファイル）を読んでいると，1, 2時間はあっという間にたちます．
ベアメタルハイパバイザを用いたネットワークブートシステムの性能評価（PDFファイル）, 第21回学術情報処理研究集会発表論文集, 2017年9月.
- 筑波大学では1000台以上の端末でBitVisorベースのシステムが動いており，それを利用できる学生数は15000人を越えます．それにより，BitVisorのバグをより気にするようになりました．

おわりに

BitVisorの話というよりはC言語やセキュアプログラミングの話でした．
BitVisorのコミットログからは，開発者の息づかいのようなものが伝わってくる気がします．