カーネル空間ですべてのプロセスを動かすには -TAL, SFI, Wasmとか -

2019/7/20 カーネル/VM探検隊15回の @nullpo_head (https://twitter.com/nullpo_head) の発表資料です。

高レベル言語ランタイム、型付きアセンブリ、Software Fault Isolationなどの手法を紹介しつつ、任意のプログラムを安全にカーネル空間で動かそうという野望に答えるクールな挑戦達を紹介します。

Transcript

1. カーネル空間で すべてのプロセスを動かすには -TAL, SFI, Wasmとか- Kernel / VM 探検隊 15回 7/19 Nullpo_head 1
2. Nullpo_head (Takaya Saeki) 低レイヤ方面 • Noah,VMMによるシステムコー ル変換を使ってLinuxバイナリを macOSで動かすやつ • Xv6を自作OSに移植したやつ • Xv6をMIPSに移植したやつ 仕事 • Web屋さん 2
3. 最近のトレンド 3
4. Today’s trend DPDK SPDK 4
5. USER SPACE KERNEL SPACE App Context Switch Overhead! 5
6. DPDK Solution; カーネルを バイパスする 6 USER SPACE !!
7. 待てよ・・・ 全てカーネル 空間で動かす 方がむしろ速いの では？？ 7
8. USER SPACE KERNEL SPACE App Context Switch Overhead! 8
9. USER SPACE KERNEL SPACE App 9
10. USER SPACE KERNEL SPACE App 10 単一メモリ空間
11. USER SPACE KERNEL SPACE 虚無 終 11 App ただの関数呼び出し 速い！ 単一メモリ空間
12. そもそもなぜ特権レベルによる 分離が必要だったか？ プロセス達やカーネルを隔離するため • 互いのメモリ空間の読み書きを分離 • 特権命令の拒否 => Hardware Isolation 12
13. KERNEL SPACE ✘特権命令の発行 ✘メモリ読み放題 13 単一メモリ空間 App App
14. KERNEL SPACE Software App Isolation Needed!! ✘特権命令の発行 ✘メモリ読み放題 14 App App 単一メモリ空間
15. 本題 プロセスをカーネル空間で動か すCOOLなプロダクト達のご紹介 15
16. 達成すべきIsolation 1. 特権命令の排除 2. メモリ空間の分離 i.e.割り当てられたメモリ範囲のみでの 1. R/W 2. Execute これでコンテキストスイッチとサヨナラ！ 16
17. Cool Isolation Techniques Overview 1. 高レベル言語ランタイムによるisolation • Java, Ruby, … 2. 型の力によるisolation • Kernel Mode Linux • Singularity, Verve 3. SFIによるisolation • SFIとは • NaCl • Nebulet / Wasmer 17
18. Cool Isolation Techniques Overview 1. 高レベル言語ランタイムによるisolation👈 • Java, Ruby, … 2. 型の力によるisolation • Kernel Mode Linux • Singularity 3. SFIによるisolation • SFIとは • NaCl • Nebulet / Wasmer 18
19. 1. 高レベル言語によるisolation 19
20. アイデア • 「そもそもJavaみたいなメモリ安 全な言語にユーザープログラムを限定す ればそれで良いっしょ？」 • めっちゃわかりやすい発想。 • JavaOSとか 20
21. 達成すべきIsolation 1. 特権命令の排除 => CPU命令なんて発行する手段がない 2. メモリ空間の分離 i.e.割り当てられたメモリ範囲のみでの 1. R/W 2. Execute => そもそもポインタがない 21
23. 高レベル言語によるisolation • CooL • 動く • 惜しい点 • 言語依存性 • 言語ランタイムの安全性 • ロマン 23
24. Cool Isolation Techniques Overview 1. 高レベル言語ランタイムによるisolation • Java, Ruby, … 2. 型の力によるisolation • Kernel Mode Linux • Singularity, Verve 3. SFIによるisolation • SFIとは • NaCl • Nebulet / Wasmer 24
25. Cool Isolation Techniques Overview 1. 高レベル言語ランタイムによるisolation • Java, Ruby, … 2. 型の力によるisolation • Kernel Mode Linux👈 • Singularity, Verve 3. SFIによるisolation • SFIとは • NaCl • Nebulet / Wasmer 25
26. Kernel Mode Linux Toshiyuki Maezawa et al. – The University of Tokyo Maeda Toshiyuki. Kernel mode linux: Toward an operating system protected by a type theory. In Advances in Computing Science – ASIAN 2003. Programming Languages and Distributed Computation Programming Languages and Distributed Computation. Springer Berlin Heidelberg, 2003. 26
27. Overview – Kernel Mode Linux By 前田 俊行先生 (当時 東大旧米澤研) • 型検査をパスしたプログラムがisolation を満たす安全性があることを証明できる 「型付きアセンブリ(TAL)」を利用 • カーネルがTALをロード時に型検査、コ ンパイルしてカーネル空間で動かす 27
28. 達成すべきIsolation – Kernel Mode Linux • 特権命令の排除 • TALからその手のInstructionを排除する • メモリ空間の分離 • 型がついたTALは不正なメモリR/W/Eを行わ ないことが保証できる 28
29. システム 1. コンパイラ Popcorn • Cライク(実際はMLライク)な型安全な言語 • 型付けされたTALx86を吐く 2. TALx86アセンブラ • アセンブル 3. 型検査器 • 型検査を行い安全性を検証 4. カーネル空間でプロセスを起動 29
30. パフォーマンス 30
31. Kernel Mode Linux • CooL • 静的型付きアセンブリの利用 • 実際のアセンブリのサブセット • 惜しい点 • 現状TALx86へコンパイルする言語が 結局のところそもそも型安全言語 • C, C++… 31
32. Cool Isolation Techniques Overview 1. 高レベル言語ランタイムによるisolation • Java, Ruby, … 2. 型の力によるisolation • Kernel Mode Linux • Singularity, Verve 3. SFIによるisolation • SFIとは • NaCl • Nebulet / Wasmer 32
33. Cool Isolation Techniques Overview 1. 高レベル言語ランタイムによるisolation • Java, Ruby, … 2. 型の力によるisolation • Kernel Mode Linux • Singularity, Verve 3. SFIによるisolation • SFIとは • NaCl • Nebulet / Wasmer 33
34. Singularity, Verve Microsoft Research Galen C. Hunt and James R. Larus. Singularity: rethinking the software stack. SIGOPS Operating Systems Review, 41(2):37–49, 2007. Jean Yang and Chris Hawblitzel. Safe to the last instruction: automated verification of a type-safe operating system. In Proc. PLDI, 2010. 34
35. Singularity Overview By MSR • MSの色々野心的な研究用OS • Software Isolated Process + Microkernel • ほぼすべての実装がC#製でType safe • Type safeなMSILアセンブリを実行する 35
36. Microkernel + SIP • IPCコストが ネック => SIPならOK! 36
37. Verve Singularityの進化 • TALアセンブリを実行する！ • BartokコンパイラがMSILではなくTALを 吐くようになった • BootLoader以外の全コンポーネントが Boogieによってメモリ安全性が証明済み • 純粋に強い 37
38. Singularity, Verve • CooL • KMLの特徴に加え、OS自身もMemory Safe • Software Isolated Process + Microkernel • C++のようなunsafeな言語も使用 • 惜しい点 • やっぱりTALx86へコンパイルする言語が そもそも型安全である必要がある 38
39. Cool Isolation Techniques Overview 1. 高レベル言語ランタイムによるisolation • Java, Ruby, … 2. 型の力によるisolation • Kernel Mode Linux • Singularity, Verve 3. SFIによるisolation • SFIとは • NaCl • Nebulet / Wasmer 39
40. Cool Isolation Techniques Overview 1. 高レベル言語ランタイムによるisolation • Java, Ruby, … 2. 型の力によるisolation • Kernel Mode Linux • Singularity, Verve 3. SFIによるisolation • SFIとは • NaCl • Nebulet / Wasmer 40
41. Software-based Fault Isolation (SFI) 参考：http://www.cse.psu.edu/~gxt29/papers/sfi-final.pdf 41
42. Software-based Fault Isolation • 信頼できないコードを安全に実 行できるよう改変して実行する 手法 • 対象は安全である必要がない • 典型的にはBinary Translation • 用途 • ブラウザプラグイン • サンドボックス全般 42
43. 達成すべきIsolation - SFI • 特権命令 • Binary Translation中にディスアセンブルして 発見する • メモリ空間の分離 • Binary Translationによって、すべてのメモリ RW命令、すべてのJump系命令をチェック機 構つきの安全なものに書き換える 43
44. SFIによるメモリ空間の分離 1/3 メモリRWが、与えられたメモリ範囲内 かどうかをチェックするよう書き換え • Rdl r1, r2, # レジスタ2のアドレスをレジ スタ1に読み込み • => if r2 >= min && r2 < max Rdl r1, r2 else error 44
45. SFIによるメモリ空間の分離 2/3 マスクテク; 全てのアドレスを与えられた メモリに収まるようマスクしてしまう • Rdl r1, r2 • => Andli r2, r2, 0x00ffffff Rdl r1, r2 45
46. SFIによるメモリ空間の分離 3/3 ディスプレースメントの考慮 • Rdl r1, -8(r2) • 割り当てられたページの前後にガード ページも作っておく 46
47. SFI • 弱点; オーバーヘッド • 素朴にやると30%くらい 47
48. Cool Isolation Techniques Overview 1. 高レベル言語ランタイムによるisolation • Java, Ruby, … 2. 型の力によるisolation • Kernel Mode Linux • Singularity, Verve 3. SFIによるisolation • SFIとは • NaCl • Nebulet / Wasmer 48
49. Cool Isolation Techniques Overview 1. 高レベル言語ランタイムによるisolation • Java, Ruby, … 2. 型の力によるisolation • Kernel Mode Linux • Singularity, Verve 3. SFIによるisolation • SFIとは • NaCl • Nebulet / Wasmer 49
50. Google Native Client https://static.googleusercontent.com/media/research.google.com /ja//pubs/archive/34913.pdf 50
51. NaCl • 「Web上に置いてあるネイティブELF」を 「ブラウザ上で実行する」ためのGoogleの やばいサンドボックス機構 • パソコンの大先生に 「怪しいWebサイトで落としたバイナリを 実行していい？」って聞いたら絶対呆れる • でもNaClなら安全 • SFIのテクニックを使ってELFバイナリの 安全性を確認する 51
52. NaCl Overview • だいたいNaCl用ツールチェイン, NaClバイ ナリチェッカー, ランタイムからなる • ただのx86 / ARM ELFではなく、いくつかの Constraintを導入してSFIを強制する • Binary Translationの代わりに実行時にバイナリが Constraintを満たしているかチェックする • ざっくり、Constraintが満たされているなら、 SFIのランタイムチェックの手法が埋め込まれて いることを保証できる 52
53. おさらい：SFIによるメモリ空間の分離 メモリRWが、与えられたメモリ範囲内 かどうかをチェックするよう書き換え • Rdl r1, r2, # レジスタ2のアドレスをレジ スタ1に読み込み • => if r2 >= min && r2 < max Rdl r1, r2 else error 53
54. NaClの具体的なメモリ空間分離 • NaClは、検証時にバイナリをdisasして、す べてのメモリアクセス命令をチェック • X86 • すべてのメモリアクセスにセグメントを強制 • AMD64 • 言語上のアドレス空間を32bit幅に制限 • 全てのアドレス計算を、%e*xで行う 54
55. NaCl • CooL • 安全ではない言語C, C++にも対応 • 形式がネイティブバイナリである • %e*xをうまく使ってオーバーヘッドを削減 • 惜しい点 • ディスコンになった 55
56. Cool Isolation Techniques Overview 1. 高レベル言語ランタイムによるisolation • Java, Ruby, … 2. 型の力によるisolation • Kernel Mode Linux • Singularity, Verve 3. SFIによるisolation • SFIとは • NaCl • Nebulet / Wasmer 56
57. Cool Isolation Techniques Overview 1. 高レベル言語ランタイムによるisolation • Java, Ruby, … 2. 型の力によるisolation • Kernel Mode Linux • Singularity, Verve 3. SFIによるisolation • SFIとは • NaCl • Nebulet / Wasmer 57
58. !!!!!!WASM!!!!!!!! 58
59. 再び: NaCl • CooL • 安全ではない言語C, C++にも対応 • 形式がネイティブバイナリである • %e*xをうまく使ってオーバーヘッドを削減 • 惜しい点 • ディスコンになった 59 Asm.js / WASM のせい
60. Wasm • ブラウザでの高速な実行のために誕生 • 型付きではないが安全なアセンブリ言語 • とはいえ全然アセンブリじゃないが・・・ • メモリ空間が外部から与えられた32bitに限定 • Control Flow Integrity • サンドボックスで動くバイナリにAOT/JIT • エコシステムの発展が進行中！ 60
61. Wasmer / Kernel-wasm • Linuxカーネル空間でwasmを動かす ランタイム • コンテキストスイッチなしに実行可能 • “eBPF”をKernel-wasm上で表現する 計画も進行中らしい 61
62. Nebulet • (Going to be) A microkernel that implements a WebAssembly "usermode" that runs in Ring 0. • Rust製 • SIP + Microkernel + Rust • ロマンがやばい • アツさに比べて割と無名 62
63. Nebuet / Wasmer Kernel-wasm • CooL! • 安全ではない言語C, C++にも対応 • 今はやりのWASM • これからの最適化が期待 63
64. これからは Wasm in Kerel空間が熱い！！ 64
65. まとめ 1. 高レベル言語ランタイムによるisolation • JavaOS 2. 型の力によるisolation • Kernel Mode Linux, Singularity, Verve 3. SFIによるisolation • Nebulet / Wasmer 65
66. 令和時代はユーザー空間を捨てろ！ カーネル空間を どんどん探検しよう！ 66