spectre and meltdownまとめ

IntelのCPUの重大なバグが発覚した、のような騒ぎから話題になったspectreとmeltdownについて調べた。

基本的にはGoogle Project Zeroチームによるブログポストが最も信頼性の高くかつまとまっているので、この記事はそれのまとめ的なもの
https://googleprojectzero.blogspot.jp/2018/01/reading-privileged-memory-with-side.html

発端

おそらくここの記事でIntelのCPUにバグが発覚したと報じ他のメディアがこれを拡散。
ただ、情報がかなり曖昧で、本当にIntel固有なものなのか、従来から指摘されている攻撃の可能性(現実的には不可能だから対処する必要はない)のことではないかなど様々な憶測が飛び交い
最終的にはGoogleやIntelが声明を発表し、去年から発覚していた攻撃手法で近日発表する予定だったが情報がリークしてしまったので、前倒しで詳細を公表するとのことだった。

概要

spectreとmeltdownは3つの攻撃手法のことを指す。どれもCPUの性質を利用することによりカーネルによって保護されている領域に対してユーザースペースからアクセスしようというものである。

当初、Intel CPUのバグと言われていたが、CPUが誤動作するため保護が破れる、という類のものではない。
これらはキャッシュや分岐予測といった様々なCPUで広く用いられている高速化手法により発生するCPUのある種の癖を利用してメモリを読みだそうとするものである。
よって、Intel固有のものではなく、AMDやARMでも起こりうると明記されている。
しかし、影響を受ける可能性が高いのはIntelのCPUでProject Zeroのブログでも主にIntelアーキテクチャでの話を元に進められている。

攻撃の原理

spectreとmeltdownの原理について簡単にブログから要約する。spectreがvariant 1と2を指し、meltdownがvariant 3を指す。

Variant 1: 境界チェックバイパス

カーネル内の境界チェックをすり抜けて、アクセスが禁止されている領域の値を読みだす方法。
この方法はユーザーがカーネルに処理を依頼して、カーネル内で処理を実行するアプリケーションを利用した攻撃である。
今回のProof of Concept(PoC)ではeBPF(extended Berkeley Packet Filter)というユーザーによってパケットフィルターを定義するインターフェースを利用している。

この攻撃で肝になるのは投機的実行である。
これはif文などの条件分岐の結果が決定する前に、どちらの結果になるかを予想して処理を進めてしまうCPUの高速化手法である。
本来であればその予想が外れた場合、投機的実行による変更は巻き戻されそれが外部に漏れることはない。
しかし、この失敗した投機的実行内でメモリアクセスが行われていた場合、そのメモリの結果はキャッシュに残る。
キャッシュに残るだけではユーザーがその値の中身を読み取ることはできないが、キャッシュにデータが残っている場合、そのアドレスへのアクセス時間は短くなる。これを利用する。

具体的なコードのスニペットをProject Zeroのブログポストより引用する

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
struct array {
unsigned long length;
unsigned char data[];
};
struct array *arr1 = ...; /* small array */
struct array *arr2 = ...; /* array of size 0x400 */
/* >0x400 (OUT OF BOUNDS!) */
unsigned long untrusted_offset_from_caller = ...;
if (untrusted_offset_from_caller < arr1->length) {
unsigned char value = arr1->data[untrusted_offset_from_caller];
unsigned long index2 = ((value&1)*0x100)+0x200;
if (index2 < arr2->length) {
unsigned char value2 = arr2->data[index2];
}
}

untrusted_offset_from_callerというのが読まれたくないメモリ領域のアドレス。本来であればif文による境界チェックによって処理は実行されないはずだが、
arr1->lengthの値がキャッシュに載っていない場合、メモリロードによる待ちが発生しその間に投機的実行によってif文の中身が実行される。
untrusted_offset_from_callerの値がキャッシュに乗っていた場合、valueの値がすぐに読みこまれ投機的実行が進む。
index2の値はvalueの値によって0x200か0x300となり、このアドレスのメモリ領域のアドレスはユーザーがアクセスできる。
投機的実行によってこのメモリ領域もキャッシュに乗る。
最終的にこの投機的実行の結果は破棄されるのだが、0x200がキャッシュに乗っているか0x300がキャッシュに乗っているかでvalueの1bitが読み込めてしまう。
キャッシュ乗っているか否かは、メモリロードの時間によって分かってしまう。

Variant 2: 分岐ターゲットインジェクション

