计算机研究与发展杂志2023年第2期
-
- 抽象解释及其应用研究进展
- 陈立前,范广生,尹帮虎,王戟,
- 抽象解释是一种对用于形式描述复杂系统行为的数学结构进行抽象和近似并推导或验证其性质的理论.抽象解释自20世纪70年代提出以来,在语义模型、程序分析验证、混成系统验证、程序转换、系统生物学模型分析等领域取得了广泛应用.近年来,抽象解释在程序分析、神经网络验证、完备性推理、抽象域改进等方面取得较大进展.基于此,系统综述了抽象解释及其应用的研究进展.首先概述了抽象解释理论的基本概念,介绍了抽象解释理论、抽象域的研究进展;然后概述了基于抽象解释的程序分析方面的研究进展;之后概述了基于抽象解释的神经网络模型验证、神经网络模型鲁棒训练、深度学习程序的分析等方面的研究进展;又对抽象解释在智能合约可信保证、信息安全保证、量子计算可信保证等方面的应用进展进行了介绍;最后指明了抽象解释未来可能的研究方向.
-
- 基于多线程并行的符号执行引擎设计与实现
- 周彭,左志强,
- 符号执行作为一种高效的测试生成技术,被广泛应用于软件测试、安全分析等领域.然而,由于程序中的执行路径数量随着分支数量的增加而指数级上升,符号执行往往无法在大规模程序上进行高效执行,缺乏可扩展性.已有的基于多进程的并行化方法具有较大的额外通信开销,并且缺乏对现有约束求解优化技术的利用.提出了基于多线程并行处理模型的符号执行加速方法.具体来讲,为解决并行符号执行中的不同工作节点负载不平衡问题,设计了不需要中间节点参与的工作窃取算法.为充分利用现有约束求解优化技术,提出了让不同工作节点共享约束求解信息的加速求解方法.基于符号执行引擎(KLEE)实现了多线程并行化符号执行方案,从而形成多线程并行化符号执行引擎(PKLEE).实验验证表明,在穷尽执行路径场景下,KLEE平均耗时是在给定8个线程下PKLEE的3~4倍;在同样的时间内,PKLEE执行的有效工作负载平均是KLEE的3倍.
-
- 模糊测试中的静态插桩技术
- 王明哲,姜宇,孙家广,
- 模糊测试是一种行之有效的软件缺陷检测方法.其基本思想是生成大量随机输入,从而广泛探索程序行为,并以此发现程序崩溃和崩溃背后的软件缺陷.显然,纯随机的输入无法高效探索程序行为,大量程序缺陷也难以导致崩溃.为了进一步提升模糊测试的有效性,模糊测试往往引入静态插桩技术,用于加快探索程序状态空间速度,提升发现缺陷的能力.因此,引入静态插桩已经成为当下模糊测试的经典实践.聚焦于模糊测试场景下的插桩需求,除了介绍静态插桩技术的基本原理外,从安全特性强化和导向信息收集两个视角出发,系统性地分析了当下静态插桩的典型方法.同时,针对插桩的额外开销问题,全面地测量了不同插桩方案下的程序的执行速度,并与基线的未插桩程序进行比对.最后基于上述分析和测量,初步展望了静态插桩的优化方向.
-
- Java指针分析综述
- 谭添,马晓星,许畅,马春燕,李樾,
- 近年来静态程序分析已成为保障软件可靠性、安全性和高效性的关键技术之一.指针分析作为基础程序分析技术为静态程序分析提供关于程序的一系列基础信息,例如程序任意变量的指向关系、变量间的别名关系、程序调用图、堆对象的可达性等.介绍了Java指针分析的重要内容:指针分析算法、上下文敏感、堆对象抽象、复杂语言特性处理、非全程序指针分析,特别是对近年来指针分析的研究热点选择性上下文敏感技术进行了梳理和讨论.
-
- 中断驱动型航天嵌入式软件原子性违反检测方法
- 于婷婷,李超,王博祥,陈睿,江云松,
- 嵌入式软件的可信性对航天任务的成败至关重要.航天嵌入式软件广泛采用中断驱动的并发机制,不确定的中断抢占可能导致并发缺陷,引发严重的安全问题.研究表明原子性违反是中断并发缺陷中最突出的一类缺陷模式.目前面向中断驱动型嵌入式软件的原子性违反检测方法都无法同时实现高精度和高可扩展性,且其对真实航天嵌入式软件的有效性尚未得到证实.为了有效提升检测该类缺陷的精度与效率,对82个航天嵌入式软件原子性违反进行实证研究,获得该类缺陷在原子区范围、中断嵌套层数、访问交错模式、共享数据访问方式、访问粒度等5个方面的表现特征.并在此基础上,提出一个精确、高效的原子性违反静态检测方法intAtom-S.首先,基于一个由数值不变式参数化的细粒度内存访问模型,引入基于规则的方法剔除标志变量访问,并采用抽象解释进行精确的共享数据分析,该分析能将共享数据访问粒度精确至数组元素,并可识别共享的内存映射I/O地址.然后,使用轻量级数据流分析技术匹配符合缺陷访问交错模式的所有并发三次访问序,作为潜在的原子性违反缺陷候选.最后,采用基于路径条件的约束求解对缺陷候选中的串行访问对和并发三次访问序进行路径可行性分析,逐步消除误报,得到最终的原子性违反结果.在基准测试集和8个真实航天嵌入式软件上的实验表明,与目前最先进的方法相比,intAtom-S误报率降低了72%,检测效率提高了3倍.此外,该方法能够快速完成对真实航天嵌入式软件的分析,平均误报率仅为8.9%,并发现了23个已被开发人员确认的缺陷.
-
- 智能合约Gas优化综述
- 宋书玮,倪孝泽,陈厅,
- 区块链2.0最显著的特征是增加了对智能合约的支持,这使得区块链拥有了运行各种应用程序的能力.智能合约是一种根据预先定义的代码逻辑自动运行的计算机软件.区别于传统软件,区块链技术赋予了智能合约不依赖可信中心机构而在相互不信任的节点上正确执行的能力,使其在数字支付、共享经济等领域被广泛地应用.为了防止滥用智能合约导致计算资源被浪费,以太坊等区块链向部署和执行智能合约这2种活动收取Gas(燃料)费用.智能合约消耗的计算资源是决定费用高低的因素.具有低效代码的智能合约浪费资源且易受攻击,此类智能合约的开发者和用户将承担不必要的费用.因此,优化智能合约以节省资源已经成为开发者和研究者重点关注的问题.首先详细分析了智能合约Gas优化所面临的主要挑战;然后回顾和总结了近年来提出的各种优化技术;最后展望了该研究方向的未来工作,旨在为智能合约的开发者和研究人员提供参考和借鉴.
-
- 基于控制流和数据流分析的内存拷贝类函数识别技术
- 尹小康,芦斌,蔡瑞杰,朱肖雅,杨启超,刘胜利,
- 内存错误漏洞仍是当前网络攻击中造成危害最严重的漏洞之一.内存错误漏洞的产生往往与对内存拷贝类函数的误用有关.目前针对内存拷贝类函数的识别主要借助于符号表和代码特征模式匹配,具有较高的误报率和漏报率,并且适用性较差.提出了一种内存拷贝类函数识别技术CPYFinder(copyfunctionfinder).该技术在内存拷贝类函数控制流特征的基础上,将二进制代码转换为中间语言表示VEXIR(intermediaterepresentation)进行数据流的构建和分析,根据内存拷贝类函数在数据流上的特征进行识别.该技术能够在较低的运行时间下对多种指令集架构(x86,ARM,MIPS,PowerPC)的二进制程序中的内存拷贝类函数进行识别.实验结果表明,相比于最新的工作BootStomp和SaTC,CPYFinder在对内存拷贝类函数识别上具有更好的表现,在精准率和召回率上得到更好的平衡,并且运行时间与SaTC几乎相等,仅相当于BootStomp耗时的19%.此外,CPYFinder在漏洞函数识别上也具有更好的表现.
-
- 支持多密文等值测试的无线体域网聚合签密方案
- 杨小东,周航,任宁宁,袁森,王彩芬,
- 无线体域网(wirelessbodyareanetwork,WBAN)技术拥有低时延和高灵活性的特点,在医疗保健、病情监控和紧急救护等领域拥有广阔的应用前景.针对目前WBAN密码方案中存在的证书管理开销过大、不支持多用户检索与多密文等值测试等问题,提出了一种支持多密文等值测试的WBAN聚合签密方案.采用基于身份的签密体制,消除了传统公钥密码方案中的证书管理问题,保证了医疗数据的机密性与可认证性.利用聚合签密技术,降低了多用户环境下对医疗密文进行验证的计算开销.引入多密文等值测试技术,实现了多数据用户同时对多医疗密文的安全检索,提高了多用户环境下密文检索的效率.在随机预言模型下,基于计算性Diffie-Hellman困难问题证明了该方案在适应性选择密文攻击下的单向性.与同类方案相比较,该方案支持更多的安全属性,并具有较低的计算开销.
-
- 支持一般电路的高效安全基于属性签名
- 黄振杰,林志伟,
- 基于属性签名(attribute-basedsignature,ABS)是一种重要的密码原语,具有广泛的应用背景,得到众多学者的关注,是密码学的研究热点.为了提高基于属性签名的安全性、表达力和效率,使用多线性映射作为工具,提出一个支持一般电路的具有完善隐私性的基于属性签名方案.引入节点权重概念并采用“从上到下”递归,显著减少生成签名的计算开销;利用左右孩子节点的对称性,缩短门节点的密钥长度.所提出的方案将不可伪造性从“选定消息且选定属性攻击下存在不可伪造”提升到更强的“自适应选择消息但选定属性攻击下存在不可伪造”;将访问结构从特殊电路拓展到一般电路,可以支持任意访问结构,达到任意的访问控制粒度;在保持签名仅为1个群元素的前提下,显著缩短主公钥、主私钥和签名钥的大小和显著降低签名密钥生成、签名生成和验证的计算开销.分析表明:所提出的方案在性能和效率方面均有明显优势,是一个实用的方案.
-
- 基于商密SM9的属性基在线/离线签名方案
- 朱留富,李继国,赖建昌,黄欣沂,张亦辰,
- 属性基签名(attribute-basedsignature,ABS)方案利用属性集标识用户.只有当属性集满足访问策略时用户才能产生有效签名.与传统数字签名方案相比,属性基签名方案不仅利用属性集隐藏用户的真实身份从而获得匿名性,而且通过制定访问策略实现了细粒度访问控制.在基于椭圆曲线的属性基签名方案中通常需要使用大量的群指数运算或配对操作,这些操作计算代价高昂,导致签名过程计算开销较大.在线/离线签名技术可以在未知消息之前将高昂的操作通过离线预计算,从而降低了轻量级设备在线计算代价.SM9标识密码算法作为我国自主设计的商用密码,已由ISO/IEC标准化并被广泛使用.以商密SM9标识密码算法为基础,利用在线/离线签名技术,构造了一种基于商密SM9的属性基在线/离线签名(attribute-basedonline/offlinesignature,ABOOS)方案.不仅可以实现细粒度访问控制,同时也适用于轻量级设备.在随机谕言机模型下,方案的安全性可以规约到q-SDH(q-strongDiffie-Hellman)困难问题.理论分析和实验仿真表明提出的方案有效降低了签名阶段的计算代价,适用于物联网等应用环境.
-
- 移动边缘计算中基于云边端协同的任务卸载策略
- 张文柱,余静华,
- 在移动边缘计算(mobileedgecomputing,MEC)中,为了利用有限的计算资源提供高效的计算服务,提出一种基于Docker的云—边—端协同任务卸载框架,解决多接入MEC协同卸载、计算资源分配问题.为提高任务的执行速率和各节点资源利用率,对任务进行预处理,如在Kahn算法中加入行满秩矩阵要求并结合任务并行计算设定输出任务执行序列;分别建立端、边、云任务计算模型,分配权重设计联合优化系统延迟与能耗的目标函数;为求解最优卸载决策,引入“全优率”参数和粒子蜂设计人工粒子蜂群(artificialparticleswarm,APS)算法作为卸载决策算法.实验表明,多任务处理证明了APS的有效性.多接入条件下,相比于本地计算、边缘计算、云计算、端—边联合和随机处理5种模式,所提方案的低延时和低能耗表现证明了其提供高效服务的优越性.
-
- 基于区块链的工业互联网动态密钥管理
- 张泽林,王化群,
- 目前,工业互联网数据面临的安全威胁日益严重,有效的网络传输对工业互联网的数据安全起到关键的作用.为了能有效适应工业互联网的结构,实现安全可靠的通信,提出一种基于区块链的动态节点的密钥管理方案.工业通信中,不信任的节点之间需要建立有效的会话密钥,并且传统的借助一个中心节点采用中间人方式实现密钥协商,但是一旦中心节点失效,则会导致整个通信系统的通信失败.而当节点数n较少时,通常采用中心节点预先设置密钥的方式,每个节点均需存储(n-1)个密钥,那么整个系统需要存储n(n-1)个密钥,一旦节点需要增加,则整个系统存储的密钥就会呈指数级增长.因此,基于区块链,利用多项式来构建通信密钥,去中心化生成共享密钥,并有效抵御节点出入对系统的威胁,保证有效的组密钥协商,比传统的PKI具有更快的处理速度,且任何节点丢失密钥,可以借助其他节点信息有效地恢复原有密钥.
-
- 面向边缘智能的协同推理综述
- 王睿,齐建鹏,陈亮,杨龙,
- 近年来,信息技术的不断变革伴随数据量的急剧爆发,使主流的云计算解决方案面临实时性差、带宽受限、高能耗、维护费用高、隐私安全等问题.边缘智能的出现与快速发展有效缓解了此类问题,它将用户需求处理下沉到边缘,避免了海量数据在网络中的流动,得到越来越多的关注.由于边缘计算中资源性能普遍较低,通过资源实现协同推理正成为热点.通过对边缘智能发展的趋势分析,得出边缘协同推理目前仍处于增长期,还未进入稳定发展期.因此,在对边缘协同推理进行充分调研的基础上,将边缘协同推理划分为智能化方法与协同推理架构2个部分,分别对其中涉及到的关键技术进行纵向归纳整理,并从动态场景角度出发,对每种关键技术进行深入分析,对不同关键技术进行横向比较以及适用场景分析.最后对动态场景下的边缘协同推理给出值得研究的若干发展方向.
-
- 基于摄像头域内域间合并的无监督行人重识别方法
- 陈利文,叶锋,黄添强,黄丽清,翁彬,徐超,胡杰,
- 在刑事侦查、智能监控、图像检索等领域,行人重识别一直是研究的热点.由于现有的大部分方法依赖有标注数据集,因此标签的缺乏使得无监督的行人重识别技术变得更具挑战性.为了克服这一问题,提出了一个用于生成可靠伪标签的框架,这些生成标签可以为现有监督行人重识别模型提供监督信号.假设数据集内的大部分图片都满足同一个摄像头拍摄的图片差异主要在于前景(行人)、同一个行人被不同摄像头拍摄到的图片差异主要在于背景.为了消除图片背景带来的差异,首先把数据集中的图片依据摄像头编号分成若干个域,通过计算每个域内的图片间的欧式距离,建立图模型,执行最大团算法寻找最相似的若干个图片并认为它们属于同一个行人;紧接着计算不同摄像头域间的团的相似度,据此进行合并;最终给出全局伪标签.所提的框架无需人为标注数据,以一种无监督的方式运行,并在Market1501和DukeMTMC-ReID数据集上进行实验,实验发现所提方法比其他相关方法具有更高的精度,从而进一步证明了所提方法的有效性.
-
- 基于邻域一致性的点云场景流传播更新方法
- 郑晗,王宁,马新柱,张宏,王智慧,李豪杰,
- 场景流是连续动态场景之间的3D运动场,广泛应用于机器人技术和自动驾驶任务.现有方法忽略了点云点的相关性,仅关注源点云和目标点云逐点的匹配关系,由于匹配关系完全依赖于点云数据的特征信息,导致在局部特征信息不足的点上准确估计场景流仍然存在挑战.根据源点云相邻点具有相关性的特性,提出NCPUM(neighborhoodconsistencypropagationupdatemethod)方法,在邻域内将场景流从高置信度点向低置信度点传播,从而优化局部特征信息不足点的场景流.具体来说,NCPUM包含2个模块:置信度预测模块,根据场景流先验分布图,预测源点云逐点的置信度;场景流传播模块,根据局部区域一致性的约束更新低置信度点集的场景流.NCPUM在合成数据集Flyingthings3D和真实驾驶场景数据集KITTI上进行评估,准确度上达到了国际先进水平.由于邻域一致性更符合真实激光雷达场景的先验假设,因此在KITTI数据集上的提升更加明显.
-
- 一种基于几何探测的快速黑盒边界攻击算法
- 刘昊,张泽辉,夏晓帆,高铁杠,
- 随着深度学习应用的愈发广泛,针对深度学习模型的安全性研究也变得至关重要.在商业应用中,深度学习的模型往往处于应用的底层,一旦对底层模型攻击成功,可能会给商业应用带来巨大的损失.好的攻击算法可以很好的对深度学习模型进行风险评估,从而避免损失.针对实际场景中存在的Hard-label问题,现存算法解决此问题都需要上万次查询,具有很高的攻击成本,提出了FastGBA(fastgeometricboundaryattack)攻击算法:一种在样本空间内针对决策边界进行几何探测的攻击算法,初始从具有较大扰动的对抗样本出发,进行二分逼近至决策边界附近,最终在决策边界附近进行邻域几何探测来缩短样本距离.FastGBA攻击算法在4个深度学习模型上同SurFree攻击算法以及HSJA(hopskipjumpattack)攻击算法进行了对比实验,在查询次数不超过500次,中等扰动(L2距离\leqslant10)的限制条件下,攻击成功率在4个深度学习模型上相较于SurFree攻击算法提升了14.5%~24.4%,相较于HSJA攻击算法提升了28.9%~36.8%.
-
- 高阶次Caputo型分数阶微分算子及其图像增强应用
- 王相海,张文雅,邢俊宇,吕芳,穆振华,
- 近年来基于分数阶微积分的信号和图像处理受到广泛关注.目前常见的应用于图像处理的分数阶微分算子包括G-L(Grünwald-Letnikov)型、R-L(Riemann-Liouville)型和Caputo型3种.G-L和R-L算子尽管能对图像有着一定的增强效果,但其对图像对比度、清晰度的提升有限;而Caputo型微分掩模算子目前多限于(0,1)阶的低阶算子,其高阶次算子的研究和应用相对较少.对高阶次Caputo型分数阶微分算子及其图像增强应用进行研究,首先针对(1,2)阶、(2,3)阶次Caputo型分数阶微分构建一种基于向前差分的微分掩模算子,并对其误差进行了论证;其次进一步给出了更高阶次Caputo型分数阶微分算子的矩阵化表现形式;最后在此基础上将所提出的高阶次Caputo型分数阶微分掩模算子应用于图像增强.实验结果表明所提出的高阶次Caputo型分数阶微分算子取得了很好的图像增强效果,对提升图像的对比度、清晰度和平均梯度具有较为明显的优势.
-
- 基于上下文增强和特征提纯的小目标检测网络
- 肖进胜,赵陶,周剑,乐秋平,杨力衡,
- 微小目标的纹理模糊、包含特征少,是目标检测领域的难点.针对小目标检测提出一种新的上下文增强模块(contextaugmentationmodule,CAM)和特征提纯模块(featurerefinementmodule,FRM)相结合的特征金字塔复合结构.利用多尺度空洞卷积的特征融合,补充网络中的上下文信息;引入通道和空间的特征提纯机制来抑制多尺度特征融合后的冲突信息,防止小目标淹没在冲突信息中;同时,引入复制—缩小—粘贴(copy-reduce-paste)的数据增强方法提高小目标的占比,使训练时小目标对损失值的贡献更大,训练更加平衡.由实验结果可知,所提出的算法在VOC数据集上目标检测的平均精度均值(MeanAveragePrecision,mAP)达到了83.6%(交并比为0.5);对小目标检测的AP值达到了16.9%(交并比为0.5~0.95),比YOLOV4,CenterNet,RefineDet的分别提高3.9%,7.7%和5.3%.在TinyPerson数据集上小目标检测的AP值为55.1%,比YOLOV5,DSFD的分别提高0.8%和3.5%.
