HOIST a system for automatically deriving static analyzers for embedded systems

John Regehr, Alastair Reid
University of Utah
[pdf] [doi]

Proceedings of the 11th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2004)
Boston, MA, USA
October 2004

Abstract

Embedded software must meet conflicting requirements such as be- ing highly reliable, running on resource-constrained platforms, and being developed rapidly. Static program analysis can help meet all of these goals. People developing analyzers for embedded object code face a difficult problem: writing an abstract version of each instruction in the target architecture(s). This is currently done by hand, resulting in abstract operations that are both buggy and imprecise. We have developed Hoist: a novel system that solves these problems by automatically constructing abstract operations using a microprocessor (or simulator) as its own specification. With almost no input from a human, Hoist generates a collection of C functions that are ready to be linked into an abstract interpreter. We demonstrate that Hoist generates abstract operations that are correct, having been extensively tested, sufficiently fast, and substantially more precise than manually written abstract operations. Hoist is currently limited to eight-bit machines due to costs exponential in the word size of the target architecture. It is essential to be able to analyze software running on these small processors: they are important and ubiquitous, with many embedded and safety-critical systems being based on them.

BibTeX

@inproceedings{DBLP:conf/asplos/RegehrR04 , abstract = {Embedded software must meet conflicting requirements such as be- ing highly reliable, running on resource-constrained platforms, and being developed rapidly. Static program analysis can help meet all of these goals. People developing analyzers for embedded object code face a difficult problem: writing an abstract version of each instruction in the target architecture(s). This is currently done by hand, resulting in abstract operations that are both buggy and imprecise. We have developed Hoist: a novel system that solves these problems by automatically constructing abstract operations using a microprocessor (or simulator) as its own specification. With almost no input from a human, Hoist generates a collection of C functions that are ready to be linked into an abstract interpreter. We demonstrate that Hoist generates abstract operations that are correct, having been extensively tested, sufficiently fast, and substantially more precise than manually written abstract operations. Hoist is currently limited to eight-bit machines due to costs exponential in the word size of the target architecture. It is essential to be able to analyze software running on these small processors: they are important and ubiquitous, with many embedded and safety-critical systems being based on them.} , acceptance = {14} , affiliation = {University of Utah} , ar_file = {ASPLOS_04} , ar_shortname = {ASPLOS 04} , author = {John Regehr and Alastair Reid} , booktitle = {Proceedings of the 11th International Conference on Architectural Support for Programming Languages and Operating Systems ({ASPLOS} 2004)} , day = {7-13} , doi = {10.1145/1024393.1024410} , editor = {Shubu Mukherjee and Kathryn S. McKinley} , file = {p021-regehr.pdf} , location = {Boston, MA, USA} , month = {October} , pages = {133--143} , publisher = {ACM} , title = {{H{O}IS{T}:} a system for automatically deriving static analyzers for embedded systems} , year = {2004} }