电子科技大学;中移物联网有限公司肖堃获国家专利权
买专利卖专利找龙图腾,真高效! 查专利查商标用IPTOP,全免费!专利年费监控用IP管家,真方便!
龙图腾网获悉电子科技大学;中移物联网有限公司申请的专利面向Armv8-a汇编代码的形式化验证方法获国家发明授权专利权,本发明授权专利权由国家知识产权局授予,授权公告号为:CN119415399B 。
龙图腾网通过国家知识产权局官网在2025-07-29发布的发明授权授权公告中获悉:该发明授权的专利申请号/专利号为:202411589807.3,技术领域涉及:G06F11/36;该发明授权面向Armv8-a汇编代码的形式化验证方法是由肖堃;李雨珊;黄钰馨;李蒙;罗蕾;陈丽蓉设计研发完成,并于2024-11-08向国家知识产权局提交的专利申请。
本面向Armv8-a汇编代码的形式化验证方法在说明书摘要公布了:本发明公开了一种面向Armv8‑a汇编代码的形式化验证方法,对Armv8‑a的处理器架构和指令集系统进行分析,提取出需要建模的各个模块构件,包括异常级别、执行状态、数据值、寄存器组、内存、指令集、汇编代码,对各个模块构件进行建模;根据汇编代码中每个汇编指令的功能和安全规范确定对应汇编指令的非形式化要求,然后结合定义的模型生成每个汇编指令的形式化逻辑表达式,从而得到形式化规约;最后采用定理证明器进行形式化验证。本发明对物理机器的各个模块构件进行建模,然后基于构建的模型生成汇编代码中每个汇编指令的形式化逻辑表达式,使用定理证明器完成Armv8‑a汇编代码的形式化验证。
本发明授权面向Armv8-a汇编代码的形式化验证方法在权利要求书中公布了:1.一种面向Armv8-a汇编代码的形式化验证方法,其特征在于,包括以下步骤: S1:对Armv8-a的处理器架构和指令集系统进行分析,提取出需要建模的各个模块构件,包括异常级别、执行状态、数据值、寄存器组、内存、指令集、汇编代码,对各个模块构件进行建模,具体方法为: S1.1:定义异常级别类型包括EL0~EL3,EL0用于普通用户应用程序执行,EL1用于操作系统内核特权级别执行,EL2用于虚拟机管理程序执行,EL3用于安全世界执行;定义执行状态类型包括AArch64和AArch32,处于AArch64状态时,处理器执行A64指令集,并使用64位宽通用寄存器;处于AArch32状态时,处理器执行A32或T32指令集,并使用32位宽通用寄存器; S1.2:定义数据值基本类型包括布尔类型,自然数类型,整数类型,有理数类型,并在此基础上依据位数和范围限制拓展定义8位,32位,64位字长以及对应的字节byte类型、32位整型类型、64位整型类型; S1.3:定义寄存器集包括通用寄存器greq、特殊寄存器sreg、处理器状态psbit;最后定义寄存器组模块,包括寄存器集实例映射到步骤1.2中的数据值类型上,并且提供符号表示法来操作映射,包括访问映射值和更新映射值; S1.4:将内存数据基于基本数据值定义,将内存中每一字节都同memval类型进行了映射,包括未初始化类型、由无符号8bit映射的字节类型,以及由块和偏移量映射的指针类型;内存操作类型包括读取load和存储store操作;内存权限类型包括可读,可写和可读写权限;最后使用Record定义内存类型将上述内容整合为一体; S1.5:定义Armv8-a指令集类型包括数据处理指令、加载存储指令、流控分支指令、系统控制指令、异常处理指令、系统寄存器访问指令和伪指令,其中数据处理指令类型包括算术和逻辑运算、移动和位移操作、符号和零扩展操作、条件比较操作;对寻址方式进行建模,包括立即数寻址、寄存器寻址、基址寻址、前后索引寻址,并基于此定义加载存储指令;流控分支指令包括无条件分支B、条件分支BC,子程序调用和返回BL、RET,异常返回ERET;系统控制指令包括访问系统寄存器指令MRS、MSR; S1.6:定义汇编代码中每个汇编指令的操作流程,包括取指,解析和执行过程,然后设计用于模拟指令执行器的递归函数,该函数逐步解释程序计数器指向的汇编指令,递归地执行指定数量的汇编指令,并更新寄存器和内存的状态,从而模拟汇编代码的执行过程; S2:根据汇编代码中每个汇编指令的功能和安全规范确定对应汇编指令的非形式化要求,然后结合步骤S1定义的模型生成每个汇编指令的形式化逻辑表达式,从而得到形式化规约; S3:根据实际需要选择定理证明器,将模拟指令执行器的递归函数和每个汇编指令的形式化逻辑表达式转换为定理证明器中形式语言定义的格式,使用定理证明器中提供的验证策略进行形式化验证。
如需购买、转让、实施、许可或投资类似专利技术,可联系本专利的申请人或专利权人电子科技大学;中移物联网有限公司,其通讯地址为:611731 四川省成都市高新区(西区)西源大道2006号;或者联系龙图腾网官方客服,联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。
1、本报告根据公开、合法渠道获得相关数据和信息,力求客观、公正,但并不保证数据的最终完整性和准确性。
2、报告中的分析和结论仅反映本公司于发布本报告当日的职业理解,仅供参考使用,不能作为本公司承担任何法律责任的依据或者凭证。