Problem Architecture Detailed Design Test Data - AST Generation - Kagebunsin - Operator - Predicate - Symbolic Executor - Theorem Prover SWAP MAP 由于AST过大，所以在符号执行的过程中会在内存中占

- Some common themes underlying all of the above - Point out some differences between CES and product - Focus on ideas leading to the prototype - Some fun “behind-the scenes” look Smallest co

#内核安全与内核验证 #研究背景 ##应用程序的可利用漏洞 - 研究众多，关注程度高 - 静态分析 - 动态分析 - 实时监控 ##内核级的Rootkit防御 - 研究较少 - 质量参差不齐的驱动, 恶意代码注入 - 防御方案实施困难 #内核的形式化验证 ##模型检查 - 建立内核的抽象模型 - 给出内核的行为规范 - 采用工具进行全自动

- 可信编译器研究 - 同步数据流语言可信编译器研究 - Lustre到C 的可信编译器 L2C - L2C 项目进展情况 - 总结及展望