Abstract
This paper describes the design and implementation of a language for specifying the semantics of an instruction set, along with a run-time system to support the static analysis of executables written in that instruction set. The work advances the state of the art by creating multiple analysis phases from a specification of the concrete operational semantics of the language to be analyzed.
Supported by ONR under grant N00014-01-1-0796 and by NSF under grants CCF-0540955 and CCF-0524051.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
IA-32 Intel Architecture Software Developer’s Manual, http://developer.intel.com/design/pentiumii/manuals/243191.htm
Amme, W., Braun, P., Zehendner, E., Thomasset, F.: Data dependence analysis of assembly code. In: IFPP 2000 (2000)
Balakrishnan, G.: WYSINWYX: What You See Is Not What You eXecute. PhD thesis, Univ. of Wisc. (2007)
Balakrishnan, G., Gruian, R., Reps, T., Teitelbaum, T.: CodeSurfer/x86—A Platform for Analyzing x86 Executables. In: Bodik, R. (ed.) CC 2005. LNCS, vol. 3443, pp. 250–254. Springer, Heidelberg (2005)
Balakrishnan, G., Reps, T.: Analyzing Memory Accesses in x86 Executables. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol. 2985, pp. 5–23. Springer, Heidelberg (2004)
Balakrishnan, G., Reps, T.: DIVINE: DIscovering Variables IN Executables. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 1–28. Springer, Heidelberg (2007)
Christodorescu, M., Goh, W., Kidd, N.: String analysis for x86 binaries. In: PASTE 2005 (2005)
Cifuentes, C., Fraboulet, A.: Intraprocedural static slicing of binary executables. In: ICSM 1997 (1997)
Cook, T.A., Franzon, P.D., Harcourt, E.A., Miller, T.K.: System-level specification of instruction sets. In: DAC 1993 (1993)
Cooper, K., Kennedy, K.: Interprocedural side-effect analysis in linear time. In: PLDI 1988 (1988)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL 1979 (1979)
De Sutter, B., De Bus, B., De Bosschere, K., Keyngnaert, P., Demoen, B.: On the static analysis of indirect control transfers in binaries. In: PDPTA 2000 (2000)
Debray, S., Muth, R., Weippert, M.: Alias analysis of executable code. In: POPL 1998(1998)
Harcourt, E., Mauney, J., Cook, T.: Functional specification and simulation of instruction set architectures. In: PLC 1994 (1994)
Lim, J., Reps, T.: A system for generating static analyzers for machine instructions. TR-1622, C.S.Dept., Univ. of Wisconsin, Madison, WI (October 2007)
Mauborgne, L., Rival, X.: Trace Partitioning in Abstract Interpretation Based Static Analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005)
Müller-Olm, M., Seidl, H.: Analysis of Modular Arithmetic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 46–60. Springer, Heidelberg (2005)
Pettersson, M.: A term pattern-match compiler inspired by finite automata theory. In: Pfahler, P., Kastens, U. (eds.) CC 1992. LNCS, vol. 641, pp. 258–270. Springer, Heidelberg (1992)
Ramsey, N., Davidson, J.: Specifying instructions’ semantics using λ-RTL (unpublished manuscript, 1999)
Regehr, J., Reid, A., Webb, K.: Eliminating stack overflow by abstract interpretation. In: TECS 2005 (2005)
Reps, T., Balakrishnan, G., Lim, J.: Intermediate-representation recovery from low-level code. In: PEPM 2006 (2006)
Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, Prentice-Hall, Englewood Cliffs (1981)
Wadler, P.: Efficient compilation of pattern-matching. The Impl. of Func. Prog. Lang. (1987)
Zhang, J., Zhao, R., Pang, J.: Parameter and return-value analysis of binary executables. In: COMPSAC 2007 (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lim, J., Reps, T. (2008). A System for Generating Static Analyzers for Machine Instructions. In: Hendren, L. (eds) Compiler Construction. CC 2008. Lecture Notes in Computer Science, vol 4959. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78791-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-78791-4_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78790-7
Online ISBN: 978-3-540-78791-4
eBook Packages: Computer ScienceComputer Science (R0)