免费论文
收费论文
发表论文
我要投稿
设为首页 招标网
联系我们
经济学|管理学|法学|计算机|医学|教育|文学|政治|艺术|哲学|更多 经济学|管理学|法律|计算机|医学|教育|文学|政治|艺术|哲学|更多
 论文搜索
  推荐服务: 论文发表 收费论文
期刊论文格式
毕业论文格式
期刊论文范文
毕业论文范文
论文致谢
毕业论文答辩
开题报告
论文选题
英文摘要书写
模块化构造软件系统安全性证明的研究
中文名称: 模块化构造软件系统安全性证明的研究
全文提供: 购买充值卡,就可下载本篇论文全文  
论文编号: 3767764收藏本论文】【我的收藏】【我要投稿
英文名称: A Modular Approach on Building Certified Software System
学位类型: 博士毕业论文
作者: 涉及隐私,隐去***  作者本人请参看权力声明>>
导师: 涉及隐私,隐去***
毕业学校: 涉及隐私,隐去***
专业: 计算机软件与理论
毕业年份: 涉及隐私,隐去***
关键字: 软件安全 程序验证 汇编语言 携带证明的代码 模块化验证 计算机程序 软件开发
简介目录: 点击此处 免费索取本论文简介和目录>>
全文提供: 购买充值卡,就可下载本篇论文全文  

       论文发表:快速、低价、包过!发表论文就找论文天下

论文简介:计算机程序正逐步影响到人类社会的方方面面。无论在互联网还是个人电脑上,计算机程序的安全问题日益严峻。然而现实世界中的程序并不尽如人意,病毒肆虐,网络攻击防不胜防。这些问题都源于程序中潜伏着许多错误,其中一个小的错误有可能会导致整个软件系统的崩溃。而在诸多关键的领域,例如核反应堆、航天飞机的控制系统等等,计算机程序的半点闪失都将带来不可计数的惨痛损失。在软件开发过程中使用形式化的方法是提高软件质量的途径。在众多的形式化方法中,程序的静态验证是一种非常可靠的方法。 本文采用方法是在携带证明的代码的框架中静态地验证程序。所谓携带证明的代码是首先静态地验证代码的安全性,然后将这个验证的详细过程作为安全性证明附加在程序上。主机在运行程序前检查程序携带的安全性证明的正确性。如果安全性证明是正确的,那么说明程序满足主机的安全策略,可以安全地运行而不破坏主机上的软件系统。 本文首先在一个简单的验证框架中定义了程序、抽象机器、抽象机器的操作语义、安全,还有一个用来静态验证程序的推理系统。此框架可以用来构造简单的携带证明的代码。然而与以前的许多相关研究一样,此框架不能很好地支持模块化的程序验证。现实中的大量程序通常使用模块化的开发方式,模块化的开发方式可以把一个复杂的程序分解为若干个小的模块,不同的模块分别被开发,最后这些模块可以被链接到一起从而构成完整的程序。模块性在软件工程方面占有重要的地位。程序静态验证也应该具备模块性,即不同模块的验证可以分别进行,然后链接成为完整的安全性证明。另一方面,一个程序的不同模块可能是不同风格的代码,难以使用同一种验证推理系统去验证所有的模块。 本文在简单验证框架上进行扩展,使之支持模块化验证。在此模块化框架中不同的模块可以分开进行验证,并分别得到各自的安全性证明,模块在链接的同时安全性证明也被链接到一起,从而得到整个程序的安全性证明。而且此框架支持不同的模块使用不同的验证逻辑进行验证。框架的特点是采用一个抽象的程序推理系统,它支持良好的模块验证。多个验证推理系统可以被统一嵌入到这个抽象的程序推理系统中。通过采用这种方法,一个模块不管使用哪些推理系统进行验证,只要这个验证推理系统可以被嵌入到抽象层次上,那么这个模块的安全性证明就可以被转换成抽象的推理系统中的安全性证明。本文研究了如何将一个支持控制栈推理的验证推理系统嵌入到验证框架中,并移植了一个已有的动态内存分配模块。同时本文还研究了如何将一个类型化的验证推理系统嵌入到验证框架中,并验证了一个小的调用动态内存分配的模块。最后本文介绍了如何将两个使用不同的推理系统验证的模块连同安全性证明链接到一起。 本文还研究了框架中的各个模块的安全性证明产生的自动性问题。本文不仅提出了验证推理系统SCAP中的验证条件生成器,而且提出了验证推理系统TALP的类型检查器。通过验证条件生成器与类型检查器的可靠性证明,模块的安全性证明的构造过程被大大简化。有利于验证规模较大的模块。 文中所有的形式化定义,形式化描述以及证明都已使用的定理辅助证明工具Coq实现。因此所有的证明,包括框架的性质证明,示例程序的安全性证明的正确性可以使用机器自动检查。 本文的工作虽然是对模块化验证框架的研究的初步探索,但是本文中的验证框架所表现出的良好的模块性为大规模程序的安全性验证带来良好的应用和研究前景。
本类相关论文:
·LAMOST二维光谱数据处理方法研究与软件开发
·基于模型的汽车电子软件综合方法研究
·工作流模型若干问题的研究及其在广电运营系统中的
·工程优化设计网格的关键技术研究及其应用
·面向服务突现的整体智能模型及其应用研究
·.NET和分布式(网络)数据库集成技术支持下的
·面向方面技术在大规模嵌入式软件中的应用
·面向数字化仪器设备的嵌入式软件应用框架研究
·复杂流程分布式控制系统构件研究与模型变换
·文本信息人工标注辅助系统的设计与实现
软件安全论文 程序验证论文
·基于虚拟机的关键信息提取与分析
·基于故障注入的软件安全测试技术研究
·基于专家系统的恶意代码检测
·用形式化方法构建安全的线程机制
·基于模拟器的缓冲区溢出漏洞动态检测技术研究
·指针程序的分析以及循环不变形状图的推断
·有限元法在略阳电厂边坡稳定性分析中的应用与研究
·程序验证与系统分析中的若干符号计算问题
·面向多核处理器的低级并行程序验证
·用于指针逻辑的自动定理证明器的设计与实现
汇编语言论文 计算机程序论文
·智能型港口起重机用力矩限制器的研究
·低级并行代码中几种同步机制的验证
·基于汇编语言的控制流错误检测算法研究
·汇编语言学习支撑平台的设计与实现
·基于虚拟寄存器的中间语言
·论计算机程序中思想与表达的界限
·论计算机软件的专利保护
·新技术条件下的专利权客体
·兰营徐采场最优开采深度的研究
软件开发论文  
·河流沉积微相自动识别方法研究与算法设计
·三高气田钻柱设计
·精密控制震源发射信号设计和信号提取方法研究
·航天轴承的故障诊断的方法研究及系统开发
·船舶复杂推进轴系扭振机理及计算软件研究
 
  推荐期刊投稿
