题目：基于Dalvik字节码的符号执行技术研究

随着Android系统的流行，Android应用的安全性已经成为威胁产业发展的严峻问题。传统的人工动态分析是一种有效的手段，但是效率较低。随着软件产业的快速发展，应用程序的规模越来越大，人工分析的难度变得越来越大，因此需要一些辅助的自动化分析工具。使用有效的静态和动态恶意应用分析工具，能够自动的处理和分析应用程序信息，生成恶意应用的行为报告，可以辅助安全专家快速了解恶意应用的行为，大大的提高安全分析的效率，并且节约大量的人力和时间成本。

基于符号执行的程序分析技术，在多个软件安全分析方向有着重要应用，诸如权限泄露检测、安全测试和触发行为分析等。目前国内外对符号执行技术也有很多深入的研究，并且已经开发出了一些针对C/Java等语言的符号执行工具。但是符号执行技术还存在一些难题尚待解决，诸如效率不高和循环处理不够完善等，同时目前业界还没有可用的针对Android虚拟机Dalvik字节码的符号执行系统。

本文研究了Android虚拟机Dalvik的工作机制及其字节码的语法规则，基于开源的Android应用安全分析工具Androguard，对应用的虚拟机字节码进行处理和分析，在此基础上构建基于语句的程序控制流图，通过符号执行技术对程序的行为进行分析，获得程序的路径条件，之后通过约束求解器找到特定行为的触发条件。通过对以上技术的研究，本文实现了一个基于符号执行技术的自动化应用分析系统，该系统能在不需要应用源码的情况下，分析应用的路径执行信息，并给出不同路径条件的解。最后，本文通过实验验证了该符号执行系统功能的正确性，为后续实现更为完善的自动化应用分析工具来辅助人工进行安全分析奠定了技术基础。