摘要:当前的量子程序一般由量子电路表示, 由多个量子门组成. 如果程序包含了被直接表示为酉矩阵的门, 需要将这些量子门转化为基本门所构成的量子电路. 该步骤被称为量子电路合成. 然而, 当前的合成方法可能会生成包含数千个门的量子电路. 这些量子电路的质量较低, 在部署到真实含噪声的量子硬件时非常容易输出错误的结果. 此外, 在保证门数量较小的情况下, 当量子比特数量增至8时, 量子电路合成需要数周甚至数月的时间. 在这项工作中, 提出一种量子电路合成方法, 实现从酉矩阵到高质量量子电路的快速合成. 首先介绍一种迭代方法, 通过插入电路模块来逼近目标酉矩阵. 在迭代中, 提出一种具有奖励机制的前瞻策略减少冗余量子门. 在量子电路合成的加速过程中, 为了减少候选电路模块的空间, 提出一种剪枝方法, 首先描述每个候选电路模块的闭包来刻画电路的表示空间, 然后基于模块的表示空间重叠率进行剪枝, 以此构建一个小而高质量的候选集合. 此外, 为了减少搜索最优门参数的开销, 将选定的候选与目标酉矩阵打包成统一电路, 然后通过计算其在基态上的期望来快速获得近似距离. 实验证明, 与当前的最优的量子电路合成方法QuCT和QFAST相比, 该方法在5–8量子比特量子电路合成中实现了减少门数量为原有方法的37.04%–62.50%, 同时实现3.7–20.6倍的加速.

摘要:约束求解是验证神经网络的基础方法. 在人工智能安全领域, 为了修复或攻击等目的, 常需要对神经网络的结构和参数进行修改. 面对此类需求, 提出神经网络的增量验证问题, 旨在判断修改后的神经网络是否仍保持安全性质. 针对这类问题, 基于Reluplex框架提出了一种增量可满足性模理论算法DeepInc. 该算法利用旧求解过程中关键计算格局的特征, 启发式地检查关键计算格局是否适用于证明修改后的神经网络. 实验结果显示, DeepInc的效率在大多数情况下都优于Marabou. 此外, 即使与最先进的验证工具α, β-CROWN相比, 对于修改前后均未满足预设安全性质的网络, DeepInc也实现了显著的加速.

摘要:单球驱动平衡机器人是一种具有全向运动性的机器人, 其灵活性能在狭小或复杂环境中得到充分体现, 因此受到广泛关注. 在该型机器人运动学和动力学设计过程中, 保证其模型的正确性至关重要. 基于测试和仿真的传统方法难以穷尽系统所有状态, 因此可能无法捕捉到某些设计缺陷或潜在的安全风险. 为确保单球驱动平衡机器人满足安全攸关机器人的正确性、安全性验证要求, 在定理证明器HOL Light中, 基于实分析库、矩阵分析库、机器人运动学和动力学库等定理证明库, 构建单球驱动平衡机器人运动学和动力学的形式化模型, 并进行高阶逻辑推导与证明.

摘要:元解释学习(meta-interpretive learning, MIL)是一种归纳逻辑程序设计(inductive logic programming, ILP)方法, 旨在从一组实例、元规则和其他背景知识中学习一个程序. MIL采用深度优先和失败驱动策略在程序空间中搜索适当的子句以生成程序. 事实上, 这种机制不可避免地引发了对相同目标重复证明的问题. 提出一种剪枝策略, 该策略利用Prolog内置的数据库机制来存储未能达成的目标及其对应的错误信息, 从而有效避免冗余的证明过程. 此后, 这些累积的错误信息能够作为指导, 帮助MIL系统在未来的学习过程中进行优化和调整. 证明剪枝算法的正确性, 并在理论上计算程序空间的缩减比例. 将所提出的方法应用于两个现有的MIL系统Metagol和Metagol_AI, 从而产生了两个新的MIL系统Metagol_F和Metagol_{AI_F}. 在4个不同任务上的实证结果表明, 所提出的策略可以显著减少学习相同程序的时间消耗.

摘要:操作系统是软件的基础平台, 操作系统内核的安全性往往影响重大. Rust是逐渐兴起的内存安全语言, 具有生命周期、所有权、借用检查、RAII等安全机制, 使用Rust语言构建内核逐渐成为当前热门的研究方向. 但目前使用Rust构建的系统多包含部分unsafe代码段, 无法从根本上保证语言层面的安全性, 因而针对unsafe代码段的验证对于保证Rust构建的内核正确可靠尤为重要. 以某使用Rust构建的微内核为对象, 提出GhostFunc的safe和unsafe代码段组合验证方法, 将两类代码段采用不同层级的抽象, 使用GhostFunc进行组合验证. 针对任务管理与调度模块, 基于$ {\lambda _{{\text{Rust}}}} $形式化Arc<T> 等unsafe代码段, 并给出形式化GhostFunc的具体实现, 完成此方法的验证实例. 所有验证工作基于定理证明的方法, 在Coq中采用Iris分离逻辑框架完成正确性的验证.

