Kinder, Johannes ; Veith, Helmut
Hrsg.: Bloem, Roderick ; Sharygina, Natasha (2010)
Precise Static Analysis of Untrusted Driver Binaries.
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (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.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2010 |
| Herausgeber: | Bloem, Roderick ; Sharygina, Natasha |
| Autor(en): | Kinder, Johannes ; Veith, Helmut |
| Art des Eintrags: | Bibliographie |
| Titel: | Precise Static Analysis of Untrusted Driver Binaries |
| Sprache: | Deutsch |
| Publikationsjahr: | Oktober 2010 |
| Verlag: | IEEE Computer Society |
| Buchtitel: | Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010) |
| Zugehörige Links: | |
| Kurzbeschreibung (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. |
| Freie Schlagworte: | Secure Services |
| ID-Nummer: | TUD-CS-2010-1881 |
| Fachbereich(e)/-gebiet(e): | LOEWE > LOEWE-Zentren > CASED – Center for Advanced Security Research Darmstadt LOEWE > LOEWE-Zentren LOEWE |
| Hinterlegungsdatum: | 30 Dez 2016 20:23 |
| Letzte Änderung: | 30 Mai 2018 12:53 |
| PPN: | |
| Zugehörige Links: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum