嵌入式操作系统的形式化验证方法研究

目录

声明

第一章绪论

1.1 研究背景

1.1.1 嵌入式操作系统安全及其意义

1.1.2 软件系统的形式化验证

1.2.1 早期阶段

1.2.2 壮大阶段

1.2.3 当前阶段

1.3 研究内容与意义

1.3.1 嵌入式操作系统验证中存在的问题

1.3.2 本文研究内容

1.4 本文的组织结构

第二章嵌入式操作系统的验证框架研究

2.1 概述

2.2 系统设计与形式化验证需求

2.3 分离逻辑理论基础及验证实例

2.3.1 分离逻辑理论基础

2.3.2 验证链表反转程序

2.4 嵌入式操作系统的模块化验证框架

2.4.1 原子模块

2.4.2 模块化验证过程

2.4.3 抽象层形式化规范

2.4.4 实现层形式化规范

2.5 双链表删除程序的模块化验证实例

2.6 本章小结

第三章内存管理的验证方法研究

3.1 概述

3.1.1 所面临的挑战

3.1.2 解决方法

3.2 内存验证方案

3.2.1 内存分配算法分析

3.2.2 内存分配算法的验证计划

3.3 TLSF动态内存分配算法的验证

3.3.1 MPI抽象模型

3.3.2 MPO抽象模型

3.3.3 顶层TLSF抽象模型

3.3.4 状态不变量

3.4.1 验证对象评估

3.4.2 验证工作

3.4.3 验证方法对比分析

3.5 本章小结

第四章任务管理的验证方法研究

4.1 概述

4.1.1 所面临的挑战

4.1.2 解决方法

4.2 任务管理模块分析

4.2.1 数据结构分析

4.2.2 调度行为分析

4.3 ARM汇编模型

4.4.1 任务管理的建模

4.4.2 任务管理的验证实例

4.5 验证对象评估

4.6 本章小结

第五章可信执行环境设计与安全性验证

5.1 概述

5.1.1 TEE 攻击模型

5.1.2 TEE 设计及验证计划

5.2 基于TrustZone的TEE 设计

5.2.1 TEE 多级架构

5.2.2 安全通道设计

5.2.3 不同TEE 设计架构对安全性验证工作的影响

5.3验证挑战与解决方法

5.3.1 TEE 调度程序验证

5.3.2 端到端的安全性验证

5.4 端到端的安全性验证框架

5.4.2 实现层状态机m的安全属性建模验证

5.4.3 集成验证系统

5.5 TEE 监控模块的安全性验证

5.5.1 API的正确性验证

5.5.2 无干扰性建模与验证

5.6.1 验证工作

5.6.2 TEE 性能评估

5.6.3 TEE 安全性评估

5.6.4 TEE 设计与验证方法对比分析

5.6.5 集成验证系统与现有验证系统的对比分析

5.7 本章小结

第六章总结与展望

6.1全文总结

6.2未来工作展望

致谢

参考文献

攻读博士学位期间取得的成果