操作系统内核验证的研究进展.pdf

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