この攻撃では、KVM上でのゲストマシンから同じCPU上での他のゲストマシンのページアドレスやKVMのモジュールがどこにロードされているかを特定するものである。
当然、アドレスが分かっただけではMMUによって保護されているはずなのでそのまま中身を知ることはできない。が、PoCではeBPFを使うことによってデータを取り出している
(ここの詳細は理解できなかった。ROPの要領でコードを実行させて、Variant 1と同じ方法でキャッシュからデータを引き出す?)。

この攻撃ではindirection branch(分岐先のアドレスがメモリ上にあるような分岐)の分岐予測を利用する。indirection branchの分岐先がキャッシュされていない場合、そのロードの時間がかかる。
そのため、投機的実行のためにどのアドレスに分岐するか、その命令アドレスに対してどこに分岐したかの履歴をもとに予測する機構がついている。
この機構の詳細は公開されていない。そのため、この機構のリバースエンジニアリングから説明されている。
そのリバースエンジニアリングの結果を元に、予め分岐予測機構の状態を設定し、hyper callなどの実行時間の差から分岐予測が失敗したかどうかを知ることでアドレスを知る、というのが概要である。

正直、ここの説明は自分では理解できない点も多かった。

Variant 3: Rogue data cache load

(1/13 補足)cyber.wtfのブログ内容についても言及を加え、ARMプロセッサの例についても補足

ユーザースペースからカーネル空間のメモリを直接読む攻撃。これがMeltdownと呼ばれるもので、今回の騒動で最も広い範囲に影響が出ると考えられているようだ。

詳細はこちらのブログ参照
https://cyber.wtf/2017/07/28/negative-result-reading-kernel-memory-from-user-mode/

基本的なアイデアとしては、メモリの権限設定のチェックが完了する前にプロセッサはメモリの読み込みを投機に実行していて、Variant 1と同じ要領でメモリの値が読めるというもののようだ。
コードのスニペットを上記ブログより引用する

1
2
3
Mov rax, [somekerneladdress]
And rax, 1
Mov rbx,[rax+Someusermodeaddress]

カーネル空間からのメモリ呼び出しの直後にその値に依存するユーザー空間アドレスへの読み込みを行い、その後、どこがキャッシュされているかでそのカーネル空間のメモリの値を確定させようというものである。
ページテーブルによる例外が発生する前に、後ろの2つの命令が投機的実行されると可能になってしまうというわけである。
ここで後ろ2つの命令が投機的実行されてしまうとVariant 1と同じように、どのアドレスがキャッシュされているかによってユーザー空間からカーネル空間のメモリの値が読める。

しかし、cyber.wtfではこのような不正なアクセスをした場合は投機的実行中raxの値が常に0になるような挙動をしたので結果的には失敗した、としている。
Googleのチームは、cyber.wtfチームがやっていたカーネル空間をキャッシュするために呼び出していたprefetch命令を使うのを辞めたところうまくいった、としている。

また、ARMプロセッサの場合、この攻撃の亜種としてカーネルモードでしか読めないシステムレジスタを読み出せてしまうことがある。
ARM社のwhite paperよりコードを引用する。

1
2
3
4
5
6
7
8
LDR R1, [R2] ; arranged to miss in the cache
CMP R1, #0
BEQ over ; This will be taken
MRC p15, 0, R3, c2, c0, 0 ; read of TTBR0
LSL R3, R3, #imm
AND R3, R3, #0xFC0
LDR R5, [R6,R3] ; R6 is an PL0 base address
over

4行目のコードがTTBR0というページテーブルに関する情報が格納されているシステムレジスタをR3レジスタに格納して、
その結果を使ってユーザー空間のアドレスを決定してロードする、ということをしている(PL0とはARMでのユーザーモードを意味する)。
3行目が分岐命令で、本来ならばoverまで飛ぶのだが、分岐予測が失敗すると4行目以降が投機的に実行され、
最終的にVariant 1と同じようにどのユーザーアドレスがキャッシュされているかでシステムレジスタの値が読めてしまう。

まとめ

とりあえずProject Zeroのブログポストのうち、攻撃原理に関わるところを中心にまとめてみた。
Intelプロセッサのアーキテクチャやセキュリティ分野にそこまで詳しいわけではないので、誤りも多々含まれるかもしれないが、見つけたらご指摘お願いします。

ARMなどからも発表があるのでそちらの方も読み込んだらまた補足をしていきたいと思う。

RustでOSを書くプロジェクトもろもろ

