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

来源 :中国科学技术大学 | 被引量 : 0次 | 上传用户:seuarchi
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
并行系统的安全性随着其流行程度的增加,显得日益重要。以往在这方面大多数研究的重点是,在并行机制的实现(OS,线程库)已经安全的假定下,如何保证并行程序本身的安全性。对于如何保证并行机制本身的安全性,目前的解决方案不是不完整,就是非常复杂。到了如今,大多数并行机制的实现者仍然主要依赖传统的动态测试方法。为了探索如何用形式化验证的方法来保证并行机制本身的安全,本文中设计了一个类似GNU pth library的用户级别线程库,并用类MIPS的汇编语言编写了它的一个实现。与通常的线程库不同的是,该线程库携带了安全规范及其证明。这些规范与证明保证,如果用户程序对该线程库API的调用始终满足规范,那么线程库的代码必然可以安全执行。更重要的是,从这些规范与证明不仅能得到线程库本身的安全性,还能得到线程库和用户程序交互的安全性。为了让本文的验证方法可以用于更复杂的代码,文中还提出了一些简化程序规范和降低证明代价的方法。本文中的所有形式化工作,都是在证明辅助工具Coq上完成的。对于本文提出的线程库,其安全性证明可以用机器检查。而该线程库的安全性,仅仅依赖于证明检查工具的正确性,这意味着它是一个携带证明代码包(PCC package),可以直接用于对安全性要求非常高的场合。
其他文献
学位
随着网络的普及和数据库技术的快速发展,信息量呈现出爆炸式增长。大量数据中潜藏着无数有价值的信息,如何挖掘利用这些信息成为当今数据挖掘领域研究热点。贝叶斯分类算法以
本文主要研究了定性仿真建模和定性仿真平台原型实现问题。定性仿真理论自上世纪七八十年代被提出以来,逐渐成为系统仿真和人工智能领域的研究热点,越来越受到科研人员和工程
伴随着多媒体和网络技术的发展和广泛应用,多媒体信息的内容保护已经成为人们关注和亟待解决的问题。数字图像作为一类非常重要的多媒体信息,它的版权保护和内容认证受到了广
经过近十几年的发展,架构设计已经成为软件工程领域一门重要的学科。在一个软件项目设计之初,首先进行体系架构设计已经成为广大软件开发人员的共识。但大多数项目只是停留在
桌面网格是一种由桌面PC机组成的网格,具有结构更复杂、动态性更强等特点。充分利用桌面网格的空闲计算能力可以为大规模计算提供一种廉价和便捷的解决方案,其关键是如何把任
本文研究了基于P2P网络视频监控末梢终端,以及为保护传输数据安全的编码路径保护技术。首先,针对当前互联网范围内的网络图像传输设计的现状与不足,解决协调访问终端和图像压
在抄表系统中,嵌入式系统的引入及其应用己经成了一个新的发展热点问题。而嵌入式操作系统的应用是近年来嵌入式系统向高端发展的趋势。嵌入式操作系统负责嵌入式系统的全部
目前逆向工程已经成为实现产品再创新开发及快速制造的重要技术之一,其在汽车、家电、模具、娱乐和医疗等行业具有广阔的应用前景。作为逆向工程中数据模型的一种重要的表现
近年来,随着DHT(分布式哈希表)的发明,各种大规模高容错的分布式系统在实际应用中变得十分普遍。基于DHT的各种应用需求也随之应运而生,例如一些基于DHT的数据库系统就具有复