seL4的形式化验证步骤是啥是否对已知的所有攻击形式免疫本来是想偷懒

本来是想偷懒看大牛总结的，不过看来都太忙。自问自答，抛砖引玉吧。
seL4的形式验证步骤，看http://ssrg.nicta.com.au/publications/papers/Klein_EHACDEEKNSTW_09.pdf 里写的是：
写出IPC、syscall、调度等所有微内核对象的抽象规范Abstract Specification（in Isabelle）。写出如上对象的可执行规范Executable Specification(in Haskell)，并证明其正确实现了第一步的抽象规范。手写C实现。通过一个SML写的C-Isabelle转换器，和Haskabelle联合形式证明C代码和第二步的Haskell定义语义一致。证明方法可概述为：构建一个机器模型，模型中包含寄存器、内存、IRQ、cache等所有可被代码影响的硬件。然后证明对抽象规范每一步状态转换，可执行规范都产生唯一对应的状态转换（换言之，两个状态机等价）。该转换器据称精确（对验证而言）实现了绝大部分C99规范但不是全部。为此(及形式验证的需要）对seL4里使用C进行了如下限制：1，栈变量不得取引用，必要时以全局变量代替；2，因为C99不定义函数调用时参数求值的顺序，限制所有函数参数必须事先显式求值；3，禁止函数指针。此外，该转换器不支持union，因为kernel编程对精确的要求，他们另外写了一个工具实现所有bitfield的需求，生成数组并直接内联进对应架构编译后的汇编代码。
【seL4的形式化验证步骤是啥是否对已知的所有攻击形式免疫】 对已知攻击的防御，从http://ertos.nicta.com.au/research/l4.verified/proof.pml 来看有：
缓冲区溢出解引用空指针指针类型错误内存泄漏（含野指针）算术溢出及其导致的异常（超过32位边界等等）seL4开发者很骄傲的表示这些都是does not occur in seL4的，当然我还没看懂不敢背书。是否还有其他类型的攻击没防御到就等黑客界大牛过来点评了。

seL4的形式化验证步骤是啥是否对已知的所有攻击形式免疫

推荐阅读

手机|郑爽高价卖旧手机买家吐槽觉得自己被骗了

小左聊体育|一穿四！北美TSM击败TL晋级决赛

西厢有情|是一种教养，不麻烦别人

PP体育TB|大连媒体呼唤亮剑精神，中超16强动态：李霄鹏承认球员能力欠缺

面粉过期了还能吃吗

猫肉能吃吗，猫肉能经常吃吗？

任天堂|Switch Pro还要继续等：任天堂2023年3月前不会推出新硬件

《妄想山海》怎么获得好装备？

游戏日报|第五人格5款超有趣动态涂鸦，萌新都没有，全是老玩家的象征

所谓日本化妆品批发是真是假

南昌万达旅游城里面都有些啥

六点下班八点健身，中间有一小时路程，求教健身达人，啥时候吃完饭比较科学又能保证运动时有足够的能量

篮坛小快灵张文东让日本“金星”黯然失色，昔日豪杰——中日擂台赛上建丰功

怎样在周围人脱离单身的时候坚持自我，过好自己的生活

小雨鑫@春天过后养生常识

『海蛇』史前怪物35米长的海蛇，如果活着出现在现代，人类还敢出海吗？

少儿学古诗精选集儿童学唐诗

[大虾头]你不知道的香蕉

『恢复』武汉轨道交通28日起部分恢复运营车站、列车深度消毒

贝尔希BESy卫浴|吉安市盛世家纺有限公司|梦悠妍布艺：窗帘2倍和1.5倍的区别