摘要:

摘要:近年来，形式化验证技术受到了越来越多的关注，它在保障安全关键领域系统的安全性和正确性方面发挥着重要的作用.模型检测作为形式化验证中自动化程度较高的分支，具有十分广阔的发展前景.研究并提出了一种新的模型检测技术，可以有效地对迁移系统进行模型检测，包括不安全性检测和证明安全性.与现有的模型检测算法不同，提出的基于不可满足核（unsatisfied core，UC）的近似逼近可达性分析（UC-based approximate incremental reachability，UAIR），主要利用不可满足核来求解一系列的候选安全不变式，直至生成最终的不变式，以此来实现安全性证明和不安全性检测（漏洞查找）.在基于SAT求解器的符号模型检测中，使用由可满足性求解器得到的UC构造候选安全不变式，如果迁移系统本身是安全的，得到的初始不变式只是安全不变式的一个近似.然后，在检查安全性的同时，逐步改进候选安全不变式，直到找到一个真正的不变式，证明系统是安全的；如果系统是不安全的，该方法最终可以找到一个反例证明系统是不安全的.作为一种全新的方法，利用不可满足核进行安全性模型检测，取得了相当好的效果.众所周知，模型检测领域没有绝对最好的方法，尽管该方法在基准的可解数量上无法超越当前的成熟方法，例如IC3，CAR等，但是该方法可以解出3个其他方法都无法解出的案例，相信本方法可以作为模型检测工具集很有价值的补充.

摘要:约束求解应用到程序分析的多个领域，在并发程序分析方面也得到了深入的应用.并发程序随着多核处理器的快速发展而得到广泛使用，然而并发缺陷对并发程序的安全性和可靠性造成了严重的影响，因此，针对并发缺陷的检测尤为重要.并发程序线程运行的不确定性导致的线程交织爆炸问题，给并发缺陷的检测带来了一定挑战.已有并发缺陷检测算法通过约减无效线程交织，以降低在并发程序状态空间内的探索开销.比如，最大因果模型算法把并发程序状态空间的探索问题转换成约束求解问题.然而，其在约束构建过程中会产生大量冗余和冲突的约束，大幅度增加了约束求解的时间以及约束求解器的调用次数，降低了并发程序状态空间的探索效率.针对上述问题，提出了一种有向图约束指导的并发缺陷检测方法GC-MCR （directed graph constraint-guided maximal causality reduction）.该方法旨在通过使用有向图对约束进行过滤和约减，从而提高约束求解速度，并进一步提高并发程序状态空间的探索效率.实验结果表明：GC-MCR方法构建的有向图可以有效优化约束的表达式，从而提高约束求解器的求解速度并减少求解器的调用次数.与现有的J-MCR方法相比，GC-MCR的并发程序缺陷检测效率可以取得显著提升，且不会降低并发缺陷的检测能力，在现有研究方法广泛使用的38组并发测试程序上的测试时间可以平均减少34.01%.

摘要:TrustZone作为ARM处理器上的可信执行环境技术，为设备上安全敏感的程序和数据提供一个隔离的独立执行环境.然而，可信操作系统与所有可信应用运行在同一个可信环境中，任意组件上的漏洞被利用都会波及系统中的其他组件.虽然ARM提出了S-EL2虚拟化技术，支持在安全世界建立多个隔离分区来缓解这个问题，但实际分区管理器中仍可能存在分区间信息泄漏等安全威胁.当前的分区管理器设计及实现缺乏严格的数学证明来保证隔离分区的安全性.详细研究了ARM TrustZone多隔离分区架构，提出一种基于精化的TrustZone多安全分区建模与安全性分析方法，并基于定理证明器Isabelle/HOL完成了分区管理器的建模和形式化验证.首先，基于逐层精化的方法构建了多安全分区模型RMTEE，使用抽象状态机描述系统运行过程和安全策略要求，建立多安全分区的抽象模型并实例化实现分区管理器的具体模型，遵循FF-A规范在具体模型中实现了事件规约；其次，针对现有分区管理器设计无法满足信息流安全性验证的不足，设计了基于DAC的分区间通信访问控制，并将其应用到TrustZone安全分区管理器的建模与验证中；再次，证明了具体模型对抽象模型精化的正确性以及具体模型中事件规约的正确性和安全性，从而完成模型所述137个定义和201个定理的形式化证明（超过11 000行Isabelle/HOL代码）.结果表明：该模型满足机密性和完整性，并可有效防御分区的恶意攻击.

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

