seL4チュートリアル

TIER IV 2023 / 03 / 13 seL4チュートリアル 高野祐輝 （TIER IV）

TIER IV 01 / 背景と目的 02 / 導入 03 / seL4概要 seL4チュートリアル 04 / システムコール呼び出し 高野 祐輝（TIER IV） 05 / システム実装 06 / スペックから読み解くseL4 07 / まとめ

TIER IV 自己紹介 高野祐輝『ゼロから学ぶ Rust』講談社, 2022 高野祐輝『並行プログラミン グ入門』オライリー・ジャパン , 2021

背景と目的 01

TIER IV 背景 1. 自動運転システムには高い安全性とリアルタイム性が必要 2. 安全性（safety） 3. a. ソフトウェアの設計に誤りが無いか b. OSなどの基盤ソフトウェアにバグが無いか c. 自動運転システムのソフトウェアにバグが無いか リアルタイム性 a. 従来のリアルタイムとは異なる b. リアルタイム性が必要なソフトウェアと、ある程度の速度が動けば良いシステムが混在 c. 自己位置推定や機械学習など、計算量の予測が難しいタスクが多い

TIER IV 目的 1. 2. 安全性（safety） a. 形式検証された OS（seL4）を適用し、安全性を高めたい！ b. seL4上で動作するカーネルを設計・実装したい！ c. その上で自動運転システムを動かしたい！ リアルタイム性 a. リアルタイムタスクとベストエフォートタスクの両方をうまく扱いたい！ b. seL4上で動作するカーネルで、計算量の予測が難しいタスクをうまくスケジューリングした い！

導入 02

TIER IV MicrokernelとMonolithic Kernel 1. 2. 3. Microkernel a. 必要最小限の機能をカーネルで実装 b. 他大部分はユーザランドで実装 Monolithic Kernel a. 入出力、デバイスなど含む多くの機能を、カーネルで実装 b. LinuxはMonolithic Kernelと呼ばれる LinusとTanenbaumの論争 a. Microkernel vs Monolithic Kernel論争はあまりにも有名 b. https://www.oreilly.co.jp/BOOK/osp/OpenSource_Web_Version/appen_A/appen_A.html

• https://www.oreilly.co.jp/BOOK/osp/OpenSource_Web_Version/appen_A/appen_A.html

TIER IV Microkernel vs Monolithic Kernel論争 タネンバウム教授「LINUXはモノリシックな形態のシステムだ。その点で、LINUXの 設計は、1970年代に大きく後戻りしてしまっている。既存の動作しているCプログラム を、わざわざBASICで書き直したようなものだ。」 Linus「MINIXはマイクロカーネル的な働きをうまく行なっておらず、マルチタスク処理に 問題がある。私がファイルシステムのマルチスレッド処理に問題があるOSを作ったとした ら、他の人の作ったものをそんなに性急に非難しないだろう。」

TIER IV Microkernel vs Monolithic Kernel論争 タネンバウム教授「1991年の今どきに、モノリシックなカーネルを設計することは根本 的に間違いだ。あなたは、私の生徒でないことに感謝した方がいい。そんな設計では 進級できないだろう :-) 」 Linus「大丈夫。アインシュタインも数学と物理の単位はお粗末だったよ。」

TIER IV 形式手法 1. 数学的に厳密に設計を記述し、設計の正しさを検証する手法 2. 形式手法は使えない？ 3. a. これは間違い。そう言われている時期もあった（ 2015年頃までの認識） b. AWSなどいわゆる ビッグテックのサービスでは、既に広く形式手法が適用されている c. これらを利用していないのは、既に技術的ビハインド d. おそらく、システム屋がどうやって形式手法を取り入れていくかが、本邦の課題 参考文献 a. J. Bornholt, et al., Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3, ACM SOSP 2021 b. C. Newcombe, et al., How Amazon Web Services Uses Formal Methods, Communications of the ACM, April 2015, Vol. 58 No. 4, Pages 66-73

