摘要:

摘要:作为轻量级的高可靠嵌入式数据库,SQLite3已被广泛应用于航空航天和操作系统等多个安全攸关领域,其提供了丰富灵活API函数以支持用户快速实现项目构建.然而,不正确的API函数调用序列会导致严重后果,包括运行错误、内存泄露和程序崩溃等.为了高效准确地监控SQLite3数据库API函数的正确调用情况,提出了基于多核系统的并行运行时验证方法.该方法首先分析API函数文档,自动挖掘相关API调用序列规约描述,辅助人工将其形式化表达为具有完全正则表达能力的命题投影时序逻辑公式;然后,在程序运行时,采用多任务调度策略,将程序执行产生的状态序列分割并对不同片段并行验证.实验结果表明:该方法能够发现调用SQLite3数据库API函数的30个被验证C程序中,违背API函数调用序列规约的达16个.另外,与传统串行运行时验证方法的对比实验表明,提出的并行运行时验证方法能够有效提高多核系统的验证效率.

摘要:LTL合成(linear temporal logic synthesis)是程序合成(program synthesis)的一类重要子问题,旨在自动构建一个控制器(controller),且要求该控制器和环境(environment)的行为交互满足给定的LTL公式.一般来说,可以将LTL合成定义为二人博弈(two-player game)问题,博弈的双方是环境和控制器,该问题的解称为合成策略.近年来,有研究从理论角度讨论了LTL合成与非确定规划(non-deterministic planning)的相关性.基于此,提出了一种新的利用非确定规划求解LTL合成问题的方法,并证明了方法的正确性和完备性.具体而言,首先获得LTL公式对应的Büchi自动机,结合二人博弈定义,将LTL合成问题转换为完全可观测的非确定规划模型;然后交由高效规划器求解.通过实验结果说明:与其他LTL合成方法相比,提出的基于规划的合成方法在解质量方面具有较大的优势,能够获得规模较小的合成策略.

摘要:异步通信程序是进程间通过异步消息通信实现非阻塞并发的程序.当前异步通信程序的程序验证问题通常将其归约至向量加法系统及其扩展模型,因而复杂度很高,缺乏高效工具.基本并行进程作为向量加法系统的一个子类,其可达性的验证问题为NP完备.首先,改进了Osualdo等人提出的为异步通信程序建模的Actor通信系统,将其归约至基本并行进程.然后,实现了基本并行进程的模型检测工具RABLE,实验结果表明,验证方法在异步通信程序的一系列程序验证问题上具有比已有工具更高效的结果.

摘要:时间自动机的模型学习算法旨在通过提供输入和观察输出构建软硬件系统的形式化模型.确定性单时钟时间自动机的学习是其中的一个重要研究方向,但是该算法具有一定的局限性,在状态较多时学习速度较慢,很难应用到复杂的系统中.由此,提出了一种改进的学习算法,使用逻辑时间分类树代替逻辑时间观察表作为学习算法的内部数据结构,有效地减少了成员查询次数,降低了算法的空间复杂度,并能够高效率地构建假设自动机.最后进行了相关实验,实验结果表明,提出的改进算法减少了60%左右的成员查询和5%左右的等价查询.同时在该实验中,改进算法的学习速度最高可提高45倍以上.

摘要:信息物理融合系统CPS (cyber physical system)是在环境感知的基础上,集合物理与计算的系统,可以实现与环境的智能交互.CPS信息物理空间的不断变化,对CPS资源安全性造成一定的挑战.因此,如何研究这一类由时空变化而导致的CPS资源安全性问题成为关键.针对该问题,提出了面向CPS时空约束的资源建模及其安全性验证方法.首先,在TCSP (timed communicating sequential process)的基础上扩展资源向量,提出了时空资源通信顺序进程DSR-TCSP (duration-space resource TCSP),使其能够描述CPS拓扑环境下的资源;其次,从时空约束的资源安全性需求中获取时间安全需求,通过DSR-TCSP的时间属性验证算法对时间安全需求进行验证;再次,将满足时间安全需求的模型转换为偶图与偶图反应,并输入到偶图检验工具BigMC中,验证其物理拓扑安全需求,对没有通过验证的反例,修改DSR-TCSP模型,直至满足所提出的安全需求;最后,通过一个驾驶场景实例,验证该方法的有效性.

