摘要:计算机科学的发展主要涉及硬件和软件的发展，而软、硬件发展的核心问题之一是如何保证它们是安全可靠的。如今，硬件性能变得越来越高，运算速度变得越来越快，体系结构变得越来越复杂，软件的功能也变得越来越复杂，如何开发可靠的软、硬件系统，己经成为计算机科学发展的巨大挑战。特别是现在计算机系统广泛应用于许多安全攸关系统中，如高速列车控制系统、航空航天控制系统、核反应堆控制系统、医疗设备控制系统等等，这些系统中的任何错误都可能导致灾难性后果。 形式化方法己经成功应用于各种硬件设计，特别是芯片的设计。各大硬件制造商都有一个非常强大的形式化方法团队为保障系统的可靠性提供技术支持，例如IBM、AMD等等。近年来，随着形式验证技术和工具的发展，特别是在程序验证中的成功应用，形式化方法在处理软件开发复杂性和提高软件可靠性方面已显示出无可取代的潜力。各个著名的研究机构都投入了大量人力和物力从事这方面的研究。例如，美国宇航局NASA拥有一支庞大的形式化方法研究团队，他们在保证美国航天器控制软件正确性方面发挥了巨大作用，在美国研发“好奇号”火星探测器时，为了提高控制软件的可靠性和生产率，广泛使用了形式化方法。在新兴领域，如区块链及人工智能等领域，形式化方法也逐步得到应用，提升系统的整体安全可控。 本专题公开征文，共征得投稿27篇。特约编辑先后邀请了国内外在该领域比较活跃的学者参与审稿工作，每篇投稿至少邀请2位专家进行初审。大部分稿件经过初审和复审两轮评审，部分稿件经过了两轮复审。通过初审的稿件还在FMAC 2020大会上进行了现场报告，作者现场回答了与会者的问题，并听取了与会者的修改建议。最终有18篇论文入选本专题。

摘要:形式化方法为安全协议分析提供了理论工具，但经过形式化验证过的协议标准在转换为具体程序实现时，可能无法满足相应的安全属性.为此，提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型，基于Pi演算模型对协议安全属性形式化验证.最后给出了方案转换的正确性证明，并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合，能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.

摘要:在GitHub平台中，许多项目贡献者在提交Pull Request（PR）时往往会忽略提交PR描述，这使得提交的PR容易被评审者忽略或者拒绝.因此，自动生成PR描述以帮助项目贡献者提高PR通过率是很有必要的.然而，现有PR描述生成方法的表现会受到PR粒度影响，无法有效为大粒度的PR生成描述.因此，该工作专注于大粒度PR描述的自动生成.首先对PR中的文本信息进行预处理，将文本中的单词作为辅助节点构建词-句异质图，以建立PR语句间的联系；随后对异质图进行特征提取，并将提取后的特征输入至图神经网络进行图表示学习，通过节点间的消息传递，使句子节点学习到更丰富的内容信息；最后，选择带有关键信息的句子组成PR描述.此外，针对PR数据集缺少人工标注的真实标签而无法进行监督学习的问题，使用强化学习指导PR描述的生成，以最小化获得奖励的负期望为目标训练模型，该过程与标签无关，并且直接提升了生成结果的表现.在真实的数据集上进行了实验，实验结果表明，提出的大粒度PR描述生成方法在F1值和可读性上优于现有方法.

摘要:展开技术借助分支进程可在一定程度上缓解Petri网性质分析中的状态爆炸问题.但展开网中仍然包含了系统的所有状态信息.某些应用问题仅需对系统特定状态的可覆盖性进行判定，以此为目标，有望缩减网系统展开的规模.为此，针对安全Petri网的可覆盖性判定问题提出了一种目标导向的反向展开算法，结合启发式技术缩减展开的规模，以此提高目标标识可覆盖性判定的效率.进而，将反向展开算法应用于并发程序的形式化验证，将并发程序的数据竞争检测问题转换为Petri网特定标识的可覆盖性判定问题.实验对比了正向展开与反向展开在Petri网可覆盖性判定问题上的效率，结果表明：当Petri网展开的正向分支较多时，反向展开相比正向展开具有更高的可覆盖性判定效率.最后，对影响反向展开效率的关键因素做了分析与总结.

