Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code

详细信息    查看全文

• 作者：Sandrine Blazy ; Vincent Laporte ; David Pichardie
• 关键词：Coq ; Abstract interpretation ; Low ; level programming language
• 刊名：Journal of Automated Reasoning
• 出版年：2016
• 出版时间：March 2016
• 年：2016
• 卷：56
• 期：3
• 页码：283-308
• 全文大小：2,861 KB
• 参考文献：1.Balakrishnan, G., Thomas, W.: Reps. Wysinwyx: What you see is not what you execute. ACM Trans. Program. On Lang. Syst. 32(6), 23 (2010)
  2.Bardin, S., Herrmann, P., Védrine, F.: Refinement-based CFG reconstruction from unstructured programs. In: Verification, Model Checking and Abstract Interpretation (VMCAI), vol. 6538 of LNCS, pp 54–69. Springer, Berlin (2011)
  3.Bertot, Y.: Structural abstract interpretation, a formal study in Coq. In: Language Engineering and Rigorous Software Development, International LerNet alFA Summer School 2008, vol. 5520 of LNCS, pp. 153–194. Springer, Berlin (2009)
  4.Bertot, Y., Grégoire, B., Leroy, X.: A structured approach to proving compiler optimizations based on dataflow analysis. In TYPES, vol. 3839 of LNCS, pp. 66–81. Springer, Berlin (2006)
  5.Blazy, S., Laporte, V., Maroneze, A., Pichardie, D.: Formal verification of a c value analysis based on abstract interpretation. In: Static Analysis Symposium (SAS), vol. 7935 of LNCS, pp. 324–344. Springer, Berlin (2013)
  6.Blazy S., Leroy X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reason. 43(3), 263–288 (2009)MathSciNet CrossRef MATH
  7.Bonfante, G,, Marion, J.-Y., Reynaud-Plantey, D.: A computability perspective on self-modifying programs. In: SEFM, pp. 231–239 (2009)
  8.Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a data flow analyser in constructive logic. Theor. Comput. Sci. 342(1), 56–78 (2005)
  9.Cachera, D., Pichardie, D.: Comparing techniques for certified static analysis. In: Proceedings of the 1st NASA Formal Methods Symposium (NFM’09), pp. 111–115 (2009)
  10.Cachera, D., Pichardie, D.: A certified denotational abstract interpreter. In: Interactive Theorem Proving (ITP), vol. 6172 of LNCS, pp. 9–24. Springer, Berlin (2010)
  11.Cai, H., Shao, Z., Vaynberg, A.: Certified self-modifying code. In: Conference on Programming Language Design and Implementation (PLDI), pp. 66–77. ACM, New York (2007)
  12.Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: Conference on Programming Language Design and Implementation (PLDI). ACM, New York (2011)
  13.Collberg, C., Thomborson, C., Low, D.: Manufacturing cheap, resilient, and stealthy opaque constructs. In 25th Symposium on Principles of Programming Language (POPL), pp. 184–196. ACM, New York (1998)
  14.Companion website. http://​www.​irisa.​fr/​celtique/​ext/​smc .
  15.Coupet-Grimal, S., Delobel, W.: A uniform and certified approach for two static analyses. In: TYPES, vol. 3839 of LNCS, pp. 115–137 (2004)
  16.Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Symposium on Principles of Programming Language (POPL), p. 238252. ACM, New York
  17.Debray, S.K., Coogan, K.P., Townsend, G.M.: On the semantics of self-unpacking malware code. Draft, (2008)
  18.Gerth, R.T.: Formal verification of self modifying code. In: International Conference for Young Computer Scientists. International Academic Publishers, China (1991)
  19.Jensen, J., Benton, N,, Kennedy, A.: High-level separation logic for low-level code. In: Symposium on Principles of Programming Language (POPL). ACM, New York (2013)
  20.Jourdan, J.-H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: Formal verification of a C static analyzer. In 42nd Symposium Principles of Programming Languages (POPL), pp. 247–259 (2015)
  21.Kennedy, A., Benton, N., Jensen, J.B,, Dagand, P.: Coq: The world’s best macro assembler? In: Symposium on Principles and Practice of Declarative Programming (PPDP), pp. 13–24. ACM, New York (2013)
  22.Kinder, J.: Towards static analysis of virtualization-obfuscated binaries. In: Reverse Engineering (WCRE), 2012 19th Working Conference on, pp. 61–70. IEEE (2012)
  23.Klein G., Nipkow T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Programm. Lang. Syst. 28(4), 619–695 (2006)CrossRef
  24.Monniaux, D.: Réalisation mécanisée d’interpréteurs abstraits. Master’s thesis, U. Paris 7 (1998)
  25.Morrisett, G., Tan, G., Tassarotti, J., Tristan, J.-B., Gan, E.: Rocksalt: better, faster, stronger sfi for the x86. In Conference on Programming Language Design and Implementation (PLDI), pp. 395–404 (2012)
  26.Myreen, M.O.: Verified just-in-time compiler on x86. In: Symposium on Principles of Programming Language (POPL), pp. 107–118. ACM, New York (2010)
  27.Nipkow, T.: Abstract interpretation of annotated commands. In: Interactive Theorem Proving (ITP), vol. 7406 of LNCS, pp. 116–132. Springer, Berlin (2012)
  28.Pichardie, D.: Interprtation Abstraite en Logique Intuitionniste: Extraction d’analyseurs Java Certifis. PhD thesis, U. Rennes 1, (2005)
  29.Pichardie, D.: Building certified static analysers by modular construction of well-founded lattices. In: Proceedings of the 1st International Conference on Foundations of Informatics, Computing and Software (FICS), vol. 212 of Electronic Notes in Theoretical Computer Science, pp. 225–239 (2008)
  30.Pichardie D.: Building certified static analysers by modular construction of well-founded lattices. Electr. Notes Theor. Comput. Sci. 212, 225–239 (2008)CrossRef MATH
  31.Robert, V., Leroy, X.: A formally-verified alias analysis. In: Certified Proofs and Programs (CPP), vol. 7679 of LNCS, pp. 11–26. Springer, Berlin (2012)
  32.Stewart, G., Beringer, L., Appel, A.W.: Verified heap theorem prover by paramodulation. In: International Conference on Functional Programming (ICFP), pp. 3–14. ACM, New York (2012)
  33.Szor, P.: The Art of Computer Virus Research and Defense. Addison-Wesley Professional, Boston (2005)
  
• 作者单位：Sandrine Blazy (1)
  Vincent Laporte (1)
  David Pichardie (2)
  
  1. IRISA, Inria, Université Rennes 1, Campus de Beaulieu, Rennes, France
  2. IRISA, Inria, ENS Rennes, Campus de Beaulieu, Rennes, France
  
• 刊物类别：Computer Science
• 刊物主题：Mathematical Logic and Formal Languages
  Artificial Intelligence and Robotics
  Mathematical Logic and Foundations
  Symbolic and Algebraic Manipulation
  
• 出版者：Springer Netherlands
• ISSN：1573-0670

文摘

Static analysis of binary code is challenging for several reasons. In particular, standard static analysis techniques operate over control-flow graphs, which are not available when dealing with self-modifying programs which can modify their own code at runtime. We formalize in the Coq proof assistant some key abstract interpretation techniques that automatically extract memory safety properties from binary code. Our analyzer is formally proved correct and has been run on several self-modifying challenges, provided by Cai et al. in their PLDI 2007 article.