巷でよく聞くRustでOSないしベアメタルプログラミングの試みの備忘録。
Rustにはとても興味があってかつ大学での研究分野が低レイヤー系だったので面白そう思ったのだが、
いざやろうとしてみるといろいろなハードルがあるようで、ベストプラクティスも確立していないっぽい。
ので、とりあえず適当に漁った資料をまとめてみる

C以外でのベアメタルプログラミング

oruminさんのKernel/VM勉強会での発表のSpeaker Deck。自前のbinutilsとxargoを使ってベアメタルプログラミングしている

RustでOSを書いてみる(環境構築編) - Qiita
Introduction Rust for Creating Your Operating System - Qiita

実際にOSを書いた(書いている)人の環境設定について。両方共OS自作本をベースとしているっぽい。

GitHub - redox-os/redox: Redox: A Rust Operating System

Rustによる本格的なOS。GUIが動作している。POSIX準拠とかではなく全く新しいOSをつくろうとしているらしい。
独自のツールチェーンを用意する関係、ビルドはDockerによる方法が一番安定すると思う(ビルド周りのドキュメントはいい加減だったりする)。

rumprun-packages/rust at master · rumpkernel/rumprun-packages · GitHub

Rump Kernelを使ってRustでhello worldしている。しばらくメンテナンスされていないが、一応動くっぽい

Writing an OS in Rust

RustでOSを書いたというブログ(英語)

The Case for Writing a Kernel in Rust

今年のAPSysでの論文。RustでOSを書くときの所有権周りのデザインについて論じている。この論文ではOSそのもののパフォーマンスとかの評価はない。

Multiprogramming a 64 kB Computer Safely and Efficiently

上の論文の著者がSOSPに出した論文。この論文ではRustがどうのとかよりも単純にOSとしてのデザインについて論じているっぽい(まだちゃんと読んでない)

Tock Embedded Operating System

上2つのの論文の実際のプロダクト。OSSになっている。

System76でGalago Proを購入

使っていたノートパソコンが全く起動しないレベルで壊れたので新しいものを購入することにした。
趣味の開発で使うのが主な用途となるのだが、スペックの条件としては

  • メジャーなLinuxディストリビューションが動きそう
  • ディスク容量500GB以上(256GBだとすぐかつかつになったので)
  • そこそこ強いCPUとそこそこ大きいメモリ
  • 持ち運びを考えて重量は1.5kg以下

はじめはLet’s Noteなども検討したが、20万円を超える額が必至だったので断念。
それで友人に勧められたのがSystem76のGalago Pro

デフォルトOSとしてUbuntuが入っており、ディスク容量やCPUスペックなどもカスタマイズ可能。
なんでも10年くらいLinuxの乗るPCを販売している会社らしく、デバイスの不具合もちゃんとパッチを投げて対応しているらしい。
値段も海外の会社ゆえ送料が結構かかるのだが、それ込みでも20万円切る価格で買えた。
自分が注文した時期が良かったのか、注文から届くまで2週間かからなかった。

その他良い点としては

  • Ubuntuのバージョンとして16.04と17.04を選択できた
  • 画面の解像度がデフォルトでは細かすぎて字が小さいのだが、設定でいい感じになおせた

注意点・不満点としては

  • ACアダプタがアメリカ仕様のため変換アダプタが必要(変圧は必要なし)
  • キーボードは英字キーボードのみ(最近、英字キーボードを使う場面が増えていたのでそこまで問題ではなかった)
  • 購入の手続きでクレジットカードの利用明細に記されたコードを送信するのがちょっと面倒
    • 不正利用防止のためとして、利用明細に記されたコードを送るのだが、購入の情報がウェブの利用明細に反映されるまで3日ほどかかった
  • バッテリー持ちはそんなによくない。多分4時間位
  • Xenを入れたら起動しなくなった

あとは耐久性が気になる。以前使っていたのが1年位使って一度SSDが死んでメーカー修理に出して、その1年後今度は初期の起動エントリーすら出ないレベルで死ぬということになったので、そういうことにならないといいな。

ARM向け自作ハイパーバイザーT-Visorを公開しました

修士の研究としてつくったARM用ハイパーバイザ「T-Visor」を公開しました。
https://github.com/garasubo/T-Visor

(2016/05/24 ちょっと加筆しました)

背景