摘要:自动驾驶中极端的场景、无法预测的人类行为等长尾问题逐渐成为制约自动驾驶系统(autonomous driving system, ADS)发展的关键要素, 因此有效地生成安全关键场景对于提高自动驾驶系统的安全性至关重要. 现有的自动驾驶场景生成主要依赖于大量的路采数据, 采用数据驱动式场景生成方法, 并结合场景泛化技术生成相应的驾驶场景. 该方法耗时耗力, 成本高, 而且难以有效生成边缘场景. 而模型驱动式场景建模方法通过构建逻辑场景模型, 能够建模复杂的场景特征并有效生成安全关键场景. 其面临的挑战性问题是如何设计一种基于领域知识的可视化场景建模语言, 支持抽象建模复杂驾驶场景, 并进一步有效地挖掘安全攸关的边缘关键场景. 针对以上问题, 提出一种基于SML4ADS2.0的自动驾驶场景建模及边缘关键场景生成方法. 该方法基于ADS领域本体建模场景, 并结合形式化量化评估与重要性采样实现边缘关键场景生成. 首先, 提出基于SML4ADS2.0模型驱动式场景建模方法, 设计一种基于ADS领域本体的自动驾驶场景建模语言(scenario modeling language for autonomous driving system, SML4ADS2.0), 以构建自动驾驶场景模型; 其次, 通过模型转换规则实现场景模型到随机混成自动机(stochastic hybrid automata, SHA)的模型转换, 并使用模型检测工具UPPAAL-SMC对场景模型进行量化评估分析; 然后, 通过重要性采样技术在场景空间中快速检测到边缘场景, 实现逻辑场景到边缘关键具体场景的有效生成; 最后, 结合变道超车等典型场景, 进行案例展示. 实验结果表明该方法能够有效建模场景, 并解决ADS安全关键场景生成问题.

摘要:动态顺序统计树结构是一类融合了动态集合、顺序统计量以及搜索树结构特性的数据结构, 支持高效的数据检索操作, 广泛应用于数据库系统、内存管理和文件管理等领域. 然而, 当前工作侧重讨论结构不变性, 如平衡性, 而忽略了功能正确性的讨论. 且现有研究方法主要针对具体的算法程序进行手工推导或交互式机械化验证, 缺乏成熟且可靠的通用验证模式, 自动化水平较低. 为此, 设计动态顺序统计搜索树类结构的Isabelle函数式建模框架和自动化验证框架, 构建经过验证的通用验证引理库, 可以节省开发人员验证代码的时间和成本. 基于函数式建模框架, 选取不平衡的二叉搜索树、平衡的二叉搜索树(以红黑树为代表)和平衡的多叉搜索树(以2?3树为代表)作为实例化的案例来展示. 借助自动验证框架, 多个实例化案例可自动验证, 仅需要使用归纳法并调用一次auto方法或使用try命令即可, 为复杂数据结构算法功能和结构正确性的自动化验证提供了参考.

摘要:同步数据流语言Lustre是安全关键系统开发中常用的开发语言, 其现存的官方代码生成器和SCADE的KCG代码生成器既没有经过形式化验证, 对用户也处于黑盒状态. 近年来, 通过证明源代码和目标代码的等价性间接证明编译器的正确性的翻译确认方法被证明是成功的. 基于下推自动机的编译方法和基于语义一致性的验证方法, 提出Lustre语言可信编译方法, 能够将Lustre语言转换为C语言并进行形式化验证以保证编译的正确性, 并使用Isabelle对翻译转换过程进行严格的正确性证明.

摘要:操作系统内核是构建安全攸关系统软件的基础. 任何计算机系统的正确运行都依赖于底层操作系统实现的正确性, 因此, 对操作系统内核进行形式验证是很迫切的需求. 然而, 操作系统中存在的多任务并发、数据共享和竞争等行为, 给操作系统内核的验证带来很大的挑战. 近年来, 基于定理证明的方法广泛用于操作系统各功能模块的形式验证, 并取得多个成功应用. 微内核操作系统权能访问控制模块提供基于权能的细粒度访问控制, 旨在防止未经授权的用户访问系统内核资源和服务. 在权能访问控制模块实现中, 所有任务的权能空间构成多个树结构, 同时每个任务权能节点包含多种嵌套的复杂数据结构, 以及权能函数中广泛存在的对权能结构的访问、修改、(递归)删除等操作, 使得它的形式验证与操作系统其他功能模块相比更加困难. 将以并发精化程序逻辑CSL-R为基础, 通过证明权能应用程序接口函数(API函数)和其抽象规范之间的精化关系, 来验证航天嵌入式领域某微内核操作系统权能访问控制的功能正确性. 首先对权能数据结构进行形式建模, 并在此基础上定义全局不变式来保持权能空间的一致性; 然后定义反映功能正确性需求的内核函数的前后条件规范和API函数的抽象规范; 最终验证权能API函数C代码实现和抽象规范之间的精化关系. 以上所有的定义和验证均在Coq定理证明器中完成. 在验证过程中发现实现的错误, 并得到微内核操作系统设计方的确认和修改.

