微内核操作系统互斥量模块功能正确性的形式化验证

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑，操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障，造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生，对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误，因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中，互斥量可协调多任务对资源的访问，是一种常用的任务同步方式，其功能正确性对于保障多任务应用的正确性十分关键.本文基于定理证明方法，在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模，给出其接口函数的形式化规范，并实现这些接口函数的功能正确性验证.     

空间数据库管理系统VISTA的强制访问控制设计

对象关系型数据库安全访问控制是数据库安全研究的焦点之一。本文以自主开发的空间数据库管理系统VISTA为例,从安全规则、安全属性、强制访问控制三个角度详细讨论了VISTA的MAC设计方法,定义了形式化的安全规则,给出了算法流程和相应的安全信息数据结构。该设计方案也适用于其他相似的对象关系型数据库系统。     

汇编级顺序语句块的自动形式化规约及其验证

软件的形式化验证是保障软件可证明性、可靠性和安全性的重要手段,但传统形式化验证脚本的生成过程复杂且需要形式化验证专家的大量手工验证。为提高证明效率,构建一种自动证明模型,并在此基础上提出语义自动规约算法以及对所规约的语义自动生成证明脚本的算法。利用C++和Python并通过交互式定理证明器Isabelle 2017在基准数据中随机选择10个程序进行测试,结果表明,与完全人工操作相比,该算法具有较高的验证效率,可实现顺序语句块的自动化规约与验证。     

基于C级数据库管理系统的强制访问控制模块的设计

我国现在使用的大多是国外研制的C类数据库管理系统，均采用自主访问控制产品，其安全性较低，数据库强制访问控制模块是为提高C级数据库管理系统的安全性而设计，它外挂于数据库管理系统之上，可以增强系统的安全性．     

在基于角色的安全系统中实现强制访问控制

本文讨论了在基于角色的安全系统中实现强制访问控制的问题。首先介绍了角色的基本概念及在安全系统中的应用和MAC（强制访问控制）的基本概念,然后给出了一个利用角色机制实现强制访问控制的方法。这种方法源于利用角色可以方便的访问某些特定的信息上下文,通过将每个角色上下文处理的为独立的安全级并施行非循环信息流要求,实现了强制访问控制,还提出了一个阻止特洛伊木马的方法。     

基于Coq的Paxos形式化建模与验证

Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.随着Paxos在大型分布式系统中的广泛运用,比如区块链系统以及谷歌文件系统等,其安全性证明越来越重要.在定理证明工具Coq中,形式化描述和定义了Lamport的BasicPaxos算法,并且证明了其满足共识性.     

支持协作的强制访问控制模型

按照国家信息系统等级保护要求,3级以上的信息系统必须具备强制访问控制和标记.已有的强制访问控制模型的访问规则十分严格,难以满足协作环境下的访问控制新需求. 提出一种支持协作的强制访问控制模型(collaboration supported mandatory access control model, CSMAC),将主体-客体为中心的访问控制与任务为中心的访问控制相结合,使访问控制模型更符合主动安全模型的特点,大大提高了模型的灵活性,使其更适合于协作环境下的访问控制. 模型中通过控制主客体的安全标记,解决了符合安全策略的敏感信息的双向流动问题. 通过无干扰理论,对所提出模型的安全性进行了证明.     

XML数据库强制访问控制策略研究

本文提出了一种实施在本源XML数据库中的通用强制访问控制策略,它允许数据库系统安全员定义标签结构和标签访问规则,可以满足不同应用领域的安全需求。该策略基于XML模式技术,为电子商务等领域提供了技术支撑。最后讨论了在数据库中实现该策略的整体框架。     

基于Z3的Coq自动证明策略的设计和实现

形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高,而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.本文结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减轻用户手动验证程序的开销.     

通用软件封装器在Linux中强制访问控制的实现

基于Linux系统设计并实现的通用软件封装器是一个可实现多种安全措施的通用平台,如访问控制、入侵检测等.重点阐述了利用通用软件封装器在Linux中实现强制访问控制的机制,并与SELinux进行了详细的比较.给出了实验结果并进行了分析,结果达到预期目的.     

数据库访问控制模型分析

综合分析比较了几种数据库访问控制模型:自主访问控制(DAC),强制访问控制(MAC)和基于角色访问控制(RBAC)。DAC主要根据访问者身份或访问者所属工作组来进行访问控制,MAC是基于被访问信息的敏感程度,而RBAC则是控制对象角色,而不是个人。通过具体模型分析,可以得出尽管RBAC模型仍有些局限,但RBAC模型与传统访问控制模型相比更具优异性,并会在复杂环境中得到更广泛的应用。     

多旋翼飞控推进子系统的Coq形式化验证