摘要:航天器等安全关键系统是典型的嵌入式系统，具有多任务并发、中断频发等特点.操作系统是其最基础的软件，构建一个正确的操作系统是保障航天器系统高可信运行的关键.异常管理作为操作系统最底层的功能，负责引导系统控制流的突变来响应处理器状态中的某些变化，异常管理的正确性是整个操作系统正确性的基础.提出一种基于Hoare-logic的验证框架，用于证明面向SPARC处理器架构操作系统异常管理的正确性，特别针对多任务并发和中断频发实时操作系统异常嵌套与异常中发生任务切换的情况，将异常管理划分为5个阶段进行全面的形式化建模，并且在Coq证明定理辅助工具中实现了此框架.基于该框架，验证了我国北斗三号在轨实际应用的航天器嵌入式实时操作系统SpaceOS异常管理功能的正确性.

摘要:模型驱动开发以其低错误率、易仿真、易验证的特点，在嵌入式软件开发中被广泛应用.近年来，基于模型的嵌入式软件开发方法及相应工具也在逐渐发展和完善.数据流模型是各种建模工具中使用最为频繁的语义模型，然而，各种工具对于数据流模型的代码生成能力却参差不齐，特别是对于数据分支组件的支持，当前主流的建模工具都采用各种方式来回避复杂的分支建模及对应的代码生成.但是，分支建模是非常重要的，使用分支组件可以更清晰地表现出数据流的数据传递逻辑.为了解决复杂分支建模带来的代码生成难题，针对具有复杂分支组合的数据流模型.提出了一种基于分支调度标记的代码生成方法.在所提出的算法中，首先通过拓扑排序确定模型的调度顺序，再根据不同分支的影响对组件进行分支标记；之后，根据组件的分支标记构造一个基于控制流的代码生成位置表；最后，即可根据代码生成位置表进行各种主流语言的代码生成.通过构造4个具有复杂分支的数据流模型实例进行代码生成，并在生成代码行数和运行时间等方面与Simulink和Ptolemy进行对比，进一步说明该代码生成方法在复杂分支组合情况下的通用性以及所做工作的价值和意义.

摘要:嵌入式实时系统在安全关键领域变得越来越重要，其广泛应用于航空航天、汽车电子等具有严格时间约束的实时系统中.随着嵌入式系统的复杂度越来越高，在系统开发的早期设计阶段就需要对其可调度性进行分析评估.系统中的存储资源会对可调度性产生一定影响，在抢占式实时嵌入式系统引入缓存后，任务的最坏执行时间可能发生变化.因此，分析缓存相关抢占延迟对实时嵌入式系统的可调度性影响，一直以来是困扰大规模复杂系统架构设计的一个技术难题.提出一种面向软件架构级别、基于抢占调度序列的缓存相关抢占延迟计算方法，用来分析缓存相关抢占延迟约束下AADL （架构分析和设计语言）模型的可调度性.扩展了AADL关于存储资源架构设计的模型元素，来支持对缓存属性进行建模，提出一种基于模型构件进行抢占序列排序、缓存相关抢占延迟时间计算和被抢占任务最坏执行时间的估算方法，来对系统架构各功能构件在共享系统存储资源下系统的可调度性进行分析.还实现了分析缓存相关抢占延迟约束下的系统任务可调度性分析工具原型，并以某型飞机机载开放式智能信息系统为例，在航空电子系统架构设计中进行尝试，验证了该方法的在复杂系统设计中的对实时性分析的可行性.