摘要:离散数学是计算机类专业的基础课程之一，命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明，初学者准确理解语法、语义、推理系统等抽象概念是有一定难度的.近年来，已有一些学者开始在教学中引入交互式定理证明工具，以帮助学生构造形式化证明，更透彻地理解逻辑系统.然而，现有的定理证明器有较高上手门槛，直接使用会增加学生的学习负担.鉴于此，在Coq中开发了针对教学场景的ZFC公理集合论证明器.首先，形式化了一阶逻辑推理系统和ZFC公理集合论；之后，开发了数条自动化推理规则证明策略.学生可以在与教科书风格相同的简洁证明环境中使用自动化证明策略完成定理的形式化证明.该工具被用在了大一新生离散数学课程的教学中，没有定理证明经验的学生使用该工具可以快速完成数学归纳法和皮亚诺算术系统等定理的形式化证明，验证了该工具的实际效果.

摘要:公理定位能够挖掘描述逻辑中可解释的缺陷，并为逻辑蕴含结果寻找隐藏的理由，因此在描述逻辑研究中引起了广泛的关注.平衡描述逻辑表达能力和推理机求解效率问题一直是公理定位研究的重点内容.基于一种后继式判定算法，从白盒和黑盒两个角度将其用于公理定位.白盒方法利用修正的后继式规则（即定位规则）来追踪推理的具体过程，并引入定位公式的概念建立子句的布尔公式标签与逻辑蕴含的所有极小公理集之间的对应关系.黑盒方法则直接调用基于未修正的后继式规则的推理机，并进一步利用碰集树方法求得逻辑蕴含的所有理由.最后，基于这样的两种面向强表达描述逻辑本体的公理定位算法设计推理工具，从理论和实验两方面验证其可行性，并与已有的推理工具比较求解性能.

摘要:随着新兴技术的迅速发展, 领域软件对开发效率提出了新的要求. Datalog语言作为一门具有简洁语法和良好语义的声明式编程语言, 能帮助开发人员快速开发和解决问题, 近年来越来越受到重视与欢迎. 但解决真实场景问题时, 现有的单机Datalog引擎计算规模往往受限于内存容量大小, 不具有可扩展性. 为解决上述问题, 设计并实现基于核外计算的Datalog引擎. 方法首先设计一系列计算Datalog程序所需的支持核外计算的操作算子, 然后将Datalog程序转换合成带核外计算算子的C++程序, 接着方法设计基于Hash的分区策略和基于搜索树剪枝的最少置换调度策略, 将相应的分区文件调度执行计算并得到最终结果. 基于该方法, 实现原型工具DDL (disk-based Datalog engine), 并选取广泛应用的真实Datalog程序, 在合成数据集以及真实数据集上进行实验, 实验结果体现了DDL良好性能以及高可扩展性.

摘要:特征请求是软件产品的真实用户在开放平台上提出的对现有特征的改进或者对新特征的请求. 特征请求在一定程度上反映了用户的真实意愿, 代表了用户的需求. 高效、准确地分析和处理用户特征请求对于提升用户满意度、提高产品竞争力起着至关重要的作用. 用户的广泛参与, 使得特征请求成为越来越重要的需求来源. 然而, 特征请求在其来源、内容以及形式等方面均与传统的软件需求不同. 进而将其充分应用于软件开发过程所采用的具体方法, 也有别于传统的需求工程. 目前已经有许多将特征请求应用于软件开发过程中的相关研究, 比如特征请求的获取、分类、排序、质量评估、为特征请求推荐开发者, 以及定位相关代码等. 随着相关工作的不断增加, 形成一个针对特征请求分析与处理研究综述的必要性日益增强. 因此, 调研121篇关于在软件开发过程中分析和处理特征请求的国内外学术研究论文, 从将特征请求应用于软件开发过程的角度对现有成果进行系统地梳理. 总结现有针对特征请求的研究主题, 提出将特征请求应用于软件开发过程的处理流程, 并与传统的需求工程过程进行对比. 此外, 深入分析在各个需求工程活动中使用的具体方法及方法之间的差别. 最后, 对特征请求的未来研究方向进行展望, 以期为同行研究人员提供参考.

