论文部分内容阅读
近年来随着嵌入式设备的日益普及,嵌入式软件的安全性越发显得重要。在一些关键领域,如航天、医疗、军事、核能等,如果嵌入式软件存在程序漏洞,有可能导致程序在非正常状态运行,从而会带来灾难性的后果。为了解决这一类的可靠性问题,传统软件开发者通常会采用软件测试的方法去发现程序错误。但是,软件测试无法保证整个系统完全不存在缺陷。程序验证探寻一条逻辑验证为基础的解决软件安全性的道路。程序验证能够克服软件测试的一些固有缺点,能够证明程序严格地符合一定的性质,从而保证软件的可靠性。操作系统中的任务调度器由于其结构复杂而难以验证：首先任务调度器的代码涉及到诸多的复杂内核数据结构,在验证它们之前需要描述这部分内核数据结构的性质和它们相互之间应该满足的复杂关系；此外在任务调度过程中,内核需要保证调度策略的正确性,即选取具有最高优先级的就绪任务,然后通过任务上下文切换来保证高优先级的任务优先得到运行。本文以μC/OS-Ⅲ内核中的任务调度器为研究对象,选取与调度有关的核心代码,验证调度器代码满足优先调度最高优先级任务的性质。本文基于分离逻辑与SCAP验证理论,利用Coq辅助证明工具,通过定义机器模型、操作语义、逻辑断言以及推导规则等来构建验证框架。在验证框架,本文定义了内核数据结构和“优先调度最高优先级”的性质的逻辑描述,模块化地对内核代码进行推理,最终的验证结果保证μC/OS-Ⅲ任务调度器的满足可靠性的要求。本文主要贡献如下：(1)验证了μC/OS-Ⅲ任务调度器中的核心代码满足以下的关键性质：A.内存安全性、B.代码的功能正确性和C.优先调度最高优先级任务；(2)在证明辅助工具Coq中实现了整个验证框架和调度器核心代码的验证过程,所有定义和证明都可以接受机器的自动检查。