摘要:死锁是并行程序常见的缺陷之一，动态死锁分析方法根据程序运行轨迹构建锁图、分段图等模型来检测死锁.然而，锁图及其现有的各种变型无法区分同一循环中锁授权语句的多次执行，扩展锁图中记录的锁集无法捕捉线程曾经持有而又随后释放的锁信息，分段图无法刻画锁的获取和释放操作与线程启动操作耦合而导致的段间依赖关系.上述问题导致了多种死锁的误报.为解决上述问题，对已有的锁图和分段图模型进行改进，在锁图基础上扩充语句的执行时序信息，在分段图的基础上扩充锁的获取和释放信息，对段进行更细粒度的划分以建模锁对象导致的段间依赖关系；最终，在上述锁增广分段图与时序增广锁图的基础上，提出一种新的死锁检测方法.所提方法能够有效消除前述各种误报，从而提高死锁检测的准确率.文中开发相应的原型系统，并结合多个程序实例对所提方法的有效性进行评估验证.

摘要:污点分析技术是检测Android智能手机隐私数据泄露的有效方法，目前主流的Android应用污点分析工具主要关注分析的精度，常常忽略运行效率的提升.在分析一些复杂应用时，过大的开销可能造成超时或程序崩溃等问题，影响工具的广泛使用.为了减少分析时间、提高效率，提出一种基于污染变量关系图的污点分析方法.该方法定义了污染变量关系图用于描述程序中污染变量及其关系，摒弃了传统数据流分析框架，将污点分析和别名分析进行结合，从程序中抽象出污染变量关系图和潜在污染流，并在控制流图上对潜在污染流进行验证以提高精度.详细描述了基于该方法所实现的工具FastDroid的架构、模块及算法细节.实验使用了3个不同的测试集，分别为DroidBench-2.0，MalGenome以及Google Play上随机下载的1517个应用.实验结果表明：FastDroid在DroidBench-2.0测试集上的查准率和查全率分别达到93.3%和85.8%，比目前主流工具FlowDroid更高，并且在3个测试集上所用的分析时间更少且更稳定.

摘要:智能合约是实现各类区块链应用的核心软件程序.近期，以太坊区块链平台（Ethereum）上的智能合约暴露出大量错误和安全隐患，在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果，智能合约程序语言的形式化必不可少.对以太坊中间语言Yul进行形式化，首次给出了其类型系统和小步操作语义的形式化定义.该语义为可执行语义（executable semantics），由120个Yul语言程序组成的测试集进行测试.该工作在Isabelle/HOL证明辅助工具中完成，为基于定理证明的智能合约正确性、安全性验证奠定了基础.

摘要:基于交互行为的用户特征提取和身份认证方法是一种重要的身份识别方式，但高频用户的交互行为模式和操作习惯相对稳定，易被欺诈者模仿，使得现有模型对此类欺诈行为的误判较高.如何使得用户行为主动平滑变化且可区分，成为解决上述问题的关键.针对此问题，提出一种基于个体交互行为系统平滑干预模型：首先，根据用户历史交互行为日志从多个维度得到用户的交互行为变化趋势；然后，结合行为的稳定性和偏向性提出行为时域漂移算法（TDDA），为每个用户确定行为引导的时机；最后，基于Petri网提出交互行为重构系统干预模型，在系统中的非关键路径叠加行为触发因素，引导用户产生新的交互行为习惯.实验证明了提出的方法能够很好地引导用户行为平滑变化，且产生足够的区分性，使得行为伪装异常检测场景下模型的准确性显著提高.

摘要:PolarFS是阿里巴巴开发的分布式文件系统，它实现了分布式共识协议Raft的一种变体，称为ParallelRaft.ParallelRaft突破了Raft中顺序提交、顺序执行的限制，允许状态机乱序执行用户命令.然而文献表明：ParallelRaft并未开源，仅有简短的文字描述，更缺乏严格的形式化规约.更进一步，它的正确性也尚未经过必要的数学论证或形式化检验.旨在为ParallelRaft提供严格的形式化规约并证明其正确性，主要贡献包括：首先，为了理清ParallelRaft与Raft之间的关系，提出了允许乱序提交、顺序执行的ParallelRaft-SE （sequential execution）协议，并建立了从ParallelRaft-SE到Multi-Paxos的精化关系；其次，现有的ParallelRaft描述忽略了可能会违反状态一致性的“幽灵日志”问题，因此在ParallelRaft-SE的基础上提出了ParallelRaft-CE （concurrent execution）协议.ParallelRaft-CE限制了ParallelRaft-SE在乱序提交阶段的并行度，避免了“幽灵日志”问题，支持乱序执行，并保证乱序执行下的状态机一致性.证明了ParallelRaft-CE的正确性.最后，使用TLA+给出了ParallelRaft-SE和ParallelRaft-CE的形式化规约，并对协议参与者数量较小的情形，使用TLC模型检验与模拟测试工具验证了从ParallelRaft-SE到Multi-Paxos的精化关系以及ParallelRaft-CE的正确性.