TIER IV 形式手法の例 1. 設計 a. b. 2. 今、ワークショップに参 加しているぞ！ 前提 i. 我思うなら我あり ii. 我思わねば、我思う 結論: 我あり 形式仕様化 3. 証明 a. P: 我思う ¬Pを背理法の仮定とする b. Q: 我あり ¬P ¬P ⇒ P c. P ⇒ Q : 前提 i d. ¬P ⇒ P : 前提 ii モーダス・ポネンス P ¬P False P 矛盾 背理法 P⇒Q Q モーダス・ポネンス

TIER IV 形式手法の特徴 1. 2. 曖昧さがない a. これが一番重要に思う b. 自然言語の仕様だと、三者三様にとられる可能性がある c. UMLのような仕様だと、抜けが生じがち 検証可能 a. 理論的には検証可能 b. ただし、現実は、証明が難解であったり、計算量の壁にぶつかることもある

TIER IV seL4の特徴 1. Microkernelであっても高速に動作可能 2. 形式検証されている 3. a. HaskellのコードをIsabelle/HOLという形式手法ツールで検証 b. 上記Haskellコードを、人間が Cに変換 時間隔離されたタスクスケジューラを実装 A. Lyons, et al., Scheduling-Context Capabilities, Eurosys 2018 4. リアルタイムシステムの一つである自律航行ドローンにも応用されている a. Flying autonomous aircraft: Mixed-criticality support in seL4 b. https://www.youtube.com/watch?v=ijTTZgQ8cB4

• https://www.youtube.com/watch?v=ijTTZgQ8cB4

seL4概要 03

TIER IV seL4のチュートリアル 1. Hello, World!やCapabilitiesなどのチュートリアルがある https://docs.sel4.systems/Tutorials/#introduction-tutorial 2. 一応動くが、専門用語が特殊すぎて全然わからない a. この感触は久々だぜ… b. コンピュータ初心者の頃、ファイルデスクリプタやハンドラの意味がわからなかっ た。それに似ている 3. 本発表では、上記チュートリアルの序盤に登場するCapabilitiesなどについて深掘りす る

• https://docs.sel4.systems/Tutorials/#introduction-tutorial

TIER IV 登場するseL4用語 1. Capabilities a. Thread Control Block (TCB) b. Untyped capabilities 2. Capability Nodes (CNodes) 3. Capability Slots (CSlots) 4. Capability Spaces (CSpaces)

TIER IV Capabilities 1. 2. Capabilitiesは、以下へのアクセスを制御するものである a. Thread Control Block (TCB) などのカーネルオブジェクト b. IRQControlなどの抽象リソース c. メモリ領域を表す Untyped capabilities seL4には、rootタスクと呼ばれる特殊なタスクがあり、 rootタスクはすべての Capabilitiesを制御 する Untyped capabilities TCB IRQControl Capabilities

TIER IV CNodesとCSlots 1. CNodesはCapabilitiesの配列 2. CSlotsはCNodesの要素 a. 中身の方じゃ無くて箱のほう CNodes empty TCB IRQControl empty CSlot

TIER IV CSpaces 1. CSpaces a. A CSpace (capability-space) is the full range of capabilities accessible to a thread, which may be formed of one or more CNodes. b. 赤字のところが良くわからない i. c. 「スレッドにアクセスできる capabilitiesの全範囲」とは？ とにかく、CNodesの集合っぽい CNode CNode CNode CNode CSpaces

TIER IV CSpaceのアドレッシング 1. CSpace内のCapabilitiesへは以下の情報を用いてアクセスする a. Capability b. index: CNode中のCSlotへのインデックス c. depth: CNodeをトラバースするための距離 2. ここらへんから、そろそろ仕様・実装がわからないと、理解するのが難しく なってきた 3. 以降で、ソースコード・仕様を読み解いていく

システムコール呼び出し 04

TIER IV チュートリアル深掘り 1. seL4チュートリアルにあるコードを深掘りしてみる https://docs.sel4.systems/Tutorials/capabilities.html 2. 特に、seL4_TCB_ReadRegisters()関数についてみてみる チュートリアルにある Cのコード。レジスタを読み書きしているだけ。 レジスタ読み込み関数を深掘り seL4_UserContext registers; seL4_Word num_registers = sizeof(seL4_UserContext)/sizeof(seL4_Word); /* Read the registers of the TCB that the capability in seL4_CapInitThreadTCB grants access to. */ seL4_Error error = seL4_TCB_ReadRegisters(seL4_CapInitThreadTCB, 0, 0, num_registers, &registers); assert(error == seL4_NoError);

