Abstract
Obfuscation is the art of making code hard to reverse engineer and understand. In this paper, we propose a formal model for specifying and understanding the strength of obfuscating transformations with respect to a given attack model. The idea is to consider the attacker as an abstract interpreter willing to extract information about the program’s semantics. In this scenario, we show that obfuscating code is making the analysis imprecise, namely making the corresponding abstract domain incomplete. It is known that completeness is a property of the abstract domain and the program to analyse. We introduce a framework for transforming abstract domains, i.e., analyses, towards incompleteness. The family of incomplete abstractions for a given program provides a characterisation of the potency of obfuscation employed in that program, i.e., its strength against the attack specified by those abstractions. We show this characterisation for known obfuscating transformations used to inhibit program slicing and automated disassembly.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Barak B, Goldreich O, Impagliazzo R, Rudich S, Sahai A, Vadhan SP, Yang K (2012) On the (im)possibility of obfuscating programs. J ACM 59(2): 6
Blyth TS, Janowitz MF (1972) Residuation theory. Pergamon Press, Oxford
Brunton F, Nissenbaum H (2015) Obfuscation—a User’s Guide for Privacy and Protest. MIT Press, Cambridge
Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fix-points. In: Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL ’77). ACM Press, pp 238–252
Cousot P, Cousot R (1979) Systematic design of program analysis frameworks. In: Conference Record of the 6th ACM Symposium on Principles of Programming Languages (POPL ’79). ACM Press, pp 269–282
Cousot P, Cousot R (1992) Abstract interpretation frameworks. J Logic Comput 2(4): 511–547
Cousot P, Cousot R (1992) Comparing the Galois connection and widening/narrowing approaches to abstract interpretation (invited paper). In: Bruynooghe M, Wirsing M (eds) Proc. of the 4th Internat. Symp. on Programming Language Implementation and Logic Programming (PLILP ’92), vol. 631 of Lecture Notes in Computer Science. Springer, New York, pp 269–295
Cortesi A, Filé G, Giacobazzi R, Palamidessi C, Ranzato F (1995) Complementation in abstract interpretation. In: Mycroft A (ed) Proceedings of the 2nd International Static Analysis Symposium (SAS ’95), vol. 983 of Lecture Notes in Computer Science. Springer, New York, pp 100–117
Cytron R, Ferrante J, Rosen BK, Wegman MN, Zadeck FK (1991) Efficiently computing static single assignment form and the control dependence graph. ACM Trans Program Lang Syst 13(4): 451–490
Collberg C, Nagra J (2009) Surreptitious Software: obfuscation, watermarking, and tamperproofing for software protection. Addison-Wesley Professional, Boston
Cousot P (1999) The calculational design of a generic abstract interpreter. In: Broy M, Steinbrüggen R (eds) Calculational system design, vol 173. NATO science series, Series F: computer and systems sciences, vol 173. IOS Press, Amsterdam, pp 421–505
Collberg C, Thomborson CD, Low D (1998) Manufactoring cheap, resilient, and stealthy opaque constructs. In: Proc. of Conf. Record of the 25st ACM Symp. on Principles of Programming Languages (POPL ’98). ACM Press, pp 184–196
Dalla Preda M, Giacobazzi R (2005) Semantic-based code obfuscation by abstract interpretation. In: Proc. of the 32nd International Colloquium on Automata, Languages and Programming (ICALP ’05), vol. 3580 of Lecture Notes in Computer Science. Springer, New York, pp. 1325–1336
Dalla Preda M, Giacobazzi R (2009) Semantics-based code obfuscation by abstract interpretation. J Comput Secur 17(6): 855–908
Drape S, Thomborson C, Majumdar A (2007) Specifying imperative data obfuscations. In: Garay JA, Lenstra AK, Mambo M, Peralta R (eds) ISC—Information Security, vol. 4779 of Lecture Notes in Computer Science. Springer, New York, pp 299–314
Filé G, Ranzato F (1996) Complementation of abstract domains made easy. In: Maher M (ed) Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming (JICSLP ’96). The MIT Press, Cambridge, pp 348–362
Garg S, Gentry C, Halevi S, Raykova M, Sahai A, Waters B (2013) Candidate indistinguishability obfuscation and functional encryption for all circuits. In: 54th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2013. IEEE Computer Society, Berkeley, pp 40–49
Giacobazzi R (2008) 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). IEEE Press, pp 7–20
Gallagher KB, Lyle JR (1991) Using program slicing in software maintenance. IEEE Trans Softw Eng 17(8): 751–761
Giacobazzi R, Logozzo F, Ranzato F (2015) Analyzing program analyses. In: Rajamani SK, Walker D (eds) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015. ACM, Mumbai, pp 261–273
Giacobazzi R, Mastroeni I (2012) Making abstract interpretation incomplete: Modeling the potency of obfuscation. In: Static analysis—19th International Symposium, SAS 2012, Proceesings. Deauville, France, pp 129–145
Giacobazzi R, Quintarelli E (2001) Incompleteness, counterexamples and refinements in abstract model-checking. In: Cousot P (ed) Proc. of The 8th Internat. Static Analysis Symp. (SAS’01), vol. 2126 of Lecture Notes in Computer Science. Springer, New York, pp 356–373
Giacobazzi R, Ranzato F (1997) Refining and compressing abstract domains. In: Degano P, Gorrieri R, Marchetti-Spaccamela A (eds) Proc. of the 24th Internat. Colloq. on Automata, Languages and Programming (ICALP ’97), vol. 1256 of Lecture Notes in Computer Science. Springer, New York, pp 771–781
Giacobazzi R, Ranzato F (1998) Uniform closures: order-theoretically reconstructing logic program semantics and abstract domain refinements. Inform Comput 145(2): 153–190
Giacobazzi R, Ranzato F, Scozzari F (2000) Making abstract interpretation complete. J ACM 47(2): 361–416
Horwitz S, Reps TW, Binkley D (1990) Interprocedural slicing using dependence graphs. ACM Trans Program Lang Syst 12(1): 26–60
Janowitz MF (1967) Residuated closure operators. Port Math 26(2): 221–252
Jones ND, Giacobazzi R, Mastroeni I (2012) Obfuscation by partial evaluation of distorted interpreters. In: Kiselyov O and Thompson S (eds) Proc. of the ACM SIGPLAN Symp. on Partial Evaluation and Semantics-Based Program Manipulation (PEPM’12). ACM Press, pp 63–72
Jones ND, Gomard CK, Sestoft P (1993) Partial evaluation and automatic program generation. Prentice-Hall Inc, Upper Saddle River
Linn C, Debray S (2003) Obfuscation of executable code to improve resistance to static disassembly. In: CCS ’03: Proceedings of the 10th ACM conference on Computer and communications security. ACM, pp 290–299
Laviron V, Logozzo F (2009) Refining abstract interpretation-based static analyses with hints. In: Proc. of APLAS’09, vol. 5904 of Lecture Notes in Computer Science. Springer, New York, pp 343–358
Majumdar A, Drape SJ, Thomborson CD (2007) Slicing obfuscations: design, correctness, and evaluation. In: DRM ’07: Proceedings of the 2007 ACM workshop on Digital Rights Management. ACM, pp 70–81
Mastroeni I, Giacobazzi R (2015) Weakening residuation in adjoining closures. Order. RR 95/2015. http://hdl.handle.net/11562/925745 (to appear)
Mastroeni I, Zanardini D (2008) 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’08). ACM Press, pp 125–134
Reps T (1991) Algebraic properties of program integration. Sci Comput Program 17: 139–215
Reps T, Turnidge T (1996) Program specialization via program slicing. In Danvy O, Glueck R, Thiemann P (eds) Proceedings of the Dagstuhl seminar on Partial evaluation. Springer, New York, pp 409–429
Reps T, Yang W (1989) The semantics of program slicing and program integration. In: Diaz J, Orejas F (eds)Proc. of the Colloq. on Current Issues in Programming Languages, vol. 352 of Lecture Notes in Computer Science. Springer, New York, pp 360–374
Weiser M (1981) Program slicing. In: ICSE ’81: Proceedings of the 5th international conference on Software engineering. IEEE Press, pp 439–449
Author information
Authors and Affiliations
Corresponding author
Additional information
Maurizio Proietti, Hirohisa Seki, and Jim Woodcock
Rights and permissions
About this article
Cite this article
Giacobazzi, R., Mastroeni, I. & Dalla Preda, M. Maximal incompleteness as obfuscation potency. Form Asp Comp 29, 3–31 (2017). https://doi.org/10.1007/s00165-016-0374-2
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-016-0374-2