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

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

一种面向嵌入式操作系统的形式化验证方法

操作系统是整个计算机系统的核心与基石,其可靠性与安全性至关重要.操作系统的故障或漏洞可能会导致系统崩溃、数据丢失、隐私泄露和安全攻击等问题,特别是在安全攸关系统中,一旦操作系统发生错误,就可能会造成重大人员伤亡或财产损失.一直以来,如何保障操作系统的安全性和可靠性对学术界和工业界都是一个重大挑战.目前验证操作系统安全性的方法有软件测试、程序静态分析、形式化方法等.其中,形式化方法是最有潜力确保操作系统安全可信的方法,通过使用形式化方法,建立数学模型并进行系统的形式化分析和验证,从而发现潜在的错误和漏洞.在操作系统中,形式化方法可以用于验证操作系统的功能正确性、完整性以及系统安全性等.在已有的针对操作系统形式化验证的成果基础上,提出了一个面向嵌入式操作系统的形式化验证方案,采用VCC(verified C compiler)、CBMC(C bounded model checker)以及PAT(process analysis toolkit)工具分别对操作系统单元层面、模块层面和系统层面进行验证.该方法已成功应用到某操作系统的任务调度架构案例中,对于嵌入式操作系统的分析验证具有一定的通用性。

基于DH标定的机器人正向运动学形式化验证

DH坐标系在机器人运动学分析中发挥着重要的作用.在基于DH坐标系构建的机器人控制系统中,机器人结构的复杂性使得构建安全的控制系统成为一个难题,仅依靠人工方法可能导致系统漏洞和安全风险,从而危及机器人的安全.形式化方法通过演绎推理与代码抽取实现了对软硬件系统的设计、开发及验证.基于此,设计基于DH标定的机器人正向运动学的形式化验证框架.在Coq中构建机器人运动理论的形式化证明,并验证控制算法的正确性以确保机器人的运动安全.首先,对DH坐标系进行形式化建模,构建相邻坐标系间转换矩阵的形式化定义,并验证该转换矩阵与复合螺旋运动的等价性;其次,构建机械臂正向运动学的形式化定义,并对机械臂运动的可分解性进行形式化验证;再次,对工业机器人中常见连杆结构及机器人进行形式化建模,并完成正向运动学的形式化验证;最后,实现Coq到OCaml的代码抽取,并对抽取的代码进行分析与验证.

汽车电子控制系统安全设计的形式化验证

汽车电子控制系统已成为现代汽车的核心组成部分,因此,深入研究汽车电子控制系统安全设计和验证方法有助于提高车辆安全性能,增强车辆竞争力。本文阐述了汽车电子控制系统安全性的重要性,探讨了当前汽车电子控制系统安全设计和验证方法的局限性,以及汽车电子控制系统安全设计的形式化验证方法,形式化验证方法能够有效地在产品设计早期识别和消除潜在的问题和安全隐患,为汽车电子控制系统的安全设计和验证提供了新的思路。

复杂内核数据结构程序形式化验证

操作系统内核作为软件系统的基础组件,其安全可靠是构造高可信软件系统的重要环节,但是,在实际的验证工作中,操作系统内核中全局性质的不变式定义,复杂数据结构程序的形式化描述和验证仍存在很多困难.本文针对操作系统内核中满足的全局性质,在代码层以函数为单位,用全局不变式进行定义,并在不同的函数中进行形式化验证,从而证明各个函数符合操作系统内核的全局性质;针对操作系统内核中经常使用的复杂数据结构程序,本文通过扩展形状图理论,提出一种使用嵌套形状图逻辑的方法来形式化描述复杂数据结构程序,并对该方法进行了正确性证明,最终成功验证操作系统内核中关于任务创建与调度,消息队列创建与操作相关的代码.

拟态路由器BGP代理的设计实现与形式化验证

