BitVisorのコミットログで学ぶセキュアプログラミング

# BitVisor Advent Calendar 3日目

の記事です．

@y_oyama です．
筑波大学で[システムプログラム](http://www.coins.tsukuba.ac.jp/~syspro/2017/)とか[システムプログラミング序論](https://www.cs.tsukuba.ac.jp/~oyama/spintro2017/)とか[全学計算機システム](https://www.u.tsukuba.ac.jp/)とかをやっています．

# 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

```c:
 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言語の整数の符号やオーバフローや昇格についての仕様は最高の娯楽です．たとえば以下のプログラム

```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）で実行した結果は

```c:
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つのみです．残りは，暗黙の型変換によってオーバフロー無しで処理されたり，そもそもビット幅が足りていてオーバフローしていなかったりします．

```c:
long int a = -0x80000000;
```

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

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

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

また，

```c:
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 さんがすばらしい記事を書いて下さっています．
 - [C++ における整数型の怪と "移植性のある" オーバーフローチェッカー (第1回 : 整数型の怪と対策の不足)](https://qiita.com/a4lg/items/541c9d9dd5d874eeef2f)
 - [C++ における整数型の怪と "移植性のある" オーバーフローチェッカー (第2回 : 符号無し整数型のチェック)](https://qiita.com/a4lg/items/3b92538049969715bf10)
 - [C++ における整数型の怪と "移植性のある" オーバーフローチェッカー (第3回 : C言語の整数の性質を知る)](https://qiita.com/a4lg/items/9546ea49b8c1f98e6603)
 - [C++ における整数型の怪と "移植性のある" オーバーフローチェッカー (第4回 : 符号付き整数型のチェックと動機の動機)](https://qiita.com/a4lg/items/68b7fab23678b5354b01)
 - [C++ における整数型の怪と "移植性のある" オーバーフローチェッカー (第5回 : 続・符号付き整数型のチェック)](https://qiita.com/a4lg/items/bc4d2cfbce22fe749589)
- @raccy さんもすばらしい記事を書いて下さっています．
 - [C言語の整数リテラルの謎](https://qiita.com/raccy/items/419594556442bcf9d1df)
 - [C言語の整数リテラルの謎【解説編】](https://qiita.com/raccy/items/e793f67f7e0ab98ef0d9)
- [CERT C コーディングスタンダード](http://www.jpcert.or.jp/sc-rules/) は味わい深く，非常に勉強になります．
 - [INT02-C. 整数変換のルールを理解する](http://www.jpcert.or.jp/sc-rules/c-int02-c.html)
 - [INT32-C. 符号付き整数演算がオーバーフローを引き起こさないことを保証する](http://www.jpcert.or.jp/sc-rules/c-int32-c.html)
- [C99の仕様書（PDFファイル）](http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1124.pdf) を読んでいると，1, 2時間はあっという間にたちます．
- [ベアメタルハイパバイザを用いたネットワークブートシステムの性能評価（PDFファイル）](http://www.nipc.med.tuat.ac.jp/home/jacn/annai/jacn21st-info/CACN2017-01.pdf), 第21回 学術情報処理研究集会 発表論文集, 2017年9月.
 - 筑波大学では1000台以上の端末でBitVisorベースのシステムが動いており，それを利用できる学生数は15000人を越えます．それにより，BitVisorのバグをより気にするようになりました．

# おわりに

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