Document Open Access Logo

Towards a Unifying Framework for Tuning Analysis Precision by Program Transformation

Author Mila Dalla Preda

PDF
Thumbnail PDF

File

OASIcs.Gabbrielli.4.pdf
  • Filesize: 0.79 MB
  • 22 pages

Document Identifiers

Author Details

Mila Dalla Preda
  • Department of Computer Science, University of Verona, Italy

Funding

The research has been partially supported by the project "Dipartimenti di Eccellenza 2018-2020" funded by the Italian Ministry of Education, Universities and Research (MIUR).

Cite AsGet BibTex

Mila Dalla Preda. Towards a Unifying Framework for Tuning Analysis Precision by Program Transformation. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/OASIcs.Gabbrielli.4

Abstract

Static and dynamic program analyses attempt to extract useful information on program’s behaviours. Static analysis uses an abstract model of programs to reason on their runtime behaviour without actually running them, while dynamic analysis reasons on a test set of real program executions. For this reason, the precision of static analysis is limited by the presence of false positives (executions allowed by the abstract model that cannot happen at runtime), while the precision of dynamic analysis is limited by the presence of false negatives (real executions that are not in the test set). Researchers have developed many analysis techniques and tools in the attempt to increase the precision of program verification. Software protection is an interesting scenario where programs need to be protected from adversaries that use program analysis to understand their inner working and then exploit this knowledge to perform some illicit actions. Program analysis plays a dual role in program verification and software protection: in program verification we want the analysis to be as precise as possible, while in software protection we want to degrade the results of the analysis as much as possible. Indeed, in software protection researchers usually recur to a special class of program transformations, called code obfuscation, to modify a program in order to make it more difficult to analyse while preserving its intended functionality. In this setting, it is interesting to study how program transformations that preserve the intended behaviour of programs can affect the precision of both static and dynamic analysis. While some works have been done in order to formalise the efficiency of code obfuscation in degrading static analysis and in the possibility of transforming programs in order to avoid or increase false positives, less attention has been posed to formalise the relation between program transformations and false negatives in dynamic analysis. In this work we are setting the scene for a formal investigation of the syntactic and semantic program features that affect the presence of false negatives in dynamic analysis. We believe that this understanding would be useful for improving the precision of the existing dynamic analysis tools and in the design of program transformations that complicate the dynamic analysis. To Maurizio on his 60th birthday!

Subject Classification

ACM Subject Classification
  • Security and privacy → Software reverse engineering