• https://docs.sel4.systems/Tutorials/capabilities.html

TIER IV seL4_TCB_ReadRegisters()関数 1. GitHub上にあるソースコードを探しても見つからない 2. seL4_TCB_ReadRegisters()関数は、自動生成される？ a. 以下のコードが怪しい b. https://github.com/seL4/seL4/blob/f8b2440b38bff2044da27481d42689d504be9a27/libse l4/include/interfaces/sel4.xml#L88 c. https://github.com/seL4/seL4/blob/f8b2440b38bff2044da27481d42689d504be9a27/libse l4/CMakeLists.txt#L57 3. いくつかのコードが自動生成されるので、実際にコンパイルしたコードを見る必要あり

• https://github.com/seL4/seL4/blob/f8b2440b38bff2044da27481d42689d504be9a27/libsel4/include/interfaces/sel4.xml#L88
• https://github.com/seL4/seL4/blob/f8b2440b38bff2044da27481d42689d504be9a27/libsel4/CMakeLists.txt#L57

TIER IV seL4_TCB_ReadRegisters()関数の実装 libsel4/include/interfaces/sel4_client.hに配置される LIBSEL4_INLINE seL4_Error seL4_TCB_ReadRegisters(seL4_TCB _service, seL4_Bool suspend_source, seL4_Uint8 arch_flags, seL4_Word count, seL4_UserContext *regs) { seL4_Error result; seL4_MessageInfo_t tag = seL4_MessageInfo_new(TCBConfigure, 0, 3, 3); seL4_MessageInfo_t output_tag; seL4_Word mr0; seL4_Word mr1; seL4_Word mr2; seL4_Word mr3; 中略 /* Perform the call, passing in-register arguments directly. */ output_tag = seL4_CallWithMRs(_service, tag, &mr0, &mr1, &mr2, &mr3); result = (seL4_Error) seL4_MessageInfo_get_label(output_tag); 中略 return result; }

TIER IV seL4_TCBはただのポインタ 1. typedef seL4_CPtr seL4_TCB; // libsel4/include/sel4/types.h 2. typedef cptr_t seL4_CPtr; // include/basic_types.h 3. typedef word_t cptr_t; // include/arch/x86/arch/types.h 4. typedef unsigned long word_t; // include/arch/x86/arch/types.h

TIER IV seL4_UserContextはレジスタの集合 libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/types.h typedef struct seL4_UserContext_ { seL4_Word rip, rsp, rflags, rax, rbx, rcx, rdx, rsi, rdi, rbp, r8, r9, r10, r11, r12, r13, r14, r15; seL4_Word fs_base, gs_base; } seL4_UserContext;

TIER IV seL4_MessageInfo_t型とseL4_MessageInfo_new()関数の実装 libsel4/include/sel4/shared_types_gen.hに自動生成される struct seL4_MessageInfo { seL4_Uint64 words[1]; }; typedef struct seL4_MessageInfo seL4_MessageInfo_t; LIBSEL4_INLINE_FUNC seL4_MessageInfo_t CONST seL4_MessageInfo_new(seL4_Uint64 label, seL4_Uint64 capsUnwrapped, seL4_Uint64 extraCaps, seL4_Uint64 length) { seL4_MessageInfo_t seL4_MessageInfo; 中略 (label, capabilities, extra capabilities, length) seL4_MessageInfo.words[0] = 0 | (label & 0xfffffffffffffull) << 12 | (capsUnwrapped & 0x7ull) << 9 | (extraCaps & 0x3ull) << 7 | (length & 0x7full) << 0; return seL4_MessageInfo; } seL4_MessageInfo_new() word (seL4_MessageInfo_t)

TIER IV

seL4_CallWithMRs()関数の実装
1.

seL4_CallWithMRs()はシステムコール呼び出し関数（ CPUアーキテクチャ依存）
a.

x86_64の場合以下にある

b.

https://github.com/seL4/seL4/blob/d90fada8b3b0ce889d8e07a05f19896cbc0b7067/libse
l4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h#L269-L307

LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_CallWithMRs
(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
中略
x64_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0,
&msg1, &msg2, &msg3, 0); // syscall命令を呼び出す
中略
return info;
}

• https://github.com/seL4/seL4/blob/d90fada8b3b0ce889d8e07a05f19896cbc0b7067/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h#L269-L307

TIER IV seL4_TCB_ReadRegisters()の可換図式 (TCB, seL4_TCB_ReadRegisteres()) has (label, capabilities, extra capabilities, length) seL4_TCB_ReadRegisters() has seL4_MessageInfo_new() registers seL4_MessageInfo_t { word[1] } seL4_CallWithMRs() = x64_sys_send_recv(seL4_SysCall) (TCB, seL4_MessageInfo_t)

システムコール実装 05

TIER IV システムコール実装に関するコールグラフ handleSyscall(); // src/api/syscall.c handleInvocation(); // src/api/syscall.c decodeInvocation(); // src/object/objecttype.c decodeTCBInvocation(); // src/object/tcb.c decodeReadRegisters(); // src/object/tcb.c invokeTCB_ReadRegisters(); // src/object/tcb.c

TIER IV

invokeTCB_ReadRegisters()関数の実装
1.

src/object/tcb.cに定義される

https://github.com/seL4/seL4/blob/4ce6cbe9ea4c6656edd98d76bcf5ad3e10caf313
/src/object/tcb.c#L1934
2.

