学位论文 > 优秀研究生学位论文题录展示

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

作　者: 王海波
导　师: 陈意云
学　校: 中国科学技术大学
专　业: 计算机应用技术
关键词: 软件安全线程的动态创建和退出程序验证多线程汇编代码
分类号: TP311.53
类　型: 硕士论文
年　份: 2009年
下　载: 29次
引　用: 0次
阅　读: 论文下载

内容摘要

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

全文目录

摘要  4-6
Abstract  6-10
第1章绪论  10-20
  1.1 引言  10-12
  1.2 形式程序验证和PCC 技术  12-16
    1.2.1 安全领域基本原则  12
    1.2.2 程序验证  12
    1.2.3 经典Hoare 逻辑  12-13
    1.2.4 携带证明的代码  13-14
    1.2.5 基础的携带证明的代码  14-15
    1.2.6 验证汇编程序设计CAP  15-16
  1.3 研究现状  16-18
    1.3.1 Rely-Guarantee 方法  16
    1.3.2 CMAP 方法  16-17
    1.3.3 并发分离逻辑  17-18
    1.3.4 AIM 验证框架  18
  1.4 本文概述  18-20
    1.4.1 主要贡献  18-19
    1.4.2 章节安排  19-20
第2章验证框架  20-38
  2.1 元逻辑  20-21
  2.2 Coq 辅助定理证明工具  21-22
  2.3 目标机器模型  22-25
    2.3.1 讨论  25
  2.4 领域相关逻辑理论与技术  25-26
  2.5 开放式验证汇编编程框架OCAP  26-28
  2.6 基于栈的控制流的模块化推理方法SCAP  28-30
  2.7 AIM 验证框架  30-32
    2.7.1 AIM 框架的逻辑系统  30
    2.7.2 AIM 框架的内存模型  30-32
  2.8 本文的扩展验证框架  32-38
    2.8.1 线程的创建与退出  33-34
    2.8.2 扩展框架的内存模型  34-35
    2.8.3 扩展框架中的目标机器模型与抽象机器模型  35
    2.8.4 扩展框架的逻辑系统  35-38
第3章扩展框架的可靠性证明  38-49
  3.1 扩展框架的抽象机器模型  39-41
  3.2 扩展框架的推理规则  41-44
  3.3 虚拟指令的规范  44-46
  3.4 扩展框架的可靠性证明  46-47
  3.5 验证举例  47-49
第4章 Coq 实现  49-57
  4.1 Coq 工具  49
  4.2 机器模型  49-51
  4.3 OCAPLITE 推理方法  51-52
  4.4 分离逻辑  52-54
  4.5 抽象机器模型  54-55
  4.6 SCAP 推理方法  55
  4.7 讨论  55-57
第5章相关工作比较  57-61
  5.1 Mth  57-59
  5.2 CTL  59-60
  5.3 Verisoft XT  60-61
第6章结束语  61-63
  6.1 文章总结  61-62
  6.2 后续工作展望  62-63
参考文献  63-67
致谢  67-68
在读期间发表的学术论文与取得的研究成果  68

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

内容摘要

全文目录

相似论文