·中国药物与临床
·广播歌选
·怀化医专学报
·绿风
·护理管理杂志
·实用口腔医学杂志
·房地产导刊
·中国仪器仪表
·沈阳农业大学学报
·浙江大学学报(理学版)
 
·中国图象图形学报
·红豆
·语文研究
·小溪流(成长校园)
·海军航空工程学院学报
·油气储运
·新疆新闻出版
·医药保健杂志
·中国乡镇企业会计
·建筑热能通风空调
 
·南京工程学院学报(自然科学版)
·改革与理论
·社会
·池州学院学报
·浙江国际海运职业技术学院学报
·中国林业
·曲阜师范大学学报(自然科学版)
·农业经济
·石油教育
·现代教育科学
   免费论文
公共管理 | 法学 | 理学 | 医药学
政治 | 社会学 | 文学 | 艺术 | 哲学
工学 | 计算机 | 文化 | 英语论文
经济学 | 财政 税收 | 证券金融
管理学 | 会计审计 | 工商管理 | 教育
财务管理 | 论文写作指导 | 应用文
   收费论文
马列毛邓 | 哲学宗教 | 社会科学
政治法律 | 军 事 | 经 济
文化科学教育体育 | 语言文字
文学 | 艺术 | 历史地理 | 自然科学
数理化 | 天文 | 生物科学 | 医药卫生
农业科学 | 工业技术 | 交通运输
航空航天 | 环境安全
   浏览历史

联系论文网 | 收费论文 | 发表论文 | 论文翻译 | 友情链接 | 全部分类 | 网站地图 | 期刊导航
版权所有 2008-2018 论文天下 www.lunwentianxia.com 京ICP备08104503号