HOIST: a system for automatically deriving static analyzers for embedded systems
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 im-precise. 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 func-tions that are ready to be linked into an abstract interpreter. We demonstrate that Hoist generates abstract operations that are cor-rect, having been extensively tested, sufficiently fast, and substan-tially 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.
References
[1]
Atemu: A sensor network emulator/simulator/debugger. Center for Satellite and Hybrid Communication Networks, University of Maryland, 2004. http://www.cshcn.umd.edu/research/atemu/.]]
[2]
Atmel, Inc. ATmega128 datasheet, 2002. http: //www.atmel.com/atmel/acrobat/doc2467.pdf.]]
[3]
Gogul Balakrishnan and Thomas Reps. Analyzing memory accesses in x86 executables. In Proc. of the Intl. Conf. on Compiler Construction (CC), Barcelona, Spain, April 2004.]]
[4]
Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 35(8):677--691, August 1986.]]
[5]
Dennis Brylow, Niels Damgaard, and Jens Palsberg. Static checking of interrupt-driven software. In Proc. of the 23rd Intl. Conf. on Software Engineering (ICSE), pages 47--56, Toronto, Canada, May 2001.]]
[6]
Mihai Christodorescu and Somesh Jha. Static analysis of executables to detect malicious patterns. In Proc. of the 12th USENIX Security Symp., Washington, DC, August 2003.]]
[7]
Cristina Cifuentes. Interprocedural data flow decompilation. Journal of Programming Languages, 4(2):77--99, 1996.]]
[8]
Christian S. Collberg. Reverse interpretation + mutation analysis = automatic retargeting. In Proc. of the ACM SIGPLAN 1997 Conf. on Programming Language Design and Implementation (PLDI), Las Vegas, NV, June 1997.]]
[9]
Olivier Coudert and Jean Christophe Madre. Implicit and incremental computation of primes and essential primes of boolean functions. In Proc. of the Design Automation Conf. (DAC), pages 36--39, Anaheim, CA, June 1992.]]
[10]
Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of the 4th Symp. on Principles of Programming Languages (POPL), pages 238--252, Los Angeles, CA, January 1977.]]
[11]
Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. of the 5th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL), pages 84--97, Tucson, AZ, January 1978.]]
[12]
Saumya Debray, Robert Muth, and Matthew Weippert. Alias analysis of executable code. In Proc. of the 25th Symp. on Principles of Programming Languages (POPL), pages 12--24, San Diego, CA, January 1998.]]
[13]
Matthew B. Dwyer and Lori A. Clarke. A flexible architecture for building data flow analyzers. In Proc. of the 18th Intl. Conf. on Software Engineering (ICSE), pages 554--564, Berlin, Germany, March 1996.]]
[14]
Jakob Engblom. Static properties of commercial embedded real-time programs, and their implication for worst-case execution time analysis. In Proc. of the 5th IEEE Real-Time Technology and Applications Symp. (RTAS), Vancouver, Canada, June 1999.]]
[15]
Jakob Engblom, Andreas Ermedahl, Mikael Nolin, Jan Gustafsson, and Hans Hansson. Worst-case execution-time analysis for embedded real-time systems. Journal of Software Tool and Transfer Technology (STTT), 4(4):437--455, August 2003.]]
[16]
Nicolas Fritz, Daniel Kästner, and Florian Martin. Automatically generating value analyzers for assembly code. In Proc. of the 2003 Workshop on Compilers and Tools for Constrained Embedded Systems (CTCES), San Jose, CA, October 2003.]]
[17]
John K. Gough and Herbert Klaeren. Eliminating range checks using static single assignment form. In Proc. of the 19th Australian Computer Science Conf., Melbourne, Australia, January 1996.]]
[18]
Philippe Granger. Improving the results of static analyses of programs by locally decreasing iterations. In Proc. of the Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 68--79, New Delhi, India, December 1992.]]
[19]
John L. Hennessy and Thomas Gross. Postpass code optimization of pipeline constraints. ACM Transactions on Programming Languages and Systems (TOPLAS), 5(3):422--448, July 1983.]]
[20]
Jason Hill, Robert Szewczyk, Alec Woo, Seth Hollar, David Culler, and Kristofer Pister. System architecture directions for networked sensors. In Proc. of the 9th Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 93--104, Cambridge, MA, November 2000.]]
[21]
Wilson C. Hsieh, Dawson R. Engler, and Godmar Back. Reverse-engineering instruction encodings. In Proc. of the 2001 USENIX Annual Technical Conf., pages 133--146, June 2001.]]
[22]
Daniel Kästner. PROPAN: A retargetable system for postpass optimizations and analyses. In Proc. of the ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems (LCTES), Vancouver, Canada, June 2000.]]
[23]
Stephen Lawton. Eternally yours at 8 bits. Electronic Business, October 2002.]]
[24]
Sorin Lerner, David Grove, and Craig Chambers. Composing dataflow analyses and transformations. In Proc. of the 29th Symp. on Principles of Programming Languages (POPL), Portland, OR, January 2002.]]
[25]
Jørn Lind-Nielsen. BuDDy--A binary decision diagram package. http://www.itu.dk/research/buddy/.]]
[26]
Cullen Linn and Saumya Debray. Obfuscation of executable code to improve resistance to static disassembly. In Proc. of the 10th ACM Conf. on Computer and Communications Security (CCS), Washington, DC, October 2003.]]
[27]
Thomas Lundqvist and Per Stenström. An integrated path and timing analysis method based on cycle-level symbolic execution. Journal of Real-Time Systems, 17(2/3):183--207, November 1999.]]
[28]
Henry Massalin. Superoptimizer: A look at the smallest program. In Proc. of the 2nd Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 122--126, Palo Alto, CA, October 1987.]]
[29]
Antoine Miné. The octagon abstract domain. In Proc. of the 8th Working Conference on Reverse Engineering (WCRE), Stuttgart, Germany, October 2001.]]
[30]
Norman Ramsey and Jack W. Davidson. Machine descriptions to build tools for embedded systems. In Proc. of the 1998 ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems (LCTES), pages 176--192, Montreal, Canada, June 1998.]]
[31]
Rahul Razdan and Michael D. Smith. A high-performance microarchitecture with hardware-programmable functional units. In Proc. of the 27th Intl. Symp. on Microarchitecture (MICRO), pages 172--180, San Jose, CA, November 1994.]]
[32]
John Regehr, Alastair Reid, and Kirk Webb. Eliminating stack overflow by abstract interpretation. In Proc. of the 3rd Intl. Conf. on Embedded Software (EMSOFT), pages 306--322, Philadelphia, PA, October 2003.]]
[33]
Thomas Reps, Mooly Sagiv, and Greta Yorsh. Symbolic implementation of the best transformer. In Proc. of the 5th Intl. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI), Venice, Italy, January 2004.]]
[34]
Xavier Rival. Symbolic transfer function-based approaches to certified compilation. In Proc. of the 31st Symp. on Principles of Programming Languages (POPL), Venice, Italy, January 2004.]]
[35]
Simulavr: An AVR simulator. http://savannah.nongnu.org/projects/simulavr.]]
[36]
Mark Stephenson, Jonathan Babb, and Saman Amarasinghe. Bitwidth analysis with application to silicon compilation. In Proc. of the ACM SIGPLAN 2000 Conf. on Programming Language Design and Implementation (PLDI), pages 108--120, Vancouver, Canada, June 2000.]]
[37]
G. A. Venkatesh. A framework for construction and evaluation of high-level specifications for program analysis techniques. In Proc. of the ACM SIGPLAN 1989 Conf. on Programming Language Design and Implementation (PLDI), pages 1--12, Portland, OR, July 1989.]]
[38]
Robert Wahbe, Steven Lucco, Thomas E. Anderson, and Susan L. Graham. Efficient software-based fault isolation. In Proc. of the 14th ACM Symp. on Operating Systems Principles (SOSP), pages 203--216, Asheville, NC, December 1993.]]
[39]
Zhichen Xu, Barton Miller, and Thomas Reps. Safety checking of machine code. In Proc. of the ACM SIGPLAN 2000 Conf. on Programming Language Design and Implementation (PLDI), Vancouver, Canada, June 2000.]]
[40]
Kwangkeun Yi and Williams Ludwell Harrison III. Automatic generation and management of interprocedural program analyses. In Proc. of the 20th Symp. on Principles of Programming Languages (POPL), pages 246--259, Charleston, SC, January 1993.]]
[41]
Greta Yorsh, Thomas Reps, and Mooly Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In Proc. of the 10th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Barcelona, Spain, March 2004.]]
Index Terms
- HOIST: a system for automatically deriving static analyzers for embedded systems
Recommendations
HOIST: a system for automatically deriving static analyzers for embedded systems
ASPLOS '04Embedded 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 ...
HOIST: a system for automatically deriving static analyzers for embedded systems
ASPLOS XI: Proceedings of the 11th international conference on Architectural support for programming languages and operating systemsEmbedded 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 ...
HOIST: a system for automatically deriving static analyzers for embedded systems
ASPLOS 2004Embedded 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 ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2004296 pages
Copyright © 2004 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 07 October 2004
Published in SIGPLAN Volume 39, Issue 11
Check for updates
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations36Total Citations
- 735Total Downloads
- Downloads (Last 12 months)10
- Downloads (Last 6 weeks)0
Reflects downloads up to 18 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in