共查询到19条相似文献,搜索用时 70 毫秒
2.
3.
操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误,因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中,互斥量可协调多任务对资源的访问,是一种常用的任务同步方式,其功能正确性对于保障多任务应用的正确性十分关键.本文基于定理证明方法,在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模,给出其接口函数的形式化规范,并实现这些接口函数的功能正确性验证. 相似文献
4.
以μC/OS-Ⅲ内核中的任务调度器为研究对象,选取调度相关的核心代码,验证调度器代码满足优先调度最高优先级任务的性质。基于分离逻辑与SCAP验证理论,利用Coq辅助证明工具,通过定义机器模型、操作语义、逻辑断言以及推导规则构建验证框架。在验证框架中,定义内核数据结构和内核相关性质的逻辑描述,模块化地对内核代码进行推理。验证结果表明,μC/OS-Ⅲ任务调度器满足可靠性要求,并且可以通过机器的自动检查。 相似文献
5.
《计算机应用与软件》2017,(11)
定理证明是形式化验证的主要方法之一,其中定理证明器的使用是难点。为了提高证明效率,论述HOL4系统中主要的三种证明方法:支持高级证明步骤。自动推理和化简器,为定理的证明提供了一个完整而通用的理论框架。详细说明了以上三种证明方法的相关对策的功能和应用环境,并为应用中可能出现的问题提出解决方案。给出的对策应用实例不仅体现了三种方法中相关对策的实用性,还进一步表明了提出解决方案的有效性。 相似文献
6.
7.
强制访问控制是保护数据库管理系统安全的有效机制.DMOSMAC是一个依赖于安全操作系统实现强制访问控制机制的数据库管理系统.在分析该系统实现的基础上,对该系统进行了形式化分析.给出了信息流的概念,将信息流集合作为被验证系统状态的一部分.信息流集合始终是一个递增的集合,利用信息集合流可防止删除等操作的证明被绕过的可能,保证验证过程的严密性.在信息流的基础上提出了一种对系统代码进行抽象、抽取的形式化分析方法.即抽象DMOSMAC系统状态,从源代码中提取操作规则,将BLP模型中的状态、访问规则分别与DMOSMAC系统的状态、操作规则建立映射关系,BLP模型中简单安全性和*-特性转换为面向信息流的状态不变式,继承BLP模型的相关安全公理和定理进行分析和证明;最后用定理证明器COQ进行安全性证明的方法. 相似文献
8.
形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高,而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.本文结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减轻用户手动验证程序的开销. 相似文献
9.
10.
区域覆盖算法广泛用于群机器人解决资源勘查、目标搜救、地形测绘等问题.目前,对区域覆盖算法的研究主要是用传统计算机仿真和数值计算方法对算法模型进行测试,然而,软件系统缺陷可能会使测试结果出现偏差,导致任务失败.因此,本文采用定理证明的形式化方法,基于交互定理证明器HOL-Light中集合库、实分析库等定理证明库,实现了群... 相似文献
11.
介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入应用所面临的问题和解决方向. 相似文献
12.
13.
并行程序验证的复杂性在于执行流程的不确定性以及由此导致的执行规模变大,使得验证的内容和目标之间的关系不明确。为解决该问题,提出一种基于隔离逻辑的并行程序可靠性验证方法。通过变量的执行关系图,描述变量相关的语句及执行关系,将所需验证的程序性质逻辑式转换为变量并行语句序列的逻辑组合式,使得性质表达式与并发程序的语句相关联。根据逻辑组合式确定语句执行序列和前后件逻辑表达式,基于并发隔离逻辑的公理系统对语句执行序列进行验证,并根据验证结果对并发程序进行修改和完善。通过对银行柜台业务办理的功能模块验证结果表明该方法是有效的。 相似文献
14.
When it comes to data storage, cloud computing and cloud storage providers play a critical role. The cloud data can be accessed from any location with an internet connection. Additionally, the risk of losing privacy when data is stored in a cloud environment is also increased. A variety of security techniques are employed in the cloud to enhance security. In this paper, we aim at maintaining the privacy of stored data in cloud environment by implementing block-based modelling to boost the privacy level with Anti-Codify Technique (ACoT) and block cipher-based algorithms. Initially, the cipher text is generated using Deoxyribo Nucleic Acid (DNA) model. Block-cipher-based encryption is used by ACoT, but the original encrypted file and its extension are broken up into separate blocks. When the original file is broken up into two separate blocks, it raises the security level and makes it more difficult for outsiders to cloud data access. ACoT improves the security and privacy of cloud storage data. Finally, the fuzzy-based classification is used that stores various access types in servers. The simulation results shows that the ACoT-DNA method achieves higher entropy against various block size with reduced computational cost than existing methods. 相似文献
15.
基于逻辑程序的安全协议验证 总被引:5,自引:1,他引:4
安全协议本质上是分布式并发程序,可以自然地描述为多个子进程的并发合成系统.将安全协议对应的并发合成系统抽象为逻辑程序进行消解,能够对安全协议无穷多个会话的交叠运行进行验证.该文提出了安全协议逻辑程序中逻辑规则的一个分类方法,基于该分类方法提出了安全协议逻辑程序不动点的迭代计算方法.逻辑规则的分类优化了安全协议逻辑程序不动点的迭代计算和安全性质验证过程中的计算.由于安全协议逻辑程序不动点迭代计算过程不一定终止,文中提出了每进行k≥1步安全协议逻辑程序不动点迭代计算验证一次安全性质的验证策略. 相似文献
16.
17.
18.
云存储是由云计算提供的一个重要服务,允许数据拥有者将数据远程存储到云服务器上,同时又能够从云服务器上便捷、高效地获取这些数据,没有本地存储和维护数据的负担。然而,这种新的数据存储模式也引发了众多安全问题,一个重要的问题就是如何确保云服务器中数据拥有者数据的完整性。因此,数据拥有者以及云存储服务提供商亟需一个稳定、安全、可信的完整性审计方案,用于审核云服务器中数据的完整性和可用性。不仅如此,一个好的数据完整性审计方案还需满足如下功能需求:支持数据的动态操作,包括插入、删除、修改;支持多用户、多云服务器的批量审计;确保用户数据的隐私性;注重方案的执行效率,尽量减少数据拥有者和云服务器的计算开销与通信开销。为了促进云存储服务的广泛应用与推广,文章重点对云数据完整性审计方案的研究现状进行综述,描述云存储以及数据完整性审计的相关概念、特点,提出云计算环境下数据完整性审计模型和安全需求,阐述云存储数据完整性审计的研究现状,并重点分析部分经典方案,通过方案对比,指出当前方案存在的优点及缺陷。同时,文章还指出了本领域未来的研究方向。 相似文献
19.
目前,PACS系统已经日益成为各级医院实现信息化建设的重要组成部分,在网络应用越来越广泛的今天,异地多院区联接形成医院PACS系统对存储应用有更高的要求。文章从医院PACS系统存储的实例出发,探讨了基于云存储的PACS系统存储设计。 相似文献