【摘 要】
：
整数溢出引起的软件系统安全性问题屡见不鲜,已有的模型检测技术由于存在状态空间爆炸、不能有效支持中断驱动型程序检测等缺点而少有工程应用.结合真实案例,对航天嵌入式软件整数溢出问题的分布和特征进行了系统性的分析.在有界模型检测技术的基础上,结合整数溢出特征,提出了基于整数溢出变量依赖的程序模型约简技术;同时,针对中断驱动型程序,结合中断函数特征抽象,提出了基于干扰变量的中断驱动程序顺序化方法.经过基准测试程序和真实航天嵌入式软件实验,结果表明:该方法在保证整数溢出问题检出率的前提下,不仅能够提高分析效率,还使
【机 构】
：
北京控制工程研究所,北京轩宇信息技术有限公司
【基金项目】
：
国家自然科学基金(61802017),装备预研领域基金(61400020407)。
论文部分内容阅读
整数溢出引起的软件系统安全性问题屡见不鲜,已有的模型检测技术由于存在状态空间爆炸、不能有效支持中断驱动型程序检测等缺点而少有工程应用.结合真实案例,对航天嵌入式软件整数溢出问题的分布和特征进行了系统性的分析.在有界模型检测技术的基础上,结合整数溢出特征,提出了基于整数溢出变量依赖的程序模型约简技术;同时,针对中断驱动型程序,结合中断函数特征抽象,提出了基于干扰变量的中断驱动程序顺序化方法.经过基准测试程序和真实航天嵌入式软件实验,结果表明:该方法在保证整数溢出问题检出率的前提下,不仅能够提高分析效率,还使
其他文献
HDFS分布式文件系统作为Apache Hadoop的核心组件之一,在工业界得到了广泛应用.HDFS采用了多副本机制保证数据的可靠性,但是由于多副本的存在,在节点失效、网络中断、写入失败时可能会导致数据不一致.与传统文件系统相比,HDFS被认为其数据一致性有所降低,但用户并不知道何时会出现不一致的情况,目前也没有相关工作对其一致性机制进行验证说明.当数据存在一致性问题时,会增加上层应用的不确定性.可见,对数据一致性的研究十分必要.HDFS的软件规模庞大,且在分布式环境下运行,针对这些特点,采用了着色Pet
人工免疫系统(artificial immune system,简称AIS)是人工智能技术的重要分支之一,被广泛应用于异常检测、数据挖掘、机器学习等多个领域.检测器是其核心知识集,其生成、优化和检测操作决定了人工免疫的应用效果.目前,人工免疫的问题空间以实值形态空间为主,但实值非自体空间“黑洞”、检测器生成速率慢、检测器高重叠冗余、“维度灾难”等问题,使得人工免疫检测的效果不甚理想.鉴于此,使用邻域形态空间,并改进邻域否定选择算法(neighborhood negative selection a
采用红外测温仪、室温拉伸试验、光学显微镜(OM)、扫描电子显微镜(SEM)与能谱仪(EDS),研究了柔性辊冷却装置下不同退火温度对430铁素体不锈钢薄带冷却效率的影响,分析了带钢的组织与力学性能.结果 表明:当退火温度由800℃升高至1100℃,用柔性辊得到的带钢的冷却速度先增大后减小;对比不同退火温度下的试验钢的晶粒尺寸:在850～950℃退火时,铁素体晶粒较细小均匀并呈等轴状;试样在退火温度为850～900℃时获得的性能较优,此时抗拉强度为480～500MPa,屈服强度为280～300 MPa,伸长率
近年来,手势作为一种输入通道,已在人机交互、虚拟现实等领域得到了广泛的应用,引起了研究者的关注.特别是随着先进人机交互技术的出现以及计算机技术(特别是深度学习、GPU并行计算等)的飞速发展,手势理解和交互方法取得了突破性的成果,引发了研究的热潮.综述了动态手势理解与交互的研究进展与典型应用:首先阐述手势交互的核心概念,分析了动态手势识别与检测进展;而后阐述了动态手势交互在人机交互中的代表性应用,并
摘要：针对长江干线航道“中梗阻”问题，学界提出了荆汉生态新水道的系统解决方案。通过梳理长江中游地区航运发展条件，从航道、港口、运输安全等方面，分析了荆汉生态新水道的实施对长江中游航运发展的综合影响。研究结果表明：① 荆汉生态新水道的建设，在长江中游区域将形成“双通道”的运输格局，促进长江干线航道区段标准统一和区域高等级航道网络化，形成与长江上游地区的便捷通道，大幅提高长江干线大型船舶的通达程度，实
新时代以来,中共中央办公厅、国务院办公厅、中共中央宣传部、教育部等部门,多次下发加强高校思政课建设的相关文件,更加突出“高校是党领导下的高校,是中国特色社会主义高校”的理念.针对专科、本科、硕士、博士等不同层次,以及部分高校有重点马克思主义学院的现实,分别规定了思政课的设置与要求.课题组依据相关文件,把加强高校思政课实效性研究放在世界百年未有之大变局、党和国家事业发展全局中考虑,结合了高等医学院校四年制与五年制不同学制的实际,也充分考虑到医学相关课程的设置,规范和建立了一套在医学院校设置思政课的基本课程体
抽象语义表示(abstract meaning representation,简称AMR)文本生成的任务是给定AMR图,生成与其语义一致的文本.相关工作表明,人工标注语料的规模大小直接影响了AMR文本生成的性能.为了降低对人工标注语料的依赖,提出了基于多任务预训练的AMR文本生成方法.特别地,基于大规模自动标注AMR语料,提出与AMR文本生成任务相关的3个预训练任务,分别是AMR降噪自编码、句子降噪自编码以及AMR文本生成任务本身.此外,基于预训练模型,在朴素微调方法的基础上,进一步提出了基于多任务训练的
近年来,写密集型应用程序越来越普遍.如何有效地处理这种工作负载,是数据库系统领域深入研究的方向之一.写操作开销主要由以下两个方面的因素构成:(1)硬件级别,即写操作引起的I/O,目前无法在短时间内消除这种开销;(2)软件开销,即修改内存数据拷贝以及构造日志记录造成的多次写操作.日志即数据(log-as-database,称其为单拷贝系统)的架构能够减少写操作引起的I/O,同时降低软件方面的开销.目前,业界对单拷贝系统展现出浓厚的兴趣.现有的单拷贝系统大部分建立在特殊的基础设施之上,例如infiniband
为了在构造多接收方签密方案时,既不牺牲安全性又可以节约通信和计算开销,首先将随机数重用的安全理论丰富到另一种常见情况,提出了随机数部分重用的概念,并以签密体制为研究对象,定义了随机数部分重用的多接收方签密方案、随机数部分重用可再生的签密方案及安全模型;然后给出并证明了可再生性定理——随机数部分重用的安全条件为方案是可再生的;最后证明了LWWD16的格基签密方案是一个随机数部分重用可再生的签密方案,并基于LWWD16首次构造了一个基于格的随机数部分重用的多消息多接收方签密方案,证明了方案满足抗自适应选择密文
降雨会严重降低拍摄图像质量和影响户外视觉任务.由于不同图像中,雨的形状、方向和密度不同,导致单幅图像去雨是一项困难的任务.提出一种新的基于双注意力的残差循环单幅图像去雨集成网络(简称RDARENet).在网络中,因为上下文的信息对于去除雨痕十分重要,所以首先采用多尺度的扩张卷积网络去获得更大的感受野.雨痕信息可以认为是多个雨层特征的叠加,为了更好地提取雨痕的特征和恢复背景图层信息,运用了通道和空间