面向Armv8-a汇编代码的形式化验证方法
2025-02-27 18:05
No.1344732113920073728
技术概要
PDF全文
本技术公开了一种面向Armv8‑a汇编代码的形式化验证方法,对Armv8‑a的处理器架构和指令集系统进行分析,提取出需要建模的各个模块构件,包括异常级别、执行状态、数据值、寄存器组、内存、指令集、汇编代码,对各个模块构件进行建模;根据汇编代码中每个汇编指令的功能和安全规范确定对应汇编指令的非形式化要求,然后结合定义的模型生成每个汇编指令的形式化逻辑表达式,从而得到形式化规约;最后采用定理证明器进行形式化验证。本发明对物理机器的各个模块构件进行建模,然后基于构建的模型生成汇编代码中每个汇编指令的形式化逻辑表达式,使用定理证明器完成Armv8‑a汇编代码的形式化验证。
背景技术
操作系统作为现代计算机应用的基础平台,支持各类软件的运行,并直接影响计算机系统的稳定性和安全性。操作系统中的小漏洞可能导致严重的系统错误或安全威胁,甚至引发生命和财产损失。因此,确保操作系统的安全性和可靠性是维护计算机软件生态健康运行的关键因素。 传统的软件测试方法在发现错误和漏洞方面存在局限,测试无法覆盖所有情况和路径,漏洞可能隐藏在边缘情况或复杂交互中。因此,虽然传统测试方法是重要的质量保障手段,但无法完全消除系统中的错误和漏洞。而随着系统功能的扩展、代码规模的增大以及内部逻辑的复杂化,确保系统的可靠性和安全性成为一项重要且富有挑战性的任务。在现有技术中,形式化方法是解决这一挑战的有效途径。 形式化方法是一种以数学和形式化语言为基础,能够提高软硬件系统的可靠性和正确性的技术。该方法的核心理念是通过精确而严格的规约和验证过程,消除软硬件设计和实现中的歧义,降低错误和漏洞的发生概率。形式化方法包括形式规约和形式验证两个主要步骤。形式规约是对系统行为和性质的详细、数学化描述,通常使用形式化语言。这样的规约消除了对系统规范的模糊理解,提供了准确且一致的描述。形式验证则通过数学分析方法,对形式规约进行验证,以确保系统满足规约中定义的性质。 近些年来,针对操作系统内核验证的工作:澳大利亚国家信息通信中心(NICTA)的seL4项目,使用了交互式定理证明器Isabelle/HOL,通过三层验证框架完成了微内核的形式化验证。耶鲁大学根据深度规约和认证抽象层开发出的CertiKOS框架,通过Coq验证了并发操作系统内核mC2。中国科学技术大学开发出了针对C语言子集的操作系统内核验证框架,验证了抢占式操作系统μC/OS-II的关键模块。 现代操作系统主要使用高级语言开发,但汇编代码在关键部分仍然发挥着不可或缺的作用。相比高级语言,汇编代码可以实现对硬件的直接访问和控制:能够直接操作CPU寄存器、执行特权指令以及与硬件设备进行高效交互,这在许多性能敏感的场景中至关重要。例如,在上下文切换和中断处理时,汇编代码可以确保最小的延迟和最高的执行效率。此外,汇编语言还允许开发者在内存管理和系统调用中实现更精细的控制,确保操作系统在资源受限的环境中运行时的可靠性和高效性。因此,汇编代码中潜在的错误或漏洞都可能导致系统崩溃或安全隐患,所以对操作系统的验证离不开汇编代码的安全性。
实现思路
阅读余下40%
技术概要为部分技术内容,查看PDF获取完整资料
该技术已申请专利,如用于商业用途,请联系技术所有人!
技术研发人员:
肖堃  李雨珊  黄钰馨  李蒙  罗蕾  陈丽蓉
技术所属: 电子科技大学  中移物联网有限公司
相关技术
一种服务开发方法、装置、设备及存储介质 一种服务开发方法、装置、设备及存储介质
一种高精度双层优化方法的神经网络搜索架构构建方法 一种高精度双层优化方法的神经网络搜索架构构建方法
跨总线域的设备对宿主机空间DMA访问方法及相关设备 跨总线域的设备对宿主机空间DMA访问方法及相关设备
一种客户信息定期维护方法及系统 一种客户信息定期维护方法及系统
代码发布方法、装置、计算机设备和可读存储介质 代码发布方法、装置、计算机设备和可读存储介质
一种基于统一管理平台的子应用数据获取方法及装置 一种基于统一管理平台的子应用数据获取方法及装置
利用深度学习的BIM模型错误自动检测系统 利用深度学习的BIM模型错误自动检测系统
一种基于智能反射面的室内T型走廊场景路径损耗的分析方法 一种基于智能反射面的室内T型走廊场景路径损耗的分析方法
模型评估任务处理方法及装置 模型评估任务处理方法及装置
基于大数据的异常信号智能识别方法 基于大数据的异常信号智能识别方法
技术分类
电信、广播电视和卫星传输服务 电信、广播电视和卫星传输服务
互联网软件服务 互联网软件服务
集成电路设计 集成电路设计
信息集成数字服务 信息集成数字服务
电气机械制造 电气机械制造
计算机、通信、电子设备制造 计算机、通信、电子设备制造
医药制造、生物基材料 医药制造、生物基材料
石油煤矿化学用品加工 石油煤矿化学用品加工
化学原料制品加工 化学原料制品加工
非金属矿物加工 非金属矿物加工
金属制品加工 金属制品加工
专用设备制造 专用设备制造
通用设备制造 通用设备制造
通用零部件制造 通用零部件制造
汽车制造业 汽车制造业
铁路、船舶、航天设备制造 铁路、船舶、航天设备制造
电力、热力生产和供应 电力、热力生产和供应
燃气生产和供应 燃气生产和供应
水生产和供应 水生产和供应
房屋建筑、土木工程 房屋建筑、土木工程
交通运输、仓储和邮政 交通运输、仓储和邮政
农、林、牧、渔业 农、林、牧、渔业
采矿业 采矿业
农副、食品加工 农副、食品加工
烟草、酒水加工 烟草、酒水加工
纺织皮具居家制品 纺织皮具居家制品
文教体娱加工 文教体娱加工
苏ICP备18062519号-5 © 2018-2025 【123技术园】 版权所有,并保留所有权利