验证带有线程动态创建和退出多线程程序

摘要

随着计算机硬件平台运算能力的不断提升，计算机软件的规模及复杂度日益增长，同时软件安全性问题也日益突出。如何解决软件安全性，已然成为目前计算机工业领域与研究领域关注的热点问题。当前软件主要依靠安全的程序设计语言与软件测试来提高软件的可靠性。然而安全的程序设计语言，如Java、C＃等提供的众多安全特性都依赖于其运行环境；软件测试则很大程度依赖于测试者的能力，且软件测试有着与生俱来的不完备性，测试用例很难覆盖软件使用时所遇到的全部情况，因此经过测试的软件依然可能存在着安全隐患。程序验证是计算机研究领域针对解决软件安全性问题，从而构建高可信软件提出的一种应对方案。程序验证中使用形式化的方法对软件进行验证，形式化的方法基于数学的特种技术，因此程序验证具有完备性和可靠性，经过程序验证为安全的软件，安全性具有极高的可信度。综上所述，为了提高软件的安全性和可靠性，使用程序验证的方法验证软件的安全性具有重要意义。
　　 在目前的软件开发中，多线程技术大量应用，为研究如何验证应用多线程技术的软件的安全性，本文使用程序验证的方法对带有线程动态创建和退出操作的多线程程序的安全性进行验证。本文的工作使用基于携带证明的代码技术，使用Hoare逻辑的汇编语言级形式化程序验证方法(CAP)，提出了一种验证带有线程动态创建和退出的多线程程序的验证框架。该验证框架包含抽象机模型、指令规范、逻辑推理系统、验证框架的可靠性定理及证明。本文的具体工作，包括验证框架的形式化定义以及验证框架的可靠性证明，是在计算机辅助定理证明工具Coq(Coq Development Team，2008)中实现的，这些实现是计算机可检查的，从而保证了整个验证框架的严格性和可靠性。
　　 通过验证工作，本文研究了多线程程序在线程的动态创建和退出中出现的问题，特别是内存划分的改变及内存的初始化和销毁。同时，本文还介绍了这些工作在计算机辅助定理证明工具Coq中的实现，包括如何在Coq中定义数据结构、机器指令等，以及Coq证明中的难点。
　　 本文的工作是对原有的AIM验证框架的扩展，主要贡献和创新包括：1）通过对线程的动态创建和销毁机制进行研究，扩展框架在运行时系统及并发用户代码部分都形式化的给出了线程动态创建和销毁的规范，并在原框架中加入显式的内存推理机制，从而提出了一个推理带有线程动态创建和销毁机制多线程程序的方法；2）提出了对程序内存划分的显式的推理机制，该机制可用于验证底层程序的内存划分；3）使用计算机辅助定理证明工具Coq实现了框架的形式化定义及可靠性证明。
　　 本文的工作是在原有工作基础上对证明操作系统做出的进一步尝试。操作系统包含虚拟存储，地址映射，硬件驱动等诸多机制，尽管本文的扩展框架模型与真实的操作系统内核还存在着差距，但是本文工作为验证操作系统内核提供了一种途径。同时，本文也为汇编语言及程序的形式验证，特别是为携带证明的代码的技术的应用积累了重要的理论和实践经验。