摘要:可信执行环境(TEE)的安全问题一直受到国内外学者的关注. 利用内存标签技术可以在可信执行环境中实现更细粒度的内存隔离和访问控制机制, 但已有方案往往依赖于测试或者经验分析表明其有效性, 缺乏严格的正确性和安全性保证. 针对内存标签实现的访问控制提出通用的形式化模型框架, 并提出一种基于模型检测的访问控制安全性分析方法. 首先, 利用形式化方法构建基于内存标签的可信执行环境访问控制通用模型框架, 给出访问控制实体的形式化定义, 定义的规则包括访问控制规则和标签更新规则; 然后利用形式化语言B以递增的方式设计并实现该框架的抽象机模型, 通过不变式约束形式化描述模型的基本性质; 再次以可信执行环境的一个具体实现TIMBER-V为应用实例, 通过实例化抽象机模型构建TIMBER-V访问控制模型, 添加安全性质规约并运用模型检测验证模型的功能正确性和安全性; 最后模拟具体攻击场景并实现攻击检测, 评估结果表明提出的安全性分析方法的有效性.

摘要:自动机的确定化是将非确定性自动机转换为接收相同语言的确定性自动机, 是自动机理论的基本问题之一. ω自动机的确定化是诸多逻辑, 如SnS, CTL*, μ演算等, 判定过程的基础, 同时也是解决无限博弈求解问题的关键, 因此对ω自动机确定化的研究具有重要意义. 主要关注一类ω自动机——Streett自动机的确定化. 非确定性Streett自动机可以转换为等价的确定性Rabin或Parity自动机, 在前期工作中已经分别得到了状态复杂度最优以及渐进最优算法, 为了验证提出的算法的实际效果, 也为了形象地展示确定化过程, 开发一款支持Streett自动机确定化的工具是必要的. 首先介绍4种不同的Streett确定化结构: μ-Safra tree和H-Safra tree (最优)将Streett确定化为Rabin自动机, compact Streett Safra tree和LIR-H-Safra tree (渐进最优)将Streett确定化为Parity自动机; 然后, 根据Streett确定化算法, 基于开源工具GOAL (graphical tool for omega-automata and logics), 实现了Streett确定化工具NS2DR&PT, 以支持上述4种结构; 最后, 通过随机生成100个Streett自动机, 构造相应的测试集, 进行对比实验, 结果表明各结构状态复杂度的实际效果与理论论证一致, 此外, 对运行效率也进行了比较分析.

摘要:异步程序使用异步非阻塞调用方式来实现程序的并发, 被广泛应用于并行与分布式系统中. 验证异步程序复杂性很高, 无论是安全性还是活性均达到EXPSPACE难. 提出一个异步程序的程序模型系统, 并在其上定义两个异步程序上的问题: $ \epsilon $等价性问题和$ \epsilon $可达性问题. 通过将3-CNF-SAT规约到这两个问题, 再将其规约至非交互式Petri网的可达性证明两个问题是NP完备的. 案例表明, 这两个问题可以解决异步程序上一系列的程序验证问题.

摘要:各类安全攸关系统的可靠运行离不开软件程序的正确执行. 程序的演绎验证技术为程序执行的正确性提供高度保障. 程序语言种类繁多, 且用途覆盖高可靠性场景的新式语言不断涌现, 难以为每种语言设计支撑其程序验证任务的整套逻辑规则, 并证明其相对于形式语义的可靠性和完备性. 语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果. 对每种程序语言, 提供其形式语义后可直接获得面向该语言的程序验证过程. 提出一种面向大步操作语义的语言无关演绎验证技术, 其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法. 特别地, 借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力, 从而允许借助辅助信息对子结构进行推理. 证明所提出验证技术的可靠性和相对完备性, 通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性, 并在Coq辅助证明工具中形式化了所有理论结果和验证实例, 为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.

摘要:随着移动通信的发展, 迎来了第5代移动通信技术(5G). 5G认证与密钥协商 (5G authentication and key agreement, 5G-AKA)协议的提出主要是为了实现用户和服务网络的双向鉴权. 然而, 最近的研究认为其可能会遭受信息破译和消息重放攻击. 同时, 发现当前5G-AKA的一些变种不能满足协议的无连接性. 针对上述缺陷, 提出一个改进方案: SM-AKA. SM-AKA由两个并行子协议组成, 通过巧妙的模式切换使更加轻量的子协议(GUTI子模块)被频繁采用, 而另一个子协议(SUPI子模块)则主要用于异常发生时的鉴权. 依据这种机制, 它不仅实现用户和归属网之间的高效认证, 还能提升鉴权的稳定性. 此外, 变量的新鲜性也得到有效维持, 可以防止消息的重放, 而严格的加解密方式进一步提升协议的安全性. 最后, 对SM-AKA展开完整的评估, 通过形式建模、攻击假定和Tamarin推导, 证明该方案可以达到鉴权和隐私目标, 而理论分析部分也论证了协议性能上的优势.

