Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Precise static analysis of untrusted driver binaries
 
conference paper

Precise static analysis of untrusted driver binaries

Kinder, Johannes  
•
Veith, Helmut
2010
Proceedings of the 10th International Conference on Formal Methods in Computer Aided Design (FMCAD 2010)
10th International Conference on Formal Methods in Computer Aided Design

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.

  • Files
  • Details
  • Metrics
Type
conference paper
Author(s)
Kinder, Johannes  
Veith, Helmut
Date Issued

2010

Publisher

IEEE

Published in
Proceedings of the 10th International Conference on Formal Methods in Computer Aided Design (FMCAD 2010)
Start page

43

End page

50

Subjects

static analysis

•

device drivers

•

binaries

Editorial or Peer reviewed

REVIEWED

Written at

OTHER

EPFL units
IIF  
Event nameEvent placeEvent date
10th International Conference on Formal Methods in Computer Aided Design

Lugano, Switzerland

October 20-23, 2010

Available on Infoscience
July 13, 2011
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/69554
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés