えいごわかんない https://www.youtube.com/watch?v=5xE24p-RauQcamkesからmicrokit-vmmへの移行に関する調査donerworksのuse caseで足りなかった点複数のVCPUを作れない x86サポート https://www.youtube.com/watch?v=4ESGgf80lcg spinでsDDFのプロトコルを検証する話 https://www.youtube.com/watch?v=0W5cMTnyBLk&t=32s

モチベ mallocは複雑でよく使われてるやつでもバグが多い→形式検証 おそらく初めての平行性を考慮した高パフォーマンスで互換性のある形式検証されたmalloc実装 方法論 F*/KaRaMeLでextraction Steelという分離論理検証フレームワークで↑の検証 実装はGrapheneOSで使われているhardened_mallocを参考にした 評価

背景 問題意識 問題への貢献 具体的な手法など 理想的なVMMのメモリ管理demand paging virtual memoryというか擬似的な物理メモリでホストのサイズに関係ないように見えるもの memory sharing CoW etc.

背景 問題意識 storage stackにおけるcrash saftyの形式的検証 prefix-preserving disk model最後のフラッシュ以降のある時点の状態に回復 snapshot-consistent model 最後のフラッシュ以前のある時点の状態に回復 問題への貢献

背景 問題意識 driver domainとかdaemonized VMの文脈におけるunikernel ドライバをVMで動かすやつでGPOS乗せるのは明らかに無駄 問題への貢献 linuxのnet/storage周りのドライバをunikernel化して実装・評価(Kite) ROPやらsyscall数やらを減らせた イメージのサイズ・起動時間の短縮(いつもの) https://github.com/ssrg-vt/kite

背景 問題意識 BPF JITの信頼性向上 問題への貢献 jitterbug: JITの形式検証用フレームワーク RV32向けBPF JITの形式検証この過程で見つけた16個のバグのupstreamへのパッチ 具体的な手法など C likeなDSLで実装するRosette

背景 問題意識 時間制約が厳しいクラウドサービスのためにコンテナをMCSにもっていきたい isolation 問題への貢献 realtime container向けのアーキテクチャrealtime co-kernel hierarchical scheduling time division networkin

背景 問題意識 NFVの文脈でもunikernelの起動速度とセキュリティ性能は魅力的i.e. ハードウェア上に実装されていた処理機構をunikernel上にオフロード しかしon-the-flyに新しい機能(unikernel)を導入するという要件がある 問題への貢献 既存のVIM(virtual infrastructure manager)をClickOS上に移植して性能評価 具体的な手法など

背景 問題意識 armベースのMCS上のSPH(static partitioning hypervisor)の特徴や要件の理解 問題への貢献 著名なOSS: Jailhouse, Xen (Dom0-less), Bao, and seL4 CAmkES VMMについてrealtime & safty評価(i) performance, (ii) interrupt latency, (iii) inter-VM communication, (iv) boot time, and (v) code size 具体的な手法など SPHはVMへの資源割当を静的に行う代わりにレイテンシ,isolationなどを頑張る 実際のシステムを利用する際の設定の参考にもなるe.g. superpageを使ってTLB missを許容可能なオーバーヘッドで著しく減らすことができるが,page coloringを有効にすることで無効になってしまう

背景 問題意識 軍用に耐えるクラウドのためのVMM実装 separation kernelは強すぎる汎用のVMMの大体にするのは難しい 問題への貢献 separation VMMseparation kernelのTCBや形式検証などの制約を弱める 一般のHWやOSをサポートする EAL 5くらいを目標とした実装

背景 問題意識 x86などの複雑なアーキテクチャ上のソフトウェアサンドボックスの実装は脆弱になりやすいソフトウェアサンドボックスはバイナリ解析してポリシー守ってるか検証する感じのやつの意 形式検証する 問題への貢献 NaClみたいなのを作ったCoqでx86の大部分のモデルを書いて宣言的な実装からコード生成で解析タスクの処理を作る 具体的な手法など

