ZetZ、略してZZは、RustにインスパイアされたCのダイアレクト(diarect, 方言)だ。コンパイル時に仮想マシン内でシンボリック実行することによって、コードの形式的検証を行う。
ZZはハードウェアに近い部分で動作するソフトウェアをターゲットにしているが、クロスプラットフォームなANSI-C準拠のライブラリ構築にも使用することができる。実際には、ZZはCコードのトランスパイラとして、処理結果を任意の標準的Cコンパイラに入力することで動作する。多くの言語が行っている安全性へのアプローチとは対照的に、ZZは、例えば生のポインタアクセスのように"安全でない(unsafe)"と見なした機能の除外や制限は行わない。その代わりに静的単一代入(static single assignment, SSA)を使用して、yices2やz3といったSMTプローバ(prover)内において、コードに未定義動作が存在しないことの証明をコンパイル時に行うのだ。
以下のスニペットは、ZZのコードがどのようなものかを示している。
using <stdio.h>::{printf}
export fn main() -> int {
let r = Random{
num: 42,
};
printf("your lucky number: %u\n", r.gen());
return 0;
}
struct Random {
u32 num;
}
fn gen(Random *self) -> u32 {
return self->num;
}
未定義動作がコード内にリークするのを防ぐために、ZZは、すべてのメモリアクセスが正しいことを要求する。例えば配列の要素を指定する場合には、呼び出し側が満足すべき制約を指定するキーワードwhereを使って、アクセスするインデックスが有効な値であることをコンパイラに示さなければならない。
fn bla(int * a)
where len(a) >= 3
{
a[2];
}
同じように、キーワードmodelを使えば、関数の振る舞いに関する制約を指定することができる。
fn bla(int a) -> int
model return == 2 * a
{
return a * a; //-- This would fail here
}
これらすべてを実現するためにZZでは、Cの構文にさまざまな制約を導入して、形式的証明(formal proving)により相応しいものにしている。例えば、ZZではeast-const("const"を右側に付ける)を採用し、関数ポインタは関数型を通じて使用可能である。
開発者兼メンテナのAvid Picciani氏に、ZZについて詳しく聞いた。
InfoQ: あなたのバックグラウンドと、現在のプロとしての業務について教えてください。
Picciani: バックグラウンドは大規模ハードウェアです。特にNokiaでは、Linux携帯電話のすべてに関わっていました。
現在はdevguard.ioの創業者です。当社は、データ主権(data sovereignty)を目的に、クラウドレスのIoT管理ツールを提供しています。
注目機能として開発者に支持されているのはcarrier shellです。これはネットワークの設定を一切行わずに、百万単位のデバイスに対するリモートシェルをオープン可能にするものです。ed25519というIDがたったひとつあれば、あらゆる物理ネットワーク上のすべてのデバイスと通信することができます。ピアツーピアの通信はもちろん暗号化されていて、データを見ることも保存することもできません。
Rustを搭載したデバイスを約25万台提供しましたが、もっと低いレベルの、Rustを搭載できない、あるいはしたくないような組込み機器へも拡張したいと考えています。
InfoQ: ZZはどのように生まれたのかを教えてください。
Picciani: 当社のプロダクトを極めて低レベルのハードウェア(ESP32やAVR 8bit)に提供するために、極限的なメモリ効率と移植性を備えたツールが必要でした。ですが、Rust言語からCに戻るということには、少なからず抵抗があったのです。当社では皆がRustを気に入っていますし、C言語は落とし穴が多すぎます。
一方で、有名でないチップ用のコンパイラや規制承認プロセスなど、私たちが必要としている商用ツールはたくさんあるのですが、どれもRustには対応していません。
ZZは、プログラミングをもっとよいものにするために、現在のコンピュータ科学には何ができるのか、6ヶ月にわたる研究の結果なのです。特にF*やZ3など、Microsoftの研究には影響を受けています。それをもっと、実践的な言語に移したに過ぎません。devguardではF*を、おもに暗号処理で使用しています。alloyにも触れておく必要があるでしょう。alloyは反例(counter-example)ベースのチェック、というアイデアにインスパイアされたものです。
InfoQ: ZZの最も大きなメリットは何で、どのようなシナリオの下で実現可能なのでしょうか？汎用言語と考えてもよいのでしょうか、あるいは、もっとニッチな言語なのですか？
Picciani: Rustには、(2度の変更可能な借用(mutable borrow)を許可しないという)プログラム安全にするための魔法の弾丸があるのですが、ZZはC言語上のレイヤ以外の何ものでもありません。必要ならば安全でない操作はいくらでもできます。安全性の形式的証明を自身で別に書き加えればよいだけです。プログラミングの方法がまったく違うのです。例えるならば、数学の先生とペアプログラミングを行って、コードの処理が失敗するような限界的なケースを絶えず突き付けられているようなものです。
形式的証明は極めて退屈で時間の掛かるものですから、その意味では、ZZは汎用プログラミング言語ではありません。WebサービスをZZで記述することはまったく可能ですし、実際私たちはそうしているのですが、NodeJSのような手軽さを身上とするようなものと競合するようなことは決してありません。状態マシン生成にalloyを直接統合するようになれば、状況は変わるかも知れません。そうなれば、セキュリティクリティカルなWebアプリケーションをZZで実装しようという考えも現れることでしょう。
InfoQ: 現時点での完成度については、どのように考えていますか？
Picciani: ZZはいろいろな面で非常に若い言語ですし、主要な2つのアイデア — Cのトランスパイラであること、記号的検証(symbolic verification) — についても、もっと詳細部分を具体化する必要があります。現時点で動作しているので、多くの人たちに実際の開発で試してもらうように勧めてはいますが、コンパイラの重大なバグや大幅な言語変更は覚悟しておかなくてはなりません。商用コードに関しては、Rustと併用して、慎重に使用することをお勧めしたいと思います。Cシステムコードとのインターフェースに関しては、ZZは特に優れています。
私の会社のdevguard.ioでは、クラウドを使わない自動車テレメトリ用の新プロダクトを4月頃に提供する予定です。このプロダクトはZephyr OSとNordic NRF91上に、ZZを中心として構築されていて、現在はそれに取り組んでいるところです。ZZを使用した最大のオープンソースコードは、おそらくdevguard carrierのZZブランチでしょう。それが完了すれば、ZZは製品開発レベルに達したと言えると思います。
ZZを使用するには、ブートストラップとしてRustをインストールした上で、ZZのコードをコンパイルするためにRustのパッケージマネージャであるCargoが使用する.tomlファイルを用意する必要がある。