組み込みの世界でもLinuxのような汎用システム向けOSが使われるようになる一方、
リアルタイム性の保障やセキュリティ等の観点からリアルタイムOSの需要も高い。
そこで、ハイパーバイザを使って汎用OSとリアルタイムOSを同時に動かす、というような研究や製品が結構あります。
具体例を上げれば、ロボットの姿勢制御などをリアルタイムOSできっちりとやる一方、
画像処理やネットワーク機能とかを使ってクールな機能だけど最悪バグっても安全には支障がないといったものをLinux側で、といった感じです。
実際にARMの一部シリーズではIntel VT-xのような仮想化支援のハードウェア機構が備わっていて、
KVMやXenはこれらに対応してARM上でも動くようになっています。

しかし、XenやKVMはLinuxをベースにしていてシステム全体が重い、リアルタイムでないなどの問題点があります。
Linuxなどのスケジューラは短い一定周期ごとに確実にこれこれをしなければいけない、といったような要請(ハードリアルタイム)を満たしにくいことが知られています。
リアルタイム性や組み込み用途というものを重視しようということで開発したのがT-Visorです。
このT-Visorは動作にLinuxやその他標準ライブラリを要さず、Cortex-A7/A15での動作が可能です。
方式としてはハードウェア上で直接動くType-1型で、仮想マシン上で動くOSをに対して変更がいらない完全仮想化をおこなっています。

ざっくりとした技術的な説明

このT-VisorはARMv7-Aの拡張のひとつであるVirtualization Extensionsを利用することで、
完全仮想化Type-1型のハイパーバイザを実現しています。
この拡張でHypモードというプロセッサモードが追加され、プロセッサ全体に影響を与えるような命令に対してトラップをかけてこのHypモードにさせる、ということが可能です。

メモリアクセスですが、通常のMMUに加えてStage-2のMMUというものがあり、これは仮想マシン上での物理アドレスを中間物理アドレスとして受け取り、
実物理アドレスに変換させたうえでメモリアクセスをさせると言うものです。
これにより、仮想マシンは自由にMMUを使うことができる一方、ハイパーバイザ側でアクセスできるメモリ領域を制限することができます。

仮想デバイスドライバは基本的には実装していません。ARMのIOはすべてMMIOなので、アクセスできるメモリ領域を制限することで、
仮想マシンから触れるデバイスは制限されています。
また、外部からの割り込みも一度ハイパーバイザにトラップされるので、割り込みについてもどの仮想マシンが受け取るかを制御できます。

割り込みに関してはGICという割り込みコントローラで管理されています。
ゲストOSもこのGICを使って割り込みをコントロールするので、競合が起きないよう対応が必要です。
このGICはある程度の部分が仮想化対応されているのですが、ある程度の部分に関してはなされていないので、
先述のStage-2 MMUを使うことで、アクセスをコントロールすることで仮想割り込みコントローラを実装して対応します。

リアルタイム性を保障するためスケジューリング方式が重要になってきますが、ユーザーが設定しやすいようにということを意識してフレームワークが設計されています。
具体的には実装すべき関数をいくつか定め、その中ではあくまでスケジューリングに関することのみを行い、
仮想マシン内部などには干渉する必要がないようにされています。
サンプルとして固定優先度式とEDF方式のスケジューラが実装されていますが、設定により静的にひとつのスケジューラのみが組み込まれるようになっています。

仮想マシンの数やそのメモリ割当等の設定はコンパイル時に決定されます。
現状はソースコードにベタ書きしていく感じになっているので、まともなconfigureについてはfuture workのひとつです。

起動に関してですが、ブートローダはU-Bootを使って動作させていました。
ただし、U-Boot固有の機能に何か依存していたわけではなく、メモリ上に外部からハイパーバイザとゲストOSが展開できるようなものならなんでもよいです。

動作確認として無修正のLinuxを動かし、各種ベンチマークの動作を確認しました。
また、複数のリアルタイムOSを動かして、OS間通信ができることも確認しています。
Xen4.4とも比較実験をおこなっていて、詳細は省きますが、基本的にポジティブな結果が出ました。
ただし、Xen4.5で割り込みに関して性能改善がなされたらしく、そちらとはまだ比べられていません。

主要なソースコードの中身

ソースコード読みたい人向けに簡単に説明しておきます。

  • vcpu.c
    • 仮想CPUの状態管理を行う
  • hyp_call.c
    • 仮想マシンからのhyp例外を管理する
  • virtual_gic.c
    • 割り込みコントローラについての仮想化を担っている
  • schedulers/
    • 各種スケジューラの実装
  • users/
    • この以下のディレクトリのうちひとつを選択することで、ハイパーバイザ上でどのようなアプリケーションを使うかを決定する
  • boards/
    • ハードウェア依存部分を置くところ。

課題と今後やりたいこと

