XBIL - A hardware resource oriented binary intermediate language

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

3 Scopus citations

Abstract

In the modern world, program analysis and verification on binary code have been widely used. While on embedded system, a variety of platforms make the binary analyzing and verifying work bump up against difficulties. But the problem of expressing instruction cycle time, interrupt and pipeline mechanism in binary intermediate language has not been addressed. In this paper, we show how we attack this problem by introducing a hardware resource oriented binary intermediate language - xBIL, which can be used to present the instructions with instruction cycle time and interrupt properties reserved. We also propose the execution algorithm and semantics of this language. xBIL has been applied on the analysis of a commercial automotive operating system which is used on over 1.38M cars in China and successfully found several bugs.

Original languageEnglish
Title of host publicationProceedings - 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems, ICECCS 2012
PublisherIEEE Computer Society
Pages211-219
Number of pages9
ISBN (Print)9782954181004
DOIs
StatePublished - 2012
Event17th International Conference on Engineering of Complex Computer Systems, ICECCS 2012 - Paris, France
Duration: 18 Jul 201220 Jul 2012

Publication series

NameProceedings - 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems, ICECCS 2012

Conference

Conference17th International Conference on Engineering of Complex Computer Systems, ICECCS 2012
Country/TerritoryFrance
CityParis
Period18/07/1220/07/12

Keywords

  • Binary Intermediate Language
  • Pipeline Analysis
  • Semantics

Fingerprint

Dive into the research topics of 'XBIL - A hardware resource oriented binary intermediate language'. Together they form a unique fingerprint.

Cite this