基本的に、tcb_t型の値から、get_register()関数でレジスタを読み出すのみ
exception_t invokeTCB_ReadRegisters(tcb_t *tcb_src, bool_t suspendSource,
word_t n, word_t arch, bool_t call)
{
中略
for (i = 0; i < n_gpRegisters && i + n_frameRegisters < n
&& i + n_frameRegisters < n_msgRegisters; i++) {
setRegister(thread, msgRegisters[i + n_frameRegisters],
getRegister(tcb_src, gpRegisters[i]));
}
後略

• https://github.com/seL4/seL4/blob/4ce6cbe9ea4c6656edd98d76bcf5ad3e10caf313/src/object/tcb.c#L1934

TIER IV

getRegister()関数の実装
1.

include/machine/registerset.hに定義される

2.

配列から値を読み込むのみ

static inline word_t PURE getRegister(tcb_t *thread, register_t reg)
{
return thread->tcbArch.tcbContext.registers[reg];
}

TIER IV コンテキスト include/arch/x86/arch/object/structures.h typedef struct arch_tcb { user_context_t tcbContext; #ifdef CONFIG_VTX /* Pointer to associated VCPU. NULL if not associated. * tcb->tcbVCPU->vcpuTCB == tcb. */ struct vcpu *tcbVCPU; #endif /* CONFIG_VTX */ } arch_tcb_t; include/arch/x86/arch/object/structures.h struct user_context { user_fpu_state_t fpuState; word_t registers[n_contextRegisters]; #if defined(ENABLE_SMP_SUPPORT) && defined(CONFIG_ARCH_IA32) /* stored pointer to kernel stack used when kernel run in current TCB context. */ word_t kernelSP; #endif #ifdef CONFIG_HARDWARE_DEBUG_API user_breakpoint_state_t breakpointState; #endif }; typedef struct user_context user_context_t;

スペックから読み解くseL4 06

TIER IV seL4のCとHaskellどちらを読むか: Pros and Cons 1. C a. Pros: 実行されるコードをそのまま解釈可能 b. Cons: 型システムが貧弱（代数的データ型とモナドが無い）で仕様を読み解くのが つらい 2. Haskell a. Pros: 型システムがしっかりしており（代数的データ型とモナドがある）、関数の型 を読むだけである程度仕様が理解できる セマンティクスを理解するためならHaskellの方が良さそう b. Cons: モナドがある（難しい）

TIER IV Haskellの特徴 1. 純粋関数型言語（副作用無し） a. 2. オフサイドルール a. 3. 4. 純粋であるだけなら、難しくは無い 少し難しい 高カインド型 a. モナドを実装可能 b. 難しい seL4の仕様はHaskellで書かれており、CよりHaskellの方を読んだ方が良い https://github.com/seL4/l4v

• https://github.com/seL4/l4v

TIER IV decodeTCBInvocation in Haskell 1. decodeTCBInvocation関数のHaskell実装 https://github.com/seL4/l4v/blob/3e8114fd8fde75ac52e349939a131bf6fec4b069/spec/haskell/src/SEL4/Object /TCB.lhs#L70-L88 2. Cよりも意味がわかりやすい Haskellバージョン decodeTCBInvocation :: Word -> [Word] -> Capability -> PPtr CTE -> [(Capability, PPtr CTE)] -> KernelF SyscallError TCBInvocation decodeTCBInvocation label args cap slot extraCaps = case genInvocationType label of TCBReadRegisters -> decodeReadRegisters args cap TCBWriteRegisters -> decodeWriteRegisters args cap 中略 _ -> throw IllegalOperation cap_t型の定義が見つからない。 諦めた。 Cバージョン exception_t decodeTCBInvocation(word_t invLabel, word_t length, cap_t cap, cte_t *slot, bool_t call, word_t *buffer);

• https://github.com/seL4/l4v/blob/3e8114fd8fde75ac52e349939a131bf6fec4b069/spec/haskell/src/SEL4/Object/TCB.lhs#L70-L88

TIER IV Capability in Haskell 1. Capability型の定義 https://github.com/seL4/l4v/blob/fb150e8a7cd26a31d46a499c23f538b91cd2e673/spec/haskell/src/SEL4/Obje ct/Structures.lhs#L46-L83 2. Capabilityは8種類あることが判明 data Capability = ThreadCap { capTCBPtr :: PPtr TCB } | NullCap | NotificationCap { capNtfnPtr :: PPtr Notification, capNtfnBadge :: Word, capNtfnCanSend, capNtfnCanReceive :: Bool } | IRQHandlerCap { capIRQ :: IRQ } | EndpointCap { capEPPtr :: PPtr Endpoint, capEPBadge :: Word, capEPCanSend, capEPCanReceive :: Bool, capEPCanGrant, capEPCanGrantReply :: Bool } | UntypedCap { capIsDevice :: Bool, capPtr :: PPtr (), capBlockSize :: Int, capFreeIndex :: Int } | CNodeCap { capCNodePtr :: PPtr CTE, capCNodeBits :: Int, capCNodeGuard :: Word, capCNodeGuardSize :: Int } | IRQControlCap deriving (Eq, Show)

• https://github.com/seL4/l4v/blob/fb150e8a7cd26a31d46a499c23f538b91cd2e673/spec/haskell/src/SEL4/Object/Structures.lhs#L46-L83

TIER IV Capability 種類 用途 ThreadCap Thread Control Blockを操作 NullCap 空のCapability NotificationCap シグナルを操作 IRQHandlerCap 割り込みハンドラを操作 EndpointCap IPCを行うためのCapability UntypedCap 空メモリへのCapability CNodeCap Capability Node。木構造で複数の Capabilityを保持 IRQControlCap 割り込みを制御

TIER IV PPtrとVPtr型 1. ポインタは、物理メモリと仮想メモリ別々の型で表現されている https://github.com/seL4/l4v/blob/fb150e8a7cd26a31d46a499c23f538b91cd2e673/spec/haskell /src/SEL4/Machine/RegisterSet.lhs#L70-L74 2. 物理メモリ: PPtr型 3. 仮想メモリ: VPtr型 newtype PPtr a = PPtr { fromPPtr :: Word } deriving (Show, Eq, Num, Bits, FiniteBits, Ord, Enum, Bounded) newtype VPtr = VPtr { fromVPtr :: Word } deriving (Show, Eq, Num, Bits, FiniteBits, Ord, Enum, Bounded)

• https://github.com/seL4/l4v/blob/fb150e8a7cd26a31d46a499c23f538b91cd2e673/spec/haskell/src/SEL4/Machine/RegisterSet.lhs#L70-L74

TIER IV CNodeのエントリ 1. CNodeのエントリは、CTE型で表現 https://github.com/seL4/l4v/blob/fb150e8a7cd26a31d46a499c23f538b91cd2e673/spec/haskell/src/SEL4/Obje ct/Structures.lhs#L208-L211 2. MDBNode型で木構造を表現 data CTE = CTE { cteCap :: Capability, cteMDBNode :: MDBNode } deriving Show ヌルMDBノード data MDBNode = MDB { mdbNext, mdbPrev :: PPtr CTE, mdbRevocable, mdbFirstBadged :: Bool } deriving Show nullMDBNode :: MDBNode nullMDBNode = MDB { mdbNext = nullPointer, mdbPrev = nullPointer, mdbRevocable = False, mdbFirstBadged = False }

• https://github.com/seL4/l4v/blob/fb150e8a7cd26a31d46a499c23f538b91cd2e673/spec/haskell/src/SEL4/Object/Structures.lhs#L208-L211

TIER IV TCB in Haskell 1. TCBもちゃんとある https://github.com/seL4/l4v/blob/fb150e8a7cd26a31d46a499c23f538b91cd2e673/spec/haskell /src/SEL4/Object/Structures.lhs#L218-L276 2. tcbCTableが、スレッドの Capabilitiesのルートノード 3. tcbArchが、アーキテクチャ依存の TCB data TCB = Thread { tcbCTable :: CTE, 中略 tcbArch :: ArchTCB } deriving Show

• https://github.com/seL4/l4v/blob/fb150e8a7cd26a31d46a499c23f538b91cd2e673/spec/haskell/src/SEL4/Object/Structures.lhs#L218-L276

TIER IV 再掲: システムコール実装に関するコールグラフ handleSyscall(); // src/api/syscall.c handleInvocation(); // src/api/syscall.c decodeInvocation(); // src/object/objecttype.c decodeTCBInvocation(); // src/object/tcb.c Haskellで実装されているの はここまで。 decodeReadRegisters(); // src/object/tcb.c invokeTCB_ReadRegisters(); // src/object/tcb.c ここはHaskellにはない。

TIER IV

decodeReadRegisters in Haskell
1.

Cと同名の関数が定義される
https://github.com/seL4/l4v/blob/3e8114fd8fde75ac52e349939a131bf6fec4b069/spec/haskell/src/SEL4/Object
/TCB.lhs#L141-L153

2.

やや長いが、Arch.decodeTransferが本体

decodeReadRegisters :: [Word] -> Capability ->
KernelF SyscallError TCBInvocation
decodeReadRegisters (flags:n:_) cap = do
rangeCheck n 1 $ length frameRegisters + length gpRegisters
transferArch <- Arch.decodeTransfer $ fromIntegral $ flags `shiftR` 8
self <- withoutFailure $ getCurThread
when (capTCBPtr cap == self) $ throw IllegalOperation
return ReadRegisters {
readRegsThread = capTCBPtr cap,
readRegsSuspend = flags `testBit` 0,
readRegsLength = n,
readRegsArch = transferArch }
decodeReadRegisters _ _ = throw TruncatedMessage

• https://github.com/seL4/l4v/blob/3e8114fd8fde75ac52e349939a131bf6fec4b069/spec/haskell/src/SEL4/Object/TCB.lhs#L141-L153

TIER IV decodeTransfer関数 1. 2. decodeTransfer関数は、CopyRegisterSetsという型の値を返すだけ ダミー実装っぽい spec/haskell/src/SEL4/Object/TCB/X64.lhs decodeTransfer :: Word8 -> KernelF SyscallError CopyRegisterSets decodeTransfer _ = return X64NoExtraRegisters spec/haskell/src/SEL4/API/Invocation/X64.lhs data CopyRegisterSets = X64NoExtraRegisters deriving Show

まとめ 07

TIER IV まとめ 1. 2. 3. seL4の読み解き方 a. CとHaskellのコード両方を読むと理解が進む b. Isabelle/HOLのコードは読まなくても OK Capabilitiesの概念が独特 a. Cのコードを読んだだけでは、たぶん理解できない b. CNodeとCSpaceはまだ完全に把握していない c. Haskellのコードを読むとわかりそう チュートリアルがわかりづらい

TIER IV CONTACT US https://tier4.jp/ Thanks Again !

• https://tier4.jp/