Paper Info
Title
xBIL -- A Hardware Resource Oriented Binary Intermediate Language
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.
Year
DOI
Venue
2012
10.1109/ICECCS.2012.44
ICECCS
Keywords
Field
DocType
instruction cycle time,xbil,automotive operating system,commercial automotive operating system,pipeline analysis,hardware resource,binary intermediate language,interrupt property,china,binary code,cars,automobiles,semantics,operating systems (computers),intermediate language,language semantics,work bump verification,pipeline mechanism,embedded system,program analysis,interrupt mechanism,binary analyzing,binary codes,hardware resource oriented binary,execution algorithm,embedded systems,program verification,hardware resource oriented binary intermediate language,pipeline processing,hardware,pipelines,registers
Interrupt,Pipeline transport,Programming language,Computer science,Binary code,Real-time computing,Program analysis,Computer hardware,Instruction cycle,Semantics,Automotive industry,Binary number
Conference
ISBN
Citations 
PageRank 
978-1-4673-2156-3
0
0.34
References 
Authors
0
6
Name
Order
Citations
PageRank
Jianqi Shi15712.50
Longfei Zhu2356.10
Huixing Fang3124.71
Jian Guo494.61
Huibiao Zhu558386.68
Xin Ye600.34