为确保拟态路由器中协议代理等“拟态括号”关键组件的安全性和功能正确性,设计实现了边界网关协议(BGP)代理,并采用形式化方法对BGP代理的安全性和功能正确性进行了验证。BGP代理通过监听邻居路由器与主执行体之间的BGP会话报文,模拟邻居路由器与从执行体展开BGP会话,实现各执行体的BGP状态一致。采用VeriFast定理证明器,编写基于分离逻辑的形式化规约,证明程序不会出现空指针引用等内存安全问题,并验证了BGP代理各功能模块实现的高级属性符合功能规约。BGP代理实现与验证代码量之比约为1.8:1,程序设计实现和程序验证所耗费的时间之比约为1:3。经过形式化验证的BGP代理处理100000条BGP路由所花费的时间为0.16 s,约为未经过验证的BGP代理的7倍。研究工作为应用形式化方法证明拟态防御设备与系统中关键组件的安全性和功能正确性提供了参考。

拟态路由器TCP代理设计实现与形式化验证研究

拟态路由器基于拟态防御的动态异构冗余架构进行设计,对于未知漏洞后门具有良好的防御能力。协议代理在拟态路由器中处于内外联络的枢纽位置,协议代理的安全性和功能正确性对于拟态路由器有着重要意义。本文设计实现了拟态路由器的TCP协议代理,并采用形式化方法,对其安全性和功能正确性进行了验证。TCP协议代理嗅探邻居和主执行体之间的TCP报文,模拟邻居和从执行体建立TCP连接,并向上层应用层协议代理提供程序接口。基于分离逻辑与组合思想,采用Verifast定理证明器,对TCP协议代理的低级属性,包括指针安全使用、无内存泄露、无死代码等,进行了验证;同时,还对TCP协议代理的各主要功能模块的部分高级属性进行了形式化验证。搭建了包含3个执行体的拟态路由器实验环境,对实现结果进行了实际测试,结果表明所实现的TCP代理实现了预期功能。TCP协议代理实现总计1611行C代码,其中形式化验证所需人工引导定理检查器书写的证明共计588行。实际开发过程中,书写代码实现与书写人工证明所需的时间约为1︰1。本文对TCP协议代理的实现与形式化验证工作证明了将形式化验证引入拟态路由器的关键组件开发中是确实可行的,且证明代价可以接受。

TrustZone中断隔离机制的形式化验证

TrustZone技术通过对硬件进行安全扩展,为软件提供了相互隔离的可信执行环境和通用执行环境.中断隔离机制是TrustZone的关键隔离机制,确保安全中断和非安全中断分别在可信执行环境和通用执行环境中被处理,该机制不正确可能导致安全中断被通用执行环境处理,从而影响可信执行环境的安全性.本文提出ARMv8 TrustZone架构中断隔离机制的形式化验证方法,在定理证明器Isabelle/HOL中建立包含中断隔离机制关键软硬件的形式化模型,该模型为状态迁移系统,包括中断处理程序、TrustZone Monitor、中断控制器等组件;在证明模型满足正确性的基础上,通过展开定理验证无干扰、无泄露、无影响等信息流安全属性,结果表明TrustZone中断隔离机制满足信息流安全属性,在中断处理过程中不存在隐蔽的信息流通道.

基于SMT的区域控制器同步反应式模型的形式化验证

在安全关键系统的软件开发过程中,形式化验证是一种经检验的提高软件质量的技术.然而,无论从理论上还是从应用角度来看,软件的验证都必须是完整的,数据流验证应该是对实现层软件模型进行验证的必要体现.因此,环境输入、泛型函数、高阶迭代运算和中间变量对于分析形式化验证的可用性至关重要.为了验证同步反应式模型,工程师很容易验证控制流模型(即安全状态机).现有工作表明,这类工作无法全面地验证安全关键系统的同步反应式模型,尤其是数据流模型,导致这些方法没有达到工业应用的要求,这成为对工业安全软件进行形式化验证的一个挑战.提出了一种自动化验证方法.该方法可以实现对安全状态机和数据流模型的集成进行验证.采用了一种基于程序综合的方法,其中,SCADE模型描述了功能需求、安全性质和环境输入,可以通过对Lustre模型的程序综合,采用基于SMT的模型检查器进行验证.该技术将程序合成作为一种通用原理来提高形式化验证的完整性.在轨道交通的工业级应用(近200万行Lustre代码)上评估了该方法.实验结果表明,该方法在大规模同步反应式模型长期存在的复杂验证问题上是有效的.

共识协议的形式化验证研究现状与展望

分布式系统在计算环境中发挥重要的作用,其中的共识协议算法用于保证节点间行为的一致性.共识协议的设计错误可能导致系统运行故障,严重时可能对人员和环境造成灾难性的后果,因此保证共识协议设计的正确性非常重要.形式化验证能够严格证明设计模型中目标性质的正确性,适合用于验证共识协议.然而,随着分布式系统的规模增大,问题复杂度提升,使得分布式共识协议的形式化验证更为困难.采用什么方法对共识协议的设计进行形式化验证、如何提升验证规模,是共识协议形式化验证的重要研究问题.对目前采用形式化方法验证共识协议的研究工作进行调研,总结其中提出的重要建模方法和关键验证技术,并展望该领域未来有潜力的研究方向.

基于健壮半径求解的循环神经网络形式化验证方法

随着软硬件技术的发展,神经网络在各行各业取得了广泛的应用,然而在应用过程中也暴露出健壮性的不足。因此,采用形式化的手段来检验和保障神经网络的安全性是至关重要的。然而,由于循环神经网络结构复杂、激活函数非线性等因素,目前关于这类神经网络的形式化验证工作非常有限。针对循环神经网络难于验证的问题,本文提出了VR-RRS,一种基于健壮半径求解的循环神经网络形式化验证方法。首先,基于神经网络验证的经典近似求解框架,通过逐层回溯迭代的方式得到循环神经网络各层神经元近似区间上下界关于输入的线性表达式,在此基础上利用赫尔德不等式推导出各层神经元的近似上下界关于扰动半径的解析解。随后,针对经典近似求解方法精度不高的问题,通过对激活函数的近似方式进行分析和优化,提出一种基于多路径回溯的求解策略。该策略以细粒度近似方法构造不同的回溯路径,在此基础上将这些回溯路径求解的近似区间取交集,能够得到更为精确的近似区间。最后,采用改进的二分法对健壮半径进行求解,主要针对经典二分法中精度不足的问题,优化了判断神经网络健壮性的标准。通过在不同结构的循环神经网络上与已有方法开展对比实验,结果表明了该方法在求解出的健壮半径和验证成功率上具有明显优势。

适用于形式化验证的断言优化方法

在实际工业验证场景中,形式化验证的局限性主要体现在因为状态空间爆炸导致验证结果不明确。断言编码方式始终是直接影响到形式化验证结果的主要因素,而目前已有的断言优化方法并未以断言与状态空间大小的关系分析为基础。文中针对影响锥模型不能分析断言中时序关系对状态空间的影响的问题,提出长序列模型,分析形式化验证中断言与状态空间大小的定性关系。在此基础上,提出适用于形式化验证的断言优化方法,方法包含断言逻辑化简、辅助验证逻辑、参考模型和断言禁用条件,并以某商用HDLC IP核为例,对比优化前后的验证结果,证明优化的有效性。

基于概率模型的Raft协议形式化验证

共识协议作为分布式系统的关键要素和核心组件,用于解决分布式场景下可能出现故障的节点间保证同一数据一致的问题,其准确性和高效性直接决定了系统的性能。Raft共识协议是目前分布式系统中常见且有效的算法。本文首先使用概率模型检测方法对Raft共识协议进行形式化建模,然后利用概率模型检测的属性规约技术对它的相关属性进行描述,最后通过模型检测工具验证并分析Raft共识协议的一致性和高效性。实验结果表明,Raft共识协议满足一致性,但是在领导者选举阶段,当跟随者维护的最新日志序号的差值范围增加时,选举回合数也会增多,使得整个服务周期选举时间增加,从而影响协议的执行效率。

L4虚拟内存子系统的形式化验证

第二代微内核L4在灵活度和性能方面极大地弥补了第一代微内核的不足,这引起学术界和工业界的关注.内核是实现操作系统的基础组件,一旦出现错误,可能导致整个系统瘫痪,进一步对用户造成损失.因此,提高内核的正确性和可靠性至关重要.虚拟内存子系统是实现L4内核的关键机制,聚焦于对该机制进行形式建模和验证.构建了L4虚拟内存子系统的形式模型,该模型涉及映射机制所有操作、地址空间所有管理操作以及带TLB的MMU行为等;形式化了功能正确性、功能安全和信息安全三方面的属性;通过部分正确性、不变式以及展开条件的推理,在定理证明器Isabelle/HOL中证明了提出的形式模型满足这些属性.在建模和验证过程中,发现源代码在功能正确性和信息安全方面共存在3点问题,给出了相应的解决方案或建议.

