1.一种基于Go语言可执行形式化语义的程序漏洞分析方法，其特征在于，包括：

S1：将Go语言的官方拓展的巴科斯范式语法格式GO[EBNF]转换为K框架可支持的BNF语法格式GO[BNF]；

S2：根据GO[BNF]和Go语言的特点，应用K框架，基于重写逻辑，描述Go语言的可执行语义GO[KS]，包括语法、配置和规则，GO[KS]包含基本语义和并发语义，其中基本语义涵盖Go语言的基本类型定义、基本表达式和基本语句，并发语义包含基于信道实现数据读写；

S3：采用基于测试用例的方法分析GO[KS]的正确性，分别在K框架和IntelliJ IDEA工具中单个执行测试用例，通过比较每个测试用例的结果的一致性分析GO[KS]的正确性；

S4：应用Go语言的可执行语义GO[KS]，基于K框架，对Go程序进行符号执行分析，查找程序漏洞；

步骤S3包括：

基于K框架编译GO[KS]；

对GO[KS]的每个语义规则从官方测试套件中选择合适的测试用例，基于K框架批量运行测试用例，检查是否全部涵盖GO[KS]，如果没有，则开发新的测试用例，实现测试用例全部涵盖GO[KS]，形成一个语义覆盖率为100％的测试集；

通过比较每个测试用例的结果的一致性来分析语义的正确性，具体为：基于语义覆盖率为100％的测试集中的测试用例，分别在K框架和工具IntelliJ IDEA中单个运行测试集中的测试用例，对在K框架执行的结果和在工具IntelliJ运行的程序结果进行比较分析，验证GO[KS]正确性，若每个测试用例的运行结果都一致，则表示GO[KS]正确，否则不正确。

2.如权利要求1所述的基于Go语言可执行形式化语义的程序漏洞分析方法，其特征在于，步骤S2中Go语言的可执行语义GO[KS]的语法，是基于K框架定义的，GO[KS]的配置是基于K框架使用格单元表示的，用于描述Go程序的状态，不同的格单元用于描述Go程序不同的状态信息，格单元包含全局配置格单元、协程配置格单元、信道配置格单元，全局配置格单元包括用于表示程序计算的格单元、用于存储全局变量的格单元；协程配置格单元包括用于表示协程的计算的格单元、用于表示协程唯一标志的格单元；信道配置格单元包括用于表示信道唯一标志的格单元、用于表示信道操作次数的格单元、用于表示信道类型的格单元、用于表示信道状态的格单元以及用于表示信道队列的格单元。

3.如权利要求1所述的基于Go语言可执行形式化语义的程序漏洞分析方法，其特征在于，步骤S2中Go语言的可执行语义GO[KS]的规则，是基于K框架应用重写逻辑对Go程序的状态转换关系进行重写后得到，重写内容包含格单元内的信息转换前和转换后的信息。

4.如权利要求1所述的基于Go语言可执行形式化语义的程序漏洞分析方法，其特征在于，步骤S2的基本语义包含基本类型定义、基本表达式和基本语句，其中，变量声明，包含无类型声明、有类型声明、无类型声明且赋值、有类型声明且赋值、批量声明、批量声明且赋值；

数组声明，针对有类型的一维数组声明定义；

函数声明和定义，针对带参数的函数声明，包括有类型返回和无类型返回；

结构体定义，结构体包含结构体内参数和参数类型，参数类型包含整型、字符型、布尔型；

基本表达式，包含简单运算、复杂运算、逻辑运算和变量自增自减；

基本语句，一部分在是基本类型定义的基础上得到的基本语句，包含变量赋值，数组赋值，一部分是一般语句，包含函数调用、return语句、if语句、for语句、println语句、switch语句、select语句、函数定义、package和import。

5.如权利要求1所述的基于Go语言可执行形式化语义的程序漏洞分析方法，其特征在于，步骤S2的并发语义中基于信道实现数据读写，包含go语句、make语句、信道发送、信道接收、信道关闭，其中，go语句用于描述协程创建的静态语义，make语句用于描述信道创建的静态语义，信道发送、信道接收和信道关闭用于描述信道的状态变化、信道内的数据变化。

6.如权利要求1所述的基于Go语言可执行形式化语义的程序漏洞分析方法，其特征在于，在K框架中编译GO[KS]后，通过K框架启用符号分析模型，对Go程序进行符号执行分析，对程序漏洞进行查找与分析。