2014SyScan360——程序分析及约束求解器

　　2014年7月16日，由SyScan主办，360公司承办的SyScan360国际前瞻信息安全会议隆重召开。本次会议上汇集了来自美、意、西、葡等9个地区的18名顶级安全专家，向与会者分享安全领域最新的科研成果，议题涵盖Window、ios、Android系统安全，汽车攻击、云服务攻击等诸多领域。

　　来自COSEINC的资深安全研究员的Edgar Barbosa为大家带了关于《程序分析及约束求解器》的主题演讲。Edgar Barbosa曾参与开发了虚机rootkit“Blue Pill”，并发表过几篇论文。他擅长于内核开发、rootkit研究、逆向工程、硬件虚拟化及程序分析。

　　Edgar表示，程序分析更多的是要专注于特定的目标，即是要找到漏洞和Bug，逆向工程主要的工作就是要做漏洞的挖掘，结合逆向工程可以提取协议和格式的信息，其包括协议和文件解析器。

　　在演讲中，Edgar首先针对漏洞挖掘时采用模糊测试用的Fuzzing 进行了基础性的讲解。他提到，Fuzzing有六个类别，一个是找到目标，二是生成数据，将谋划的数据输入执行程序，然后监视它的异常，是不是能够被跟踪，再验证它的可用性。比如我们想要创造一个FTP服务器的Fuzzing需要产生一些随机的数据，我们要了解FTP协议，而且它也需要一些其他的应用。

　　然而，Edgar表示，虽然模糊测试仍然是漏洞挖掘的有效手段，它能产生很多崩溃，这些崩溃作为分析问题的起点，用来确定漏洞的可利用性。但是对于某些具体的产品来说，Fuzzing并不是很有用。所以实现漏洞挖掘的自动化成为必要，自动化的实现可以让用户不必学习内部的知识，不必了解数据结构，不必了解新的格式和协议。对此，Edgar认为，实现漏洞挖掘自动化需要做到：

　　理解输入数据时如何影响软件的执行；

　　审计程序函数不需要包括协议和文件格式的任何先验知识；

　　报告错误并立即分析出错根源；

　　不产生误报；

　　自动增加和程序路径的覆盖。

　　那么，如何才能做到以上几个方面？Edgar认为，这需要把程序分析的问题能够把它转换成为约束求解器的问题来解决，然后让约束求解器帮助解决问题。什么是约束求解器？约束求解器和约束编程的概念是一样的，约束编程实际上是一个最接近的一种计算机科学的方法，它可以接近于编程方面的圣杯，它可以解决用户面临的问题。

　　Edgar说自己最喜欢的强大的SMT求解器是微软的Z3，它能够管理核心机管理的核心代码的求解性，而且Z3在微软的产品当中发现了好几个漏洞。它是一个自动化的、可满足性校验的工具，对于所有的东西不需要理解，除非你想自己创建一个SMT的求解器，否则你不需要知道，而且在Linux、MAc、Windows上都可以用。

　　最后，Edgar展示了如何将x86汇编码翻译成中间语言和SMT公式，并就在程序分析时使用求解器的利与弊，求解器与污点数据分析的关系进行了讨论。