摘要:布尔可满足性求解能够验证的问题规模通常受限,因此,如何高精度地预测其可满足性既是重要的研究问题,也是一项具有挑战性的工作.相关研究工作一般使用由文字节点和子句节点组成的图来表示布尔可满足性问题的结构,但是这种表征方法缺少了变量、子句之间的重要关系信息.在所提方法中,通过将原始布尔可满足性问题实例表征为多关系异构图的方式来表达变量和句子之间的关系,并设计使用消息传递关系网络模型来捕获实例的关系信息,提取了更多的结构特征.结果表明:该模型在预测精度、泛化能力和资源需求等方面均优于现有模型,对所选数据集的平均预测精度为81%.该模型在小规模问题(变量数为100)上训练,在大规模数据集上预测的平均预测精度达到了80.8%.同时,该模型对随机生成的非均匀随机问题的预测精度达到99%,这意味着它学习了预测可满足性的重要特征.此外,模型预测所花费的时间随着问题规模的增大也只是成线性增长.总结而言,基于关系消息传递网络提出了一个预测精度更高、泛化能力更好的布尔可满足性预测方法.

摘要:机载软件被广泛应用于航空航天领域,大幅提升了机载设备的性能.随着机载软件规模逐渐增大、功能逐渐增多,给软件的开发带来了难度.如何保障机载软件的正确性和安全性,也成为一个难题.基于模型的开发可以有效提升开发效率,而形式化方法能够有效保障软件的正确性.为了降低开发难度,同时保障机载软件的正确性、安全性,提出一种基于SysML状态机图子集的机载软件分层精化建模与验证方法.首先,使用SysML状态机图对机载软件的动态行为进行建模,根据提出的精化规则对初始模型进行手动逐层精化,得到精化设计模型;然后,针对软件模型动态变化的特性,将SysML状态机模型自动转换为时间自动机网络,并从软件需求中手动提取形式化TCTL性质进行模型检验.其次,为了实现编码自动化,将SysML模型自动转换至Simulink,利用Simulink Coder生成源代码.最后,以一个自动飞行控制软件为例进行了开发和验证,实验结果表明了该方法的有效性.

摘要:智能合约是一套以数字形式定义的承诺.通过智能合约,可以大大减少协议制定的中间环节,提高协议制定的效率.区块链技术为智能合约的执行提供了可信平台.随着区块链应用的拓广与深入,智能合约的作用必然越来越突出,智能合约的可靠性问题也将更加突显.以提高智能合约可靠性为目的的研究日益得到重视,但尚未有人对智能合约的时间性质可能引起的可靠性问题进行过系统的研究.通过分析典型智能合约,对智能合约时间约束的不同表现形式进行梳理,提炼出相应的时间约束模式并对其进行形式化;定义Solidity智能合约到时间自动机的转换规则,并实现其到实时模型检测工具UPPAAL入口模型的自动转换;再利用UPPAAL验证合约的时间相关性质.最后对两个实际合约进行实例研究,结果表明了所提炼模式的普遍性以及所提出形式化验证方案的可行性和有效性.

摘要:TSO-to-TSO可线性化、TSO-to-SC可线性化和TSO可线性化是Total Store Order (TSO)内存模型下可线性化的3个变种.提出了k-限界TSO-to-TSO可线性化和k-限界TSO可线性化,考察了k-限界TSO-to-TSO可线性化、k-限界TSO-to-SC可线性化和k-限界TSO可线性化的验证问题.它们分别是这3种可线性化的限界版本,都使用k-扩展历史,这样的扩展历史对应的执行有着限界数目(不超过k个)的函数调用、函数返回、调用刷出和返回刷出动作.k-扩展历史对应执行中的写动作数目是不限界的,进而执行中使用的存储缓冲区的大小也是不限界的,对应的操作语义是无穷状态迁移系统,所以3个限界版本可线性化的验证问题是不平凡的.将定义在并发数据结构与顺序规约之间的k-限界TSO-to-TSO可线性化、k-限界TSO-to-SC可线性化和k-限界TSO可线性化的验证问题归约到k-扩展历史集合之间的TSO-to-TSO可线性化问题,从而以统一的方式验证了TSO内存模型下可线性化的3个限界版本.验证方法的关键步骤是判定一个并发数据结构是否有一个特定的k-扩展历史.证明了这个问题是可判定的,证明方法是将这一问题归约为已知可判定的易失通道机器的控制状态可达问题.本质上,这一归约将每一个函数调用或函数返回动作转化为写、刷出或cas(compare-and-swap)动作.在TSO-to-TSO可线性化的定义中,一个函数调用或函数返回动作会同时影响存储缓冲区和控制状态.为了模拟函数调用或函数返回动作对存储缓冲区的影响,在每个函数调用或函数返回动作之后立刻执行一个特定的写动作.这个写动作及其对应的刷出动作模拟了函数调用或函数返回动作对存储缓冲区的影响.引入观察者进程,为每个函数调用或函数返回动作“绑定”一个观察者进程的cas动作,以这种方式模拟了函数调用或函数返回动作对控制状态的影响.因此证明了TSO内存模型下可线性化的这3个限界版本都是可判定的,进而证明了在TSO内存模型下判定可线性化的这3个限界版本的复杂度都在递归函数的Fast-Growing层级F_ω^ω中.通过证明已知对应复杂度的单通道简单通道机器的可达问题和TSO内存模型下可线性化的3个限界版本可以互相归约得到这个结论.

