explicit_bzeroとω矛盾

void explicit_bzero(void* s, size_t n)という関数があります。これの動作は、void bzero(void* s, size_t n)という関数と同じです。

void bzero(void* s, size_t n)という関数は、memset(s, '\0', n)と同じ動作をします。つまり、memset関数の方が上位互換な関数ということになります。上位互換な関数があるのにわざわざbzeroを使うのは変だとか、ゼロクリアみたいなよく使うものに関して専用の関数がある方が見通しが良いとかの論争があるようです*1

セキュリティと最適化

セキュリティのことを考えると、パスワードの平文のようなものは使い終わったらすぐにメモリ上から消す必要があります(メモリに入っている値を読む攻撃とかがあり得るので、平文をメモリ上に置いておく時間はなるべく短い方が良いです)。このためにbzeroを使うことを考えます。

コンパイラが賢いと、「この領域はこの後使うことがないようだ。だから、ゼロ埋めしてもしなくてもプログラムの見た目の挙動は変わらない。つまり、このbzeroは取り除ける。」と判断することがあります(as-ifルールによる最適化)。

しかし、セキュリティのためのゼロ埋めというのは、物理的実体のあるメモリに0を書き込んでほしいという、一種のIO要求です。 プログラムの見た目の挙動は変らないからといって、取り除かれてしまっては困ります。

explicit_bzeroというのは、そういった最適化が行われないことが保証される関数になっています。これで安心して平文パスワードの痕跡を物理世界から消すことができます*2*3

explicit_bzeroの実装

musl libcという、軽量libc実装があります。musl libcでexplicit_bzeroがどのように実装されているのかを見てみます。

explicit_bzero.c\string\src - musl - musl - an implementation of the standard library for Linux-based systems

#define _BSD_SOURCE
#include <string.h>

void explicit_bzero(void *d, size_t n)
{
    d = memset(d, 0, n);
    __asm__ __volatile__ ("" : : "r"(d) : "memory");
}

explicit_bzeroの中では、memsetに丸投げしていることが分かります。__asm__を使っている部分は、最適化を抑制するためのインラインアセンブリになっています。

__asm__で書かれるインラインアセンブリは、コロン区切りで必要な情報が書かれています。読み方は以下の通りです。

  1. "" アセンブリで書かれた命令語が入る。今回は空っぽ
  2. 出力オペランドが入る。今回は空っぽ
  3. "r"(d) 入力オペランドが入る。任意のレジスタx86だとメモリ上でも可?)に入った、dという変数
  4. "memory" 破壊されるオペランドが入るが、この場合はメモリが読み書きされることがあるという意味

つまり、「アセンブリ機械語としては何も出力しなくてよいです」「でも最適化で消さないでください(__volatile__)」「dという変数の値によって、何が起こるかが変わります」「メモリ上の値が読み書きされる可能性があります」という意味になっています。

dという変数の値やメモリの状態によって、何が起こるかが変わります」と言っているので、memset自体が最適化で消されないようになっているようです。

最適化抑制用のメモリバリアってω矛盾っぽい

学術用語の濫用は慎むべきですが、ちょっと思ったことを書いておきます。

ω矛盾(している公理系)とは、「すべてのxについて¬P(x)が証明できる」にもかかわらず、「∃x P(x)も証明できる」ような公理系のことです。一見矛盾しているようですが、必ずしも矛盾しているとは限りません。なぜなら、その公理系で∀x ¬P(x)が証明できるとは限らないからです。先ほど書いた「すべてのxについて……」というのはあくまでメタ視点での記述であることに注意してください。

メモリバリアは、コンパイラから見ると以下のようにふるまうような記述になっています。

  • この記述の前後で、値が変わっているメモリ番地が存在する(ことがありうる)

しかし、メモリバリアはただの空文字列なので、アセンブリには何も出力されません。つまり、プログラムは常に以下の性質を満たします。

  • この記述の前後で、全てのメモリ番地において、値が変わっているということは(必然的に)ありえない

ただし、この性質はコンパイラが最適化するために使えない情報です。

P(x)を「この記述の前後でメモリ番地xの値が変わっている」と読むと、前者の性質は、∃x P(x)に相当しています(「プログラムや外界の状況に応じて、そういうことがありうる」という意味を表すために可能性演算子◇を用いて◇∃x P(x)と書くべきかもしれません)。

一方、後者の性質は、∀x ¬P(x)と書くことができます(同様に必然性演算子□を用いて□∀x ¬P(x)と書くべきかもしれません)。

コンパイラの内部で後者の性質が証明できてしまうと矛盾が生じてまずいですが、個別のxについて¬P(x)を証明できたとしてもω矛盾になるだけなので大丈夫です。

これを利用すると、「∃x P(x)なので最適化は抑制される」「個別のxについて¬P(x)が証明できるので以降のメモリアクセスは最適化できる」のような、真に最適化してほしくないところだけを抑止し、他の部分の最適化まで抑止しないような、そういったさらにすごいコンパイラが作れたりしないのかな、ということをちょっと思いました。

*1:どこかのブログで読んだような気がしますが、忘れました。

*2:この辺の話も、同じブログで読んだような気がしますが、忘れました。

*3:キャッシュとかの影響により、物理世界から消すこと自体は保証されないような気もします。