摘要:数据竞争是多线程程序的常见漏洞之一, 传统的数据竞争分析方法在查全率和准确率方面难以两全, 而且所生成检测报告难以定位漏洞的根源. 鉴于Petri网在并发系统建模和分析方面具有行为描述精确、分析工具丰富的优点, 提出一种基于Petri网展开的新型数据竞争检测方法. 首先, 对程序的某一运行轨迹进行分析和挖掘, 构建程序的一个Petri网模型, 它由单一轨迹挖掘得到, 却可隐含程序的多个不同运行轨迹, 由此可在保证效率的同时降低传统动态分析方法的漏报率; 其次, 提出基于Petri网展开的潜在数据竞争检测方法, 相比静态分析方法在有效性上有较大提升, 而且能明确给出数据竞争的产生路径; 最后, 对上一阶段检测到的潜在数据竞争, 给出基于CalFuzzer平台的潜在死锁重演调度方法, 可剔除误报, 保证数据竞争检测结果的真实性. 开发相应的原型系统, 结合公开的程序实例验证了所提方法的有效性.

摘要:经过多年的技术发展和攻防对抗, Android平台应用加固技术已较为成熟, 防护粒度逐步从通用的DEX动态修改发展为高度定制化的Native层混淆机制, 通过不断提高逆向分析的难度和工作量, 增强客户端代码防护能力. 针对近期崛起的OLLVM混淆加固技术, 提出一种基于Capstone和流敏感混合执行的自动化反混淆决方案(CiANa). CiANa采用Capstone引擎分析基本块及其指令结构, 识别散落在程序反汇编控制流程图中的真实块, 并基于流敏感的混合执行确定各真实块间的执行顺序, 最后对真实块汇编指令进行指令修复得到反混淆后的可执行二进制文件. 实验对比结果表明, CiANa可有效恢复ARM/ARM64架构下经OLLVM混淆的Android Native文件. CiANa是目前为止首个在ARM/ARM64架构中, 支持对全版本(Debug/Realse版本) OLLVM进行有效反混淆并生成可执行文件的框架, 为逆向分析提供了必要的辅助支撑.

摘要:近年来, 随着电影、游戏、虚拟现实应用等对真实感要求的不断提高, 针对人体组织、牛奶等半透明材质的实时渲染变得越发重要. 针对当前大部分次表面散射计算方法难以正确估计散射范围的问题, 提出了一种全新的次表面散射计算方法用以精确表示最大散射距离. 首先, 针对暴力蒙特卡洛光子追踪结果进行模拟, 以得到反射剖面结果. 其次通过多项式模型进行反射剖面拟合, 计算精确着色点处的最大散射范围. 最后, 提出了一种新的重要性采样方案以减少蒙特卡洛所需的采样数, 进一步提高计算效率. 此外, 方法所需的参数仅由着色点上的反射率以及材质平均自由程提供, 以便于灵活调整渲染效果. 实验证明, 所提模型避免了之前对于散射范围的错误估计, 对材质反射率复杂的区域具有更好的渲染精度, 且渲染速率满足实时要求.

摘要:近年来, 人工智能技术突飞猛进, 人工智能系统已经渗透到人们生活中, 成为人们生活中不可或缺的一部分. 然而, 人工智能系统需要数据训练模型, 数据扰动会对其结果造成影响. 并且随着人工智能系统业务多样化, 规模复杂化, 人工智能系统的可信性愈发受到人们的关注. 首先, 在梳理不同组织和学者提出的人工智能系统可信属性基础上, 提出人工智能系统的9个可信属性; 接着, 从数据可信性、模型可信性和结果可信性分别介绍现有的人工智能系统数据、模型、结果可信性度量方法, 设计人工智能系统可信证据收集方法. 其次, 总结当前人工智能系统的可信度量评估理论与方法. 然后, 结合基于属性的软件可信评估方法与区块链技术, 建立一个人工智能系统可信度量评估框架, 包括可信属性分解及可信证据获取方法、联邦式可信度量模型与以及基于区块链的人工智能系统可信度量评估架构. 最后, 讨论人工智能系统可信度量技术面临的机遇和挑战.

