摘要:

摘要:当前的量子程序一般由量子电路表示, 由多个量子门组成. 如果程序包含了被直接表示为酉矩阵的门, 需要将这些量子门转化为基本门所构成的量子电路. 该步骤被称为量子电路合成. 然而, 当前的合成方法可能会生成包含数千个门的量子电路. 这些量子电路的质量较低, 在部署到真实含噪声的量子硬件时非常容易输出错误的结果. 此外, 在保证门数量较小的情况下, 当量子比特数量增至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对模型进行评估分析, 结果表明所提出的抽象建模技术在模型的抽象表达能力、准确性及语义等价性方面具有较好的效果.

摘要:最小弱连通支配集问题是一个经典的NP难问题, 在许多领域都有广泛的应用. 提出一种高效的局部搜索算法求解该问题. 在该算法中, 首先采用一个基于锁定顶点和频率反馈信息的初始解构造方法. 该方法可以确保将一定处于最优解中的顶点和大概率存在于最优解中的顶点添加到初始解中, 从而可以得到高质量的初始解. 其次, 提出基于双层格局检测策略, 年龄属性和禁忌策略的方法来避免循环问题. 第三, 提出扰动策略, 使得算法能够有效跳出局部最优. 第四, 将两个评分函数Dscore和Nscore与避免循环问题的策略相结合, 提出有效的顶点选择方法, 帮助算法选择适合添加到候选解中或从当前候选解中删除的顶点. 最后, 与现有的最优启发式算法和CPELX求解器, 在4组基准测试实例上对提出的局部搜索算法进行了对比. 实验结果表明, 该算法在4组经典基准测试实例上表现出更好的性能.

摘要:最小负载着色问题(minimum load coloring problem, MLCP) 源于构建光通信网络的波分复用(wavelength division multiplexing, WDM)技术, 是一个被证明的NP完全问题. 由于NP完全问题有着随问题规模呈指数增长的解空间, 因此启发式算法常被用来解决这类问题. 在对国内外相关工作的深入分析基础上得知, 现有的多类求解MLCP问题的启发式算法中局部搜索算法表现是最好的. 研究针对当前求解MLCP问题的局部搜索算法在数据预处理和邻域空间搜索上的不足, 提出了两点相应的优化策略: 一是在数据的预处理阶段, 提出一度顶点规则来约简数据的规模, 进而减小MLCP问题的搜索空间; 二是在算法的邻域空间搜索阶段, 提出两阶段多重选择策略(two-stage best from multiple selections, TSBMS)来帮助局部搜索算法在面对不同规模的邻域空间时可以高效地选择一个高质量的邻居解, 它有效地提高了局部搜索算法在处理不同规模数据时的求解表现. 将这个优化后的局部搜索算法命名为IRLTS. 采用74个经典的测试用例来验证IRLTS算法的有效性. 实验结果表明, 无论最优解还是平均解, IRLTS算法在大多数测试用例上都明显优于当前表现最好的3个局部搜索算法. 此外, 还通过实验验证了所提策略的有效性以及分析了关键参数对算法的影响.

摘要:随着城市规模不断增加, 城市交通系统面临着越来越多的挑战, 如交通拥堵、交通安全等问题. 交通仿真是一种解决城市交通问题的方法, 其采用虚实结合的计算技术, 以处理实时交通数据、优化城市交通效率, 是平行城市理论在智能交通的重要实现方法. 然而, 传统的计算系统在运行大规模城市交通仿真中会出现计算资源不足、仿真延迟过长等问题. 针对上述问题, 基于平行城市理论, 结合天河新一代超算的异构体系结构, 提出一种平行城市交通仿真并行算法. 该算法能够精确模拟车辆、道路、交通信号等交通要素, 并采取路网划分、车辆并行化行驶、信号灯并行化控制等方法, 以实现高性能交通仿真. 该算法运行在16节点、超过2.5万核心的天河新一代超算平台, 并针对北京市五环内240万辆车、7797个路口和17万条车道的真实交通场景进行仿真. 相比于传统的单节点仿真, 每步仿真时间从2.21 s减少到0.37 s, 取得近6倍的加速效果, 在国产超算异构平台上成功实现百万车辆规模的城市交通仿真.

