一种用于漏洞检测的符号执行系统的约束求解方法

本发明公开了一种用于漏洞检测的符号执行系统的约束求解方法，包括获取源程序并利用构建的符号执行系统转换为路径语言的中间语言程序；将得到的中间语言程序转换成使用符号值及其表达式表示的模拟执行程序和可约束求解的一阶逻辑公式；对约束的一阶逻辑公式进行布尔可满足性求解，用以根据是否存在可满足的解，判断是否存在漏洞。本发明通过构建符号执行系统，对路径语言中中间语言程序进行约束求解，从而解决现有技术中获得约束路径的结构复杂，求解缓慢，效率低下的问题。