摘要:近年来, 随着全球定位系统(global positioning system, GPS)的大范围应用, 越来越多的电动自行车装配了GPS传感器, 由此产生的海量轨迹数据是深入了解用户出行规律、为城市规划者提供科学决策支持等诸多应用的重要基础. 但是, 电动自行车上普遍使用的价格低廉的GPS传感器无法提供高精度的定位, 同时, 电动自行车轨迹地图匹配过程因以下原因更具有挑战性: (1)存在大量停留点; (2)高采样频率导致相邻轨迹点的距离较短; (3)电动自行车可行驶的路段更多, 存在大量无效轨迹. 针对上述问题, 提出一种可自适应路网精度的电动自行车轨迹地图匹配方法KFTS-AMM. 该方法融合基于分段卡尔曼滤波算法的轨迹简化算法(KFTS), 和分段隐马尔可夫模型的地图匹配算法(AMM). 首先, 利用卡尔曼滤波算法可用于最优状态估计的特性, KFTS能够在轨迹简化过程中对轨迹点进行自动修正, 使轨迹曲线变得平滑并减少了异常点对于地图匹配准确率的影响. 同时, 使用基于分段隐马尔可夫模型的地图匹配算法AMM, 避免部分无效轨迹对整条轨迹匹配的影响. 此外, 在轨迹数据的处理过程加入了停留点的识别与合并, 进一步提升匹配准确率. 在郑州市真实电动自行车轨迹数据的实验结果表明, KFTS-AMM在准确率上相对于已有的对比算法有较大的提升, 并可通过使用简化后的轨迹数据显著提升匹配速度.

摘要:近年来, 深度强化学习在序列决策领域被广泛应用并且效果良好, 尤其在具有高维输入、大规模状态空间的应用场景中优势明显. 然而, 深度强化学习相关方法也存在一些局限, 如缺乏可解释性、初期训练低效与冷启动等问题. 针对这些问题, 提出了一种基于显式知识推理和深度强化学习的动态决策框架, 将显式的知识推理与深度强化学习结合. 该框架通过显式知识表示将人类先验知识嵌入智能体训练中, 让智能体在强化学习中获得知识推理结果的干预, 以提高智能体的训练效率, 并增加模型的可解释性. 将显式知识分为两种, 即启发式加速知识与规避式安全知识. 前者在训练初期干预智能体决策, 加快训练速度; 而后者将避免智能体作出灾难性决策, 使其训练过程更为稳定. 实验表明, 该决策框架在不同强化学习算法上、不同应用场景中明显提高了模型训练效率, 并增加了模型的可解释性.

摘要:为汽车自动驾驶提供安全高效的自动驾驶行为决策, 是汽车自动驾驶领域面临的挑战性问题之一. 目前, 随着自动驾驶行业的蓬勃发展, 工业界与学术界提出了诸多自动驾驶行为决策方法, 但由于汽车自动驾驶行为决策受环境不确定因素的影响, 决策本身也要求实效性及高安全性, 现有的行为决策方法难以完全支撑这些要素. 针对以上问题, 提出了一种基于贝叶斯网络构建RoboSim模型的自动驾驶行为决策方法. 首先, 基于领域本体分析自动驾驶场景元素之间的语义关系, 并结合LSTM模型预测场景中动态实体的意图, 进而为构建贝叶斯网络提供驾驶场景理解信息; 然后, 通过贝叶斯网络推理特定场景的自动驾驶行为决策, 并使用 RoboSim模型的状态迁移承载行为决策的动态执行过程, 以减少贝叶斯网络推理的冗余操作, 提高了决策生成的效率. RoboSim模型具有平台无关、能模拟仿真执行周期的特点, 并支持多种形式化的验证技术. 为确保行为决策的安全性, 使用模型检测工具UPPAAL对RoboSim模型进行验证分析. 最后, 结合变道超车场景案例, 进一步证实所提方法的可行性, 为设计安全、高效的自动驾驶行为决策提供了一种可行的途径.