摘要:随着信息物理融合系统CPS （cyber physical system）研究的深入，CPS的安全性问题越来越受到人们的广泛关注，如何验证CPS时空不一致的安全性问题已经成为研究热点.针对该问题，提出了面向CPS时空性质验证的混成AADL（architecture analysis & design language）建模与模型转换方法.首先，扩展AADL行为附件的时空描述能力，提出了混成AADL（hybrid architecture analysis & design language），用于建模CPS的时空性质；其次，在进程代数中引入微分方程以及位置描述，提出了HP-TCSP，能够验证CPS的时空性质；再次，通过模型转换，将混成AADL转换为HP-TCSP，从而可以将混成AADL描述的CPS模型在HP-TCSP中进行时空一致性验证；最后，通过一个飞机避撞系统实例，验证该方法的有效性.

摘要:在芯片设计领域，采用模型驱动的FPGA设计方法是目前较为安全可靠的一种方法.但是，基于模型驱动的FPGA设计需要证明FPGA设计模型和生成Verilog/VHDL代码的一致性；同时，芯片设计的正确性、可靠性和安全性也至关重要.目前，多采用仿真方法对模型和代码的一致性进行验证，很难保证设计的可靠性和安全性，并存在验证效率低、工作量大等问题.提出一种新型验证设计模型和生成代码一致性的方法，该方法利用MSVL语言进行系统建模，并通过模型提取命题投影时序逻辑公式描述的系统的性质，通过统一模型检测的原理，验证模型是否满足性质的有效性.进而，应用信号灯控制电路系统作为验证实例，对验证方法做了检验和说明.

摘要:机器人操作系统（robot operating system，简称ROS）是一种开源的元操作系统，能够在异种计算簇上提供基于消息机制的结构化通信层.为改善ROS1中存在的数据分发实时性、可靠性问题，ROS2提出了面向数据流的数据分发服务机制.采用概率模型检验的方法，分析、验证ROS2系统数据分发机制的实时性和可靠性.首先，提出一种面向数据流的ROS2数据分发服务的形式化验证框架，并对通信系统模块建立概率时间自动机模型；其次，运用概率模型检测器，通过数据丢失率和系统响应时间等参数分析、验证ROS2面向数据流的数据分发服务的实时性、可靠性；最后，基于重传机制、服务质量（quality of service，简称QoS）策略分析，通过设置和调整服务质量参数，实现不同的数据需求和传输方式的量化性能分析，为ROS2应用的设计人员以及基于数据流的分布式数据分发服务的形式化建模、验证和量化性能分析提供参考.

摘要:Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包，主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不同事件的时间戳触发组件，时间自动机模型能够表达这个特征，因此选用Uppaal作为验证工具.首先定义了离散事件模型的形式语义；其次设计了一组从离散事件模型到时间自动机的映射规则；然后在Ptolemy环境中实现了一个插件，可以自动将离散事件模型转换为时间自动机模型，并通过调用Uppaal验证内核完成验证；最后，以一个交通信号灯控制系统为例进行了成功的转换和验证，实验结果证实了该方法能够验证Ptolemy离散事件模型的正确性.