摘要:软件概念漂移指同类型软件的软件结构和组成成分会随着时间的推移而改变. 在恶意软件分类领域, 发生概念漂移意味着同一家族的恶意样本的结构和组成特征会随时间发生变化, 这会导致固定模式的恶意软件分类算法的性能会随时间推移而发生下降. 现有的恶意软件静态分类研究方法在面临概念漂移场景时都会有显著的性能下降, 因此难以满足实际应用的需求. 针对这一问题, 鉴于自然语言理解领域与二进制程序字节流分析领域的共性, 基于BERT和自定义的自编码器架构提出一种高精度、鲁棒的恶意软件分类方法. 该方法首先通过反汇编分析提取执行导向的恶意软件操作码序列, 减少冗余信息; 然后使用BERT理解序列的上下文语义并进行向量嵌入, 有效地理解恶意软件的深层程序语义; 再通过几何中位数子空间投影和瓶颈自编码器进行任务相关的有效特征筛选; 最后通过全连接层构成的分类器输出分类结果. 在普通场景和概念漂移场景中, 通过与最先进的9种恶意软件分类方法进行对比实验验证所提方法的实际有效性. 实验结果显示: 所提方法在普通场景下的分类F1值达到99.49%, 高于所有对比方法, 且在概念漂移场景中的分类F1值比所有对比方法提高10.78%–43.71%.

摘要:模糊测试技术能够自动化挖掘软件当中的漏洞, 然而目前针对网络协议的模糊测试工具对于协议实现内部状态空间探索有限, 导致覆盖率较低. 有限状态机技术能够对网络协议实现进行全方位建模, 以深入了解网络协议实现的系统行为和内部状态空间. 将有限状态机技术和模糊测试技术相结合, 提出一种基于有限状态机引导的网络协议模糊测试方法. 以广泛使用的TLS协议为研究对象, 利用有限状态机学习来对于TLS协议实现进行建模, 用来反映协议内部状态空间及其系统行为. 随后, 基于有限状态机对于TLS协议模糊测试进行引导, 使模糊测试的深度更深、覆盖代码更广. 为此, 实现一个原型系统SNETFuzzer, 并且通过一系列对比实验发现SNETFuzzer在覆盖率等重要指标中优于已有工作. SNETFuzzer在实验中成功发现多个漏洞, 其中包含两个新漏洞, 证明了其实用性和有效性.

摘要:代码注释生成是软件工程领域的重要研究任务. 当前主流的注释生成方法训练深度学习模型以生成注释, 依靠在开放的代码注释数据集上采用BLEU等指标来进行注释质量评价, 主要反映生成注释与数据集中人工参考注释的相似性. 但由于开放注释数据集中人工参考注释的质量难以保障, 其有效性受到越来越多质疑. 因此, 面向代码注释生成任务, 亟需一种直观有效的代码注释质量评价方法, 一方面改进开放注释数据集的质量, 另一方面提升生成注释的评价效果. 针对该问题, 对现有量化的注释质量评价方法进行调研和分析, 并将一套多维度注释质量评价指标用于对主流开放数据集、典型注释生成方法以及ChatGPT生成代码注释的质量评价, 由此给出一些具有参考价值的研究发现: 1)现有主流开放数据集中的代码注释质量俱有待提高, 均存在不同程度的不准确、可读性差、过于简短、缺乏有用信息等问题; 2)现有方法生成的注释普遍在词汇和语义上与代码更接近, 缺乏代码高层意图等对开发者更有用的信息; 3)生成注释的BLEU值较低, 一个重要原因是数据集中大量的参考注释本身质量不佳, 譬如与代码缺乏关联、自然性较差等, 应过滤或改进此种参考注释; 4)大语言模型ChatGPT生成的代码注释内容丰富但较为冗长, 其质量评价需要根据开发者意图与具体场景进行针对性改进. 基于这些发现, 也对未来代码注释生成任务及注释质量评价研究给出若干建议.

