本发明涉及计算机软件的验证，具体涉及一种面向risc-v架构的二进制程序验证方法及系统。
背景技术：
1、risc-v（reduced instruction set computing - v）是一种开源指令集架构（isa），因其高度的可配置性和模块化而广泛应用于定制微处理器和嵌入式系统开发中。尽管risc-v架构提供了极大的软件和硬件开发灵活性，但现有的软件验证工具常常无法有效支持汇编语言和无源代码的二进制文件，特别是在对安全性和可靠性要求极高的应用场景，如嵌入式系统和操作系统。当前工具的不足主要体现在对底层语言和编译后代码的理解不足，无法全面覆盖这些程序的所有潜在错误。
2、在软件验证领域，静态分析、动态测试、定理证明和模型检验各自提供了独特的优势和应用方法。这些技术是理解和确保程序行为符合预期的关键工具，特别是在处理低级语言如汇编代码和二进制文件时。虽然每种方法都有其应用场景，但它们在处理特定类型的错误和验证特定方面的程序正确性时表现出各自的优缺点。以下详细描述了这些方法的操作方式和它们在实际中的应用。（1）静态分析：静态分析工具通过不执行程序的方式分析汇编代码或二进制文件，预测程序在运行时可能出现的问题。这些工具深入检查汇编程序的语法和结构，特别关注指令的正确使用、寄存器的分配、数据流和控制流的正确性。静态分析可以识别如未初始化的寄存器访问、错误的跳转指令、非法的内存访问等问题。此外，它还可以检查安全漏洞，如缓冲区溢出和权限错误。（2）动态测试：动态测试涉及在真实或虚拟的硬件环境中执行汇编或二进制程序。通过实时监控程序的行为，这种方法可以捕获那些仅在特定运行条件下才会显现的错误，包括运行时错误、资源访问冲突和性能瓶颈。动态测试通常需要精心设计的测试用例来模拟各种可能的执行路径和用户交互。此方法对于验证程序在实际硬件上的兼容性和行为尤为重要，尤其是在复杂的系统集成和多任务操作环境中。（3）定理证明：在汇编程序或二进制文件的验证中，定理证明使用形式化逻辑和数学方法来证明程序符合预定义的规范。使用如isabelle或coq等形式化语言，专家可以构建汇编程序的精确数学模型，并应用霍尔逻辑来推导和验证程序行为的正确性。这种方法非常适合验证关键算法的实现，如加密协议和安全通信。汇编程序（汇编语言程序）是一种低级编程语言，它允许程序员通过使用易于记忆的符号代码（而非二进制代码）直接控制硬件。二进制文件包含一系列可直接由计算机处理器执行的机器语言指令，这些文件通常是编译后的程序，如可执行文件和库文件。（4）模型检验：模型检验通过构建汇编或二进制程序的状态机模型，系统地探索所有可能的程序执行路径。这包括使用时序逻辑描述的验证规约，以检查程序是否满足如死锁自由、事件正确性等性质。此外，模型检验还可以将状态机模型和形式化规约转化为布尔表达式，并使用sat (satisfiability) / smt(satisfiability modulo theories) 求解器进行求解。sat求解器用于确定一组逻辑公式是否存在满足解，而smt求解器则是其扩展，可以处理包含理论（如整数算术、实数算术、数组等）的逻辑公式。这些技术使得模型检验能够自动化地验证规约的正确与否。
3、在验证汇编程序和二进制文件的现有方法中，常见的挑战包括技术局限性、高复杂性以及对专业知识的依赖性。虽然静态分析、动态测试、定理证明和模型检验各有其独特的应用优势，它们也面临着无法全面覆盖所有执行路径、处理复杂依赖和环境交互的困难，以及在无源代码情况下的应用局限。这些方法在实际应用中常常无法完全满足高安全和可靠性标准的需求，尤其是在面对汇编和二进制级别的验证挑战时。因此，开发一种更高效、更全面的验证方法成为了行业的迫切需求，以确保软件产品在复杂环境中的稳定性和安全性。每种方法在实际应用中遇到的具体技术问题和缺陷。（1）静态分析：静态分析工具主要设计用于分析高级编程语言，对于汇编代码，虽然能够进行一定的错误检测和流程分析，但在分析二进制文件时通常表现出较大的局限性。由于静态分析不执行代码，它通常无法完全准确地捕捉到运行时可能发生的动态行为和环境依赖问题。此外，这些工具在处理汇编代码中底层逻辑和数据流的理解上往往不足，可能会漏检关键错误或产生误报，尤其是在面对复杂的系统交互和外围设备操作时。（2）动态测试：动态测试通过实际执行程序来检测汇编和二进制文件中的错误，它能够直接观察程序的运行时行为，包括对资源冲突、运行时错误和性能问题的检测。然而，这种方法的有效性极度依赖于测试用例的全面性和深度。设计能覆盖所有潜在执行路径的测试用例非常困难，特别是对于具有复杂输入和多路径执行的大型应用程序。此外，动态测试通常耗时长，成本高，且可能无法在没有适当硬件环境的情况下执行。（3）定理证明：定理证明方法使用数学逻辑来证明程序符合特定的规范。对于汇编程序，定理证明可以提供极高的验证准确性，尤其适用于验证关键系统的核心算法和安全性要求高的组件。然而，它需要高度专业化的知识，并且在构建形式化证明时耗时且复杂，特别是对于复杂的汇编程序或没有源代码的二进制文件，将其逻辑精确地表达为数学模型非常具有挑战性。（4）模型检验：模型检验通过构建汇编程序或二进制文件的行为模型并探索所有可能的状态来验证程序的正确性。这种方法特别适用于处理复杂交互行为的程序验证，因为它可以系统地分析所有可能的程序状态。模型检验的自动化能力使其成为现代软件验证中一个强大的工具，特别是在需要验证程序对各种输入和事件响应的正确性时。不过，模型检验的成功在很大程度上依赖于模型的准确性和完整性，需要精心设计模型来确保覆盖所有关键的程序行为和可能的状态变化。
4、总而言之，现有验证方法和工具的不足主要体现在对底层语言和编译后代码的理解不足，无法全面覆盖这些程序的所有潜在错误。
技术实现思路
1、本发明要解决的技术问题：针对现有技术的上述问题，提供一种面向risc-v架构的二进制程序验证方法及系统，本发明旨在通过高效、全面且自动化的方式验证risc-v汇编程序和二进制文件的正确性，提高软件在实际部署前的可靠性和安全性。
2、为了解决上述技术问题，本发明采用的技术方案为：
3、一种面向risc-v架构的二进制程序验证方法，包括下述步骤：
4、s101，获取输入的源文件，所述源文件为elf二进制文件；
5、s102，将输入的源文件利用elf文件处理器进行解析并加载至模拟器，通过模拟器为加载的源文件提供实际硬件环境的运行时模拟；
6、s103，利用risc-v指令解码器从内存中提取相应长度的二进制指令，并依据risc-v的编码规则解码得到具体的汇编指令及其操作数；
7、s104，利用汇编转c转换器将解码得到的汇编指令及其操作数转换为c语言代码文件；
8、s105，利用验证逻辑生成器对转换得到的c语言代码文件进行验证工具兼容处理；
9、s106，利用c程序的模型检查器cbmc对c语言代码文件进行验证并生成验证结果；
10、步骤s101之前还包括将汇编程序、高级语言内联汇编语言程序或高级语言程序形式的源代码文件编译为elf二进制文件；所述将汇编程序、高级语言内联汇编语言程序或高级语言程序形式的源代码文件编译为elf二进制文件时，包括进行断言语句的处理：
11、s201，获取输入的源代码文件；
12、s202，按行读取源代码文件，若读取结束，则判定断言语句处理完毕，退出；否则，跳转步骤s203；
13、s203，判断该行是否存在未被注释的断言语句，若存在未被注释的断言语句，则跳转步骤s204；否则，跳转步骤s202继续按行读取源代码文件；
14、s204，记录该行中断言语句的序号i，声明第i个全局变量assert_reti为0，采用if语句替换assert语句，且在if语句中设置第i个全局变量assert_reti的值1以表明assert语句中的条件表达式成立。
15、可选地，步骤s101之后、s102之前还包括针对elf二进制文件形式的源文件进行全局变量处理的下述步骤：
16、针对输入的elf二进制文件形式的源文件，声明一个结构体数组gv，用于存储elf二进制文件形式的源文件的全局变量信息，包括变量名、变量值和变量地址；
17、逐一解析并读取elf二进制文件形式的源文件中的全局变量，若成功读取到elf二进制文件形式的源文件中的全局变量则流程继续；否则若全局变量全部读取完毕，则结束读取并将全局变量的名称和内存地址信息保存到结构体数组gv中。
18、可选地，步骤s102中将输入的源文件利用elf文件处理器进行解析并加载至模拟器时，模拟器的内存分配区域包括模拟器保留区域、elf文件程序段、elf文件栈空间和elf文件堆空间，且将输入的源文件利用elf文件处理器进行解析获得的数据段.data、代码段.text和只读数据段.rodata分别加载在elf文件程序段中，且在虚拟地址空间中的位置通过基址base+入口地址entry的方式确定，其中基址base为表示elf文件操作的起始空间的基址，入口地址entry为数据段.data、代码段.text和只读数据段.rodata的段起始点相对于文件开头的偏移量。
19、可选地，步骤s103中利用risc-v指令解码器从内存中提取相应长度的二进制指令，并依据risc-v的编码规则解码得到具体的汇编指令及其操作数包括：
20、s301，从程序计数器pc获取指令字并将其存储在指令寄存器中准备进行解码；
21、s302，从指令寄存器中提取指令字的操作码opcode，识别指令格式；
22、s303，根据指令字的操作码opcode确定指令类型；
23、s304，根据指令类型提取指令的字段，包括功能码、源寄存器、目标寄存器和立即数；
24、s305，根据操作码opcode和提取的字段得到具体的汇编指令及其操作数。
25、可选地，步骤s104中利用汇编转c转换器将解码得到的汇编指令及其操作数转换为c语言代码文件包括：
26、s401，设置程序计数器pc指向基址base+入口地址entry的位置准备读取汇编指令，其中基址base为表示elf文件操作的起始空间的基址，入口地址entry为数据段.data、代码段.text和只读数据段.rodata的段起始点相对于文件开头的偏移量；
27、s402，若程序计数器pc的值为0，则判定转换完毕，跳转步骤s105；否则，从程序计数器pc指向的地址读取16位或32位的二进制指令，其中读取16位或32位的数据长度是根据指令是否为压缩指令来确定的；
28、s403，将读取到的16位或32位的二进制指令运用risc-v指令解码器进行解码，得到具体的汇编指令及其操作数；
29、s404，检查是否到达程序的结尾，如果到达程序的结尾，则流程结束并跳转步骤s105；否则，跳转步骤s405；
30、s405，判断解码出的汇编指令是否是jalr或ecall指令，如果是jalr或ecall指令则跳转步骤s406；否则，汇编转c转换器将汇编指令及其操作数转换为c语言代码并追加到缓冲字符串中通过模拟器模拟执行，将程序计数器pc的值加上2或4使其指向下一条指令，跳转步骤s402；
31、s406，判断解码出的汇编指令是否是ecall指令，若是ecall指令，则跳转步骤s407；否则，判定为真实机器的处理系统调用，将系统调用函数追加到缓冲字符串中，将程序计数器pc的值加上2或4使其指向下一条指令，跳转步骤s402；
32、s407，追加c函数结束字符串到缓冲字符串中；
33、s408，将缓冲字符串输出到c语言代码文件中；清空缓冲字符串，写出初始字符串，将程序计数器pc的值加上2或4使其指向下一条指令，跳转步骤s402。
34、可选地，步骤s405中汇编转c转换器将汇编指令及其操作数转换为c语言代码包括：
35、s501，初始化数据结构，所述数据结构包括寄存器结构体和用于存储全局变量地址和值的结构体数组addr_val；
36、s502，识别汇编指令的类型，所述汇编指令的类型存储、加载、运算、直接跳转、间接跳转或者系统调用；
37、s503，基于汇编指令的类型将汇编指令及其操作数转换为c语言代码：
38、若汇编指令的类型为存储指令，将汇编指令及其操作数转换为c语言代码包括：步骤a：读取汇编指令的指令操作的目标地址；步骤b：如果目标地址位于栈空间内，则将汇编指令及其操作数转换为数据存储操作的c语言代码，结束并退出；否则跳转步骤c；步骤c：如果目标地址为全局或静态变量的存储地址，则将汇编指令及其操作数转换为数据存储操作的c语言代码，结束并退出；否则跳转步骤d；步骤d：判断目标地址是否通过参数寄存器传递，如果是，进行数据存储操作，结束并退出；否则抛出异常；所述数据存储操作用于向地址指向的内存中写入对应的数据，所述抛出异常用于避免非法内存访问导致的运行时错误；
39、若汇编指令的类型为加载指令，将汇编指令及其操作数转换为c语言代码包括：步骤a：读取汇编指令的指令操作的目标地址；步骤b：如果目标地址位于栈空间内，则将汇编指令及其操作数转换为数据加载操作的c语言代码，结束并退出；否则跳转步骤c；步骤c：如果目标地址为全局或静态变量的存储地址，则将汇编指令及其操作数转换为从全局变量加载数据的c语言代码，结束并退出；否则跳转步骤d；步骤d：判断目标地址是否通过参数寄存器传递，如果是，进行数据存储操作，结束并退出；否则抛出异常；
40、若汇编指令的类型为直接跳转指令jal，所述直接跳转指令jal用于实现函数调用，通过jal ra,offset的命令形式跳转到目标地址，其中offset为目标地址偏移量，并将返回地址保存在返回地址寄存器ra中；将汇编指令及其操作数转换为c语言代码包括：步骤a：读取直接跳转指令jal的操作寄存器；步骤b：判断直接跳转指令jal的操作寄存器是否为返回地址寄存器ra，若为返回地址寄存器ra，则计算并记录返回地址并保存到模拟返回地址寄存器ra的寄存器中，将返回地址压入函数调用栈以便在函数返回时使用；否则跳转步骤c；步骤c：将程序计数器pc的值加上目标地址偏移量offset，将直接跳转指令jal的跳转逻辑转换为c语言中的goto target_address语句；
41、若汇编指令的类型为间接跳转指令jalr，所述间接跳转指令jalr用于通过伪指令ret实现函数返回，将汇编指令及其操作数转换为c语言代码包括：步骤a：读取间接跳转指令jalr的操作字段，包括寄存器和立即数；步骤b：判断间接跳转指令jalr是否为函数返回指令，若为函数返回指令则从函数调用栈中出栈最近一次保存的返回地址，将出栈的地址更新到模拟器中的ra寄存器变量中，将返回操作转换为c语言中的goto ra语句；否则，计算跳转地址，所述跳转地址为基址寄存器加上一个偏移量，并保存在临时变量target_address中，生成c语言中的goto target_address语句执行实际的跳转到临时变量target_address的地址；
42、若汇编指令的类型为运算或者系统调用，则直接根据转换关系表将运算或者系统调用转换为c语言代码。
43、可选地，步骤s106中利用验证逻辑生成器对转换得到的c语言代码文件进行验证工具兼容处理包括：
44、s601，对预处理阶段识别并记录的全局变量进行声明和初始化，在c文件的开始部分声明并赋值全局变量，确保其能被验证工具正确识别和使用；
45、s602，声明并初始化基本内存资源和变量，包括通用寄存器和栈空间，初始化栈指针寄存器指向栈空间末端地址，将所有其他寄存器初始化为零；
46、s603，将汇编转c转换器转换后的c程序封装成一个无返回值类型的函数，并添加至此；
47、s604，在转换后的c代码中添加主函数main，调用已转换的函数；
48、s605，在主函数main中插入断言语句，条件表达式为断言语句assert对应的全局变量值是否为1，确保断言语句assert的数量和汇编文件中的一致。
49、此外，本发明还提供一种面向risc-v架构的二进制程序验证系统，包括相互连接的微处理器和存储器，所述微处理器被编程或配置以执行所述面向risc-v架构的二进制程序验证方法。
50、此外，本发明还提供一种计算机可读存储介质，该计算机可读存储介质中存储有计算机程序或指令，该计算机程序或指令被编程或配置以通过处理器执行所述面向risc-v架构的二进制程序验证方法。
51、此外，本发明还提供一种计算机程序产品，包括计算机程序或指令，该计算机程序或指令被编程或配置以通过处理器执行所述面向risc-v架构的二进制程序验证方法。
52、和现有技术相比，本发明主要具有下述优点：
53、1、本发明包括将输入的源文件利用elf文件处理器进行解析并加载至模拟器并模拟执行；利用risc-v指令解码器从内存中提取相应长度的二进制指令解码得到具体的汇编指令及其操作数；利用汇编转c转换器将解码得到的汇编指令及其操作数转换为c语言代码文件；利用验证逻辑生成器对转换得到的c语言代码文件进行验证工具兼容处理；利用c程序的模型检查器cbmc对c语言代码文件进行验证并生成验证结果，本发明能够通过高效、全面且自动化的方式验证risc-v汇编程序和二进制文件的正确性，提高软件在实际部署前的可靠性和安全性。
54、2、本发明能够支持c语言、risc-v架构汇编语言、c与汇编混源代码，以及elf二进制文件的验证。理论上还可以通过简单的扩展来支持更多编译型语言的程序验证。例如通过增加特定的语言解析器和适配器，工具可以轻松地适应如rust、fortran等其他编程语言。
1.一种面向risc-v架构的二进制程序验证方法，其特征在于，包括下述步骤：
2.根据权利要求1所述的面向risc-v架构的二进制程序验证方法，其特征在于，步骤s101之后、s102之前还包括针对elf二进制文件形式的源文件进行全局变量处理的下述步骤：
3.根据权利要求1所述的面向risc-v架构的二进制程序验证方法，其特征在于，步骤s102中将输入的源文件利用elf文件处理器进行解析并加载至模拟器时，模拟器的内存分配区域包括模拟器保留区域、elf文件程序段、elf文件栈空间和elf文件堆空间，且将输入的源文件利用elf文件处理器进行解析获得的数据段.data、代码段.text和只读数据段.rodata分别加载在elf文件程序段中，且在虚拟地址空间中的位置通过基址base+入口地址entry的方式确定，其中基址base为表示elf文件操作的起始空间的基址，入口地址entry为数据段.data、代码段.text和只读数据段.rodata的段起始点相对于文件开头的偏移量。
4.根据权利要求1所述的面向risc-v架构的二进制程序验证方法，其特征在于，步骤s103中利用risc-v指令解码器从内存中提取相应长度的二进制指令，并依据risc-v的编码规则解码得到具体的汇编指令及其操作数包括：
5.根据权利要求1所述的面向risc-v架构的二进制程序验证方法，其特征在于，步骤s104中利用汇编转c转换器将解码得到的汇编指令及其操作数转换为c语言代码文件包括：
6.根据权利要求5所述的面向risc-v架构的二进制程序验证方法，其特征在于，步骤s405中汇编转c转换器将汇编指令及其操作数转换为c语言代码包括：
7.根据权利要求1所述的面向risc-v架构的二进制程序验证方法，其特征在于，步骤s106中利用验证逻辑生成器对转换得到的c语言代码文件进行验证工具兼容处理包括：
8.一种面向risc-v架构的二进制程序验证系统，包括相互连接的微处理器和存储器，其特征在于，所述微处理器被编程或配置以执行权利要求1～5中任意一项所述面向risc-v架构的二进制程序验证方法。
9.一种计算机可读存储介质，该计算机可读存储介质中存储有计算机程序或指令，其特征在于，该计算机程序或指令被编程或配置以通过处理器执行权利要求1～5中任意一项所述面向risc-v架构的二进制程序验证方法。
10.一种计算机程序产品，包括计算机程序或指令，其特征在于，该计算机程序或指令被编程或配置以通过处理器执行权利要求1～5中任意一项所述面向risc-v架构的二进制程序验证方法。
