Abstract
What You See Is Not What You eXecute: computers do not execute source-code programs; they execute machine-code programs that are generated from source code. Not only can the WYSINWYX phenomenon create a mismatch between what a programmer intends and what is actually executed by the processor, it can cause analyses that are performed on source code to fail to detect certain bugs and vulnerabilities. This issue arises regardless of whether one’s favorite approach to assuring that programs behave as desired is based on theorem proving, model checking, or abstract interpretation.
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
PREfast with driver-specific rules, Windows Hardware and Driver Central (WHDC) (October, 2004), http://www.microsoft.com/whdc/devtools/tools/PREfast-drv.mspx
Amme, W., Braun, P., Zehendner, E., Thomasset, F.: Data dependence analysis of assembly code. Int. J. Parallel Proc (2000)
Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Comp. Construct. pp. 5–23 (2004)
Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260–264. Springer, Heidelberg (2001)
Boehm, H.-J.: Threads cannot be implemented as a library. In: PLDI, pp. 261–268 (2005)
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, Springer, Heidelberg (1997)
Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL, pp. 62–73 (2003)
Bush, W., Pincus, J., Sielaff, D.: A static analyzer for finding dynamic programming errors. Software–Practice&Experience 30, 775–802 (2000)
Chen, H., Wagner, D.: MOPS: An infrastructure for examining security properties of software. In: Conf. on Comp. and Commun. Sec, November 2002, pp. 235–244 (2002)
Cifuentes, C., Fraboulet, A.: Intraprocedural static slicing of binary executables. Int. Conf. on Softw. Maint. 188–195 (1997)
CodeSurfer, GrammaTech, Inc. http://www.grammatech.com/products/codesurfer/
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S.: Bandera: Extracting finite-state models from Java source code. In: ICSE (2000)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL (1977)
Coutant, D.S., Meloy, S., Ruscetta, M.: DOC: A practical approach to source-level debugging of globally optimized code. In: PLDI (1988)
Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: PLDI (2002)
Debray, S.K., Muth, R., Weippert, M.: Alias analysis of executable code. In: POPL (1998)
Dwyer, M., Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: ICSE (1999)
Engler, D.R., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. In: Op. Syst. Design and Impl. pp. 1–16 (2000)
Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Elec. Notes in Theor. Comp. Sci. 9 (1997)
Gerth, R.: Formal verification of self modifying code. In: Proc. Int. Conf. for Young Computer Scientists, pp. 305–313 (1991)
Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: POPL, pp. 338–350 (2005)
Guo, B., Bridges, M.J., Triantafyllis, S., Ottoni, G., Raman, E., August, D.I.: Practical and accurate low-level pointer analysis. In: 3nd Int. Symp. on Code Gen. and Opt (2005)
Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Softw. Tools for Tech. Transfer 2(4) (2000)
Hennessy, J.L.: Symbolic debugging of optimized code. Trans. on Prog. Lang. and Syst. 4(3), 323–344 (1982)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58–70 (2002)
Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. Trans. on Prog. Lang. and Syst. 12(1), 26–60 (1990)
Howard, M.: Some bad news and some good news. In: MSDN (October, 2002), http://msdn.microsoft.com/library/default.asp?url=/library/en-us/dncode/html/secure10102002.asp
IDAPro disassembler, http://www.datarescue.com/idabase/
Kidd, N., Reps, T., Melski, D., Lal, A.: WPDS++: A C++ library for weighted pushdown systems (2004), http://www.cs.wisc.edu/wpis/wpds++/
Lal, A., Reps, T.: Improving pushdown system model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 343–357. Springer, Heidelberg (2006)
Lal, A., Reps, T., Balakrishnan, G.: Extended weighted pushdown systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 434–448. Springer, Heidelberg (2005)
Necula, G.: Translation validation for an optimizing compiler. In: PLDI (2000)
Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol. 1384, Springer, Heidelberg (1998)
Reps, T., Balakrishnan, G., Lim, J.: Intermediate-representation recovery from low-level code. In: Part. Eval. and Semantics-Based Prog. Manip (2006)
Reps, T., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, Springer, Heidelberg (2003)
Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. of Comp. Prog. 58(1–2), 206–263 (2005)
Rival, X.: Abstract interpretation based certification of assembly code. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 41–55. Springer, Heidelberg (2002)
Schwoon, S.: Moped system, http://www.fmi.uni-stuttgart.de/szs/tools/moped/
Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technical Univ. of Munich, Munich, Germany (July, 2002)
Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, ch. 7, pp. 189–234. Prentice-Hall, Englewood Cliffs (1981)
Wagner, D., Foster, J., Brewer, E., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: Network and Dist. Syst. Security (February, 2000)
Wall, D.W.: Systems for late code modification. In: Giegerich, R., Graham, S.L. (eds.) Code Generation – Concepts, Tools, Techniques, pp. 275–293. Springer, Heidelberg (1992)
Wilson, R.P., Lam, M.S.: Efficient context-sensitive pointer analysis for C programs. In: PLDI, pp. 1–12 (1995)
Zellweger, P.T.: Interactive Source-Level Debugging of Optimized Programs. PhD thesis, Univ. of California, Berkeley (1984)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Balakrishnan, G., Reps, T., Melski, D., Teitelbaum, T. (2008). WYSINWYX: What You See Is Not What You eXecute. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)