まず第一に、複数OSは動かせることは確認しているものの、ひとつのVMに対して仮想CPUを複数提供することには失敗しています。
また、このハイパーバイザはコアをひとつしか使うことができません。
前者に対してはPSCIというコアを管理するためのインターフェースがARM側では定義されているので、
それに乗っ取り、仮想CPUを操作するインターフェースを実装済みではあるのですが、いざLinuxを動かしてみると起動途中で止まってしまいます。
どうも2つのコアとも処理できるスレッドがなくなってスリープしているようなのですが、はっきりとした原因がわかっていません。
原因として考えられるのは

  • 割り込みコントローラの仮想化部分がバグっていてハードウェアからの信号待ちのようになってしまって動かなくなっている
  • コア間の状態保存・復帰がバグっている
  • キャッシュ・TLBなどが適切にcleanできていない
    などなのですが、未だにはっきりとつかめていません。

また、仮想マシンの管理のconfigがよくない感じなのは前述のとおりなのですが、それ以外にもコードの構造がひどいことは重々承知していて、
そこをまず叩き直さなければならないという話もあります。
そもそも一人で書いているはずなのに気分でコード規約が変わって名前の付け方が色々おかしいとか、もしかしたらインデントも統一されていない部分もあるかも…
あとは今のところ全部C言語とアセンブラで書かれているのですが、C++で書くともっとすっきりするかもしれませんね。

OSや組み込み開発に対してほとんど知識がない状態ではじめたため、かなり拙い部分もありますが、まあなんとか動作することができたのはよかったかなっと

補足

現在、動作確認はCubieboard 2で行っています。
Raspberry Pi2だと割り込みコントローラの関係上、動かすのに大変な労力が必要となります。

あと、課題とかいろいろ書きましたが、現在は基本的に開発止まっています。
私の能力では解決が難しいというのがひとつ、つくったとしてもそれを使ったアプリケーションをつくる機会がないといったモチベーションの問題がひとつです。
ただ、興味ある人がいれば連絡くれると幸いです。ある程度協力できると思います。

ちなみにこのタイミングで公開したのは、ソースコードを多少はマシにしたかったというのもそうなのですが、
これについて書いた論文がリジェクトされたからです。
評価が甘かったりアプリケーションが見えにくかったというのが主な原因なのだろうか、アカデミアの道は厳しいですね。
この手の分野はクローズドソースなものが多すぎたり、ハードウェア依存な部分が多かったりで、実装までこぎつけても評価が…ってなるのは悲しい

論文紹介ー"Jitsu: Just-In-Time Summoning of Unikernels"

システム系論文紹介 Advent Calendar 2015の12日目の記事です。

論文概要

Jitsuという、Unikernelを使う組込みプロセッサでWebサービスを提供するためのツールをつくりましたというお話。
著者はMirageOSを開発でお馴染みの方々が並んでいますね。
会議は今年のNSDIで、USENIX系の会議なので論文も著者のスライドも無料で手に入るので、
こんなブログを読まずともそちらを読んでしまえば全て完了するのではという気がしますが…

予備知識

最近ちょくちょく話題になりこの論文のキーともなるUnikernelについて簡単に説明しておこうと思います。

Unikernelとは、動かすプロセスを1つに限定することで様々なOSの抽象化を簡略化してライブラリのようにすることで、
アプリケーション単体でプロセッサで動くイメージとしたもの、といったとこでしょうか。
代表的なのはMirageOSとかOSvとかですね。
Unikernelの詳しい説明については、
Unikernels: Library Operating Systems for the Cloud
がよいでしょう。
英語版Wikipediaにも記事があります。
Unikernel - Wikipedia, the free encyclopedia
もう少し体系的でざっくりとした話だと、このスライドとかわかりやすいかもしれません。
An Introduction to Drawbridge(ja) // Speaker Deck

今回使うUnikernelはMirageOSなのですが、これはOCamlで書かれており、
OCamlにはARM用のコンパイラがあること、MirageOSが動作する環境であるXenがARM向けに対応していることなどが幸いしてか、
一部のARMボード上(CubieBoard2など)で動作するようです。
私も試してみようとCubieBoard2を購入したのですが、コンパイルでこけてしまいましたが。

論文の中身

研究背景

クラウド環境からサービスを提供することが流行っているが、クラウド環境への通信のオーバーヘッドが厄介。
また、IoTのデバイスはセキュリティの脆弱性が問題になる。
そこで、組込みハードウェア上でXenなどのハイパーバイザを動かしサービスを提供できれば、
ユーザーに近い位置でのサービス提供が可能となるため通信のレイテンシが緩和される。
また、ハイパーバイザを使うことで各サービスを独立で動かせる。

