Static analysis of device drivers
Static analysis of device drivers
复制标题
设备驱动程序的静态分析
DOI：
10.1145/2103799.2103809
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Amani S
中科院分区：
文献类型：
--
作者：
Amani S
我们认为，当前操作系统强制实施的设备驱动程序体系结构使关于驱动程序行为的手动和自动推理都变得复杂。特别是，它使得静态验证驱动程序是否正确地与内核的其余部分交互变得困难，在某些情况下是不可能的。这一限制不能仅通过更好的核查工具来解决。我们认为，静态驱动程序验证有效性的质的提高必须依赖于改进的驱动程序体系结构，从而产生更容易编写、理解和验证的驱动程序。为了支持我们的说法，我们提出了一种称为主动驱动程序的设备驱动程序体系结构，它满足了这些要求。我们概述了使用现有的模型检测工具来指定和验证主动驱动协议的方法，并描述了初步的实验结果。
We argue that the device driver architecture enforced by current operating systems complicates both manual and automatic reasoning about driver behaviour. In particular, it makes it hard and in some cases impossible to statically verify that the driver correctly interacts with the rest of the kernel. This limitation cannot be addressed solely via better verification tools. We maintain that qualitative improvement in the effectiveness of static driver verification must rely on an improved driver architecture, leading to drivers that are easier to write, understand, and verify.To support our claims, we present a device driver architecture, called active drivers, that satisfies these requirements. We outline our methodology for specifying and verifying active driver protocols using existing model checking tools and describe initial experimental results.