摘要:信息物理融合系统(cyber-physical system, CPS)在安全攸关领域具有广泛的应用, 保障其安全性至关重要. 形式化验证是证明系统安全性的有效手段, 但在现实世界中的复杂CPS系统上应用仍面临挑战. 因此, 反例生成的方法被提出, 旨在通过寻找系统中违背安全规约的反例行为来证明系统的不安全. 现有的基于路径的CPS系统反例生成方法采用分治策略, 针对系统模型中各条路径上的行为空间分别进行探索, 能够有效发现系统中的不安全行为. 然而, 在大规模系统中, 这类方法面临严重的路径爆炸问题, 路径数量随着离散状态数目指数级增长, 反例生成的效率和性能显著下降. 为缓解反例生成中的路径爆炸问题, 基于系统模型与规约提出路径过滤与动态选择两种技术. 首先, 设计面向规约的路径过滤方法, 通过分析系统规约的语法树和路径上的行为约束, 快速过滤不可能包含不安全行为的路径. 其次, 引入多臂老虎机算法来指导反例生成过程中路径的动态选择, 动态调整用于探索不同路径的计算资源以最大化反例生成的性能. 在一系列经典测试案例上的实验结果表明, 所提方法显著缓解了路径爆炸问题, 提高了CPS系统反例生成的效率和性能, 将发现不安全行为的成功率提升了两倍以上.

摘要:Rust作为一种新兴的安全系统级编程语言, 以其创新的所有权模型和借用检查机制提供了内存安全和并发安全保证. 尽管Rust的设计宗旨在于安全性, 但现有研究揭示了其仍面临诸多安全挑战. 形式化验证作为一种基于严格数学基础的方法, 为Rust安全性提升提供了强有力保障. 通过构建精准清晰的语义模型, 可以证明遵循Rust检查规则的程序满足安全性要求; 借助Rust自动化验证工具能够帮助用户确保其Rust程序的安全性和正确性. 对Rust形式化验证工作进行全面系统性分析. 首先介绍Rust核心语义和复杂特性, 并探讨Rust形式化语义的研究与验证工作, 强调Rust类型系统在形式化验证中的潜力. 其次, 阐述面向Rust程序的自动化验证方法, 并对比分析不同验证工具的功能、支持的语言特性、采用的验证技术和适用场景, 这对于在Rust项目实际开发流程中指导工具的选择和集成有重要意义. 此外, 还总结Rust程序验证的典型实例, 展示形式化验证在确保程序正确性方面的显著成效, 并结合验证实例总结工具使用建议供用户参考. 最后讨论当前领域的技术挑战, 并指出未来可能的研究方向, 涵盖了unsafe Rust代码的验证、并发代码的验证、可信编译, 以及大模型驱动的形式化验证等. 旨在为Rust社区提供坚实的安全基础, 并推动形式化验证在Rust开发中的应用.

摘要:随着智能信息物理融合系统(intelligent cyber-physical system, ICPS)的快速发展, 智能技术在感知、决策、规控等方面的应用日益广泛. 其中, 深度强化学习因其在处理复杂的动态环境方面的高效性, 已被广泛用于ICPS的控制组件中. 然而, 由于运行环境的开放性和ICPS系统的复杂性, 深度强化学习在学习过程中需要对复杂多变的状态空间进行探索, 这极易导致决策生成时效率低下和泛化性不足等问题. 目前对于该问题的常见解决方法是将大规模的细粒度马尔可夫决策过程(Markov decision process, MDP)抽象为小规模的粗粒度马尔可夫决策过程, 从而简化模型的计算复杂度并提高求解效率. 但这些方法尚未考虑如何保证原状态的时空语义信息、聚类抽象的系统空间和真实系统空间之间的语义一致性问题. 针对以上问题, 提出基于因果时空语义的深度强化学习抽象建模方法. 首先, 提出反映时间和空间价值变化分布的因果时空语义, 并在此基础上对状态进行双阶段语义抽象以构建深度强化学习过程的抽象马尔可夫模型; 其次, 结合抽象优化技术对抽象模型进行调优, 以减少抽象状态与相应具体状态之间的语义误差; 最后, 结合车道保持、自适应巡航、交叉路口会车等案例进行了大量的实验, 并使用验证器PRISM对模型进行评估分析, 结果表明所提出的抽象建模技术在模型的抽象表达能力、准确性及语义等价性方面具有较好的效果.