背景 問題意識 プログラム検証によってエンドユーザーが問題を解決しようとするとき,情報収集が難しい プログラム検証ツールのどれをどんな問題に適用すればいいか判断するには高度な知識と相当期間の情報収集が必要になってくる論文書いてメンテ終了などよくあり,プロトタイプで終わってるとか リポジトリにドキュメントが一切なくて論文読めとか 問題への貢献 プログラム検証ツールの分類PV0-6 読みやすいまとめhttps://slebok.github.io/proverb

背景 問題意識 multi-tenacy isolation on the cloud hypervisorの介入で遅くなるならhypervisorを無くせばいい IaaSくらいのレイヤのクラウドコンピューティング文脈っぽい 問題への貢献 resource isolation without hypervisor 既存のHWで実現できるNoHype architecture一VM,一コア HW機能によるmemory partitioning

背景 問題意識 seL4は小さなTCBでエッジへの適用などが期待できるがuserlandのツールがあまり成熟していない 組み込みVMMの需要 seL4上のVMMは存在するが成熟したものではない 現在seL4上のVMMソリューションは,既存の実装をフォークしてユースケースに場当たり的ななカスタマイズをしたものでエコシステムに適合した標準があると嬉しいフォーク先で重複した機能の開発が行われているなどの問題 問題への貢献 seL4上のVMMのユースケースの検討 標準化への設計方針などの検討

背景 問題意識 microkernel based multiserver systemの再考としてseL4上でRumpを動かす形式検証済みの信頼できる下地の上に,安いコストでPOSIXぽい環境を作る 互換性,信頼性,パフォーマンスの折り合いをつける 問題への貢献 seL4上にRumpを移植 具体的な手法など

背景 問題意識 組み込みMCSでVMMの需要があるが,VMMはMCSに対応したスケジューリングをしない 既存のVMMではスケジューリングはおろか,その他の資源の分離もMCSに対応したものではない type-2 hypervisorだとGPOS上でVMMをやるのでTCBがかなり大きくなる 問題への貢献 ARM上で動くtype-1 hypervisor T-visorscheduling theoryの発展に対応するために柔軟なスケジューリングフレームワークを設計ユーザ定義のスケジューラを容易に書ける 実装が小さい i.e. TCBが小さい

背景 問題意識 シスプロの文脈でも形式的手法が浸透してきてよいが,でかいモデルをつくるとメンテナンスがダルい・再利用可能性が低いなどがある proof assistant lock-in定理証明支援系は学習コストが高いので一度特定のツールを使うことにするとなかなか移行できない 特に依存型→LCFみたいなのは移植がほぼ無理 問題への貢献 Lem: 単一の仕様記述言語から複数の定理証明支援系/プログラム言語上の定義への変換(portable definition), 可視化latex/html 各定義が変換された先で同じ意味ををもつことは保証されない

背景 問題意識 プログラム言語の意味論レベルでは扱えてない挙動をリンカが担っているe.g. weak symbol 一般のソフトウェアはプログラム言語の意味論だけでなくリンカの挙動にも大いに依存している(Linker Speak) 形式検証済みコンパイラでも,こういった部分は扱えていないかごく一部 問題への貢献 ELFバイナリのリンクに関する形式化あるべき挙動を形式的に記述するというより現在一般に利用されているリンカの挙動に近い形にする

背景 問題意識 高信頼システムの構築には,かなり厳密な設計・検証が必要だが毎度一からやるのは面倒 MILSを高信頼組み込みシステムの設計につかうとどうなるか 問題への貢献 MILSは,高信頼組み込みシステムの構築と相性が良さそうという考察 具体的な手法など MLSというのが前身にあって,複数のセキュリティレベルを持つ部品が相互作用するようなシステムの検証が考えられていたが(e.g. bell-lapadula),検証(certification)の前にセキュリティ特性の解析を要求されるので複雑でMILSで整理された