実現したこと

組込みデバイスで動くネットワークアプリケーションをセキュアに管理するためのツールを、Xenのツールスタックとして実装した。
VMとしてUnikernelを使うことでより低いlatencyでネットワークリクエストに応答する。

実装

XenのツールスタックをXenStoreを拡張し実装。
目標としては、サービスがネットワークに対してきちんと応答するようにするが、必要のないときはリソースがもったいないのでサービスを停止させましょうというもの。
そのために

  • Unikernelのブート時間の最適化
  • VM間コミュニケーションプロトコル”Conduits”の実装
  • 外部クライアントからのアクセスに対して、起動時間のレイテンシを隠蔽するためのディレクトリサービス”Synjitsu”の実装
    を行っている。
    Xen上でVMの設定値を管理・保存するためのツールスタック
    XenStoreを拡張することによって行なわれる。

ブート時間最適化

起動時の仮想デバイスの割りあてを並列処理したことと、
OCamlによるXenStoreトランザクションを利用することで高速化。
また、Unikernelを用いるたので、そもそものバイナリサイズが小さいためそれも高速化に寄与している。

Conduits

vchanという共有メモリを用いたデータパスを利用し、OCamlでvchanのプロトコルを実装。
ランデブーのためのインターフェースがvchanにはないので、XenStoreの名前空間を拡張してランデブーインターフェースを提供。

Directory Service

DNSのリクエストをどのUnikernelに割り当てるかをマップしているもの。
DNSのリクエストによりUnikernelが起動し、その後外部クライアントからTCPのリクエストが送られてくるのだが、
起動が完了していないとリクエストに応答できない。
そこで、起動前の場合、ひとまずリクエストをXenStoreに保存しておき、Unikernelとの間に割り込んでいるSynJitsuがTCPのACKを返しておく。
その後、Unikernelが起動すると溜まったリクエストへの応答を開始し、Synjitsuを介さずにクライアントとUnikernelが直接やり取りを開始する。
このようなことをしないと起動前のTCPパケットがタイムアウトして再送までの時間がかかってしまうため、
サービスのレスポンスが下がってしまう。
わかりやすい図が論文にあるので、そちらを参照されたい。

評価

いろいろなパフォーマンスを計測するための実験を行っているが、
そもそもARMボード上でこのようなことをやるというのがなく、
比較ができていないといった印象を受けた。
セキュリティに関しては、CVEのリストにある脆弱性のうち、どれがJitsuでは影響があるか調べている。
Unikernelを用いているため、
基本的にはLinuxのデバイスドライバ部分やカーネルそのものバグとXenに関するものしか受けず、
SSH overflowのようなアプリケーションよりのものは影響を受けない。

関連研究・議論

コンテナ型仮想化であるDockerやDrawbridgeなどが紹介されている。
UnikernelがよりOSの各種抽象化を省略しアプリケーション特化の構成になっている。

この研究はXenのABIを変えたりなどはしていないため、他のツールと併用することも可能。
ConduitsもMirageOSに特化したものではないため、プロトコルを実装すれば他のunikernelでも利用可能。

まとめ・私見・愚痴

Unikernelを使うことでARMボード上でWebサービスを素早く提供できるJitsuというXenのツールスタックを実装した、というものでした。
全体的に雑な説明になってしまいましたが、まあ、細かい話は論文を直接読んだほうがいろいろ手っ取り早くわかるでしょう。

最近ではDockerでUnikernelを動かすとかよくわからない話も上がってきたりして、
段々と注目度が上がっているようなので、このようなUnikernelを活用したシステムがこれからもいろいろと出てくるのでしょうか。

12日目といってもまだ2人目ですね。
システム系やっている人ってやっぱり少ないなあと思うし、
成果を出すのに時間がかかることが多かったりするせいか評価されることも少ないし、
いろいろとつらいなあと思う今日このごろ。

LaVie Z750にWindows 8.1+Arch Linuxのデュアルブート環境構築

今使っているLet’s noteがパーティション分けミスってLinuxの容量がかつかつになってしまったっていのと、ハードウェア的にポツポツと不具合が出てきていたので、新しいパソコンを買った。
LaVie Z750を選んだのは軽いのと、SSD 256GBにOffice付きのわりに安かったから。

今までUbuntuに甘えてきたが、思い切ってArch Linuxにすることにした。
Gentooも考えたが以前挫折したこと、資料がArchのほうが充実している感じだったことを考慮してArchを選んだ。
Archのバージョンは2015.01.01のを使った(以前ダウンロードしていたので)。

