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, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 5: Dennis Brylow , Niels Damgaard , Jens Palsberg, Static checking of interrupt-driven software, Proceedings of the 23rd International Conference on Software Engineering, p.47-56, May 12-19, 2001, Toronto, Ontario, Canada
• 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, Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, p.57-70, June 16-18, 1997, Las Vegas, Nevada, United States
• 9: O. Coudert , J. C. Madre, Implicit and incremental computation of primes and essential primes of Boolean functions, Proceedings of the 29th ACM/IEEE conference on Design automation, p.36-39, June 08-12, 1992, Anaheim, California, United States
• 10: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 11: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 12: Saumya Debray , Robert Muth , Matthew Weippert, Alias analysis of executable code, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-24, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268948]
• 13: Matthew B. Dwyer , Lori A. Clarke, A flexible architecture for building data flow analyzers, Proceedings of the 18th international conference on Software engineering, p.554-564, March 25-29, 1996, Berlin, Germany
• 14: J. Engblom, Static Properties of Commercial Embedded Real-Time Programs, and Their Implication for Worst-Case Execution Time Analysis, Proceedings of the Fifth IEEE Real-Time Technology and Applications Symposium, p.46, June 02-04, 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 Programs by Local Decreasing Iteration, Proceedings of the 12th Conference on Foundations of Software Technology and Theoretical Computer Science, p.68-79, December 18-20, 1992
• 19: John L. Hennessy , Thomas Gross, Postpass Code Optimization of Pipeline Constraints, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.3, p.422-448, July 1983 [doi>10.1145/2166.357217]
• 20: Jason Hill , Robert Szewczyk , Alec Woo , Seth Hollar , David Culler , Kristofer Pister, System architecture directions for networked sensors, Proceedings of the ninth international conference on Architectural support for programming languages and operating systems, p.93-104, November 2000, Cambridge, Massachusetts, United States
• 21: Wilson C. Hsieh , Dawson R. Engler , Godmar Back, Reverse-Engineering Instruction Encodings, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.133-145, June 25-30, 2001
• 22: Daniel Kästner, PROPAN: A Retargetable System for Postpass Optimisations and Analyses, Proceedings of the ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems, p.63-80, June 18, 2000
• 23: Stephen Lawton. Eternally yours at 8 bits. Electronic Business, October 2002.
• 24: Sorin Lerner , David Grove , Craig Chambers, Composing dataflow analyses and transformations, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.270-282, January 16-18, 2002, Portland, Oregon
• 25: Jørn Lind-Nielsen. BuDDy--A binary decision diagram package. http://www.itu.dk/research/buddy/.
• 26: Cullen Linn , Saumya Debray, Obfuscation of executable code to improve resistance to static disassembly, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA [doi>10.1145/948109.948149]
• 27: Thomas Lundqvist , Per Stenström, An Integrated Path and Timing Analysis Method based onCycle-Level Symbolic Execution, Real-Time Systems, v.17 n.2-3, p.183-207, Nov. 1999 [doi>10.1023/A:1008138407139]
• 28: Henry Massalin, Superoptimizer: a look at the smallest program, Proceedings of the second international conference on Architectual support for programming languages and operating systems, p.122-126, October 1987, Palo Alto, California, United States
• 29: Antoine Miné, The Octagon Abstract Domain, Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE'01), p.310, October 02-05, 2001
• 30: Norman Ramsey , Jack W. Davidson, Machine Descriptions to Build Tools for Embedded Systems, Proceedings of the ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems, p.176-192, June 01, 1998
• 31: Rahul Razdan , Michael D. Smith, A high-performance microarchitecture with hardware-programmable functional units, Proceedings of the 27th annual international symposium on Microarchitecture, p.172-180, November 30-December 02, 1994, San Jose, California, United States [doi>10.1145/192724.192749]
• 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, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-13, January 14-16, 2004, Venice, Italy
• 35: Simulavr: An AVR simulator. http://savannah.nongnu.org/projects/simulavr.
• 36: Mark Stephenson , Jonathan Babb , Saman Amarasinghe, Bidwidth analysis with application to silicon compilation, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.108-120, June 18-21, 2000, Vancouver, British Columbia, Canada
• 37: G. A. Venkatesh, A framework for construction and evaluation of high-level specifications for program analysis techniques, Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation, p.1-12, June 19-23, 1989, Portland, Oregon, United States
• 38: Robert Wahbe , Steven Lucco , Thomas E. Anderson , Susan L. Graham, Efficient software-based fault isolation, Proceedings of the fourteenth ACM symposium on Operating systems principles, p.203-216, December 05-08, 1993, Asheville, North Carolina, United States
• 39: Zhichen Xu , Barton P. Miller , Thomas Reps, Safety checking of machine code, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.70-82, June 18-21, 2000, Vancouver, British Columbia, Canada
• 40: Kwangkeun Yi , Williams Ludwell Harrison, III, Automatic generation and management of interprocedural program analyses, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.246-259, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158642]
• 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

Primary Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Languages, Reliability, Verification

Keywords:
abstract interpretation, object code, program verification, static analysis