用形式化方法构建安全的线程机制

发布时间：2020-11-11 14:58

　　 并行系统的安全性随着其流行程度的增加,显得日益重要。以往在这方面大多数研究的重点是,在并行机制的实现(OS,线程库)已经安全的假定下,如何保证并行程序本身的安全性。对于如何保证并行机制本身的安全性,目前的解决方案不是不完整,就是非常复杂。到了如今,大多数并行机制的实现者仍然主要依赖传统的动态测试方法。 为了探索如何用形式化验证的方法来保证并行机制本身的安全,本文中设计了一个类似GNU pth library的用户级别线程库,并用类MIPS的汇编语言编写了它的一个实现。与通常的线程库不同的是,该线程库携带了安全规范及其证明。这些规范与证明保证,如果用户程序对该线程库API的调用始终满足规范,那么线程库的代码必然可以安全执行。更重要的是,从这些规范与证明不仅能得到线程库本身的安全性,还能得到线程库和用户程序交互的安全性。为了让本文的验证方法可以用于更复杂的代码,文中还提出了一些简化程序规范和降低证明代价的方法。 本文中的所有形式化工作,都是在证明辅助工具Coq上完成的。对于本文提出的线程库,其安全性证明可以用机器检查。而该线程库的安全性,仅仅依赖于证明检查工具的正确性,这意味着它是一个携带证明代码包(PCC package),可以直接用于对安全性要求非常高的场合。
【学位单位】：中国科学技术大学
【学位级别】：硕士
【学位年份】：2009
【中图分类】：TP338.6
【文章目录】：
摘要
Abstract
第1章 绪论
    1.1 研究背景和意义
    1.2 研究现状
        1.2.1 基于类型系统的并发系统安全研究
        1.2.2 基于程序验证的并发系统安全研究
    1.3 本文工作与贡献
    1.4 章节安排
第2章 术语表
第3章 基本设定与主要技术
    3.1 归纳构造演算与证明辅助工具 Coq
        3.1.1 归纳构造演算
        3.1.2 证明辅助工具Coq
    3.2 抽象机器模型
    3.3 并发代码的推理方法
        3.3.1 假设-保证推理方法
        3.3.2 并发分离逻辑
    3.4 基于语法的携带基础证明代码
        3.4.1 携带基础证明代码
        3.4.2 用语法制导的推理规则描述程序逻辑
        3.4.3 抽象控制栈
        3.4.4 支持假设-保证推理方法
        3.4.5 携带证明代码模块的连接
第4章 一个简单的线程库
    4.1 API
    4.2 线程模型与基本数据结构
    4.3 实现简要
第5章 线程库的安全规范与证明
    5.1 证明方法
    5.2 接口规范
    5.3 实现规范
    5.4 实现规范的证明
    5.5 接口规范的证明
第6章 证明的简化
第7章 实用价值分析
    7.1 实用价值
    7.2 TCB 范围
第8章 相关工作比较
    8.1 Mth
    8.2 Verisoft XT
第9章 结论
参考文献
致谢
在读期间发表的学术论文与取得的其他研究成果

【相似文献】

相关期刊论文 前10条

1 胡恬;王宏;;原代码级的软件安全问题研究[J];软件导刊;2007年01期

2 羊建林;周安民;;Windows异常处理与软件安全[J];信息安全与通信保密;2011年04期

3 ;软件安全消费新观念[J];电脑采购周刊;1999年10期

4 丹三;;软件安全不容忽视[J];电脑采购周刊;1999年10期

5 ;开卷有益[J];计算机安全;2003年07期

6 吕华鹏;;软件反跟踪技术浅析[J];才智;2008年11期

7 王远景;;软件常见安全性缺陷与测试手段[J];科技创新导报;2009年28期

8 林洪，陈国良;并行系统的通讯效率问题[J];小型微型计算机系统;1996年01期

9 吕金和;;由指针和数组带来的软件安全性缺陷[J];计算机安全;2010年05期

10 赵妍;;计算机软件安全检测方法探讨[J];科技传播;2010年16期

相关博士学位论文 前10条

1 冯博;软件安全开发关键技术的研究和实现[D];北京邮电大学;2010年

2 王桂彬;大规模异构并行系统软件低功耗优化关键技术研究[D];国防科学技术大学;2011年

3 成斌;基于TCPN模型的并行系统性能分析方法研究[D];上海大学;2011年

4 郭宇;模块化构造软件系统安全性证明的研究[D];中国科学技术大学;2007年

5 王志芳;指针逻辑的扩展与应用[D];中国科学技术大学;2009年

6 石岩;凝视红外成像信息处理系统图像预处理方法与系统软件研究[D];华中科技大学;2005年

7 李隆;使用事务内存同步机制的并行程序验证的研究[D];中国科学技术大学;2008年

8 张秀峰;AOP技术及其在软件安全中的应用[D];北京邮电大学;2008年

9 葛琳;可信软件开发框架下的出具证明编译研究[D];中国科学技术大学;2007年

10 陈研;面向有状态应用的并行系统设计研究[D];上海交通大学;2007年

相关硕士学位论文 前10条

1 蒋信予;用形式化方法构建安全的线程机制[D];中国科学技术大学;2009年

2 翟宇;基于软件安全契约的AOP监控方法[D];吉林大学;2011年

3 贾景玺;有限元并行系统用于岔管计算的研究[D];兰州大学;2011年

4 邓凡;软件安全检查工具前端的设计与实现[D];西安电子科技大学;2009年

5 贾燕成;基于以太网并行系统实时仿真调度算法研究[D];云南大学;2012年

6 吴侃;星载并行系统主从式互连总线容错技术研究[D];国防科学技术大学;2011年

7 赵志威;基于加壳与加密技术的软件安全的研究[D];华中科技大学;2012年

8 王涛;基于安全模式的软件安全设计方法[D];吉林大学;2011年

9 刘艳;分布式网络并行系统在舰载指控系统中的应用研究[D];哈尔滨工程大学;2003年

10 杜洪伟;软件安全领域垂直搜索引擎的优化设计与实现[D];天津大学;2010年

本文编号：2879340