一种面向UEFI模块的形式化建模与验证方法

来源 :计算机技术与发展 | 被引量 : 0次 | 上传用户:kaokao514
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
固件作为一种固化在ROM中的特殊软件程序,主要负责加电自检,硬件设备初始化,引导操作系统等基础功能,运行级别和安全等级较高,亟需一种高效、可靠的UEFI模块安全检测方法.采用形式化方法对UEFI模块进行规约与验证,对于提高固件的安全性具有重要意义.基于现有的有限状态自动机和下推自动机基础,分别对UEFI模块中的安全漏洞属性和UEFI模块程序控制流进行形式化建模,利用模型检验对上述模型进行形式化验证.其中利用数据抽象思想将UEFI模块抽象为程序控制流且压缩其状态规模来缓解模型检验时的状态爆炸问题,并给出了相关模型的定义以及模型间转换、组合的算法.实验结果表明,对UEFI模块的抽象及压缩能够很好地缓解模型检验中的状态爆炸问题,并且该形式化验证方法能够实现对UEFI模块安全漏洞的自动化验证,且能够达到较低的漏报率.
其他文献
随着人工智能的兴起,深度学习技术在多个领域有了广泛的应用与发展,将深度学习技术与PCB芯片文字识别相结合,实现具体的场景应用,具有重要意义.基于深度学习进行文字识别,完成图像中文字信息的自动获取,进一步提高了准确率,极大地节约了人工及时间成本.但传统深度学习模型巨大的参数量以及内存消耗等限制了其在小型设备如移动终端上的应用与发展,难以满足人们日益增长的需求.基于此,该文提出了一种基于轻量级网络的文字识别算法LWTR.该算法框架主要包括卷积神经网络(进行特征提取)、循环神经网络(进行标签预测)以及CTC(实
新冠疫情环境下,人们外出均需佩戴口罩进行防护,所以目前对人脸口罩检测的研究迫在眉睫.该文提出一种基于残差结构的SSD(single shot multbox detector)网络用于口罩检测,通过在SSD网络的定位分类前添加残差结构,将特征提取网络和分类定位层进行分离,进而使得进入分类定位层的卷积特征更加抽象,可以有效解决SSD网络同时学习局部信息和高层信息双重任务的问题,维护特征提取网络的稳定性,并利用交叉熵损失函数解决戴口罩和未戴口罩的二分类问题,利用smooth L1 loss损失函数解决口罩位置
针对部分图像加密算法与明文无关,安全性差以及加密效率低的问题,设计一种基于分段线性混沌映射且与明文关联的图像加密算法.首先,将初始值和参数作为密钥,迭代分段线性混沌映射,产生混沌序列;其次,利用产生的混沌序列设计一个混沌密码发生器,产生与明文图像大小相同的4个随机矩阵,记作X、Y、R和W,运用X矩阵对明文做前向扩散,得到矩阵A,再运用R和W矩阵设计一种与明文关联的置乱方法对矩阵A进行置乱得到矩阵B,在置乱的过程中还进行了循环移位操作使加密效果更好;最后运用Y矩阵对矩阵B做后向扩散,得到呈现噪声样式和不再具
科技资源服务是云计算环境下数据服务领域的重要业务之一.但是,由于科技资源归属单位不同,条块分割,实现跨平台服务与共享存在很大障碍.为了解决资源空间分散、业务并发等问题,需要构建基于分布式虚拟化存储技术的科技资源服务业务虚拟化资源池,统一管理资源并提供可靠的数据访问和交互功能.针对这一应用背景,基于云计算理论,在软硬件虚拟化技术的基础上,该文提出了一种分布式虚拟化科技服务资源池多层次模型架构,该模型将资源池应用、汇聚、虚拟和物理层进行了统一描述;在此基础上,利用Pi演算这一描述移动并发系统的数学工具,对所构
随着气象业务技术体制的调整,对气象数据中心的连续稳定运行提出了更高要求,利用虚拟化、分布式、数据备份、业务容灾等多种先进技术,提高硬件资源利用率和软件资源复用率,增强业务系统抗风险能力.数据中心含众多服务器和异构计算资源,引入虚拟网络、虚拟存储、CBT变化数据跟踪等技术、方法,可有效确保系统运行可靠性.在气象监测预报预警支撑系统中,采用VMware的异构虚拟化特性将不同类型的存储进行集中统一管理,简化了系统复杂度,使用vMotion技术实现虚拟化平台的高可用性;数据存储系统采用RAID2.0+块虚拟化架构
网络功能虚拟化(network functions virtualization,NFV)改变了传统网络以及硬件网络设备的形态.许多NFV应用(如网络资源管理、网络安全防护)需要获取指定物理资源、虚拟资源和虚拟网络功能等NFV对象的状态信息,并加以分析和利用.如何根据应用需求灵活地获取NFV对象的状态信息,是NFV管理和编排的一项重要工作.在大型NFV环境中,由于NFV对象的数量急速增加、类型不断丰富,导致难以灵活高效地按需获取NFV对象的状态信息.对此,该文提出了一种信息获取需求与获取技术解耦(info
新冠疫情导致全球在线教育异军突起,如何打破时间、空间的限制实时监督学生的在线学习状态随时调整教学策略进而提高学习效率具有重要意义.基于2D与3D图像处理技术,提出了一种在线评估学习状态的方法,将学习者的学习状态分为无人、多人、用户未授权、分心以及疲劳五种.利用AdaBoost算法与ResNet模型实现人脸检测和识别,并加入质心跟踪算法提高人脸识别检测效率;利用RGB-D图像实时获取人脸三维模型,通过EPNP算法获取学习者头部姿态进而评估学习姿态;提取学习者眼睛和嘴巴的实时图像特征,获取学习者眼睛与嘴巴纵横
传统的矩阵分解算法对药品进行推荐时,由于存在数据稀疏性问题,导致推荐结果不准确.因此提出了一种融合药品语义的混合推荐算法(H-DS).首先利用药品的类别信息构建出药品的分类矩阵,从而计算出药品的类别关联度;然后预处理药品主治功能的描述文本,使用卷积神经网络进行训练,得到其对应的特征;最后用概率矩阵分解算法结合药品类别和功能两方面的语义信息来改进模型,修正矩阵分解的项目隐因子特征,从而实现了对药品的精准推荐.实验表明,在MAE和RMSE评价指标上,H-DS较传统的概率矩阵分解算法(PMF)误差降低了6% ~
随着高等教育的普及,学生人数的增多,高校科研室的事务管理越来越繁杂,虽然部分高校科研室设计开发了自己的科研室管理平台,但存在各科研室之间缺乏沟通、公共资源未能共享、缺乏科研室成员自学习网络教学资源等问题.因此,在深入分析高校科研室管理需求的基础上,设计了基于SSM(SpringMVC+Spring+Mybatis)框架的科研室管理系统.该系统包括首页、管理模块、项目研讨、学习乐园等四大功能模块,其中,在学习乐园模块提出基于虚拟教师的网络教学资源组织模型,实现网络教学资源科学有效的组织与管理.实践表明,科研
现有研究表明,域名生成算法(domain generation algorithm,DGA)已成为僵尸网络建立命令和控制服务通信的关键技术之一.由于利用DGA域名随机性的检测方法已趋于成熟,为逃避检测,DGA算法可能采用加密流量形式进行传输.针对基于域名随机性的检测模型缺乏对加密DGA流量的识别等问题,该文基于DoH(DNS-over-HTTPS)协议验证了DGA流量进行加密传输的可能性,分析了命令控制服务过程所产生的HTTP报文内容、HTTP流量及对应的TCP流量.因利用DoH协议进行传输的数据包中不再