Paris, France France
July 18, 2012 to July 20, 2012
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.
Hardware, Binary codes, Registers, Semantics, Pipelines, Program processors, Context, Semantics, Binary Intermediate Language, Pipeline Analysis
Jianqi Shi, Longfei Zhu, Huixing Fang, Jian Guo, Huibiao Zhu, Xin Ye, "xBIL -- A Hardware Resource Oriented Binary Intermediate Language", ICECCS, 2012, Engineering of Complex Computer Systems, IEEE International Conference on, Engineering of Complex Computer Systems, IEEE International Conference on 2012, pp. 211-219, doi:10.1109/ICECCS.2012.44