Skip to main content
SpringerLink
Log in
Book cover

International Static Analysis Symposium

SAS 2012: Static Analysis pp 129–145Cite as

Making Abstract Interpretation Incomplete: Modeling the Potency of Obfuscation

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7460))

Abstract

Recent studies on code protection showed that incompleteness, in the abstract interpretation framework, has a key role in understanding program obfuscation. In particular, it is well known that completeness corresponds to exactness of a given analysis for a fixed program semantics, hence incompleteness implies the imprecision of an analysis with respect to the program semantics. In code protection, if the analysis corresponds to attacker capability of understanding a program semantics, then to study incompleteness means to study how to make an attacker harmless. We recently showed that this is possible by transforming the program semantics towards incompleteness, which corresponds to a code obfuscation. In this paper, we show that incompleteness can be induced also by transforming abstract domains. In this way we can associate with each obfuscated program (semantics) the most imprecise, harmless, analysis. We show that, for both the forms of completeness, backward and forward, we can uniquely simplify domains towards incompleteness, while in general it is not possible to uniquely refine domains. Finally, we show some examples of known code protection techniques that can be characterized in the new framework of abstract interpretation incompleteness.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Birkhoff, G.: Lattice Theory, 3rd edn. AMS Colloquium Publication, AMS (1967)

    MATH  Google Scholar 

  2. Collberg, C., Nagra, J.: Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection. Addison-Wesley Professional (2009)

    Google Scholar 

  3. Collberg, C., Thomborson, C.: Breaking abstrcations and unstructural data structures. In: Proc. of the 1994 IEEE Internat. Conf. on Computer Languages, ICCL 1998, pp. 28–37 (1998)

    Google Scholar 

  4. Collberg, C., Thomborson, C.: Watermarking, tamper-proofing, and obduscation-tools for software protection. IEEE Trans. Software Eng., 735–746 (2002)

    Google Scholar 

  5. Collberg, C., Thomborson, C.D., Low, D.: Manufactoring cheap, resilient, and stealthy opaque constructs. In: Proc. of Conf. Record of the 25th ACM Symp. on Principles of Programming Languages, POPL 1998, pp. 184–196. ACM Press (1998)

    Google Scholar 

  6. Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the 2nd International Symposium on Programming, pp. 106–130. Dunod, Paris (1976)

    Google Scholar 

  7. Cousot, P., Cousot, R.: 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, POPL 1977, pp. 238–252. ACM Press (1977)

    Google Scholar 

  8. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference Record of the 6th ACM Symposium on Principles of Programming Languages, POPL 1979, pp. 269–282. ACM Press (1979)

    Google Scholar 

  9. Cousot, P., Cousot, R.: Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation (Invited Paper). In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  10. Dalla Preda, M., Giacobazzi, R.: Semantic-Based Code Obfuscation by Abstract Interpretation. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1325–1336. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Drape, S., Thomborson, C., Majumdar, A.: Specifying Imperative Data Obfuscations. In: Garay, J.A., Lenstra, A.K., Mambo, M., Peralta, R. (eds.) ISC 2007. LNCS, vol. 4779, pp. 299–314. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. Filé, G., Giacobazzi, R., Ranzato, F.: A unifying view of abstract domain design. ACM Comput. Surv. 28(2), 333–336 (1996)

    Article  Google Scholar 

  13. Filé, G., Ranzato, F.: Complementation of abstract domains made easy. In: Maher, M. (ed.) Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming, JICSLP 1996, pp. 348–362. The MIT Press (1996)

    Google Scholar 

  14. Gallagher, K.B., Lyle, J.R.: Using program slicing in software maintenance. IEEE Trans. on Software Engineering 17(8), 751–761 (1991)

    Article  Google Scholar 

  15. Giacobazzi, R.: 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 2008), pp. 7–20. IEEE Press (2008)

    Google Scholar 

  16. Giacobazzi, R., Mastroeni, I.: Transforming Abstract Interpretations by Abstract Interpretation. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 1–17. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Giacobazzi, R., Quintarelli, E.: Incompleteness, Counterexamples, and Refinements in Abstract Model-Checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 356–373. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  18. Giacobazzi, R., Ranzato, F.: Refining and Compressing Abstract Domains. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 771–781. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  19. Giacobazzi, R., Ranzato, F.: Uniform closures: order-theoretically reconstructing logic program semantics and abstract domain refinements. Inform. and Comput. 145(2), 153–190 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  20. Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretation complete. Journal of the ACM 47(2), 361–416 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  21. Horwitz, S., Reps, T.W., Binkley, D.: Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst. 12(1), 26–60 (1990)

    Article  Google Scholar 

  22. Janowitz, M.F.: Residuated closure operators. Portug. Math. 26(2), 221–252 (1967)

    MathSciNet  MATH  Google Scholar 

  23. Jones, N.D., Giacobazzi, R., Mastroeni, I.: Obfuscation by partial evaluation of distorted interpreters. In: Kiselyov, O., Thompson, S. (eds.) Proc. of the ACM SIGPLAN Symp. on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2012), pp. 63–72. ACM Press (2012)

    Google Scholar 

  24. Majumdar, A., Drape, S.J., Thomborson, C.D.: Slicing obfuscations: design, correctness, and evaluation. In: DRM 2007: Proceedings of the 2007 ACM Workshop on Digital Rights Management, pp. 70–81. ACM (2007)

    Google Scholar 

  25. Mastroeni, I., Zanardini, D.: Data dependencies and program slicing: From syntax to abstract semantics. In: Proc. of the ACM SIGPLAN Symp. on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2008), pp. 125–134. ACM Press (2008)

    Google Scholar 

  26. Reps, T., Turnidge, T.: Program Specialization via Program Slicing. In: Danvy, O., Gltick, R., Thiemann, P. (eds.) Partial Evaluation. LNCS, vol. 1110, pp. 409–429. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  27. Ward, M.: The Closure Operators of a Lattice. Annals of Mathematics 43(2), 191–196 (1942)

    Article  MathSciNet  MATH  Google Scholar 

  28. Weiser, M.: Program slicing. In: ICSE 1981: Proceedings of the 5th International Conference on Software Engineering, pp. 439–449. IEEE Press (1981)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Università di Verona, Verona, Italy

    Roberto Giacobazzi & Isabella Mastroeni

Authors
  1. Roberto Giacobazzi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Isabella Mastroeni
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Département d’Informatique, École Normale Supérieure, 45, rue d’Ulm, 75005, Paris, France

    Antoine Miné

  2. Department of Computing and Information Sciences, Kansas State University, 234 Nichols Hall, 66506, Manhattan, KS, USA

    David Schmidt

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Giacobazzi, R., Mastroeni, I. (2012). Making Abstract Interpretation Incomplete: Modeling the Potency of Obfuscation. In: Miné, A., Schmidt, D. (eds) Static Analysis. SAS 2012. Lecture Notes in Computer Science, vol 7460. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33125-1_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-33125-1_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-33124-4

  • Online ISBN: 978-3-642-33125-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation