# seL4 summit 2024
えいごわかんない

- https://www.youtube.com/watch?v=5xE24p-RauQ
- camkesから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
- rust-seL4の進捗について
- https://www.youtube.com/watch?v=O0SrqPTc_kU
- ROS2 on Linux on seL4(camkes) の話
- デバドラとかコンポーネントを切り分けてセキュアにするみたいなやつ
- https://www.youtube.com/watch?v=VfsN1PriVK0
- seL4のVMM上で認証取得済みRTOSを動かす話
- デフォルトのround robinスケジューラだとRTOSに時間を全部割り当てるのがうまくできないので､MCSを使うと良いというハックがあるらしい
- https://www.youtube.com/watch?v=8JLKtpB1KPM
- seL4をSMPにするための前段階としてのmultikernel化構想
- multikernel化することで既存の証明コードベースの多くが再利用可能になるらしい
- Hoare logicをrely gurantee logicに移植する
- rely guaranteeよくわからないtripleに加えて環境へのアサーションが付くんだっけ？
- https://www.youtube.com/watch?v=2lFYm7cjMpQ
- seL4の検証ロードマップ
- MCSやる､SMPやる､アーキテクチャ増やす､プラットフォーム増やす､ポータブルにする
- https://www.youtube.com/watch?v=uAHVV0Lzopw
- pancake言語: sel4のデバドラを書くための鼻から悪魔を出さないCを目指した言語
- 型システムとか無い(C相当のやつはある)
- CakeMLのツールチェインを再利用して,proof effortを減らしている
- まだPoCという感じで､最近まで共有可変状態を扱うためにFFIが必要だった(発表時点では実現したらしい)
- https://www.youtube.com/watch?v=oyWB3jLj_P8
- 現代の国防という観点から形式検証とそのOSへの適用の重要性に関するスピーチ