摘要:程序终止性判定是程序分析与验证领域中的一个研究热点.针对非线性循环程序,提出了一种基于反例制导的神经网络型秩函数的构造方法.该方法采用学习组件和验证组件交互的迭代框架,其中,学习组件利用程序轨迹作为训练集合构造一个候选秩函数;验证组件运用可满足性模理论(satisfiability modulo theories,SMT)确保候选秩函数的有效性;而由SMT返回的反例则进一步用于扩展学习组件中的训练集合,以对候选秩函数进行精化.实验结果表明,所提出的方法比已有的机器学习方法在秩函数的构造效率和构造能力上具有优势.

摘要:基于自动机理论的模型检测技术在形式化验证领域处于核心地位,然而传统自动机在时态算子上不具备可组合性,导致各种时态逻辑的模型检测算法不能有机整合.为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测,提出一种RTCTL^*正时态测试器构造方法以及相关符号化模型检测算法,既证明了所提出的RTCTL^*正时态测试器构造方法是完备的,也证明了该算法时间复杂度与被验证系统呈线性关系,与公式长度呈指数关系.基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK 2.0.0.完成了MCTK与著名的符号化模型检测工具nuXmv之间的实验对比分析工作,结果表明:MCTK虽然在内存消耗上要多于nuXmv,但是MCTK的时间复杂度双指数级小于nuXmv,使得利用MCTK验证大规模系统的实时时态性质成为可能.

摘要:时间Petri网为实时系统提供了一种形式化的建模方法,时间计算树逻辑(TCTL)为描述实时系统与时间相关的设计需求提供了一种逻辑化的表达方式,因此,基于时间Petri网的TCTL模型检测广泛应用于实时系统的正确性验证.然而对于一些涉及优先级的实时系统,例如多核多任务实时系统,这里不仅需要考虑任务之间的时间约束,还要考虑任务执行的优先级以及引入优先级带来的抢占式调度问题,致使相应的建模和分析变得更加困难.为此,提出了点区间优先级时间Petri网,通过在时间Petri网上定义变迁发生的优先级以及变迁的可挂起性,从而可以模拟实时系统的抢占式调度机制.首先,高优先级的任务抢占低优先级的任务所占用的资源,导致后者被中断;然后,前者执行完毕后释放资源;最后,后者再次获得资源,从中断的地方恢复.通过点区间优先级时间Petri网来模拟多核多任务实时系统,使用TCTL来描述它们的设计需求,设计了相应的模型检测算法,开发了相应的模型检测器以验证它们的正确性.通过一个实例,来说明该模型和方法的有效性.

摘要:分析实际程序时往往需要分析程序中函数的调用,一般使用过程间分析来实现全程序分析.函数内联是一种最为精确、易于实现的过程间分析方法.通过函数内联,可以使得已有过程内分析方法和工具支持包含函数调用的程序的分析.但是函数内联后代码的规模急剧增加,同时将产生大量中间变量,增加程序分析的变量维度,导致程序分析过程时空开销大大增加.考虑基于抽象解释框架下函数内联过程间分析的一些不足,并提出了相应的优化方法.基于抽象解释的程序分析关注自动推导程序变量之间的不变式约束关系,因此程序变量构成的程序环境大小(即各程序点处须考虑的相关变量集合)对分析的时空开销具有重要影响.为了减少函数内联后程序分析的开销,提出了面向内联函数块的程序环境降维优化方法.该方法针对内联函数后的程序代码,分析确定不同程序点处需维护的程序环境(即相关变量集合),而不是所有程序点共享同一全局程序环境,从而实现程序状态的降维.详细描述了基于该方法所实现的工具DRIP (dimension reduction for analyzing function inlined program)的架构、模块及算法细节.并在WCET Benchmarks测试集开展了分析实验.实验结果表明:DRIP在变量消除上取得的效果良好,甚至在某些测试集上能减少一半以上的变量,并在一定程度上降低了分析过程的时空开销.

