西北工业大学深圳研究院;西北工业大学唐时博获国家专利权
买专利卖专利找龙图腾,真高效! 查专利查商标用IPTOP,全免费!专利年费监控用IP管家,真方便!
龙图腾网获悉西北工业大学深圳研究院;西北工业大学申请的专利一种基于符号执行的处理器特权完整性验证方法获国家发明授权专利权,本发明授权专利权由国家知识产权局授予,授权公告号为:CN118350014B 。
龙图腾网通过国家知识产权局官网在2025-07-22发布的发明授权授权公告中获悉:该发明授权的专利申请号/专利号为:202410503035.0,技术领域涉及:G06F21/57;该发明授权一种基于符号执行的处理器特权完整性验证方法是由唐时博;胡伟;朱嘉诚;慕德俊设计研发完成,并于2024-04-25向国家知识产权局提交的专利申请。
本一种基于符号执行的处理器特权完整性验证方法在说明书摘要公布了:本发明公开了一种基于符号执行的处理器特权完整性验证方法,首先,将处理器RTL设计的Verilog代码转换为功能等效的C++代码,并在转换后的C++代码中插入与特权完整性相关的断言;然后,使用符号执行引擎搜索符号路径,以识别可能导致断言违反的漏洞;最后,构建了一个包含CPU模块和快速缓存模块的最小验证平台,生成概念验证,用于模拟和验证搜索阶段发现的漏洞。本发明可以有效地识别并验证处理器设计中的特权转换完整性问题。
本发明授权一种基于符号执行的处理器特权完整性验证方法在权利要求书中公布了:1.一种基于符号执行的处理器特权完整性验证方法,其特征在于,包括如下步骤: 步骤1:代码转换; 采用开源工具Verilator,将Verilog代码转换为功能等效的C++代码; 编写C++的封装文件,用于实例化硬件设计的顶层模块; 通过使用KLEE的klee_make_symbolic函数,将相关的输入信号符号化; 在封装文件中插入了与特权提升相关的断言,断言定义了符号执行过程中需要检测的安全漏洞条件; 步骤2:对搜索路径进行优化; 利用KLEE引擎的高级功能,通过交错使用深度优先搜索DFS和广度优先搜索BFS策略,对搜索路径进行优化; 步骤3:符号执行分析; 将带有断言的C++代码编译成LLVM的中间代码表示LLVMIR; 通过符号执行引擎对LLVMIR代码进行分析,探索所有可能的执行路径,识别违反断言的状态,即潜在的特权提升漏洞; 符号执行过程中,当遇到分支指令时,将探索所有可能的路径,并使用约束求解器确定这些路径的可满足性; 在硬件环境中,将处理器指令的执行模拟为相应的符号表达式,遇到分支指令时,搜索进程可以独立探索和分析不同的路径;从这些执行路径收集路径条件,并使用约束求解器来确定这些路径条件的满足性;如果路径条件不能被满足,那么该路径被认为是不可行的,并终止搜索;类似地,当沿着一条路径检测到错误时,该路径会被暂停搜索,并自动生成满足路径条件的输入值; 步骤4:测试用例分析; 在利用KLEE进行符号执行分析时,设置KLEE引擎的搜索方式,要求返回每个违反断言状态的所有反例,而不是在遇到第一个违反断言状态时就停止搜索; 利用KLEE工具链,分析生成的反例,这些反例中包含了触发违反断言状态的具体数据;通过这一过程,识别出引发特权提升漏洞的特定输入和条件,为每个识别的违反断言状态生成对应的测试用例; 步骤5:最小系统模拟与PoC生成; 构建一个最小系统模拟平台,仅包括能运行触发漏洞指令的处理器模块和缓存管理单元,禁用其他与内存相关的模块以提高模拟效率并减少干扰; 通过编写汇编程序并在模拟平台上执行,自动转换为可用于最小系统验证的初始化文件,重放测试用例中的漏洞场景,生成PoC。
如需购买、转让、实施、许可或投资类似专利技术,可联系本专利的申请人或专利权人西北工业大学深圳研究院;西北工业大学,其通讯地址为:陕西省西安市南山区粤海街道高新技术产业园南区虚拟大学园;或者联系龙图腾网官方客服,联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。
1、本报告根据公开、合法渠道获得相关数据和信息,力求客观、公正,但并不保证数据的最终完整性和准确性。
2、报告中的分析和结论仅反映本公司于发布本报告当日的职业理解,仅供参考使用,不能作为本公司承担任何法律责任的依据或者凭证。