摘要:学习型索引因其低内存占用和高查询性能的特点, 正辅助或逐步取代传统的索引结构. 然而, 数据更新导致的在线重新训练使其无法适应数据频繁更新的场景. 为了在不过多消耗内存的前提下尽量避免由于数据频繁更新导致的索引重构, 提出了一种自适应的感知更新分布学习型索引结构DRAMA. 使用类LSM-Tree的延迟学习方式主动学习数据更新的分布特征; 利用近似拟合技术快速建立更新分布模型; 采用模型合并策略代替频繁的重训练过程; 采用一种混合压缩技术降低索引中模型参数的内存占用率. 在真实和合成的数据集上构建了索引并进行验证. 结果表明, 相比于传统索引和最先进的学习型索引, 该索引可以在不额外消耗过多内存的情况下, 有效降低数据更新环境下的查询延迟.

摘要:交通流预测是智能交通系统(intelligent transportation system, ITS)中交通管理的重要基础和热门研究方向. 传统的交通流预测方法通常需要借助大量高质量历史观测数据进行预测, 而针对更为普遍的数据稀缺的交通路网场景预测精度则急剧下降. 针对这一问题, 提出一种基于时空图卷积网络的迁移学习模型(transfer learning based on spatial-temporal graph convolutional network, TL-STGCN), 结合数据充足的源路网的交通流特征, 辅助预测数据稀缺的目标路网未来交通流. 首先, 采用基于时间注意力的时空图卷积网络学习源路网和目标路网交通流数据的时空特征表示; 其次, 结合迁移学习方法, 提取两个路网特征表示的域不变时空特征; 最后, 利用这些域不变时空特征对目标路网未来交通流做出预测. 为了验证模型的有效性, 在真实世界数据集上进行实验. 结果表明, 与现有方法对比, TL-STGCN在平均绝对误差、均方根误差以及平均绝对百分比误差指标中均取得最高精度, 证明对于数据稀缺的交通路网预测任务, TL-STGCN具有更好的预测性能.

摘要:Rollup是一种新兴的区块链链下交易处理方案. 随着应用的持续发展 , 不同类型Rollup间的互操作需求日益增长. 现有Rollup间互操作方案通常使用第三方服务商来协助完成, 存在着信任假设的安全风险和单点故障等问题. 基于原生链完成Rollup间互操作无需引入新的信任假设, 但会消耗原生链的计算与存储资源, 降低原生链的交易吞吐量, 从而严重影响跨Rollup性能. 基于此, 提出一种基于原生链的跨Rollup方案, 通过聚合交易批量处理的方式, 有效减少单笔交易的链上平均计算与存储资源开销. 具体而言, 提出基于零知识证明的交易有效性证明方案, 显著减少交易有效性验证的链上计算开销. 提出基于索引表数据压缩的交易存储方案, 降低跨Rollup交易的平均链上存储开销. 提出聚合规模均衡调整算法, 得到最优的聚合规模, 实现链上资源消耗与处理时延之间的平衡. 最后, 对方案进行实验验证. 实验结果表明, 所提方案在完全去信任化的前提下, 能降低链上计算开销和存储开销, 实现链上资源消耗与处理时延的平衡, 并且与现有跨Rollup方案相比, 所提方案的系统吞吐量也具有很好的表现.

摘要:传统的分布式拒绝服务攻击(DDoS)检测与防御机制需要对网络流量进行镜像、采集以及远程集中式的攻击特征分析, 这直接造成额外的性能开销, 无法满足高性能网络的实时安全防护需求. 随着可编程交换机等新型网络设备的发展, 可编程数据平面能力得到增强, 为直接在数据面进行高性能的DDoS攻击检测提供了实现基础. 然而, 当前已有的基于可编程数据面的DDoS攻击检测方法准确率低, 同时受限于编程约束, 难以在可编程交换机 (如Intel Tofino)中进行直接部署. 针对上述问题, 提出了一种基于可编程交换机的DDoS攻击检测与防御机制. 首先, 使用基于源目地址熵值差的攻击检测机制判断DDoS攻击是否发生. 在DDoS攻击发生时, 设计了一种基于源目地址计数值差的攻击流量过滤机制, 实现对DDoS攻击的实时防御. 实验结果表明, 该机制能够有效地检测并防御多种DDoS攻击. 相较于现有工作, 该机制在观察窗口级攻击检测中的准确率平均提升了17.75%, 在数据包级攻击流量过滤中的准确率平均提升了3.7%.