摘要:并发文件系统由于复杂的实现,容易产生死锁、无限循环等终止性漏洞,已有的文件系统证明工作都忽视了终止性的证明.证明了一个并发文件系统AtomFS的终止性,保证了每个文件系统接口在公平调度的条件下都能返回.证明AtomFS接口的终止性要说明当其遇到阻碍时,阻碍源头(其他线程)终将产生进展,促使当前线程阻碍的消除,证明的核心在于说明锁耦合(lock coupling)遍历算法的终止性.然而还存在着两点挑战:(1)文件系统的树形结构允许阻碍的线程分布在多条路径上,全局地识别出多个阻碍源头使证明失去了局部性;(2) rename接口由于需要遍历两条路径,会带来“跨路径阻碍”现象,多个rename可能相互跨路径阻碍成环,导致无法找到阻碍源头.提出了两个核心的技术点来应对这些挑战:(1)使用局部思想仅确定单个阻碍源头;(2)使用偏序法解决跨路径阻碍成环问题.成功地构建了一个终止性证明框架CRL-T,并验证了AtomFS的终止性,所有的证明都在Coq中实现.

摘要:目前嵌入式系统广泛应用于航空电子、远程医疗、汽车电子等具有高可靠性要求的系统中.随着嵌入式系统的复杂度越来越高,为了保障系统的高可靠性需求,需要在系统开发的早期设计阶段对系统的可靠性进行分析评估,以提高系统的开发效率.嵌入式系统中软硬件功能的失效都会对系统可靠性产生影响,而AADL的可靠性模型缺乏对硬件构件错误的影响及传播机制进行刻画分析的能力.综合考虑软硬件错误发生失效后对系统可靠性的影响,提出了一种面向系统架构级别的软硬件综合可靠性分析方法.该方法基于电子电路设计中事务级建模方法,扩展了AADL事务级错误模型的语法和语义,来支持AADL对硬件构件错误传播的硬件功能行为建模,在此基础上,利用AADL模型实例化机制实现对嵌入式系统可靠性建模,刻画了错误行为在硬件构件之间、软硬件构件之间的传播与影响.同时,定义了AADL硬件构件事务级错误模型到广义随机Petri网模型的映射规则,实现了系统软硬件综合的可靠性行为仿真计算模型组合,支持嵌入式系统的软硬件综合可靠性分析.开发了软硬件综合可靠性建模与分析工具原型,并以某型飞机空气增压系统为例,在航空电子系统架构设计中进行尝试,验证了该方法在复杂嵌入式系统设计中进行软硬件综合可靠性分析的可行性与优越性.

摘要:代码自然性(code naturalness)研究是自然语言处理领域和软件工程领域共同的研究热点之一,旨在通过构建基于自然语言处理技术的代码自然性模型,以解决各种软件工程任务.近年来,随着开源软件社区中源代码和数据规模的不断扩大,越来越多的研究人员注重钻研源代码中蕴藏的信息,并且取得了一系列研究成果.但与此同时,代码自然性研究在代码语料库构建、模型构建和任务应用等环节面临许多挑战.鉴于此,从代码自然性技术的代码语料库构建、模型构建和任务应用等方面对近年来代码自然性研究及应用进展进行梳理和总结.主要内容包括:(1)介绍了代码自然性的基本概念及其研究概况;(2)归纳目前代码自然性研究的语料库,并对代码自然性模型建模方法进行分类与总结;(3)总结代码自然性模型的实验验证方法和模型评价指标;(4)总结并归类了目前代码自然性的应用现状;(5)归纳代码自然性技术的关键问题;(6)展望代码自然性技术的未来发展.

