{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,26]],"date-time":"2026-10-26T17:30:49Z","timestamp":1793035849392,"version":"4.5.0"},"reference-count":121,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2010,8,1]],"date-time":"2010-08-01T00:00:00Z","timestamp":1280620800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-9986308CCF-{0540955, 0524051}"],"award-info":[{"award-number":["CCR-9986308CCF-{0540955, 0524051}"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCR-9986308CCF-{0540955, 0524051}"],"award-info":[{"award-number":["CCR-9986308CCF-{0540955, 0524051}"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"name":"HSARPA","award":["FA8750-05-C-0179"],"award-info":[{"award-number":["FA8750-05-C-0179"]}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8750-06-C-0249"],"award-info":[{"award-number":["FA8750-06-C-0249"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-01-1-{0796, 0708}"],"award-info":[{"award-number":["N00014-01-1-{0796, 0708}"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2010,8]]},"abstract":"<jats:p>Over the last seven years, we have developed static-analysis methods to recover a good approximation to the variables and dynamically allocated memory objects of a stripped executable, and to track the flow of values through them. The article presents the algorithms that we developed, explains how they are used to recover Intermediate Representations (IRs) from executables that are similar to the IRs that would be available if one started from source code, and describes their application in the context of program understanding and automated bug hunting.<\/jats:p>\n          <jats:p>Unlike algorithms for analyzing executables that existed prior to our work, the ones presented in this article provide useful information about memory accesses, even in the absence of debugging information. The ideas described in the article are incorporated in a tool for analyzing Intel x86 executables, called CodeSurfer\/x86. CodeSurfer\/x86 builds a system dependence graph for the program, and provides a GUI for exploring the graph by (i) navigating its edges, and (ii) invoking operations, such as forward slicing, backward slicing, and chopping, to discover how parts of the program can impact other parts.<\/jats:p>\n          <jats:p>To assess the usefulness of the IRs recovered by CodeSurfer\/x86 in the context of automated bug hunting, we built a tool on top of CodeSurfer\/x86, called Device-Driver Analyzer for x86 (DDA\/x86), which analyzes device-driver executables for bugs. Without the benefit of either source code or symbol-table\/debugging information, DDA\/x86 was able to find known bugs (that had been discovered previously by source-code analysis tools), along with useful error traces, while having a low false-positive rate. DDA\/x86 is the first known application of program analysis\/verification techniques to industrial executables.<\/jats:p>","DOI":"10.1145\/1749608.1749612","type":"journal-article","created":{"date-parts":[[2010,8,11]],"date-time":"2010-08-11T12:57:24Z","timestamp":1281531444000},"page":"1-84","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":194,"title":["WYSINWYX"],"prefix":"10.1145","volume":"32","author":[{"given":"Gogul","family":"Balakrishnan","sequence":"first","affiliation":[{"name":"NEC Laboratories America, Inc., Princeton, NJ"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin and GrammaTech, Inc., Ithaca, NY"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2010,8,13]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the European Conference on Object-Oriented Programming.","author":"Aigner G.","unstructured":"Aigner , G. and H\u00f6lzle , U . 1996. Eliminating virtual function calls in C++ programs . In Proceedings of the European Conference on Object-Oriented Programming. Aigner, G. and H\u00f6lzle, U. 1996. Eliminating virtual function calls in C++ programs. In Proceedings of the European Conference on Object-Oriented Programming."},{"key":"e_1_2_1_2_1","unstructured":"aiT. aiT worst-case execution time analyzer. http:\/\/www.AbsInt.com\/aiT.  aiT. aiT worst-case execution time analyzer. http:\/\/www.AbsInt.com\/aiT."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1007588710878"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349303"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Balakrishnan G. 2007. WYSINWYX: What You See Is Not What You eXecute. Ph.D. thesis Tech. rep. 1603. Computer Science Department University of Wisconsin Madison WI.   Balakrishnan G. 2007. WYSINWYX: What You See Is Not What You eXecute. Ph.D. thesis Tech. rep. 1603. Computer Science Department University of Wisconsin Madison WI.","DOI":"10.1007\/978-3-540-69149-5_22"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31985-6_19"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the International Conference on Compiler Construction. 5--23","author":"Balakrishnan G.","unstructured":"Balakrishnan , G. and Reps , T . 2004. Analyzing memory accesses in x86 executables . In Proceedings of the International Conference on Compiler Construction. 5--23 . Balakrishnan, G. and Reps, T. 2004. Analyzing memory accesses in x86 executables. In Proceedings of the International Conference on Compiler Construction. 5--23."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_15"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation.","author":"Balakrishnan G.","unstructured":"Balakrishnan , G. and Reps , T . 2007. DIVINE: DIscovering Variables IN Executables . In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation. Balakrishnan, G. and Reps, T. 2007. DIVINE: DIscovering Variables IN Executables. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems.","author":"Balakrishnan G.","unstructured":"Balakrishnan , G. and Reps , T . 2008. Analyzing stripped device-driver executables . In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems. Balakrishnan, G. and Reps, T. 2008. Analyzing stripped device-driver executables. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_17"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the IFIP Working Conference on Verified Software: Theories, Tools, Experiments.","author":"Balakrishnan G.","unstructured":"Balakrishnan , G. , Reps , T. , Melski , D. , and Teitelbaum , T . 2007. WYSINWYX: What you see is not what you execute . In Proceedings of the IFIP Working Conference on Verified Software: Theories, Tools, Experiments. Balakrishnan, G., Reps, T., Melski, D., and Teitelbaum, T. 2007. WYSINWYX: What you see is not what you execute. In Proceedings of the IFIP Working Conference on Verified Software: Theories, Tools, Experiments."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217943"},{"key":"e_1_2_1_15_1","series-title":"Lecture Notes in Computer Science","volume-title":"Bebop: A symbolic model checker for Boolean programs. In Proceedings of the Spin Workshop","author":"Ball T.","year":"2000","unstructured":"Ball , T. and Rajamani , S . 2000 . Bebop: A symbolic model checker for Boolean programs. In Proceedings of the Spin Workshop . Lecture Notes in Computer Science , vol. 1885 . Springer , 113--130. Ball, T. and Rajamani, S. 2000. Bebop: A symbolic model checker for Boolean programs. In Proceedings of the Spin Workshop. Lecture Notes in Computer Science, vol. 1885. Springer, 113--130."},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the Conference on Computer-Aided Verification.","author":"Ball T.","unstructured":"Ball , T. and Rajamani , S . 2001. The SLAM toolkit . In Proceedings of the Conference on Computer-Aided Verification. Ball, T. and Rajamani, S. 2001. The SLAM toolkit. In Proceedings of the Conference on Computer-Aided Verification."},{"key":"e_1_2_1_17_1","unstructured":"Bergeron J. Debbabi M. Desharnais J. Erhioui M. Lavoie Y. and Tawbi N. 2001. Static detection of malicious code in executable programs. Int. J. Req. Engin.  Bergeron J. Debbabi M. Desharnais J. Erhioui M. Lavoie Y. and Tawbi N. 2001. Static detection of malicious code in executable programs. Int. J. Req. Engin."},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the International Workshops on Enabling Technologies: Infrastructures for Collaborative Enterprises.","author":"Bergeron J.","unstructured":"Bergeron , J. , Debbabi , M. , Erhioui , M. , and Ktari , B . 1999. Static analysis of binary code to isolate malicious behaviors . In Proceedings of the International Workshops on Enabling Technologies: Infrastructures for Collaborative Enterprises. Bergeron, J., Debbabi, M., Erhioui, M., and Ktari, B. 1999. Static analysis of binary code to isolate malicious behaviors. In Proceedings of the International Workshops on Enabling Technologies: Infrastructures for Collaborative Enterprises."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the International Conference on Concurrency Theory (CONCUR'97)","author":"Bouajjani A.","unstructured":"Bouajjani , A. , Esparza , J. , and Maler , O . 1997. Reachability analysis of pushdown automata: Application to model checking . In Proceedings of the International Conference on Concurrency Theory (CONCUR'97) . Bouajjani, A., Esparza, J., and Maler, O. 1997. Reachability analysis of pushdown automata: Application to model checking. In Proceedings of the International Conference on Concurrency Theory (CONCUR'97)."},{"key":"e_1_2_1_21_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the International Conference on Formal Methods in Programming and Their Application","author":"Bourdoncle F.","unstructured":"Bourdoncle , F. 1993. Efficient chaotic iteration strategies with widenings . In Proceedings of the International Conference on Formal Methods in Programming and Their Application . Lecture Notes in Computer Science . Springer . Bourdoncle, F. 1993. Efficient chaotic iteration strategies with widenings. In Proceedings of the International Conference on Formal Methods in Programming and Their Application. Lecture Notes in Computer Science. Springer."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1251535.1251547"},{"key":"e_1_2_1_23_1","unstructured":"Brumley D. and Newsome J. 2006. Alias analysis for assembly. Tech. rep. CMU-CS-06-180 School of Computer Science Carnegie Mellon University Pittsburgh PA.  Brumley D. and Newsome J. 2006. Alias analysis for assembly. Tech. rep. CMU-CS-06-180 School of Computer Science Carnegie Mellon University Pittsburgh PA."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the Symposium on Logic in Computer Science. 428--439","author":"Burch J.","unstructured":"Burch , J. , Clarke , E. , McMillan , K. , Dill , D. , and Hwang , L . 1990. Symbolic model checking: 1020 states and beyond . In Proceedings of the Symposium on Logic in Computer Science. 428--439 . Burch, J., Clarke, E., McMillan, K., Dill, D., and Hwang, L. 1990. Symbolic model checking: 1020 states and beyond. In Proceedings of the Symposium on Logic in Computer Science. 428--439."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(200006)30:7%3C775::AID-SPE309%3E3.0.CO;2-H"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250743"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/316158.316183"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_21"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/586110.586142"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/502034.502042"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1108792.1108814"},{"key":"e_1_2_1_33_1","unstructured":"Cifuentes C. and Fraboulet A. 1997a. Interprocedural data flow recovery of high-level language code from assembly. Tech. rep. 421 University of Queensland.  Cifuentes C. and Fraboulet A. 1997a. Interprocedural data flow recovery of high-level language code from assembly. Tech. rep. 421 University of Queensland."},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the International Conference on Software Maintenance. 188--195","author":"Cifuentes C.","unstructured":"Cifuentes , C. and Fraboulet , A . 1997b. Intraprocedural static slicing of binary executables . In Proceedings of the International Conference on Software Maintenance. 188--195 . Cifuentes, C. and Fraboulet, A. 1997b. Intraprocedural static slicing of binary executables. In Proceedings of the International Conference on Software Maintenance. 188--195."},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the International Conference on Software Maintenance. 228--237","author":"Cifuentes C.","unstructured":"Cifuentes , C. , Simon , D. , and Fraboulet , A . 1998. Assembly to high-level language translation . In Proceedings of the International Conference on Software Maintenance. 228--237 . Cifuentes, C., Simon, D., and Fraboulet, A. 1998. Assembly to high-level language translation. In Proceedings of the International Conference on Software Maintenance. 228--237."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_2_1_37_1","unstructured":"CodeSonar. CodeSonar GrammaTech Inc. www.grammatech.com\/products\/codesonar.  CodeSonar. CodeSonar GrammaTech Inc. www.grammatech.com\/products\/codesonar."},{"key":"e_1_2_1_38_1","unstructured":"CodeSurfer. CodeSurfer GrammaTech Inc. www.grammatech.com\/products\/codesurfer.  CodeSurfer. CodeSurfer GrammaTech Inc. www.grammatech.com\/products\/codesurfer."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.53996"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSAC.2006.50"},{"key":"e_1_2_1_45_1","unstructured":"Coverity. Coverity Prevent. www.coverity.com\/html\/coverity-prevent-static-analysis.html.  Coverity. Coverity Prevent. www.coverity.com\/html\/coverity-prevent-static-analysis.html."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the International Confernece on Parallel and Distributed Processing Techniques and Applications.","author":"De Sutter B.","unstructured":"De Sutter , B. , De Bus , B. , De Bosschere , K. , Keyngnaert , P. , and Demoen , B . 2000. On the static analysis of indirect control transfers in binaries . In Proceedings of the International Confernece on Parallel and Distributed Processing Techniques and Applications. De Sutter, B., De Bus, B., De Bosschere, K., Keyngnaert, P., and Demoen, B. 2000. On the static analysis of indirect control transfers in binaries. In Proceedings of the International Confernece on Parallel and Distributed Processing Techniques and Applications."},{"key":"e_1_2_1_48_1","unstructured":"Debray S. Linn C. Andrews G. and Schwarz B. 2004. Stack analysis of x86 executables. www.cs.arizona.edu\/~debray\/Publications\/stack-analysis.pdf.  Debray S. Linn C. Andrews G. and Schwarz B. 2004. Stack analysis of x86 executables. www.cs.arizona.edu\/~debray\/Publications\/stack-analysis.pdf."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268948"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_27"},{"key":"e_1_2_1_51_1","unstructured":"DMCA &sect;1201. &sect;1201. Circumvention of Copyright Protection Systems. www.copyright.gov\/title17\/92chap12.html&num;1201.  DMCA &sect;1201. &sect;1201. Circumvention of Copyright Protection Systems. www.copyright.gov\/title17\/92chap12.html&num;1201."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781149"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292543"},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the Conference on Operating System Design and Implementation. 1--16","author":"Engler D.","unstructured":"Engler , D. , Chelf , B. , Chou , A. , and Hallem , S . 2000. Checking system rules using system-specific, programmer-written compiler extensions . In Proceedings of the Conference on Operating System Design and Implementation. 1--16 . Engler, D., Chelf, B., Chou, A., and Hallem, S. 2000. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the Conference on Operating System Design and Implementation. 1--16."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134028"},{"key":"e_1_2_1_57_1","unstructured":"Ferdinand C. 2009. Personal communication.  Ferdinand C. 2009. Personal communication."},{"key":"e_1_2_1_58_1","volume-title":"Proceedings of the 1st International Workshop on Embedded Software (EMSOFT'01)","author":"Ferdinand C.","unstructured":"Ferdinand , C. , Heckmann , R. , Langenbach , M. , Martin , F. , Schmidt , M. , Theiling , H. , Thesing , S. , and Wilhelm , R . 2001. Reliable and precise WCET determination for a real-life processor . In Proceedings of the 1st International Workshop on Embedded Software (EMSOFT'01) . 469--485. Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., and Wilhelm, R. 2001. Reliable and precise WCET determination for a real-life processor. In Proceedings of the 1st International Workshop on Embedded Software (EMSOFT'01). 469--485."},{"key":"e_1_2_1_59_1","doi-asserted-by":"crossref","unstructured":"Finkel A. Willems B. and Wolper P. 1997. A direct symbolic approach to model checking pushdown systems. Elec. Not. Theor. Comput. Sci. 9.  Finkel A. Willems B. and Wolper P. 1997. A direct symbolic approach to model checking pushdown systems. Elec. Not. Theor. Comput. Sci. 9.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081742"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_41"},{"key":"e_1_2_1_62_1","volume-title":"Proceedings of the Conference on Computer Aided Verification.","author":"Gopan D.","unstructured":"Gopan , D. and Reps , T . 2007. Low-Level library analysis and summarization . In Proceedings of the Conference on Computer Aided Verification. Gopan, D. and Reps, T. 2007. Low-Level library analysis and summarization. In Proceedings of the Conference on Computer Aided Verification."},{"key":"e_1_2_1_63_1","volume-title":"Proceedings of the Conference on Computer Aided Verification. Lecture Notes in Computer Science","volume":"1254","author":"Graf S.","unstructured":"Graf , S. and Sa\u00efdi , H . 1997. Construction of abstract state graphs with PVS . In Proceedings of the Conference on Computer Aided Verification. Lecture Notes in Computer Science , vol. 1254 . Springer, 72--83. Graf, S. and Sa\u00efdi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 1254. Springer, 72--83."},{"key":"e_1_2_1_64_1","volume-title":"Static congruence analysis of binaries. Bachelors thesis","author":"Grewe D.","unstructured":"Grewe , D. 2008. Static congruence analysis of binaries. Bachelors thesis , University des Saarlandes. Grewe, D. 2008. Static congruence analysis of binaries. Bachelors thesis, University des Saarlandes."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2005.27"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008678014487"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/379605.379665"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.234509"},{"key":"e_1_2_1_72_1","volume-title":"Some bad news and some good news. MSDN","author":"Howard M.","unstructured":"Howard , M. 2002. Some bad news and some good news. MSDN , Microsoft Corp ., msdn2.microsoft.com\/en-us\/library\/ms972826.aspx. Howard, M. 2002. Some bad news and some good news. MSDN, Microsoft Corp., msdn2.microsoft.com\/en-us\/library\/ms972826.aspx."},{"key":"e_1_2_1_73_1","unstructured":"IDAPro. IDAPro disassembler. www.hex-rays.com\/idapro\/.  IDAPro. IDAPro disassembler. www.hex-rays.com\/idapro\/."},{"key":"e_1_2_1_74_1","volume-title":"Proceedings of the USENIX Security Symposium.","author":"Kiriansky V.","unstructured":"Kiriansky , V. , Bruening , D. , and Amarasinghe , S . 2002. Secure execution via program shepherding . In Proceedings of the USENIX Security Symposium. Kiriansky, V., Bruening, D., and Amarasinghe, S. 2002. Secure execution via program shepherding. In Proceedings of the USENIX Security Symposium."},{"key":"e_1_2_1_75_1","volume-title":"Proceedings of the International Workshop on Source Code Analysis and Manipulation.","author":"Kiss A., J.","unstructured":"Kiss , A., J. J\u00e1sz , G. L. , and Gyim\u00f3thy , T . 2003. Interprocedural static slicing of binary executables . In Proceedings of the International Workshop on Source Code Analysis and Manipulation. Kiss, A., J. J\u00e1sz, G. L., and Gyim\u00f3thy, T. 2003. Interprocedural static slicing of binary executables. In Proceedings of the International Workshop on Source Code Analysis and Manipulation."},{"key":"e_1_2_1_76_1","volume-title":"Proceedings of the USENIX Security Symposium.","author":"Kruegel C.","unstructured":"Kruegel , C. , Kirda , E. , Mutz , D. , Robertson , W. , and Vigna , G . 2005. Automating mimicry attacks using static binary analysis . In Proceedings of the USENIX Security Symposium. Kruegel, C., Kirda, E., Mutz, D., Robertson, W., and Vigna, G. 2005. Automating mimicry attacks using static binary analysis. In Proceedings of the USENIX Security Symposium."},{"key":"e_1_2_1_77_1","volume-title":"Computer-Aided Verification of Coordinating Processes","author":"Kurshan R.","unstructured":"Kurshan , R. 1994. Computer-Aided Verification of Coordinating Processes . Princeton University Press . Kurshan, R. 1994. Computer-Aided Verification of Coordinating Processes. Princeton University Press."},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_44"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/207110.207163"},{"key":"e_1_2_1_80_1","volume-title":"Proceedings of the International Conference on Compiler Construction.","author":"Lim J.","unstructured":"Lim , J. and Reps , T . 2008. A system for generating static analyzers for machine instructions . In Proceedings of the International Conference on Compiler Construction. Lim, J. and Reps, T. 2008. A system for generating static analyzers for machine instructions. In Proceedings of the International Conference on Compiler Construction."},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2006.29"},{"key":"e_1_2_1_82_1","volume-title":"Proceedings of the Static Analysis Symposium. 196--212","author":"Manevich R.","unstructured":"Manevich , R. , Ramalingam , G. , Field , J. , Goyal , D. , and Sagiv , M . 2002. Compactly representing first-order structures for static analysis . In Proceedings of the Static Analysis Symposium. 196--212 . Manevich, R., Ramalingam, G., Field, J., Goyal, D., and Sagiv, M. 2002. Compactly representing first-order structures for static analysis. In Proceedings of the Static Analysis Symposium. 196--212."},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_2"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134650.1134659"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_5"},{"key":"e_1_2_1_86_1","volume-title":"Proceedings of the European Symposium on Programming.","author":"Mycroft A.","year":"1999","unstructured":"Mycroft , A. 1999 . Type-Based decompilation . In Proceedings of the European Symposium on Programming. Mycroft, A. 1999. Type-Based decompilation. In Proceedings of the European Symposium on Programming."},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/800017.800517"},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111066"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328465"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/253228.253351"},{"key":"e_1_2_1_91_1","volume-title":"Programming the Microsoft Windows Driver Model","author":"Oney W.","unstructured":"Oney , W. 2003. Programming the Microsoft Windows Driver Model . Microsoft Press . Oney, W. 2003. Programming the Microsoft Windows Driver Model. Microsoft Press."},{"key":"e_1_2_1_92_1","volume-title":"Proceedings of the Static Analysis Symposium. 238--254","author":"Pande H.","unstructured":"Pande , H. and Ryder , B . 1996. Data-Flow-Based virtual function resolution . In Proceedings of the Static Analysis Symposium. 238--254 . Pande, H. and Ryder, B. 1996. Data-Flow-Based virtual function resolution. In Proceedings of the Static Analysis Symposium. 238--254."},{"key":"e_1_2_1_93_1","unstructured":"Phoenix. Phoenix software optimization and analysis framework. http:\/\/connect.microsoft.com\/phoenix.  Phoenix. Phoenix software optimization and analysis framework. http:\/\/connect.microsoft.com\/phoenix."},{"key":"e_1_2_1_94_1","article-title":"Combining interprocedural pointer analysis and conditional constant propagation. Tech. rep","author":"Pioli A.","year":"1999","unstructured":"Pioli , A. and Hind , M. 1999 . Combining interprocedural pointer analysis and conditional constant propagation. Tech. rep . RC 21532(96749), IBM T.J. Watson Research Center. Pioli, A. and Hind, M. 1999. Combining interprocedural pointer analysis and conditional constant propagation. Tech. rep. RC 21532(96749), IBM T.J. Watson Research Center.","journal-title":"RC 21532(96749), IBM T.J. Watson Research Center."},{"key":"e_1_2_1_95_1","unstructured":"PREfast. 2004. PREfast with driver-specific rules. www.microsoft.com\/whdc\/archive\/PREfast-drv.mspx.  PREfast. 2004. PREfast with driver-specific rules. www.microsoft.com\/whdc\/archive\/PREfast-drv.mspx."},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292553"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1145\/1113830.1113833"},{"key":"e_1_2_1_99_1","volume-title":"Proceedings of the International Conference on Compiler Construction.","author":"Reps T.","unstructured":"Reps , T. and Balakrishnan , G . 2008. Improved memory-access analysis for x86 executables . In Proceedings of the International Conference on Compiler Construction. Reps, T. and Balakrishnan, G. 2008. Improved memory-access analysis for x86 executables. In Proceedings of the International Conference on Compiler Construction."},{"key":"e_1_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111542.1111560"},{"key":"e_1_2_1_101_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_15"},{"key":"e_1_2_1_102_1","doi-asserted-by":"publisher","DOI":"10.1145\/2166.357218"},{"key":"e_1_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.5555\/646542.696206"},{"key":"e_1_2_1_104_1","doi-asserted-by":"publisher","DOI":"10.1145\/1057387.1057388"},{"key":"e_1_2_1_105_1","first-page":"189","article-title":"Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications. S. Muchnick and N. Jones, Eds. Prentice-Hall, Englewood Cliffs, NJ","volume":"7","author":"Sharir M.","year":"1981","unstructured":"Sharir , M. and Pnueli , A. 1981 . Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications. S. Muchnick and N. Jones, Eds. Prentice-Hall, Englewood Cliffs, NJ , Chapter 7 , 189 -- 234 . Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications. S. Muchnick and N. Jones, Eds. Prentice-Hall, Englewood Cliffs, NJ, Chapter 7, 189--234.","journal-title":"Chapter"},{"key":"e_1_2_1_106_1","doi-asserted-by":"publisher","DOI":"10.1145\/239098.239121"},{"key":"e_1_2_1_107_1","volume-title":"Vulcan: Binary transformation in a distributed environment. MSR-TR-2001-50, Microsoft Research.","author":"Srivastava A.","year":"2001","unstructured":"Srivastava , A. , Edwards , A. , and Vo , H . 2001 . Vulcan: Binary transformation in a distributed environment. MSR-TR-2001-50, Microsoft Research. Srivastava, A., Edwards, A., and Vo, H. 2001. Vulcan: Binary transformation in a distributed environment. MSR-TR-2001-50, Microsoft Research."},{"key":"e_1_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178260"},{"key":"e_1_2_1_109_1","volume-title":"Proceedings of the Symposium on Operating Systems Design and Implementation.","author":"Swift M.","unstructured":"Swift , M. , Annamalai , M. , Bershad , B. , and Levy , H . 2004. Recovering device drivers . In Proceedings of the Symposium on Operating Systems Design and Implementation. Swift, M., Annamalai, M., Bershad, B., and Levy, H. 2004. Recovering device drivers. In Proceedings of the Symposium on Operating Systems Design and Implementation."},{"key":"e_1_2_1_110_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047915.1047919"},{"key":"e_1_2_1_111_1","volume-title":"Proceedings of the Working Conference on Reverse Engineering.","author":"van Deursen A.","unstructured":"van Deursen , A. and Moonen , L . 1998. Type inference for COBOL systems . In Proceedings of the Working Conference on Reverse Engineering. van Deursen, A. and Moonen, L. 1998. Type inference for COBOL systems. In Proceedings of the Working Conference on Reverse Engineering."},{"key":"e_1_2_1_112_1","volume-title":"Procedings of the Working Conference on Reverse Engineering.","author":"van Deursen A.","unstructured":"van Deursen , A. and Moonen , L . 1998. Type inference for COBOL systems . In Procedings of the Working Conference on Reverse Engineering. van Deursen, A. and Moonen, L. 1998. Type inference for COBOL systems. In Procedings of the Working Conference on Reverse Engineering."},{"key":"e_1_2_1_113_1","volume-title":"Proceedings of the Conference on Network and Distributed Systems Security.","author":"Wagner D.","unstructured":"Wagner , D. , Foster , J. , Brewer , E. , and Aiken , A . 2000. A first step towards automated detection of buffer overrun vulnerabilities . In Proceedings of the Conference on Network and Distributed Systems Security. Wagner, D., Foster, J., Brewer, E., and Aiken, A. 2000. A first step towards automated detection of buffer overrun vulnerabilities. In Proceedings of the Conference on Network and Distributed Systems Security."},{"key":"e_1_2_1_114_1","doi-asserted-by":"crossref","unstructured":"Wall D. 1992. Systems for late code modification. In Code Generation\u2014Concepts Tools Techniques R. Giegerich and S. Graham Eds. Springer.  Wall D. 1992. Systems for late code modification. In Code Generation\u2014Concepts Tools Techniques R. Giegerich and S. Graham Eds. Springer.","DOI":"10.1007\/978-1-4471-3501-2_15"},{"key":"e_1_2_1_115_1","unstructured":"WHDC. 2007. C++ for kernel mode drivers: Pros and cons. www.microsoft.com\/whdc\/driver\/kernel\/KMcode.mspx.  WHDC. 2007. C++ for kernel mode drivers: Pros and cons. www.microsoft.com\/whdc\/driver\/kernel\/KMcode.mspx."},{"key":"e_1_2_1_116_1","unstructured":"WHQL. 2004. Defrauding the WHQL driver certification process. blogs.msdn.com\/oldnewthing\/archive\/2004\/03\/05\/84469.aspx.  WHQL. 2004. Defrauding the WHQL driver certification process. blogs.msdn.com\/oldnewthing\/archive\/2004\/03\/05\/84469.aspx."},{"key":"e_1_2_1_117_1","volume-title":"Sept. 19","author":"Wikipedia","year":"2009","unstructured":"Wikipedia : Enforceability . Software license agreement: Enforceability (in the United States). en.wikipedia.org\/wiki\/Software license agreement&num;Enforceability , Sept. 19 , 2009 . Wikipedia: Enforceability. Software license agreement: Enforceability (in the United States). en.wikipedia.org\/wiki\/Software license agreement&num;Enforceability, Sept. 19, 2009."},{"key":"e_1_2_1_118_1","volume-title":"Sept. 19","author":"Wikipedia","year":"2009","unstructured":"Wikipedia : shrink-wrap and click-wrap licenses. Software license agreement: Shrink-wrap and click-wrap licenses. en.wikipedia.org\/wiki\/Software license agreement&num;Shrink-wrap and click-wrap licenses , Sept. 19 , 2009 . Wikipedia: shrink-wrap and click-wrap licenses. Software license agreement: Shrink-wrap and click-wrap licenses. en.wikipedia.org\/wiki\/Software license agreement&num;Shrink-wrap and click-wrap licenses, Sept. 19, 2009."},{"key":"e_1_2_1_119_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347389"},{"key":"e_1_2_1_120_1","doi-asserted-by":"publisher","DOI":"10.1145\/207110.207111"},{"key":"e_1_2_1_121_1","unstructured":"Windows DDK. 2003. Windows Server 2003 DDK. www.microsoft.com\/whdc\/devtools\/ddk.  Windows DDK. 2003. Windows Server 2003 DDK. www.microsoft.com\/whdc\/devtools\/ddk."},{"key":"e_1_2_1_122_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349313"},{"key":"e_1_2_1_123_1","volume-title":"Proceedings of the European Symposium on Programming.","author":"Xu Z.","unstructured":"Xu , Z. , Miller , B. , and Reps , T . 2001. Typestate checking of machine code . In Proceedings of the European Symposium on Programming. Xu, Z., Miller, B., and Reps, T. 2001. Typestate checking of machine code. In Proceedings of the European Symposium on Programming."},{"key":"e_1_2_1_124_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2007.163"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1749608.1749612","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1749608.1749612","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:23:45Z","timestamp":1750249425000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1749608.1749612"}},"subtitle":["What you see is not what you eXecute"],"short-title":[],"issued":{"date-parts":[[2010,8]]},"references-count":121,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2010,8]]}},"alternative-id":["10.1145\/1749608.1749612"],"URL":"https:\/\/doi.org\/10.1145\/1749608.1749612","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,8]]},"assertion":[{"value":"2009-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-08-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}