Keywords
  • Program analysis
  • analysis precision
  • program transformation
  • software protection
  • code obfuscation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Paul Ammann and Jeff Offutt. Introduction to software testing. Cambridge University Press, 2016. Google Scholar
  2. Sebastian Banescu, Christian Collberg, Vijay Ganesh, Zack Newsham, and Alexander Pretschner. Code obfuscation against symbolic execution attacks. In Proceedings of the 32nd Annual Conference on Computer Security Applications, pages 189-200, 2016. Google Scholar
  3. B. Barak, O. Goldreich, R. Impagliazzo, S. Rudich, A. Sahai, S. P. Vadhan, and K. Yang. On the (im)possibility of obfuscating programs. In CRYPTO '01: Proceedings of the 21st Annual International Cryptology Conference on Advances in Cryptology, pages 1-18. Springer-Verlag, 2001. Google Scholar
  4. Ezio Bartocci and Yliès Falcone, editors. Lectures on Runtime Verification - Introductory and Advanced Topics, volume 10457 of Lecture Notes in Computer Science. Springer, 2018. Google Scholar
  5. Tim Blazytko, Moritz Contag, Cornelius Aschermann, and Thorsten Holz. Syntia: Synthesizing the semantics of obfuscated code. In 26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, Canada, August 16-18, 2017, pages 643-659. USENIX Association, 2017. Google Scholar
  6. Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Isabel Garcia-Contreras, and Dusko Pavlovic. Abstract extensionality: on the properties of incomplete abstract interpretations. Proc. ACM Program. Lang., 4(POPL):28:1-28:28, 2020. Google Scholar
  7. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, 2018. Google Scholar
  8. C. Collberg and J. Nagra. Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection. Addison-Wesley Professional, 2009. Google Scholar
  9. C. Collberg, C. Thomborson, and D. Low. Manufacturing cheap, resilient, and stealthy opaque constructs. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of programming languages rm(POPL '98 ), pages 184-196. ACM Press, 1998. Google Scholar
  10. Kevin Coogan, Gen Lu, and Saumya K. Debray. Deobfuscation of virtualization-obfuscated software: a semantics-based approach. In Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS 2011, Chicago, Illinois, USA, October 17-21, 2011, pages 275-284. ACM, 2011. Google Scholar
  11. P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci., 277(1-2):47-103, 2002. Google Scholar
  12. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages rm(POPL '77 ), pages 238-252. ACM Press, 1977. Google Scholar
  13. P. Cousot and R. Cousot. A constructive characterization of the lattices of all retractions, preclosure, quasi-closure and closure operators on a complete lattice. Portug. Math., 38(2):185-198, 1979. Google Scholar
  14. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symposium on Principles of Programming Languages rm(POPL '79 ), pages 269-282. ACM Press, 1979. Google Scholar
  15. M. Dalla Preda, M. Christodorescu, S. Jha, and S. Debray. A semantics-based approach to malware detection. In POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 377-388. ACM Press, 2007. URL: https://doi.org/10.1145/1190216.1190270.
  16. Mila Dalla Preda, Mihai Christodorescu, Somesh Jha, and Saumya K. Debray. A semantics-based approach to malware detection. ACM Trans. Program. Lang. Syst., 30(5):25:1-25:54, 2008. Google Scholar
  17. Mila Dalla Preda and Roberto Giacobazzi. Semantics-based code obfuscation by abstract interpretation. Journal of Computer Security, 17(6):855-908, 2009. Google Scholar
  18. Mila Dalla Preda, Roberto Giacobazzi, and Niccoló Marastoni. Formal framework for reasoning about the precision of dynamic analysis. In Static Analysis, 16th International Symposium, SAS 2020, page to appear, 2020. Google Scholar
  19. Mila Dalla Preda and Isabella Mastroeni. Characterizing a property-driven obfuscation strategy. J. Comput. Secur., 26(1):31-69, 2018. Google Scholar
  20. Bjorn De Sutter, Christian S. Collberg, Mila Dalla Preda, and Brecht Wyseur. Software protection decision support and evaluation methodologies (dagstuhl seminar 19331). Dagstuhl Reports, 9(8):1-25, 2019. Google Scholar
  21. Hanne Riis Nielson Flemming Nielson and Chris Hankin. Principles of Program Analysis. Springer, 1999. Google Scholar
  22. R. Giacobazzi. Hiding information in completeness holes - new perspectives in code obfuscation and watermarking. In Proc. of The 6th IEEE International Conferences on Software Engineering and Formal Methods (SEFM'08), pages 7-20. IEEE Press., 2008. Google Scholar
  23. R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretation complete. Journal of the ACM, 47(2):361-416, March 2000. Google Scholar
  24. Roberto Giacobazzi, Francesco Logozzo, and Francesco Ranzato. Analyzing program analyses. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 261-273, 2015. Google Scholar
  25. Roberto Giacobazzi, Isabella Mastroeni, and Mila Dalla Preda. Maximal incompleteness as obfuscation potency. Formal Asp. Comput., 29(1):3-31, 2017. Google Scholar
  26. Peter W. O'Hearn. Incorrectness logic. Proc. ACM Program. Lang., 4(POPL):10:1-10:32, 2020. Google Scholar
  27. Mathilde Ollivier, Sébastien Bardin, Richard Bonichon, and Jean-Yves Marion. How to kill symbolic deobfuscation for free (or: unleashing the potential of path-oriented protections). In Proceedings of the 35th Annual Computer Security Applications Conference, pages 177-189, 2019. Google Scholar
  28. Andre Pawlowski, Moritz Contag, and Thorsten Holz. Probfuscation: an obfuscation approach using probabilistic control flows. In International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment, pages 165-185. Springer, 2016. Google Scholar
  29. Francesco Ranzato and Francesco Tapparo. Strong preservation as completeness in abstract interpretation. In Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, volume 2986 of Lecture Notes in Computer Science, pages 18-32. Springer, 2004. Google Scholar
  30. Sebastian Schrittwieser and Stefan Katzenbeisser. Code obfuscation against static and dynamic reverse engineering. In International workshop on information hiding, pages 270-284. Springer, 2011. Google Scholar
  31. Sebastian Schrittwieser, Stefan Katzenbeisser, Johannes Kinder, Georg Merzdovnik, and Edgar R. Weippl. Protecting software through obfuscation: Can it keep pace with progress in code analysis? ACM Comput. Surv., 49(1):4:1-4:37, 2016. Google Scholar
  32. Monirul I. Sharif, Andrea Lanzi, Jonathon T. Giffin, and Wenke Lee. Automatic reverse engineering of malware emulators. In 30th IEEE Symposium on Security and Privacy (S&P 2009), 17-20 May 2009, Oakland, California, USA, pages 94-109. IEEE Computer Society, 2009. Google Scholar
  33. Bernhard Steffen and Gerhard J. Woeginger, editors. Computing and Software Science - State of the Art and Perspectives, volume 10000 of Lecture Notes in Computer Science. Springer, 2019. Google Scholar
  34. Babak Yadegari, Brian Johannesmeyer, Ben Whitely, and Saumya Debray. A generic approach to automatic deobfuscation of executable code. In 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015, pages 674-691. IEEE Computer Society, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact