TU Darmstadt / ULB / TUbiblio

Precise Static Analysis of Untrusted Driver Binaries

Kinder, Johannes and Veith, Helmut Bloem, Roderick and Sharygina, Natasha (eds.) (2010):
Precise Static Analysis of Untrusted Driver Binaries.
In: Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010), IEEE Computer Society, pp. 43-50, [Conference or Workshop Item]

Abstract

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, 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.

Item Type: Conference or Workshop Item
Erschienen: 2010
Editors: Bloem, Roderick and Sharygina, Natasha
Creators: Kinder, Johannes and Veith, Helmut
Title: Precise Static Analysis of Untrusted Driver Binaries
Language: German
Abstract:

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, 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.

Title of Book: Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010)
Publisher: IEEE Computer Society
Uncontrolled Keywords: Secure Services
Divisions: LOEWE > LOEWE-Zentren > CASED – Center for Advanced Security Research Darmstadt
LOEWE > LOEWE-Zentren
LOEWE
Date Deposited: 30 Dec 2016 20:23
Identification Number: TUD-CS-2010-1881
Related URLs:
Export:
Suche nach Titel in: TUfind oder in Google
Send an inquiry Send an inquiry

Options (only for editors)

View Item View Item