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}
, png = {p021-regehr.png}
, publisher = {ACM}
, title = {H{O}IS{T}: a system for automatically deriving static analyzers for
embedded systems}
, year = {2004}
}