基本的には公式wikiのBeginner’s guideに従うだけ。
英語と日本語があるが、英語のほうがinstallまでの説明が詳しい一方、日本語はinstall後の作業の説明がついている。
Beginners’ guide - ArchWiki.html
Beginners’ Guide (日本語) - ArchWiki

躓いたのはまずパーティション分け。
今回取った方法は

  1. Windowsのコントロールパネルから「管理ツール」→「ハードディスク パーティションの作成とフォーマット」でWindowsパーティションを縮小
  2. Archのブートメディアからgdiskで空領域にパーティションを作って、mkfs.ext4で初期化
    というもの。

あとはインストール中の/bootにどこをマウントするか。
/dev/sda2をマウントすればいいのだが、はじめはこれをスキップしてしまい、後々面倒なことになった。

日本語環境化はここが参考になった。
Arch Linuxに日本語環境を構築する

Xenで使っているディスクイメージの容量拡張

Ubuntu 14.04にXenを入れてその上でArch Linux(2015-01版)を動かしている。
ディスク容量が足りなくなったので増やそうと思ったのだが、virt-managerあたりからはいけそうな雰囲気がなかったので、
適当に調べた方法を試したら上手くいった。

念の為、ディスクイメージのバックアップをとっておくことを推薦

  1. Ubuntu上でディスクイメージの後ろにほしい長さ分だけ追加
    ディスクイメージは/var/lib/libvirt/imagesの中とかにある。

    1
    dd if=/dev/zero bs=512M count=20 >> arch.img
  2. ゲストOS上でパーティションを再構築fdiskとかで一番後ろのパーティションを一度dで破壊して、nでもう1回つくるとき後ろまで最大限まで伸ばす。
    その後wで保存。自分の場合、マウントされているパーティションを伸ばしているので、認識させるには一度再起動する必要がある。

  3. 再起動後、resize2fsでパーティションを拡張、df -hでパーティションが拡張されていることを確認。

参考:Xenで使用しているディスクイメージを拡張する | misty-magic.h

あなたとHexo

Octopressの動作が最近よくわからないけど不安定なのと、
どこかでHexoいいよという話を聞いたので、このブログのHexo移転を考えている。

Hexo

所要時間3分!? Github PagesとHEXOで爆速ブログ構築してみよう! | 株式会社LIG

Octopress vs Hexo

Octopressからの移行は楽で、記事のmarkdownファイルを移動してきて、configをいじってあげればよい。

Migration | Hexo

それで新しくつくったブログがこちら。
もうちょっとしたらこちらに移す。

新しいブログ

論文紹介ー"User-guided device driver synthesis"

システム系論文紹介 Advent Calendar 2014の7日目の記事です。

論文概要

デバイスドライバをユーザーが指示を出しつつ半自動でデバイスドライバを合成するツールTermiteというものを提案しています。
この著者はこのTermiteというツールをAutomatic Device Driver Synthesis with Termiteという論文で
その2つのやり取りをオートマトンとしてみて、その上で行なわれるゲームの必勝法としてデバイスドライバの合成をしてやろうというものです。

当初は完全自動だったのですが、現代の科学では完全自動だと厳しいものがあると悟った著者らがユーザーの入力補助をうまく取り入れるという
方針に変えてこのような形になったようです。
この論文は今までやってきたことのまとめ、という形になっているようです。

Specificationの書き方

このTermiteへの入力として必要なのはdriver, device, OSそれぞれのmodelのspecificationです。
これはTermite Specification Language(TSL)によって与えられます。

TSLの具体例は論文にあります。

Device model

デバイスの動作についてのモデルです。
デバイスがどのように動くかは
デバイスのデザイナーが持っているはずのtransaction-level models(TLM)から簡単にわかります。
ただし、ベンダーが非公開にしている場合も多く、TLM to TSLのコンパイラも開発中とのこと。

デバイスモデルを仕様書から書き起こす方法についてはSOSPの論文の方に詳しく議論されていましたが、この論文ではされていませんでした。

OS model

OSがドライバに向けて発行するAPIを構築するためのモデルです。
イーサーネットならパケットを送るとか受け取るとかそんな感じです。

DeviceとOSモデルをつなげる

このデバイスとOSの定義の関係する状態を結びつける必要があるのですが、
この2つの定義をできるだけ独立に保ちたいという要請もあります。