摘要:随着开源概念的逐步深入,开源软件成为软件发展的潮流.同时,开源软件的使用受各类开源许可证约束.开源参与者在开发过程中该如何为自己的开源软件选择合适的许可证,确保高效合理地使用社区群体智慧劳动成果,仍是一个亟需解决的问题.为此,首先分析和解读了开放源代码促进会认证的常用开源许可证,通过对许可证条款内容和结构的研究,得到开源许可证框架及许可证兼容性推导模型,并将该模型应用于对我国自主研发的木兰宽松许可证的分析和解读.最后,基于上述工作研发了开源许可证选择工具,为开源开发者对许可证的理解和合规使用提供了参考和决策支持.

摘要:智能合约是区块链技术最成功的应用之一,为实现各式各样的区块链现实应用提供了基础,在区块链生态系统中处于至关重要的地位.然而,频发的智能合约安全事件不仅造成了巨大的经济损失,而且破坏了基于区块链的信用体系,智能合约的安全性和可靠性成为国内外研究的新关注点.首先从Solidity代码层、EVM执行层、区块链系统层这3个层面介绍了智能合约常见的漏洞类型和典型案例;继而,从形式化验证法、符号执行法、模糊测试法、中间表示法、深度学习法这5类方法综述了智能合约漏洞检测技术的研究进展,针对现有漏洞检测方法的可检测漏洞类型、准确率、时间消耗等方面进行了详细的对比分析,并讨论了它们的局限性和改进思路;最后,根据对现有研究工作的总结,探讨了智能合约漏洞检测领域面临的挑战,并结合深度学习技术展望了未来的研究方向.

摘要:很多强化学习方法较少地考虑决策的安全性,但研究领域和工业应用领域都要求的智能体所做决策是安全的.解决智能体决策安全问题的传统方法主要有改变目标函数、改变智能体的探索过程等,然而这些方法忽略了智能体遭受的损害和成本,因此不能有效地保障决策的安全性.在受限马尔可夫决策过程的基础上,通过对动作空间添加安全约束,设计了安全Sarsa (λ)方法和安全Sarsa方法.在求解过程中,不仅要求智能体得到最大的状态-动作值,还要求其满足安全约束的限制,从而获得安全的最优策略.由于传统的强化学习求解方法不再适用于求解带约束的安全Sarsa (λ)模型和安全Sarsa模型,为在满足约束条件下得到全局最优状态-动作值函数,提出了安全强化学习的求解模型.求解模型基于线性化多维约束,采用拉格朗日乘数法,在保证状态-动作值函数和约束函数具有可微性的前提下,将安全强化学习模型转化为凸模型,避免了在求解过程中陷入局部最优解的问题,提高了算法的求解效率和精确度.同时,给出了算法的可行性证明.最后,实验验证了算法的有效性.

摘要:为揭示传播网络中节点之间的父子影响关系,现有工作大多需要知道节点的感染时间,而该信息往往只有通过对传播过程进行实时监控才能获得.研究如何基于传播结果来学习获得传播网络中节点之间的父子影响关系.传播结果只包含每个传播过程中节点的最终感染状态,而节点的最终感染状态在实际中往往比节点的感染时间更容易获得.提出了一种基于条件熵的方法来推断网络中每个节点的潜在候选父节点.此外,能够通过从基于条件熵的推断结果中发现并修剪那些实际不太可能存在的父子影响关系来优化最终的影响关系推断结果.在人工网络和真实网络上的大量实验,验证了该方法的有效性和运行效率.

摘要:最佳排序路径查询,是智能交通中的热点问题.在实际的应用中,由于最佳排序路径查询有许多限制条件,现有的算法不能有效地解决动态网络中受限制的路径查询问题.为了解决动态网络中最佳排序路径查询问题,用规则表示每个限制条件,提出了一种新的最佳排序路径查询形式,即多规则的最短路径查询.提供了统一的框架,该框架包含了路径集合查询和最短路径查询.在路径集合查询部分,为了高效地查询出满足多规则的路径集合,在广义规则树的基础上,提出一种新的树的遍历方式,即树的继承全遍历;并基于树的继承全遍历思想,提出一种剪枝技术,对路径集合进行删减,最后求得候选路径集合.在最短路径查询部分,提出一种基于动态阈值的最短路径搜索方法.通过两个真实的动态道路网络的实验验证,所提出的算法能够高效地解决多规则的最短路径查询问题.