摘要:ARM针对ARMv8.1-M微处理器架构推出基于M-Profile向量化扩展方案的技术, 并命名为ARM Helium, 声明能为ARM Cortex-M处理器提升达15倍的机器学习性能. 随着物联网的高速发展, 微处理器指令执行正确性尤为重要. 指令集的官方手册作为芯片模拟程序, 片上应用程序开发的依据, 是程序正确性基本保障. 主要介绍利用可执行语义框架K Framework对ARMv8.1-M官方参考手册中向量化机器学习指令的语义正确性研究. 基于ARMv8.1-M的官方参考手册自动提取指令集中描述向量化机器学习指令执行过程的伪代码, 并将其转换为形式化语义转换规则. 通过K Framework提供的可执行框架利用测试用例, 验证机器学习指令算数运算执行的正确性.

摘要:网络测量是网络性能监控、流量管理和故障诊断等场景的基础. 带内网络遥测由于具有实时性、准确性和扩展性等特点使其成为当前网络测量研究的热点. 随着可编程数据面的出现和发展, 丰富的信息反馈和灵活的功能部署使得国内外学者提出许多具有实用性的带内网络遥测技术方案. 首先分析了典型的带内网络遥测方案INT和AM-PM的原理和部署挑战. 根据带内网络遥测的优化措施和扩展角度, 从数据采集流程和多任务组合方面分析了优化机制的特点, 从无线网络、光网络和混合设备网络等方面分析了技术扩展的可行性. 根据带内网络遥测在典型场景的应用, 从网内性能感知、网络级遥测系统、流量调度和故障诊断几个方面对比分析其在不同场景应用特点. 最后, 对带内网络遥测研究进行总结, 展望了未来的研究方向.

摘要:传统密码算法的安全性建立在黑盒攻击模型下. 在这种攻击模型下, 攻击者只能获取密码算法的输入输出, 而无法得知密码算法运行时的内部细节. 近年来白盒攻击模型的概念被提出. 在白盒攻击模型下, 攻击者既可以获取密码算法的输入输出, 也可以直接观测或更改密码算法运行时的内部数据. 为保证已有密码算法在白盒攻击环境下的安全性, 在不改变其功能的基础上通过白盒密码技术对其进行重新设计被称为已有密码算法的白盒实现. 研究白盒实现方案的设计与分析对于解决数字版权管理问题具有重要意义. 近年来, 出现了一类针对白盒实现方案的旁信道分析方法. 这类分析手段只需要知道很少白盒实现方案的内部细节, 却可以提取到密钥, 因此是一类对现有白盒实现方案具有实际威胁的分析手段. 对现有白盒实现方案进行此类分析对于确保方案安全性具有重要现实意义. 此类分析方法中的典型代表是基于差分功耗分析原理的差分计算分析. 基于差分计算分析, 对白-武白盒SM4方案进行了安全性分析. 基于对GF(2)上n阶均匀随机可逆矩阵统计特征的研究结果, 提出了一种改进型差分计算分析(IDCA), 可以在分析成功率几乎不变的前提下显著提升分析效率. 结果表明, 白-武白盒SM4方案在面对差分计算分析时不能保证安全性, 必须对其进行进一步改进使之满足实际应用场景下的安全性需求.

摘要:事件抽取是从非结构化的自然语言文本中自动抽取用户感兴趣的事件信息, 并以结构化的形式表示出来. 事件抽取是自然语言处理与理解中的重要方向, 在政府公共事务管理、金融业务、生物医学等不同领域有着很高的应用价值. 根据对人工标注数据的依赖程度, 目前基于深度学习的事件抽取方法主要分为两类: 有监督和远程监督学习方法. 对当前深度学习中事件抽取技术进行了全面的综述. 围绕有监督中CNN、RNN、GAN、GCN与远程监督等方法, 系统地总结了近几年的研究情况, 并对不同的深度学习模型的性能进行了详细对比与分析. 最后, 对事件抽取面临的挑战进行了分析, 针对研究趋势进行了展望.

摘要:数据中心边界广泛部署的地址转换技术产生的非对称流为负载均衡系统的设计带来了挑战. 为了解决软件负载均衡系统不能充分发挥多核处理器和网卡硬件能力的问题, 提出一种基于流特征的非对称流负载均衡方法. 首先, 分析网卡的数据包散列机制, 提出数据包调度算法, 将数据包调度至预期的CPU核; 然后, 基于会话报文序列的时间与空间特征, 构建大象流识别算法; 最后, 基于识别结果, 提出负载均衡方法. 实验结果表明, 非对称流负载均衡方法可以正确处理非对称流的负载均衡, 平均吞吐率提升约14.5%.