摘要:智能合约是运行在区块链上的计算机协议，被广泛应用在各个领域中，但是其安全问题层出不穷，因此在智能合约部署到区块链上之前，需要对其进行安全审计.然而，传统的测试方法无法保证智能合约所需的高可靠性和正确性.说明了如何使用建模、仿真与验证语言（MSVL）和命题投影时序逻辑（PPTL）对智能合约进行建模和验证：首先介绍了MSVL与PPTL的理论基础；之后，通过分析和对比Solidity与MSVL语言的特性，开发了能够将Solidity程序转换为MSVL程序的SOL2M转换器，并详细介绍了SOL2M转换器的设计思路；最终，通过投票智能合约和银行转账智能合约两个实例，给出了SOL2M转换器的执行结果.使用PPTL从功能一致性、逻辑正确性以及合约完备性这3个方面描述了合约的性质，给出了使用统一模型检测器（UMC4M）对合约进行验证的过程.

摘要:机器人操作系统（robot operating system，简称ROS）是一种广泛应用于机器人开发的开源系统，它可以为开发者提供硬件抽象、设备驱动、库函数、可视化、消息传递和软件包管理等诸多功能，应用前景广阔.ROS集成了可以实现不同功能的功能包，例如定位绘图、行动规划、感知、模拟等等，但其中可能存在一些漏洞，破坏整个机器人系统的安全性和可靠性.提出了一种差分模糊测试方法对ROS不同版本的功能包进行测试，找出其中的漏洞.该方法包括测试用例生成和差分模糊测试执行两个模块：首先，对于输入文件进行加载、处理，并基于策略生成的方法生成测试用例文件；其次，节点间使用话题通信机制实现通信，使用上一模块生成的测试用例文件作为统一的模糊输入，对ROS不同版本的功能包进行差分模糊测试；接着，对测试结果中的不一致输出进行差异计算并评估，符合评估指标的种子将被保留并反馈给用例生成模块循环生成测试用例，有效提高了种子质量及代码覆盖率；最后分析不一致输出原因，找出漏洞.将该方法应用在机器人坐标转换的实验中，实现对不同参考系下坐标转换的功能包TF和TF2的测试.最终的实验结果表明：与TF2相比，TF在功能实现上更加准确.TF2实现坐标旋转变换的函数存在漏洞.

摘要:矩阵是工程领域中常用的一种数据结构，在深度学习领域，矩阵乘法是神经网络训练中的核心技术之一.面对大型矩阵的运算问题，分块矩阵技术可将大矩阵运算转换为小矩阵运算以实现并行运算，并且能够大幅度减少矩阵运算步骤并且提高矩阵运算速度.首先对目前学术界的矩阵形式化工作进行了系统总结，并且分析了矩阵形式化的主要几种方法；其次介绍并完善了基于Coq记录类型的矩阵形式化方法，其中包括提出新的矩阵等价定义、对之前的形式化工作进行了整理和完善，并证明了一组新的引理；在此基础上，进一步实现了分块矩阵运算的形式化，讨论了该类型归纳证明的难点和解决方法；最终实现了矩阵与分块矩阵形式化的不同类型的基础库.

摘要:传统的委托计算需要额外开销验证计算结果的正确性，导致委托计算效率较低、开销较大.针对此问题，结合博弈论与理性信任建模（rational trust modeling，简称RTM）的思想，提出了基于理性信任模型的理性委托计算协议.通过设置恰当的效用函数，激励计算方诚实执行协议，以此来保证计算结果的可靠性.首先，基于理性信任建模的思想构造理性信任模型，将服务器的生存周期作为效用函数的参数，设计满足委托计算参与者利益的效用函数，并分析协议中参与者的行为策略，当参与者采取“诚实”策略时，可以得到理性委托计算的纳什均衡点；其次，利用改进的NTRU （number theory research unit）公钥密码体制实现速度快、安全性高、具有抵抗量子计算攻击的能力的优点，结合Pedersen承诺方案，设计理性委托计算协议；最后，从正确性、安全性与性能这3个方面对协议进行分析，并通过实验证明生存周期对参与者效用的影响.结果表明，该协议可有效保证计算结果的可靠性.