seL4的形式化驗證步驟是什麼？是否對已知的所有攻擊形式免疫？

本來是想偷懶看大牛總結的，不過看來都太忙。自問自答，拋磚引玉吧。

seL4的形式驗證步驟，看http://ssrg.nicta.com.au/publications/papers/Klein_EHACDEEKNSTW_09.pdf 里寫的是：

1. 寫出IPC、syscall、調度等所有微內核對象的抽象規範Abstract Specification（in Isabelle）。
2. 寫出如上對象的可執行規範Executable Specification(in Haskell)，並證明其正確實現了第一步的抽象規範。[1]
3. 手寫C實現。通過一個SML寫的C-Isabelle轉換器[2]，和Haskabelle聯合形式證明C代碼和第二步的Haskell定義語義一致。

[1] 證明方法可概述為：構建一個機器模型，模型中包含寄存器、內存、IRQ、cache等所有可被代碼影響的硬體。然後證明對抽象規範每一步狀態轉換，可執行規範都產生唯一對應的狀態轉換（換言之，兩個狀態機等價）。
[2] 該轉換器據稱精確（對驗證而言）實現了絕大部分C99規範但不是全部。為此(及形式驗證的需要）對seL4里使用C進行了如下限制：1，棧變數不得取引用，必要時以全局變數代替；2，因為C99不定義函數調用時參數求值的順序，限制所有函數參數必須事先顯式求值；3，禁止函數指針。此外，該轉換器不支持union，因為kernel編程對精確的要求，他們另外寫了一個工具實現所有bitfield的需求，生成數組並直接內聯進對應架構編譯後的彙編代碼。

對已知攻擊的防禦，從http://ertos.nicta.com.au/research/l4.verified/proof.pml 來看有：

1. 緩衝區溢出
2. 解引用空指針
3. 指針類型錯誤
4. 內存泄漏（含野指針）
5. 算術溢出及其導致的異常（超過32位邊界等等）

seL4開發者很驕傲的表示這些都是does not occur in seL4的，當然我還沒看懂不敢背書。是否還有其他類型的攻擊沒防禦到就等黑客界大牛過來點評了。