• 2023年第34卷第7期文章目次
    全 选
    显示方式: |
    • >专刊文章
    • 形式化方法与应用专题前言

      2023, 34(7):2979-2980. DOI: 10.13328/j.cnki.jos.006864

      摘要 (729) HTML (1822) PDF 530.35 K (2835) 评论 (0) 收藏

      摘要:

    • 安全的混成系统神经网络控制器生成与验证

      2023, 34(7):2981-3001. DOI: 10.13328/j.cnki.jos.006857

      摘要 (1250) HTML (2325) PDF 2.37 M (2762) 评论 (0) 收藏

      摘要:控制器生成是混成系统控制中的重要问题.生成具有安全保证的控制器,关系着混成系统在安全攸关领域的使用.提出了一种为混成系统生成具有安全保证的神经网络控制器的方法.神经网络控制器的安全性由与其同时生成的障碍证书保证.为了生成安全的神经网络控制器,首先确定控制器的网络结构,并基于混成系统构造训练数据集;然后,根据保证控制器安全的障碍证书条件编码神经网络训练时的损失函数.当训练完成后,学习到的神经网络控制器对于训练数据集中的数据是安全的,但对于整个混成系统可能并不安全.为了检验学习到的控制器在整个系统上的安全性,将其安全验证问题转化为一组混合整数规划问题,并使用数值优化器求解,以得到形式化保证的结果.工作实现了安全神经网络控制器生成工具SafeNC,并评估了它在8个基准系统上的性能.实验结果表明:SafeNC可以生成包含6个隐藏层的具有1 804个神经元的安全神经网络控制器;同时,与现有方法相比,SafeNC可为更复杂的系统生成安全的神经网络控制器,更有效且更具扩展性.

    • 自动驾驶交叉路口测试场景建模及验证方法

      2023, 34(7):3002-3021. DOI: 10.13328/j.cnki.jos.006855

      摘要 (1446) HTML (2071) PDF 3.49 M (3350) 评论 (0) 收藏

      摘要:自动驾驶汽车在缓解交通拥堵和消除交通事故方面发挥着重要作用.为了保证自动驾驶系统的安全性和可靠性,在自动驾驶汽车部署到公共道路之前,必须进行全面的测试.现有的测试场景数据大多来源于交通事故和交通违法场景,而且自动驾驶系统最基本的安全需求就是遵守交通法规,这充分体现了自动驾驶汽车遵守交通规则的重要性.然而,目前严重缺少针对交通法规构建的自动驾驶测试场景.因此,从交通法规出发,根据自动驾驶系统的安全需求,提出了交叉路口测试场景的Petri网建模及形式化验证方法.首先,依据自动驾驶测试场景对交规进行分类,提取适合自动驾驶汽车的文本交规,并进行半形式化表征;其次,以覆盖道路交通安全法规以及测试场景功能测试规程为目标,融合交叉路口场景要素的交互行为,合理选择并组合测试场景要素,布设交叉路口测试场景;然后,基于交规的测试场景被建模为一个Petri网,其中,库所描述自动驾驶汽车的状态,变迁表示状态的触发条件,并选择时钟约束规范语言(CCSL)作为中间语义语言,将Petri网转换为一个可进行形式化验证的中间语义模型,提出了具体的转换方法;最后,通过Tina软件分析验证交规场景模型的活性、有界性和可达性,结果表明了所建模型的正确性,并基于SMT的分析工具MyCCSL来分析CCSL约束,采用LTL公式以形式化方法验证交规场景模型的一致性.

    • 基于LLVM Pass的复杂嵌套循环自动并行化框架

      2023, 34(7):3022-3042. DOI: 10.13328/j.cnki.jos.006858

      摘要 (1176) HTML (1718) PDF 2.96 M (2981) 评论 (0) 收藏

      摘要:随着多核处理器的普及应用,针对嵌入式遗留系统中串行代码的自动并行化方法是研究热点.其中,针对具有非完美嵌套结构、非仿射依赖关系特征的复杂嵌套循环的自动并行化方法存在技术挑战.提出了一种基于LLVM Pass的复杂嵌套循环的自动并行化框架(CNLPF).首先,提出了一种复杂嵌套循环的表示模型,即循环结构树,并将嵌套循环的正则区域自动转换为循环结构树表示;然后,对循环结构树进行数据依赖分析,构建循环内和循环间的依赖关系;最后,基于OpenMP共享内存的编程模型生成并行的循环程序.针对SPEC2006数据集中包含近500个复杂嵌套循环的6个程序案例,分别对其进行复杂嵌套循环占比统计和并行性能加速测试.结果表明,提出的自动并行化框架可以处理LLVMPolly无法优化的复杂嵌套循环,增强了LLVM的并行编译优化能力,且该方法结合Polly的组合优化,比单独采用Polly优化的加速效果提升了9%-43%.

    • 目标导向的多线程程序UAF漏洞预测方法

      2023, 34(7):3043-3063. DOI: 10.13328/j.cnki.jos.006862

      摘要 (1116) HTML (1668) PDF 2.33 M (2887) 评论 (0) 收藏

      摘要:Use-after-free (UAF)漏洞是多线程程序的常见并发缺陷.预测性UAF漏洞检测方法因兼顾误报率和漏报率而备受关注.然而,已有的预测性UAF检测方法未结合待检测目标作针对性优化,当程序规模大或行为复杂时会导致检测效率低下.为了解决上述问题,提出一种目标导向的多线程程序UAF漏洞检测方法.首先,由程序运行轨迹挖掘程序的Petri网模型;之后,针对每一个潜在可构成UAF漏洞的内存Free/Use操作对,以触发该漏洞为目标导向,在程序的Petri网模型中添加保持操作间因果约束和数据一致性的行为控制结构;在此基础上,设计了一种基于Petri网反向展开的UAF漏洞检测方法.该方法每次只针对1个潜在的UAF漏洞,有针对性地验证其真实性,从而保证检测的效率.与此同时,为了减少待检测的潜在UAF漏洞数量,提出了一种新型向量时钟进行Free操作与Use操作间的因果关系自动识别,据此对潜在的UAF漏洞进行筛选.结合多个程序实例对所提方法进行了实验评估.实验结果表明,所提方法在检测的效率和准确性方面较主流方法有所提高.

    • 基于约束依赖图的并发程序模型检测工具

      2023, 34(7):3064-3079. DOI: 10.13328/j.cnki.jos.006856

      摘要 (1077) HTML (1703) PDF 2.37 M (3328) 评论 (0) 收藏

      摘要:模型检测是一种基于状态空间搜索的自动化验证方法,可以有效地提升程序的质量.然而,由于并发程序中线程调度的不确定性以及数据同步的复杂性,对该类程序验证时存在更为严重的状态空间爆炸问题.目前,大多采用基于独立性分析的偏序约简技术缩小并发程序探索空间.针对粗糙的独立性分析会显著增加需探索的等价类路径问题,开发了一款可细化线程迁移依赖性分析的并发程序模型检测工具CDG4CPV.首先,构造了待验证可达性性质对应的规约自动机;随后,根据线程迁移边的类型和共享变量访问信息构建约束依赖图;最后,利用约束依赖图剪裁控制流图在展开过程中的独立可执行分支.在SV-COMP 2022竞赛的并发程序数据集上进行了对比实验,并对工具的效率进行比较分析.实验结果表明,该工具可以有效地提升并发程序模型检测的效率.特别是,与基于BDD的程序分析算法相比,该工具可使探索状态数目平均减少91.38%,使时间和空间开销分别平均降低86.25%和69.80%.

    • 基于SMT的区域控制器同步反应式模型的形式化验证

      2023, 34(7):3080-3098. DOI: 10.13328/j.cnki.jos.006861

      摘要 (1094) HTML (1734) PDF 2.82 M (2754) 评论 (0) 收藏

      摘要:在安全关键系统的软件开发过程中,形式化验证是一种经检验的提高软件质量的技术.然而,无论从理论上还是从应用角度来看,软件的验证都必须是完整的,数据流验证应该是对实现层软件模型进行验证的必要体现.因此,环境输入、泛型函数、高阶迭代运算和中间变量对于分析形式化验证的可用性至关重要.为了验证同步反应式模型,工程师很容易验证控制流模型(即安全状态机).现有工作表明,这类工作无法全面地验证安全关键系统的同步反应式模型,尤其是数据流模型,导致这些方法没有达到工业应用的要求,这成为对工业安全软件进行形式化验证的一个挑战.提出了一种自动化验证方法.该方法可以实现对安全状态机和数据流模型的集成进行验证.采用了一种基于程序综合的方法,其中,SCADE模型描述了功能需求、安全性质和环境输入,可以通过对Lustre模型的程序综合,采用基于SMT的模型检查器进行验证.该技术将程序合成作为一种通用原理来提高形式化验证的完整性.在轨道交通的工业级应用(近200万行Lustre代码)上评估了该方法.实验结果表明,该方法在大规模同步反应式模型长期存在的复杂验证问题上是有效的.

    • 智能规划中面向简单偏好的高效求解方法

      2023, 34(7):3099-3115. DOI: 10.13328/j.cnki.jos.006859

      摘要 (1019) HTML (2102) PDF 2.27 M (3033) 评论 (0) 收藏

      摘要:智能规划(AI planning)简称规划,是人工智能领域的一个重要分支,在各领域均有广泛应用,如工厂车间作业调度、物资运输调度、机器人动作规划以及航空航天任务规划等.传统智能规划要求规划解(动作序列)必须最终实现整个目标集合,这种目标一般被称为硬目标(hard goal).然而,许多实际问题中,求解的重点并不只是尽快实现目标以及尽量减少动作序列产生的代价,还需考虑其他因素,如资源消耗或时间约束等.为此,简单偏好(也称软目标soft goal)的概念应运而生.与硬目标相反,简单偏好是可以违背的.本质上,简单偏好用于衡量规划解质量的优劣,而不会影响规划解是否存在.现有关于简单偏好的研究进展缓慢,在规划解质量方面不尽如人意,即求得的规划解与最优解的差距较大.提出了一种求解简单偏好的高效规划方法,将简单偏好表达为经典规划(classical planning)模型的一部分,并利用SMT (satisfiability modulo theories)求解器识别多个简单偏好之间的各种关系,从而约简简单偏好集,减轻规划器的求解负担.该方法的主要优势在于:一方面,提前对简单偏好集进行裁剪,在一定程度上缩减搜索的状态空间;另一方面,直接利用现有高效经典规划器进行求解,而无须提出专用的规划算法,可扩展性较强.基准规划问题的实验结果表明,该方法在提升规划解质量方面表现优异,尤其适用于简单偏好之间不是相互独立的情况.

    • 面向未解释程序的合作验证方法

      2023, 34(7):3116-3133. DOI: 10.13328/j.cnki.jos.006860

      摘要 (682) HTML (1502) PDF 2.82 M (2480) 评论 (0) 收藏

      摘要:未解释程序的验证问题通常是不可判定的,但是最近有研究发现,存在一类满足coherence性质的未解释程序,其验证问题是可判定的,并且计算复杂度为PSPACE完全的.在此结果的基础上,一个针对一般未解释程序验证的基于路径抽象的反例抽象精化(counterexample-guided abstraction refinement,CEGAR)框架被提出,并展现了良好的验证效率.即使如此,对未解释程序的验证工作依然需要多次迭代,特别是利用该方法在针对多个程序验证时,不同的程序之间的验证过程是彼此独立的,存在验证开销巨大的问题.发现被验证的程序之间较为相似时,不可行路径的抽象模型可以在不同的程序之间复用.因此,提出了一个合作验证的框架,收集在验证过程中不可行路径的抽象模型,并在对新程序进行验证时,用已保存的抽象模型对程序进行精化,提前删减一些已验证的程序路径,从而提高验证效率.此外,通过对验证过程中的状态信息进行精简,对现有的基于状态等价的路径抽象方法进行优化,以进一步提升其泛化能力.对合作验证的框架以及路径抽象的优化方法进行了实现,并在两个具有代表性的程序集上分别取得了2.70x和1.49x的加速.

    • >综述文章
    • 前馈神经网络和循环神经网络的鲁棒性验证综述

      2023, 34(7):3134-3166. DOI: 10.13328/j.cnki.jos.006863

      摘要 (1558) HTML (2374) PDF 10.65 M (3880) 评论 (0) 收藏

      摘要:随着智能时代的到来,部署了深度神经网络的智能系统应用已经渗透到了人类生活的各个方面.然而,由于神经网络具有黑盒特性和规模庞大的特点,其预测结果难以让人完全信服,当应用于自动驾驶等安全攸关的领域时,如何保证其安全性仍然是学术界和工业界面临的巨大挑战.为此,学术界针对神经网络一种特殊的安全性——鲁棒性展开了研究,并提出了很多鲁棒性的分析和验证方法.目前为止,验证前馈神经网络的方法包括精确验证方法和近似验证方法,已经发展得比较繁荣;而对于其他类型的网络,如循环神经网络的鲁棒性验证研究还处于起步阶段.回顾深度神经网络的发展以及部署到日常生活中面临的挑战;详尽地调研前馈神经网络和循环神经网络的鲁棒性验证方法,并对这些验证方法间的内在联系进行分析和比较;调研循环神经网络在现实应用场景中的安全性验证方法;阐明神经网络鲁棒性验证领域未来可以深入研究的方向.

    • 面向Java微服务系统的透明请求追踪及采样方法

      2023, 34(7):3167-3187. DOI: 10.13328/j.cnki.jos.006523

      摘要 (1035) HTML (1183) PDF 8.66 M (2348) 评论 (0) 收藏

      摘要:微服务因其敏捷的开发方式、快速的部署方式,逐渐成为以云为基础的软件系统的主流架构方式之一.但是,微服务系统结构复杂,动辄上百个服务实例,而且服务之间的调用关系异常复杂,当微服务系统中出现异常时,难以定位故障根因.为了解决这个问题,端到端请求追踪(trace)成为微服务系统监控的标配.然而现有的分布式请求追踪实现方式对应用程序具有侵入性,严重依赖于开发者对请求追踪的经验,无法在运行时控制追踪功能的开启和关闭.这些不足不仅会增加开发者的负担,而且限制了分布式请求追踪技术的实际应用.设计并实现对程序开发者透明的请求追踪系统Trace++,能够自动生成追踪代码,利用动态代码插桩技术将追踪代码注入到运行中的应用程序.Trace++对程序低侵入,对开发者透明,能够灵活控制追踪功能的开启和关闭.此外,Trace++的自适应采样方法有效减少了请求追踪产生的开销.在微服务系统TrainTicket上的实验结果证明,Trace++能够准确发现服务依赖关系.在开启请求追踪时,性能开销接近于源代码插桩,在关闭请求追踪时无性能开销.此外,Trace++的自适应采样方法在采样到具有代表性样本的同时减少了89.4%的追踪数据.

    • 基于多重异质图的恶意软件相似性度量方法

      2023, 34(7):3188-3205. DOI: 10.13328/j.cnki.jos.006538

      摘要 (1219) HTML (960) PDF 3.14 M (3049) 评论 (0) 收藏

      摘要:现有恶意软件相似性度量易受混淆技术影响,同时缺少恶意软件间复杂关系的表征能力,提出一种基于多重异质图的恶意软件相似性度量方法RG-MHPE (API relation graph enhanced multiple heterogeneous ProxEmbed)解决上述问题.方法首先利用恶意软件动静态特征构建多重异质图,然后提出基于关系路径的增强型邻近嵌入方法,解决邻近嵌入无法应用于多重异质图相似性度量的问题.此外,从MSDN网站的API文档中提取知识,构建API关系图,学习Windows API间的相似关系,有效减缓相似性度量模型老化速度.最后,通过对比实验验证所提方法RG-MHPE在相似性度量性能和模型抗老化能力等方面表现最好.

    • 基于实例加权和双分类器的稳定学习算法

      2023, 34(7):3206-3225. DOI: 10.13328/j.cnki.jos.006511

      摘要 (749) HTML (1101) PDF 7.51 M (2371) 评论 (0) 收藏

      摘要:稳定学习的目标是利用单一的训练数据构造一个鲁棒的预测模型,使其可以对任意与训练数据具有相似分布的测试数据进行精准的分类.为了在未知分布的测试数据上实现精准预测,已有的稳定学习算法致力于去除特征与类标签之间的虚假相关关系.然而,这些算法只能削弱特征与类标签之间部分虚假相关关系并不能完全消除虚假相关关系;此外,这些算法在构建预测模型时可能导致过拟合问题.为此,提出一种基于实例加权和双分类器的稳定学习算法,所提算法通过联合优化实例权重和双分类器来学习一个鲁棒的预测模型.具体而言,所提算法从全局角度平衡混杂因子对实例进行加权来去除特征与类标签之间的虚假相关关系,从而更好地评估每个特征对分类的作用.为了完全消除数据中部分不相关特征与类标签之间的虚假相关关系以及弱化不相关特征对实例加权过程的干扰,所提算法在实例加权之前先进行特征选择筛除部分不相关特征.为了进一步提高模型的泛化能力,所提算法在训练预测模型时构建两个分类器,通过最小化两个分类器的参数差异来学习一个较优的分类界面.在合成数据集和真实数据集上的实验结果表明了所提方法的有效性.

    • 基于双重注意力机制的事件抽取方法

      2023, 34(7):3226-3240. DOI: 10.13328/j.cnki.jos.006520

      摘要 (998) HTML (1140) PDF 7.72 M (3161) 评论 (0) 收藏

      摘要:针对事件抽取存在未充分利用句法关系、论元角色缺失的情况,提出了基于双重注意力机制的事件抽取(event extraction based on dual attention mechanism,EEDAM)方法,有助于提高事件抽取的精确率和召回率.首先,基于4种嵌入向量进行句子编码,引入依赖关系,构建依赖关系图,使深度神经网络可以充分利用句法关系.然后,通过图转换注意网络生成新的依赖弧和聚合节点信息,捕获长程依赖关系和潜在交互,加权融合注意力网络,捕捉句中关键的语义信息,抽取句子级事件论元,提升模型预测能力.最后,利用关键句检测和相似性排序,进行文档级论元填充.实验结果表明,采用基于双重注意力机制的事件抽取方法,在ACE2005数据集上,较最佳基线联合多中文事件抽取器(joint multiple Chinese event extractor,JMCEE)在精确率、召回率和F1-score分别提高17.82%、4.61%、9.80%;在大坝安全运行日志数据集上,较最佳基线JMCEE在精确率、召回率和F1-score上分别提高18.08%、4.41%、9.93%.

    • 主动自动机学习中的等价查询算法优化

      2023, 34(7):3241-3255. DOI: 10.13328/j.cnki.jos.006532

      摘要 (636) HTML (1009) PDF 5.55 M (2238) 评论 (0) 收藏

      摘要:模型学习是一种获取黑盒软件系统行为模型的有效方法,可分为主动学习和被动学习.主动学习是基于字母表构造测试用例,通过与黑盒系统主动交互,可在多项式时间内得到目标系统的最小完备自动机,其中等价查询仍是开发和应用主动自动机学习工具的障碍之一.通过探讨反例对于学习算法的影响,定义假设的比较规则,提出测试用例构造的两个原则,同时依据原则对Wp-method等价查询算法改进,产生更优的假设,有效降低查询的数量,并基于LearnLib开源工具,分别以3类自动机为实验对象验证原则和改进算法的有效性.

    • 互信息与多条元路径融合的异质网络表示学习方法

      2023, 34(7):3256-3271. DOI: 10.13328/j.cnki.jos.006535

      摘要 (1111) HTML (1247) PDF 9.42 M (3082) 评论 (0) 收藏

      摘要:异质信息网络能够对真实世界的诸多复杂应用场景进行建模,其表示学习研究也得到了众多学者的广泛关注.现有的异质网络表示学习方法大多基于元路径来捕获网络中的结构和语义信息,已经在后续的网络分析任务中取得很好的效果.然而,此类方法忽略了元路径的内部节点信息和不同元路径实例的重要性;仅能捕捉到节点的局部信息.因此,提出互信息与多条元路径融合的异质网络表示学习方法.首先,利用一种称为关系旋转编码的元路径内部编码方式,基于相邻节点和元路径上下文节点捕获异质信息网络的结构和语义信息,采用注意力机制来建模各元路径实例的重要性;然后,提出一种互信息最大化与多条元路径融合的无监督异质网络表示学习方法,使用互信息捕获全局信息以及全局信息和局部信息之间的联系.最后,在两个真实数据集上进行实验,并与当前主流的算法进行比较分析.结果表明,所提方法在节点分类和聚类任务上性能都有提升,甚至和一些半监督算法相比也表现出强劲性能.

    • 基于雾计算的智能医疗三方认证与密钥协商协议

      2023, 34(7):3272-3291. DOI: 10.13328/j.cnki.jos.006514

      摘要 (698) HTML (1674) PDF 5.02 M (2397) 评论 (0) 收藏

      摘要:在智能医疗中,将云计算技术与物联网技术结合,可有效解决大规模医疗数据的实时访问问题.然而,数据上传到远程云服务器,将带来额外的通信开销与传输时延.借助雾计算技术,以终端设备作为雾节点,辅助云服务器在本地完成数据存储与访问,能够实现数据访问的低延迟与高移动性.如何保障基于雾计算的智能医疗环境的安全性成为近期研究热点.面向基于雾计算的智能医疗场景,设计认证协议的挑战在于:一方面,医疗数据是高度敏感的隐私数据,与病人身体健康密切相关,若用户身份泄漏或者数据遭到非法篡改将导致严重后果;另一方面,用户设备和雾节点往往资源受限,认证协议在保护用户隐私的同时,需要实现用户、雾节点、云服务器之间的三方数据安全传输.对智能医疗领域两个具有代表性的认证方案进行安全分析,指出Hajian等人的协议无法抵抗验证表丢失攻击、拒绝服务攻击、仿冒攻击、设备捕获攻击、会话密钥泄漏攻击;指出Wu等人的协议无法抵抗离线口令猜测攻击、仿冒攻击.提出一个基于雾计算的智能医疗三方认证与密钥协商协议,采用随机预言机模型下安全归约、BAN逻辑证明和启发式分析,证明所提方案能实现双向认证与会话密钥协商,并且对已知攻击是安全的;与同类方案的性能对比分析表明,所提方案显著提高了安全性,并具有较高的效率.

    • 区块链中可监管的身份隐私保护方案

      2023, 34(7):3292-3312. DOI: 10.13328/j.cnki.jos.006517

      摘要 (1401) HTML (911) PDF 8.75 M (3103) 评论 (0) 收藏

      摘要:在账本公开、多方共识情况下确保交易身份的隐私保护是区块链技术面临的主要挑战之一.目前公有链中基于匿名认证和交易混淆的身份隐私保护方案由于缺乏监管又难于在行业应用中推广.借鉴门罗币中的身份隐私保护方案,引入监管方的角色,基于一次性地址加密和零知识证明设计了可监管的交易接收方身份隐私保护方案;结合可链接环签名和可撤销环签名设计了可链接可撤销环签名方案,以实现基于自主混淆的可监管交易发送方身份隐私保护方案.基于上述方案,系统在保护交易方身份隐私的同时,还支持监管方可离线恢复交易参与方的真实身份,从而达到“可控匿名”的监管目的.分析和测试结果表明,方案设计的算法运算时间均为毫秒级,可满足区块链非高频交易场景下的性能需求.

    • 基于义原级语句稀释法的文本对抗攻击能力强化方法

      2023, 34(7):3313-3328. DOI: 10.13328/j.cnki.jos.006525

      摘要 (779) HTML (1135) PDF 7.00 M (2338) 评论 (0) 收藏

      摘要:随着近年来机器学习方法在自然语言处理领域的应用越发广泛,自然语言处理任务的安全性也引起了研究者们重视.现有研究发现,向样本施加细微扰动可能令机器学习模型得到错误结果,这种方法称之为对抗攻击.文本对抗攻击能够有效发现自然语言模型的弱点从而进行改进.然而,目前的文本对抗攻击方法都着重于设计复杂的对抗样本生成策略,对抗攻击成功率提升有限,且对样本进行高侵入性修改容易导致样本质量下降.如何更简单、更高效地提升对抗攻击效果,并输出高质量对抗样本已经成为重要需求.为解决此问题,从改进对抗攻击过程的新角度,设计了义原级语句稀释法(sememe-level sentence dilution algorithm,SSDA)及稀释池构建算法(dilution pool construction algorithm,DPCA).SSDA是一种可以自由嵌入经典对抗攻击过程中的新过程,它利用DPCA构建的稀释池先对输入样本进行稀释,再进行对抗样本生成.在未知文本数据集与自然语言模型的情况下,不仅能够提升任意文本对抗攻击方法的攻击成功率,还能够获得相较于原方法更高的对抗样本质量.通过对不同文本数据集、稀释池规模、自然语言模型,以及多种主流文本对抗攻击方法进行对照实验,验证了SSDA对文本对抗攻击方法成功率的提升效果以及DPCA构建的稀释池对SSDA稀释能力的提升效果.实验结果显示,SSDA稀释过程能够比经典对抗攻击过程发现更多模型漏洞,且DPCA能够帮助SSDA在提升成功率的同时进一步提升对抗样本的文本质量.

    • 一种支持分级用户访问的文件分层CP-ABE方案

      2023, 34(7):3329-3342. DOI: 10.13328/j.cnki.jos.006526

      摘要 (766) HTML (843) PDF 10.55 M (2592) 评论 (0) 收藏

      摘要:文件分层的密文策略基于属性的加密(FH-CP-ABE)方案实现了同一访问策略的多层次文件加密,节省了加解密的计算开销和密文的存储开销.然而,目前的文件分层CP-ABE方案不支持分级用户访问,且存在越权访问的问题.为此,提出一种支持分级用户访问的文件分层CP-ABE方案.在所提方案中,通过构造分级用户访问树,并重新构造密文子项以支持分级用户的访问需求,同时消除用户进行越权访问的可能性.安全性分析表明,所提方案能够抵御选择明文攻击.理论分析和实验分析均表明,与相关方案相比,所提方案在计算和存储方面具有更高的效率.

    • 集合交集元素之和的保密计算

      2023, 34(7):3343-3353. DOI: 10.13328/j.cnki.jos.006529

      摘要 (655) HTML (851) PDF 5.55 M (2088) 评论 (0) 收藏

      摘要:安全多方计算是国际密码学的研究热点之一,保密计算集合交集元素之和问题是安全多方计算比较新的问题之一.该问题在工商业、医疗健康等领域具有重要的理论意义和实用价值.现有解决方案是在有全集情况下设计的,在计算过程中会泄露交集的势且存在一定的误判.在半诚实模型下基于Paillier同态加密算法设计了3个协议,协议1计算共有标识符的数量(即用户标识符交集的势)以及与这些用户相关联的整数值之和,协议2和协议3是在不泄露交集势的情况下计算交集元素关联值之和.整个计算过程不泄露关于协议双方私人输入的任何更多信息.所提协议是在无全集情况下设计的,采用模拟范例证明了所设计协议的安全性,用实验验证协议的高效性.

    • 基于SM9的CCA安全广播加密方案

      2023, 34(7):3354-3364. DOI: 10.13328/j.cnki.jos.006531

      摘要 (957) HTML (905) PDF 6.00 M (2738) 评论 (0) 收藏

      摘要:选择密文安全模型能有效刻画主动攻击,更接近现实环境.现有抵抗选择密文攻击的密码算法以国外算法为主,缺乏我国自主设计且能抵抗选择密文攻击的密码算法.虽然实现选择密文安全存在通用转化方法,代价是同时增加计算开销和通信开销.基于国密SM9标识加密算法,提出一种具有选择密文安全的标识广播加密方案.方案的设计继承了SM9标识加密算法结构,用户密钥和密文的大小都是固定的,其中用户密钥由一个群元素组成,密文由3个元素组成,与实际参与加密的接收者数量无关.借助随机谕言器,基于GDDHE困难问题可证明方案满足CCA安全.加密算法的设计引入虚设标识,通过该标识可成功回复密文解密询问,实现CCA的安全性.分析表明,所提方案与现有高效标识广播加密方案在计算效率和存储效率上相当.

    • 基于跨域关联与隐私保护的深度推荐模型

      2023, 34(7):3365-3384. DOI: 10.13328/j.cnki.jos.006533

      摘要 (850) HTML (984) PDF 5.28 M (2896) 评论 (0) 收藏

      摘要:推荐系统能够根据用户的偏好有效地过滤信息,已被广泛应用于各行各业,但随着用户数量的爆炸式增长,数据稀疏性和冷启动问题日益严重.多源数据融合可以有效缓解数据稀疏和冷启动情况下的推荐精度,其主要思想是融合用户在其他方面的辅助信息来填补缺失值,以优化目标服务的推荐准确度,受到了研究者的青睐,但由于数据之间的关联引入了更为严重的隐私泄露风险.针对以上问题,提出一种基于跨域关联与隐私保护的深度推荐模型,设计一种具有多源数据融合和差分隐私保护特征的深度学习协同推荐方法.该方法一方面融合辅助领域信息以提高推荐的精确度,同时修正异常点的偏差,改善推荐系统的性能;另一方面针对数据融合中的数据安全问题,基于差分隐私模型在协同训练过程中加入噪音以保证数据的安全性.为了更好地评价推荐系统中的长尾效应,首次提出一种新的评价指标-发现度,用以度量推荐算法发现用户隐性需求的能力.基于已有算法进行了性能对比与分析,实验结果证明,所提方法在保证隐私安全的前提下,比现有方法具有更好的推荐精度和多样性,能够有效地发现用户的隐性需求.

    • 基于U-Net结构的生成式多重对抗隐写算法

      2023, 34(7):3385-3407. DOI: 10.13328/j.cnki.jos.006537

      摘要 (940) HTML (893) PDF 10.20 M (2647) 评论 (0) 收藏

      摘要:人工智能的发展为信息隐藏技术带来越来越多的挑战,提高现有隐写方法的安全性迫在眉睫.为提高图像的信息隐藏能力,提出一种基于U-Net结构的生成式多重对抗隐写算法.所提算法通过生成对抗网络与隐写分析器优化网络、隐写分析对抗网络间的多重对抗训练,构建生成式多重对抗隐写网络模型,生成适合信息隐写的载体图像,提高隐写图像抗隐写分析能力;同时,针对现有生成对抗网络只能生成随机图像,且图像质量不高的问题,设计基于U-Net结构的生成式网络模型,将参考图像的细节信息传递到生成载体图像中,可控地生成高质量目标载体图像,增强信息隐藏能力;其次,采用图像判别损失、均方误差(MSE)损失和隐写分析损失动态加权组合作为网络迭代优化总损失,保障生成式多重对抗隐写网络快速稳定收敛.实验表明,基于U-Net结构的生成式多重对抗隐写算法生成的载体图像PSNR最高可达到48.60 dB,隐写分析器对生成载体图像及其隐写图像的判别率为50.02%,所提算法能够生成适合信息嵌入的高质量载体图像,保障隐写网络快速稳定收敛,提高了图像隐写安全性,可以有效抵御当前优秀的隐写分析算法的检测.

    • 基于卷积神经网络的全景分割Transformer模型

      2023, 34(7):3408-3421. DOI: 10.13328/j.cnki.jos.006530

      摘要 (1395) HTML (1186) PDF 8.76 M (2975) 评论 (0) 收藏

      摘要:提出一种基于卷积神经网络的Transformer模型来解决全景分割任务,方法借鉴CNN在图像特征学习方面的先天优势,避免了Transformer被移植到视觉任务中所导致的计算量增加.基于卷积神经网络的Transformer模型由执行特征域变换的映射器和负责特征提取的提取器这两种基本结构构成,映射器和提取器的有效结合构成了该模型的网络框架.映射器由一种Lattice卷积模型实现,通过对卷积滤波器进行设计和优化来模拟图像的空间关系.提取器由链式网络实现,通过链式单元堆叠提高特征提取能力.基于全景分割的结构和功能,构建了基于CNN的全景分割Transformer网络.在MS COCO和Cityscapes数据集的实验结果表明,所提方法具有优异的性能.

    • 基于避让阻塞的优先级天花板协议

      2023, 34(7):3422-3437. DOI: 10.13328/j.cnki.jos.006534

      摘要 (778) HTML (859) PDF 11.36 M (2289) 评论 (0) 收藏

      摘要:为了提高空间飞行器计算机的CPU利用率,新一代空间飞行器操作系统使用了一种同时包含固定时间点启动任务和偶发任务的混合调度算法.其中固定时间点启动任务往往是安全攸关任务,需要在固定时间点启动,且执行期间不能被阻塞.在固定时间点启动任务和偶发任务共存的条件下,现有的实时锁协议无法保证固定时间点启动任务的阻塞时间为零,因此在经典的优先级天花板协议的基础上,提出基于避让思想的实时锁协议,通过提前预判和设置虚拟启动点的方式,确保偶发任务对共享资源的访问不会影响到固定时间点启动任务的执行.同时暂时提升部分共享资源的访问优先级,降低了任务抢占所带来的运行开销.给出上述锁协议的最坏阻塞时间,并通过可调度率实验分析其性能,实验表明,在临界区较短的情况下,本协议可将因访问共享资源而导致的可调度性损失控制在27%以内.

    • 基于标记增强的离散跨模态哈希方法

      2023, 34(7):3438-3450. DOI: 10.13328/j.cnki.jos.006536

      摘要 (681) HTML (1074) PDF 6.65 M (2346) 评论 (0) 收藏

      摘要:跨模态哈希通过将不同模态的数据映射为同一空间中更紧凑的哈希码,可以大大提升跨模态检索的效率.然而现有跨模态哈希方法通常使用二元相似性矩阵,不能准确描述样本间的语义相似关系,并且存在平方复杂度问题.为了更好地挖掘数据间的语义相似关系,提出了一个基于标记增强的离散跨模态哈希方法.首先借助迁移学习的先验知识生成样本的标记分布,然后通过标记分布构建描述度更强的语义相似性矩阵,再通过一个高效的离散优化算法生成哈希码,避免了量化误差问题.最后,在两个基准数据集上的实验结果验证了所提方法在跨模态检索任务上的有效性.

    • 申威1621处理器上矩阵乘法优化研究

      2023, 34(7):3451-3463. DOI: 10.13328/j.cnki.jos.006519

      摘要 (889) HTML (1475) PDF 7.02 M (2848) 评论 (0) 收藏

      摘要:稠密矩阵乘法(GEMM)是很多科学与工程计算应用中大量使用的函数,也是很多代数函数库中的基础函数,其性能高低对整个应用往往有决定性的影响.另外,因其计算密集的特点,矩阵乘法效率往往也是体现硬件平台性能的重要指标.针对国产申威1621处理器,对稠密矩阵乘法进行了系统性地优化.基于对各部分开销的分析,以及对体系结构特点与指令集的充分利用,对DGEMM函数从循环与分块方案,打包方式,核心计算函数实现,数据预取等方面进行了深入优化.此外,开发了代码生成器,为不同的输入参数生成不同版本的汇编代码和C语言代码,配合自动调优脚本,选取最佳参数.经过优化和调优,单线程DGEMM性能达到了单核浮点峰值性能的85%,16线程DGEMM性能达到16核浮点峰值性能的80%.对DGEMM函数的优化不仅提高了申威1621平台BLAS函数库性能,也为国产申威系列多核处理器上稠密数据计算优化提供了重要参考.

当期目录


文章目录

过刊浏览

年份

刊期

联系方式
  • 《软件学报 》
  • 主办单位:中国科学院软件研究所
                     中国计算机学会
  • 邮编:100190
  • 电话:010-62562563
  • 电子邮箱:jos@iscas.ac.cn
  • 网址:https://www.jos.org.cn
  • 刊号:ISSN 1000-9825
  •           CN 11-2560/TP
  • 国内定价:70元
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号