摘要:动态对称可搜索加密允许用户安全地搜索和动态更新存储在半可信云服务器中的加密文档, 近年来备受关注. 然而, 现有多数对称可搜索加密方案仅支持单关键词搜索, 无法在实现联合搜索的同时满足前向和后向隐私. 此外, 多数方案不具有鲁棒性, 即无法处理客户端重复添加或删除某个关键词/文件标识符对或删除不存在的关键词/文件标识符对等不合理更新请求. 针对上述挑战, 提出一个鲁棒的前后向隐私联合动态对称可搜索加密方案RFBC. 在该方案中, 服务器为每个关键词建立两个布隆过滤器, 分别用于存储所要添加和删除的关键词/文件标识符对的相关哈希值. 当客户端发送更新请求时, 服务器利用两个布隆过滤器进行判断, 过滤不合理请求, 以满足方案的鲁棒性. 此外, 利用多关键词中最低频关键词的状态信息, 结合布隆过滤器与更新计数器, 筛选掉不包含其余关键词的文件标识实现联合查询. 通过定义方案的泄露函数, 经过一系列的安全性游戏证明RFBC支持前向隐私与Type-III后向隐私. 实验分析表明相较于相关方案, RFBC较大幅度提高了计算和通信效率. 具体来说, RFBC更新操作的计算开销分别为ODXT和BDXT的28%和61.7%, 搜索操作的计算开销分别为ODXT和BDXT的21.9%和27.3%, 而搜索操作的通信开销分别为ODXT和BDXT的19.7%和31.6%. 而且, 当不合理更新的比例逐渐增加时, 搜索效率的提升明显高于BDXT与ODXT.

摘要:随着物联网和移动互联网技术的发展, 各类移动终端设备被接入互联网中. 当对移动终端设备进行识别和认证时, 通常需要验证其提交的数字签名. 但移动终端设备本身的计算能力受限, 往往采用软件模块来保存密钥至本地或者智能芯片中, 增加了密钥泄露的风险. 现实应用中多采用门限数字签名来抵抗这一攻击, 借助多方合作来分散风险, 提升设备可用性. SM2数字签名算法是我国自主研发的椭圆曲线公钥密码算法, 于2016年成为国家密码标准, 被广泛应用于政府部门、金融机构、电子认证服务提供商等领域. 设计高可用的门限SM2数字签名备受关注, 但这类方案的构造依旧较少, 同时也缺乏对参与者权重的考量. 因此, 提出更加灵活的加权门限SM2数字签名方案. 在加权门限SM2数字签名中签名者分配不同权重, 之后多个签名者共同生成一个有效的签名. 在方法上, 基于中国剩余定理的加权门限秘密共享将SM2数字签名的秘钥进行分割. 参与者不只是单一的达到门限值就可以得到签名密钥, 而需要通过计算参与者权重之和, 并达到相应的秘密门限值t和重构门限T, 才能了解到密钥的部分信息或者恢复出签名密钥. 在秘密分割时, 对SM2数字签名算法的签名私钥进行变形, 以完成签名阶段对SM2密钥进行求逆的这一操作. 最后, 将所提方案与门限SM2签名以及联合SM2签名等已有工作进行分析比较, 该算法在提升SM2签名方案功能性的同时进一步降低了计算开销.

摘要:随着Transformer类大模型的飞速发展, 算力逐渐成为制约领域发展的瓶颈, 如何根据加速器硬件的结构特性加速和优化大语言模型的训练性能已成为研究热点. 面向天河新一代超算系统的加速芯片MT-3000, 提出并实现了适用于CPU+DSP异构架构的PyTorch扩展库——MTTorch, 其核心是一个多核并行的算子库, 对Transformer类模型训练过程中的核心算子进行向量化实现和优化. 同时, 针对MT-3000架构特性, 提出了面向多核 DSP 的高性能规约算法及乒乓算法, 显著提升了算子的运算性能. MTTorch还具有很好的通用性, 对于不同版本的 PyTorch都可以动态链接库的形式进行加载, 不改变PyTorch的原生实现. 大量实验证明, 实现的核心算子在 MT-3000 芯片上有着很好的性能, 在单DSP 簇上可以达到 8 倍的加速效果. 利用MTTorch在多节点执行训练任务时有着接近线性的加速比, 极大地提升了Transformer类模型在MT-3000 芯片上的训练效率.