【摘 要】
：
随着软件工程技术的不断发展,软件的功能变得越来越丰富,这给人们的生活带来了极大的便利性,但软件的复杂性和多样性,也使得软件安全漏洞与日俱增,传统的软件测试方法说明软件存在某些安全漏洞,但是不能保证软件不存在某类安全漏洞,相比之下形式化验证方法则可以做到这一点。操作系统作为基础系统软件,其安全性至关重要,使用形式化验证方法对操作系统内核的实现代码进行验证,是保证其安全性和正确性的有效手段。而操作系统
论文部分内容阅读
随着软件工程技术的不断发展,软件的功能变得越来越丰富,这给人们的生活带来了极大的便利性,但软件的复杂性和多样性,也使得软件安全漏洞与日俱增,传统的软件测试方法说明软件存在某些安全漏洞,但是不能保证软件不存在某类安全漏洞,相比之下形式化验证方法则可以做到这一点。操作系统作为基础系统软件,其安全性至关重要,使用形式化验证方法对操作系统内核的实现代码进行验证,是保证其安全性和正确性的有效手段。而操作系统的内核实现代码多为C与汇编的混合代码,如果使用传统的形式化验证方法进行验证,存在人工参与度高、验证效率低、验证复杂度高等问题,因此本文主要以混合代码的自动形式化验证为研究背景,重点研究了混合代码自动形式化验证技术与实现方法。本文主要工作如下:（1）基于模型检测技术,提出了一种面向汇编代码的自动形式化验证方法。为了提高验证效率,降低验证工作量,构建了ARM汇编指令模型库,该模型库为ARM汇编代码的建模与验证提供了统一的接口,利用该模型库可以方便地对汇编代码进行抽象建模和验证。（2）针对混合代码中C代码与汇编代码嵌套调用带来的建模困难和验证复杂度高等问题,提出了一种混合代码的建模与验证方法,通过对混合代码中的C代码进行编译和抽象建模,使得可以在统一的抽象级别对C语言和汇编语言代码进行验证,大大提高了验证效率。在混合代码验证方法中还加入了对中断处理程序的验证支持,并使用了中断执行预测算法对由此产生的模型状态爆炸问题进行了解决。（3）为了进一步提高混合代码验证的自动化程度,基于本文提出的混合代码自动形式化验证方法开发了一个混合代码自动形式化验证工具,该工具提供了C代码功能性验证、自动解析混合代码生成抽象模型、基于模型检测的安全属性验证等功能,利用该工具对μC/OS-II操作系统中的混合代码函数进行了验证,展示了工具使用的便利性以及验证方法的有效性。
其他文献
联邦学习是当下针对机器学习中隐私安全保护和数据孤岛问题的主要解决方法,并在物联网、医疗和金融等领域广泛应用。对于联邦学习系统在应用过程中广泛存在的用户稳定性和分布式计算管理的问题,异步联邦学习是较实际的解决办法。本文主要研究在基于卷积神经网络的异步联邦学习场景下,客户端怎样根据环境和资源条件异步控制训练流程,有效的避免因客户端出错和数据通信导致的联邦学习系统的稳定性问题,并对异步场景下的恶意攻击中
目前,我国装修市场迫切需要研发出能够代替人类进行复杂工作的装修机器人。装修机器人最重要的技术之一是自主导航技术,即在任何室内环境中,机器人具备快速到达目标点进行装修工作的能力。基于深度强化学习的自主导航技术利用机器人获得的环境信息,能够在无地图的情况下控制装修机器人快速到达目标位置完成导航任务。在之前的研究中,无论是利用基于视觉传感器还是或激光雷达传感器的深度强化学习导航算法,均存在两个亟待解决的
现代无线通信技术依赖于自适应天线技术的发展。这影响了新时代的天线设计,以适应不断变化的射频环境。可重构天线就是这样一种设计,其工作频率、辐射方向图和极化方式可以根据用户的要求进行改变。MIMO（multiple input multiple output）成为研究的热门,因为MIMO天线在不需要增加额外功率或频带的情况下提高信道容量,当然这需要收发器都具有很多根天线,且天线间的耦合需要很小。因此M
共识算法是区块链的重要组成部分。共识算法的建立不仅需要选择合理的共识节点,而且还需要完善的共识机制。现有的区块链网络中使用的Po W（工作量证明）以及Po S（权益证明）共识算法是算力和资产的证明。这种在节点之间作为竞争依据的证明方式不仅限制了区块链网络中的活力,而且极大地限制了普通节点加入共识网络,提高了节点加入区块链网络的门槛。虽然共识算法Po S（权益证明）、DPo S（委托权益证明）在共识
基于生理信号的人体疲劳监测是指利用人体采集的生理电信号来判断受试者的疲劳程度。基于生理信号的疲劳监测因其客观性、可连续性等优势而具有很好的应用前景,但不同用户在性格、年龄等生理心理方面的差异,导致不同用户的生理信号具有差异。这种用户差异使得在已有用户上建立的人体疲劳监测模型直接用于新用户时稳定性变差。为此,本文提出了基于域适应（Domain Adaption）技术和基于域泛化（Domain Gen
Android应用程序加壳是一种常见的Android应用软件代码保护技术,加壳后的Android应用原程序字节码被隐藏,可以防止敏感信息泄露,也可能被攻击者利用来隐藏恶意API进而绕过检测。当前主流的Android应用脱壳技术是非虚拟化保护技术,其脱壳方法主要是通过在固定脱壳点插入脱壳代码采集Dex文件信息并对其进行脱取,之后进行组装修复,而这种方法容易被反调试和反向劫持技术绕过。针对强度最高的虚
指静脉是一种稳定安全的生物特征,在生活中有广泛的应用前景。目前指静脉识别技术的应用存在许多挑战,如:一、传统的指静脉特征提取算法基于手工设置的特征参数（静脉模式的几何和拓扑结构,局部二进制码等）,算法的泛化能力不好,基于深度学习的方法在学习特征表示时,没有充分利用样本的类内和类间关系,算法的识别性能存在一定提升空间。二、基于红外传感器采集的指静脉图像容易出现对比度低、曝光过度、模糊等质量问题,因此
由于世界各地对石油及其附属产品需求量的增加,石油的海上开采、运输更频繁导致海上溢油事故频发。因为溢油事故发生后表面浮油对海洋环境的负面影响最为直接,所以海洋溢油治理采取的一系列紧急措施都是针对表面浮油的去除,以期短时间内最大限度去除污染源。然而在紧急处理后仍会在海水中的残留一定量的溶解性石油烃（Dissolved Petroleum Hydrocarbons,DPH）,在海洋水利条件影响下DPH发
目的:分析淋巴瘤病人生命意义感在心理痛苦与生命质量间的调节效应，为提升病人的生命质量提供参考。方法:采用生命意义感量表、心理痛苦量表、淋巴瘤病人生命质量量表对350例淋巴瘤病人进行调查，并应用分层回归分析和简单斜率法分析三者间的关系。结果:淋巴瘤病人生命质量得分为（118.75±21.53）分，其中功能状况得分最低。淋巴瘤病人生命质量与生命意义感呈正相关（r=0.405,P＜0.01）,与心理痛苦
语音是最常见的一种沟通方式,为了使机器代替人工,开发人员提出了语音识别技术,使得机器能够代替人脑来将语音转化为文本。但是带噪环境下语音识别技术的准确率会显著下降,所以往往需要使用语音增强技术作为其前端先进行处理。本文面向航空管制场景,探索了复杂噪声环境下的轻量级语音增强方案。研究了可以在不同噪声环境下自适应地学习该种噪声特征、并有针对性进行降噪的算法。由于提出的算法均基于卷积神经网络,所以将不同的