飞行器需要高可靠的飞行控制系统软件(飞控)来控制其运行.在传统开发模式下,先由人工将领域知识描述为自然语言形式的模型,再根据模型手动编写代码,然后使用软件测试技术来排除软件错误,这种模式由于人工易出错、自然语言存在二义性、测试技术的不完备性,导致难以构建出高可靠的飞控软件.基于形式验证技术的新型软件开发方法可从多方面提高飞控系统的可靠性.使用Coq定理证明器对全权提出的多旋翼飞控推进子系统进行了完整的形式验证,生成了一个可用的高可靠函数式软件库.主要工作有:首先将领域知识整理为具有层次结构以适合进行形式验证的文档,分离了基本函数和复合函数,并提出最简形式函数概念;再根据该文档进行形式化描述,定义常量、变量、基本函数、复合函数、最简形式函数和公理等;其次对各类导出函数的推导正确性建立为引理并予以证明;再次对多旋翼最长悬停时间等实际问题给出了求解算法;最后利用Coq程序抽取功能生成了OCaml语言的函数式软件库.后续将对飞控更多子系统进行基于形式验证的开发,并最终建立完整的经形式化验证的高可靠飞控系统.     

操作系统形式化设计与验证综述

对操作系统的形式化设计和验证的概念进行介绍,描述其框架和基本方法。比较和分析操作系统宏内核和微内核结构,调查多个设计和验证项目,阐述项目的验证目标、方法、优缺点和进展情况。在总结研究现状的基础上,分析和展望操作系统形式化设计和验证的发展趋势,从操作系统模型设计、验证工具、代码实现和验证重用等方面给出形式化设计和验证的思路。     

一种基于分离逻辑的块云存储系统验证工具

云存储技术目前被广泛应用于人们的生产与生活中.验证云存储系统中管理程序的正确性,能够有效地提高整个系统的可靠性.块云存储系统(CBS)具有最接近底层的存储架构.运用交互式定理证明器Coq,实现了一种辅助验证工具,用于分析和验证CBS中管理程序的正确性.基于分离逻辑的思想,对工具中证明系统的实现主要包括:首先,将CBS抽象为两层堆结构,定义建模语言形式化表示CBS的状态和管理程序;其次,定义描述CBS状态性质的堆谓词,并说明堆谓词间的逻辑关系;最后,定义描述程序行为的CBS分离逻辑三元组,以及制定验证三元组所需的推理规则.此外,还引入了几个证明实例,以此展示工具对实际CBS管理程序表示和推理的能力.     

物联网应用中访问控制智能合约的形式化验证

蓝牙、WiFi等网络技术的进步推动物联网(IoT)的发展,然而IoT在方便了人们生活的同时也存在严重的安全隐患.若无安全的访问控制,非法接入IoT的访问可能给用户带来各方面的损失.传统的访问控制方法需要一个可信任的中心节点,不适合节点分散的IoT环境.区块链及智能合约的出现为IoT应用的访问控制提供了更有效的解决方案,...     

基于Coq的分块矩阵运算的形式化

矩阵是工程领域中常用的一种数据结构,在深度学习领域,矩阵乘法是神经网络训练中的核心技术之一.面对大型矩阵的运算问题,分块矩阵技术可将大矩阵运算转换为小矩阵运算以实现并行运算,并且能够大幅度减少矩阵运算步骤并且提高矩阵运算速度.首先对目前学术界的矩阵形式化工作进行了系统总结,并且分析了矩阵形式化的主要几种方法;其次介绍并...     

基于静态分析的强制访问控制框架的正确性验证

现阶段对操作系统的强制访问控制框架的正确性验证的研究主要集中于对授权钩子放置的验证.文中基于TrustedBSD MAC框架对强制访问控制框架的正确性验证问题进行了研究,在授权钩子放置验证的基础上,提出了安全标记的完全初始化验证和完全销毁验证.为了实现上述验证,文中提出了一个路径敏感的、基于用户自定义检查规则的静态分析方法.该方法通过对集成于编译器的静态分析工具mygcc进行扩展来验证强制访问控制框架的钩子放置的准确性和完备性.该方法具有完全的路径覆盖性.且具有低的误报率和时间开销.     

基于Coq的杨忠道定理形式化证明

实现拓扑学定理的机器证明,是吴文俊院士生前的宿愿.杨忠道定理涉及一般拓扑学中的诸多基本概念,对深刻理解拓扑空间的本质有重要意义.该定理表明,拓扑空间中每一个子集的导集为闭集当且仅当此空间中的每一个单点集的导集为闭集,是一般拓扑学中的一个重要定理.基于定理证明辅助工具Coq,从公理化集合论机器证明系统出发,对一般拓扑学中的开集、闭集、邻域、凝聚点和导集等拓扑基本概念进行形式化描述,给出这些概念基本性质的形式化验证,建立了拓扑空间的形式化框架.在此基础上,实现基于Coq的杨忠道定理形式化证明.全部引理、定理和推论均完整给出Coq的形式化描述和机器证明代码,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.杨忠道定理的形式化证明是一般拓扑学形式化内容的一个深刻体现.     

FreeBSD的强制访问控制简介

随着信息安全技术的不断提升,强制访问控制作为一种安全手段,会成为现在重要的一个控制手段。采用操作系统提供的强制访问控制对操作系统内部的程序和用户进行控制,可以很好地保证系统中的各个资源在被控制的环境中有序执行,从而提高系统的安全性。