Precise static analysis of untrusted driver binaries
Precise static analysis of untrusted driver binaries
复制标题
对不受信任的驱动程序二进制文件进行精确的静态分析
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
H. Veith
中科院分区：
文献类型：
--
作者：
Johannes Kinder;H. Veith
当今台式机系统上安装的大多数封闭源驱动程序从未受到正式分析。没有供应商的支持，使这些经常匆忙编写但可以通过静态分析访问的关键程序的唯一方法是直接在二进制层面上工作。在本文中，我们描述了一个完整的体系结构，以对不依赖不符合外部组件（例如拆卸器）的二进制文件进行静态分析。为了精确地计算数据和功能指针而没有任何类型的信息，我们引入了有限的地址跟踪，这是一个针对机器代码量身定制的抽象域，并且对路径敏感，直到可调的界限限制终止。我们在二进制分析平台JAKSTAB中实现了有限的地址跟踪，并将其用于验证几个Windows设备驱动程序的API规格。即使没有关于最先进的方法[1]做出的关于可执行的布局和过程的假设[1]，我们在Windows DDK的一组驱动程序上获得了更精确的结果。由于我们的技术不需要我们自己编译驱动程序，因此我们还提供了分析300多个封闭源驱动程序的结果。
Most closed source drivers installed on desktop systems today have never been exposed to formal analysis. Without vendor support, the only way to make these often hastily written, yet critical programs accessible to static analysis is to directly work at the binary level. In this paper, we describe a full architecture to perform static analysis on binaries that does not rely on unsound external components such as disassemblers. To precisely calculate data and function pointers without any type information, we introduce Bounded Address Tracking, an abstract domain that is tailored towards machine code and is path sensitive up to a tunable bound assuring termination. We implemented Bounded Address Tracking in our binary analysis platform Jakstab and used it to verify API specifications on several Windows device drivers. Even without assumptions about executable layout and procedures as made by state of the art approaches [1], we achieve more precise results on a set of drivers from the Windows DDK. Since our technique does not require us to compile drivers ourselves, we also present results from analyzing over 300 closed source drivers.