そこで、virtual interfaceというものを導入しています。
これはデバイスモデルの重要なイベントをOSに通知するコールバックみたいなものです。
これは実際に合成されるデバイスドライバの動作というわけではなく、
これで定義を与えてやろうというものです。

また、ドライバの動きを制限するassertや、ドライバがどこに向かっていくのかを定義するgoalというものも定めることができます。

ドライバテンプレート

OSが実際に呼び出す関数を定めるテンプレートです。

User-guided code generation

コードの合成はIDEで編集するという感じでおこなわれます。
このIDEの機能としてgeneratorとverifierがあります。
generatorが自動補完のように現在の入力位置にモデルから合成したコードを埋め込むことができます。
もちろん、合成したコードに対しての変更も可能です。
verifierが書かれたコードが定義に合っているかどうかをチェックします。

Synthesis

モデル間の合成なのですが、これはデバイス・OSとドライバ間でおこなわれるゲームと見立てることでおこなわれます。
ゲームの状態を有限オートマトンとして、状態遷移はコントロール可能なものとドライバやOSが勝手に行うコントロール不可能なものの2つです。
このゲームに勝つ戦略、すなわちなってはならない状態に陥らないように行動するのがドライバで、これを合成するというわけです。
このゲームに勝つ戦略がそもそも存在しない場合、合成は失敗となります。

この合成は下手に行うと状態数爆発を起こしたりと厄介なのですが、
それを起こさないため、筆者は様々な工夫をしています。

詳しいことを書いているとキリが無いので、ここでは省略します。
また、この論文より他の関連する論文のほうが詳しく書かれているようです。
(私は読んでいません)

Debugging with counterexamples

このゲームベースの合成に失敗した時のデバッグ支援方法もTermiteは備えています。
ゲームに勝つ戦略を妨げている環境の振る舞い、counterexample strategiesを探します。
これはこのゲームの双対ゲームを解くことで得られます。
このcounterexample strategyをステップ実行することで、デバッグを支援します。

Limitations of Termite

  • DMAを扱えない
    • 状態数が爆発する
  • デバイスコントロールとは本質的に関係ないところは他の手法を使うことで簡単に合成できるが、現在のところでは手動で埋め込むしかない
  • 並列処理への対応ができない
  • リアルタイム性の保障はできないので、ハードリアルタイムなドライバはつくれない

Implementation and evaluation

このTermite、Haskellのコードおよそ3万行で10人年かかっているとのこと。
USBのwebカメラ、UARTのシリアルコントローラなどを実際に実装して評価しています。
各デバイスドライバに実装するのに1週間ほど(ドキュメントを読んでデバイスの仕様を調べる時間も含まれている)とのこと。

合成アルゴリズムも、提案している手法と従来手法を比べ、従来手法だと2時間以内に終わらなかったものが、1分〜10分ほどで終わっていることが示されています。
verificationはまだ最適化されていないため、合成より時間はかかっていますが、それでも最大でも13分ほどしかかかっていません。

実際に出来上がるドライバはどうしても手動での最適化や変更が必要なのですが、60%〜90%は自動で合成できたようです。

また、できあがったコードサイズなのですが、これも全体的に小さくなっています。
これは、このドライバがデバイス動かすロジックに集中していること、
普通のデバイスドライバはコードの再利用などを考えて冗長になっていることなどが挙げられるようです。

この方法では定義の再利用が可能というのが1つの売りなのですが、これについてもOSを変えたることで試しています。
これも定義をほとんど変えることなく再利用できたとしています。

パフォーマンスもほぼ同等とのことです。

まとめと私見

Termiteというデバイスドライバ合成ツールについての論文でした。
形式的手法を用いて定義からドライバを合成し、さらにそのデバッグについても形式的手法を用いて支援しているというのはおもしろいと思い、今回この論文を紹介しました。
私自身、デバイスドライバを書いたことは一切なく、専門分野でもなく少々準備が甘くなりつたない文章となってしまいましたが、
ご指摘・マサカリ等ありましたら、コメントお願いします。

UbuntuにインストールされたVMware Playerをアンインストール

タイトルの通り。aptで入れたわけでないのでどうするのかなあと思ったら、
vmware-uninstallってコマンドあったから打ってみたところ、

The vmware-uninstall* scripts have been deprecated.  Instead, please use
the vmware-installer.

Long form:
  vmware-installer --uninstall-product PRODUCT
Short form:
  vmware-installer -u PRODUCT

とのこと。

なのでおとなしく、vmware-installer --uninstall-product vmware-playerと入れたら消えたみたい。