【摘 要】
：
随着软件规模的不断增大,软件安全问题日益严重.作为软件系统安全检测的有效手段,形式化证明旨在利用数学方法完成对软件属性的严格验证.常用的形式化证明方法利用模式匹配来进行定理证明,但存在策略生成不完备等缺陷.本文提出一种基于注意力机制的命令预测框架,将LSTM与Coq结合,预测定理证明过程中的策略和参数.实验结果表明本文提出的模型在生成命令的准确度方面高于现有工作(本工作预测命令准确率为28.31％).
【机 构】
：
中国科学技术大学 网络空间安全学院, 合肥 230027;中国科学技术大学 计算机科学与技术学院, 合肥 230027
论文部分内容阅读
随着软件规模的不断增大,软件安全问题日益严重.作为软件系统安全检测的有效手段,形式化证明旨在利用数学方法完成对软件属性的严格验证.常用的形式化证明方法利用模式匹配来进行定理证明,但存在策略生成不完备等缺陷.本文提出一种基于注意力机制的命令预测框架,将LSTM与Coq结合,预测定理证明过程中的策略和参数.实验结果表明本文提出的模型在生成命令的准确度方面高于现有工作(本工作预测命令准确率为28.31％).
其他文献
图卷积网络(GCN)是处理图结构化数据的一种十分重要的方法,最新的研究表明,GCN极易受到对抗性攻击,即通过修改少量数据,就能显著影响GCN的结果.在对GCN的所有对抗攻击中,有一种特殊的对抗攻击方法——通用对抗攻击.这种攻击能产生应用于所有样本的扰动,并使GCN得到错误的结果.本文主要研究针对性通用对抗攻击,通过在现有算法TUA的基础上引入梯度选择的方法,提出了GTUA.在3个流行数据集上的实验结果表明:仅仅在少数类别上,本文方法与现有方法结果相同,在多数类别上,本文方法均优于现有方法,并且平均攻击成功
Kubernetes是比较流行的开源容器编排引擎,其默认调度算法只考虑了CPU和内存两种性能指标,且采用统一权重计算候选节点得分,无法满足各异的Pod应用需求.本文在此基础上扩展了Kubernetes性能指标,增加了带宽、磁盘、IO速率3种指标,并通过AHP(analytic hierarchy process,层次分析法)计算主观权重和EW(entropy weight,熵权法)根据Pod应用部署过程中节点的性能指标的资源利用率实时计算资源指标的客观权重.两种权重相结合应用到改进的TOPSIS(tech
基于深度学习的行为识别算法往往由于复杂的网络设计而难以在实际应用中达到快速、准确的识别效果.针对以上情况,提出一种轻量型的基于时移和片组注意力融合的端到端双流神经网络模型.算法在RGB与光流分支网络中,采用时间稀疏分组随机采样策略实现长时程建模,利用时移模块在时间维度上置换部分通道从而结合邻帧信息来提升时序表征能力,同时通过多路径及特征图注意融合的片组注意力模块提升网络的识别性能.实验表明,模型在行为识别公共数据集UCF101及HMDB51上分别达到了95.00％和72.55％的识别准确率.
针对密集场景下人群目标尺度变化大导致识别精度不高的问题,本文提出两种多尺度特征融合结构:注意力加权融合模块(attention-weighted fusion module,AWF)和自底向上融合模块(bottom-up fusion module,BUF).其中AWF模块引入注意力分支学习特征图的权重,并将加权后的多层尺度特征进行叠加.而BUF模块在处理特征图时使用空洞卷积捕获更多尺度信息,且浅层特征图采用拼接方式融合.经过融合模块处理的特征图具有更强的表达能力,预测的密度图更加精准.本文算法以ResN
为提高油田作业现场安全作业监管效率,保证油田作业现场近海周界区域人员闯入检测的准确性和时效性,针对现有的区域入侵检测方法在检测油田作业现场远距离小目标时效果差,达不到实时的问题,本文提出了一个基于SOLOv2和CenterNet结合的近海区域作业人员入侵检测模型,模型首先采用SOLOv2对作业现场近海区域周界进行分割,并对分割的结果进行识别,再将识别出的近海区域作为危险区域;然后使用CenterNet网络对作业人员进行检测与定位,对作业人员的位置与危险区域的位置进行计算,从而实现近海周界区域入侵检测.实验
危化品运输车辆的主要特征是车顶的危险标志和车牌下的危险品标志,这对于大多数目标检测算法来说检测起来比较困难.为了在提高检测精度的同时加快检测速度,本文提出了一种融合残差网络和双向特征金字塔网络的危化品车辆检测算法.首先通过对高速公路监控视频进行截取,制作危化品车辆数据集,然后通过残差网络进行特征提取,在本文中,使用循环残差模块替换残差块的中间卷积层.接下来通过双向特征金字塔网络进行特征融合,最后通过预测网络得到预测结果.在测试集上进行性能验证,结果显示本文模型的各项指标整体上均要优于其他网络,其中检测精度
在机器翻译模型的构建和训练阶段,为了缓解因端到端机器翻译框架在训练时采用最大似然估计原理导致的翻译模型的质量不高的问题,本文使用对抗学习策略训练生成对抗网络,通过鉴别器协助生成器的方式来提高生成器的翻译质量,通过实验选择出了更适合生成器的机器翻译框架Transformer,更适合鉴别器的卷积神经网络,并且验证了对抗式训练对提高译文的自然度、流利度以及准确性都具有一定的作用.在模型的优化阶段,为了缓解因蒙汉平行数据集匮乏导致的蒙汉机器翻译质量仍然不理想的问题,本文将Dual-GAN(dual-generat
为了缓解软件缺陷预测的类不平衡问题,避免过拟合影响缺陷预测模型的准确率,本文提出一种面向软件缺陷预测的基于异类距离排名的过采样方法(HDR).首先,对少数类实例进行3类实例区分,去除噪声实例,减少噪声数据导致的过拟合的情况,然后基于异类距离将实例进行排名,选取相似度高的实例两两组合产生新实例,以此来提升新实例的多样性,之后将有价值的被删除的少数类实例恢复.实验将HDR算法与SMOTE算法和Borderline-SMOTE算法进行比较,采用RF分类器在NASA的8个实际项目数据集上进行,结果显示在F1-me
在物联网数据传输过程中,需要认证通信双方的身份和加密传输数据.目前,已有大量的认证和密钥协商方案已经被设计,但是,现有方案容易遭受多种攻击,例如智能卡被盗攻击,拒绝服务攻击等;针对现有方案存在问题,本文提出了一种轻量级的一对多认证和密钥协商方案,在用户端和传感器端分别使用椭圆曲线密码学和异或操作来实现相互认证,利用预共享密钥的方法将传感器端扩展为多个.最后,通过功能比较,计算代价,通信代价对比,显示所提方案优于其他方案,更适合于多传感器场景.
传统的人脸表情识别方法主要针对六类基本人脸表情,但在现实场景下,存在更加丰富的由基本人脸表情组合而成的复合人脸表情,原先识别基本人脸表情的工作难以去识别复合人脸表情,并且复合人脸表情的数据集缺乏足够的训练数据.针对该问题,提出基于图卷积多标签学习的复合人脸表情识别方法.通过特征提取网络提取到人脸表情的全局特征和感兴趣区域的局部特征,使用基本和复合人脸表情之间的先验知识和数据驱动方式,构建出表情类别关系图,利用图卷积网络来学习到表情类别分类器,最后进行复合人脸表情识别.在RAF-DB和EmotioNet数据