形式化验证在加速动态仿真过程中的应用

阐述在验证芯片复杂场景的过程中,往往会由于激励的仿真时间过长或随机化程度不够,从而丢失掉部分的边界情况。形式化验证是一种通过数学的方式来对待测设计进行验证的方法,可以对模块的接口信号进行遍历,从而覆盖其约束范围内所有场景。通过形式化属性验证,对SoC中的轮询仲裁器模块进行验证,通过其得到的违例结果,反向指导SoC制造相应的激励,缩短了寻找边界场景的时间,大大提高了验证效率。

CTCS-3级列控系统规范的建模与形式化验证方法研究

CTCS-3级列控系统规范是CTCS-3级列控系统设计与开发的基础,是实现互联互通以及确保系统高效率与安全性的关键环节。然而,依靠经验与直觉制定的规范不可避免地存在某些漏洞或者安全隐患,因此对CTCS-3级列控系统规范进行建模与形式化验证显得十分必要。本文提出CTCS-3级列控系统规范建模与形式化验证方法,此方法的特点是能够在系统规范、模型、验证工具以及验证结果之间建立一条跟踪链,从而始终保证系统规范、模型及程序代码之间的一致性。结合笔者运用此方法对CTCS-3级列控系统规范建模与形式化验证的实践,证明这种方法是可行的、高效的。

基于Event-B的航天器内存管理系统形式化验证

内存管理系统位于操作系统内核的最底层,为上层提供内存分配和回收机制.在航天器这类安全攸关的关键系统中,其可靠性和安全性至关重要,必须要考虑到强实时性、有限空间限制、高分配效率以及各种边界条件约束.因此,系统通常采用较为复杂的数据结构和算法来管理内存空间,同时需要采用非常严格的形式化方法来保证航天器这类安全攸关系统的高可信性.对复杂内存管理系统的形式化验证也会比之前的验证工作带来更多难题,主要体现在:内存管理模块中的复杂数据结构的形式化描述,操作的规范语义,行为的建模,内部函数的规范及断言定义与循环不变式的定义,实时性验证等方面.针对这些问题,深入分析实际的航天器操作系统内存管理系统的特性;探索基于分层迭代的语义描述与验证的一般性方法与理论,并应用这些理论方法来验证一个具有实际应用的航天嵌入式操作系统的内存管理系统.该研究成果有望直接应用于我国新一代的航天器系统.

可信计算中信任链建立的形式化验证

为了对可信平台控制模块的信任链建立过程进行理论验证,在对基于可信平台控制模块(trusted platform control module,TPCM)的信任链建立过程进行抽象处理的基础上,给出了抽象模型中各个实体状态的进程代数描述,并利用进程代数的公理系统做了形式化验证.验证的结果表明系统具有期望的外部行为.

一个安全、原子的电子商务协议及其形式化验证

电子商务的普及与接受主要取决于下述属性的解决 :安全、原子、隐私与匿名 .形式化描述和分析是描述电子商务协议并验证它们的属性的有效方法 .面向物理商品交易的电子商务协议需要具备 3个属性 :安全、原子和隐私 .介绍了一个安全、可靠的电子商务协议 BEARCAT及其形式化描述 ,并在有入侵者的情况下 ,通过用 BAN类型的逻辑证明所期望的属性的方式对协议的强度和正确性作了形式化分析 .

安全计算机通信管理机制的形式化验证与实现

为提高下一代列车运行控制(简称列控)系统安全计算机的系统兼容性,首先对其结构进行简要分析,并对管理机制进行设计,建立了管理单元状态转移模型,同时以形式化验证工具对模型的正确性进行了验证。在此基础上对基于微控制单元(MCU,micro controller unit)的管理单元进行了软硬件的设计实现与测试。验证和测试结果表明,所设计的管理机制符合设计规范的要求,管理单元能够实现预期的状态转移功能。