Article

Control Code Obfuscation by Abstract Interpretation

Authors:

Mila Dalla Preda,

Roberto GiacobazziAuthors Info & Claims

SEFM '05: Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods

Pages 301 - 310

https://doi.org/10.1109/SEFM.2005.13

Published: 07 September 2005 Publication History

Abstract

Control code obfuscation is intended to prevent malicious reverse engineering of software by masking the program control flow. These obfuscating transformations often rely on the existence of opaque predicates, that support the design of transformations that break up the program control flow. We prove that an algorithm for control obfuscation by opaque predicate insertion can be systematically derived as an abstraction of a suitable semantic transformation. In this framework, deobfuscation is interpreted as an attacker which can observe the computational behaviour of programs up to a given precision degree. Both obfuscation and deobfuscation can therefore be interpreted as approximations of program semantics, where approximation is formalized using abstract interpretation theory. In particular we prove that abstract interpretation provides here the adequate setting to measure the potency of an obfuscation algorithm by comparing the degree of abstraction of the most abstract domains which are able to disclose opaque predicates. Keywords: Code Obfuscation, Abstract Interpretation, Program Transformation, Program analysis, Semantics.

References

[1]

C. Thomborson C. Collberg. Breaking abstrcations and unstructural data structures. In Proc. of the 1994 IEEE Internal. Conf. on Computer Languages (ICCL '98), 1998.

Digital Library

[2]

C. Thomborson C. Collberg. Watermarking, tamper-proofing, and obduscation-tools for software protection. IEEE Trans. Software Eng., pages 735-746, 2002.

Digital Library

[3]

D. Low C. Collberg, C. Thomborson. A taxionomy of obduscating transformations. Technical Report 148, Dept. of Computer Science, The Univ. of Auckland, 1997.

[4]

D. Low C. Collberg, C. Thomborson. Manifactiring cheap, resilient, and stealthy opaque constructs. In Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '98). ACM Press, 1998.

Digital Library

[5]

J. Knight C. Wang, J. Hill and J. Davidson. Software tamper resistance: Obstructing static analysis of programs. Technical report CS-2000-12, Department of Computer Science, University of Virginia, 2000.

Digital Library

[6]

Y. Caseau. Abstract interpretation of constraints on order-sorted domains. In V. Saraswat and K. Ueda, editors, Proc. of the 1991 Internat. Logic Programming Symp. (ILPS '91). pages 435-452. The MIT Press, Cambridge, Mass., 1991.

[7]

S. Chandrasekharan and S. Debray. Deobfuscation: Improving reverse engineering of obfuscated code. Draft, 2005.

[8]

E. M. Clarke, O. Grumberg. and D. E. Long. Model checking and abstraction. ACM Trans. Program. Lang. Syst., 16(5):1512-1542, 1994.

Digital Library

[9]

R. Cleaveland and J. Riely. Testing-based abstractions for value-passing systems. In B. Jonsson and J. Parrow, editors. Proc. of the 5th Internat. Conf on Concurrency Theory (CONCUR '94). volume 836 of Lecture Notes in Computer Science, pages 417-432. Springer-Verlag, 1994.

Digital Library

[10]

M. Comini and G. Levi. An algebraic theory of observables. In M. Bruynooghe, editor. Proc. of the 1994 Intetnat. Logic Programming Symp. (ILPS '94), pages 172-186. The MIT Press, Cambridgr. Mass., 1994.

Digital Library

[11]

P. Cousot. Semantic foundations of program analysis. In S. S. Muchnick and N. D. Jones. editors, Program Flow Analysis: Theory and Applications, pages 303-342. Prentice-Hall, Englewood Cliffs, NJ, 1981.

[12]

P. Cousot. Abstract interpretation. ACM Comput. Surv., 28(2):324-328. 1996.

Digital Library

[13]

P. Cousot. Types as abstract interpretations (Invited Paper). In Conference Record of the 24th ACM Symp. on Principles of Programming Languages (POPL '97). pages 316-331. ACM Press. New York, 1997.

Digital Library

[14]

P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci., 2000.

Digital Library

[15]

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 Symp. on Principles of Programming Longuages (POPL '77), pages 238-252. ACM Press, New York, 1977.

Digital Library

[16]

P. Cousot and R. Cousol. Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symp. on Principles of Programming Languages (POPL '79), pages 269-282. ACM Press. New York, 1979.

Digital Library

[17]

P. Cousot and R. Cousot. Inductive definitions. semantics and abstract interpretation. In Conference Record of the 19th ACM Symp. on Principles of Programming Languages (POPL '92), pages 83-94. ACM Press. New York, 1992.

Digital Library

[18]

P. Cousot and R. Cousot Systematic design of program transformation frameworks by abstract interpretation. In Conference Record of the Twenryninth Annual ACM SlGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 178-190. New York. NY, 2002. ACM Press.

Digital Library

[19]

D. Dams. R. Gerth. and O. Grumberg. Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst., 19(2):253-291, 1997.

Digital Library

[20]

R. Giacobazzi. "Optimal" collecting semantics for analysis in a hierarchy of logic program semantics. In C. Puech and R. Reischuk. editors, Proc. of the 13th Internat. Symp. on Theoretical Aspects of Computer Science (STACS '96), volume 1046 of Lecture Notes in Computer Science, pages 503-514. Springer-Verlag, Berlin. 1996.

Digital Library

[21]

R. Giacobazzi and E. Quintarelli. Incompleteness. counterexamples and refinements in abstract model-checking. In P. Cousot. editor, Proc. of The 8th International Static Analysis Symposium. SAS'O1, volume 2126 of Lecture Notes in Computer Science. pages 356-373. Sprillger-Verlag, 2001.

Digital Library

[22]

R. Giacobazzi. F. Ranzato. and F. Scozzari. Making abstract interpretations complete J. of the ACM., 47(2):361-416, 2000.

Digital Library

[23]

S. Graf. Characterization of a sequentially consistent memory and verification of a cache memory by abstraction. Distributed Computing. 12(2-3):75-90, 1999.

Digital Library

[24]

P. Granger. Static analysis of arithmetical congruences. Intern. J. Computer Math., 30:165-190, 1989.

[25]

C. Loiseaux, S. Graf, J. Sifakis. A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des., 6:11-44, 1995.

Digital Library

[26]

D. Low. Java control flow obfuscation. Master of science thesis, Department of Computer Science. The University of Auckland. 1998.

[27]

B. Monsuez. System F and abstract interpretation. In A. Mycroft, editor. Proc. of the 2nd Internat. Static Analysis Symp. (SAS '95). volume 983 of Lecture Notes in Computer Science, pages 279-295. Springer-Verlag, Berlin. 1995.

Digital Library

[28]

P. Ørbæk. Can you trust your data? In P.D. Mosses, M. Nielsen, and M.I. Schwartzbach. editors, Proc. of the 6th Internat. Joint Conf. CAAP/FASE. Theory and Practice of Software Devolpment (TAPSOFT 95). volume 915 of Lecture Notes in Computer Science. pages 575-589. Springer-Verlag, 1995.

Digital Library

[29]

P. Ørbæk and J. Palsberg. Trust in the lambda-calculus J. Funct. Program., 7(6):557-591, 1997.

Digital Library

[30]

R. Paige. Future directions in program transformations. In ACM SIGPLAN Not., volume 32. pages 94-97. 1997.

Digital Library

[31]

D. Plaisted. Theorem proving with abstraction. Artif. Intell., 16:47-108. 1981.

Digital Library

[32]

M. Dalla Preda and R. Giacobazzi. Semantic-based code obfuscation by abstract interpretation. In Proceedings of the 32th International Colloquium on Automata, Languages and Programming (ICALP'O5 - Track B). volume 3580, pages 1325-1336. Springer-Verlag. 2005. July 11-15, Lisboa, Portugal.

Digital Library

[33]

M. Madou S. K. Udupa. S. Debray. Deobfuscation: Reverse engineering obfuscated code. Draft, 2005.

[34]

A. Venet. Abstract interpretation of the ¿-calculus. In M. Darn, editor. Proc. of the 5th LOMAPS Meeting on Analysis and Verification of High-Level Concurrent Languages. volume 1192 of Lecture Notes in Computer Science, pages 51-75. Springer-Verlag, Berlin, 1996.

Digital Library

Cited By

Campion MDalla Preda MGiacobazzi RUrban C(2024)Monotonicity and the Precision of Program AnalysisProceedings of the ACM on Programming Languages10.1145/36328978:POPL(1629-1662)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632897
Dalla Preda MMastroeni I(2018)Characterizing a property-driven obfuscation strategyJournal of Computer Security10.3233/JCS-1467226:1(31-69)Online publication date: 1-Jan-2018
https://dl.acm.org/doi/10.3233/JCS-14672
Banescu SCollberg CGanesh VNewsham ZPretschner ASchwab SRobertson WBalzarotti D(2016)Code obfuscation against symbolic execution attacksProceedings of the 32nd Annual Conference on Computer Security Applications10.1145/2991079.2991114(189-200)Online publication date: 5-Dec-2016
https://dl.acm.org/doi/10.1145/2991079.2991114
Show More Cited By

Index Terms

Control Code Obfuscation by Abstract Interpretation
1. Software and its engineering
  1. Software creation and management
    1. Software development techniques
      1. Error handling and recovery
  2. Software notations and tools
    1. Compilers
      1. Interpreters

Recommendations

Semantics-based code obfuscation by abstract interpretation

In recent years code obfuscation has attracted research interest as a promising technique for protecting secret properties of programs. The basic idea of code obfuscation is to transform programs in order to hide their sensitive information while ...
Unveiling metamorphism by abstract interpretation of code properties

Metamorphic code includes self-modifying semantics-preserving transformations to exploit code diversification. The impact of metamorphism is growing in security and code protection technologies, both for preventing malicious host attacks, e.g., in ...
Obfuscation: The Hidden Malware

A cyberwar exists between malware writers and antimalware researchers. At this war's heart rages a weapons race that originated in the 80s with the first computer virus. Obfuscation is one of the latest strategies to camouflage the telltale signs of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

SEFM '05: Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods

September 2005

433 pages

ISBN:0769524354

Publisher

IEEE Computer Society

United States

Publication History

Published: 07 September 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Campion MDalla Preda MGiacobazzi RUrban C(2024)Monotonicity and the Precision of Program AnalysisProceedings of the ACM on Programming Languages10.1145/36328978:POPL(1629-1662)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632897
Dalla Preda MMastroeni I(2018)Characterizing a property-driven obfuscation strategyJournal of Computer Security10.3233/JCS-1467226:1(31-69)Online publication date: 1-Jan-2018
https://dl.acm.org/doi/10.3233/JCS-14672
Banescu SCollberg CGanesh VNewsham ZPretschner ASchwab SRobertson WBalzarotti D(2016)Code obfuscation against symbolic execution attacksProceedings of the 32nd Annual Conference on Computer Security Applications10.1145/2991079.2991114(189-200)Online publication date: 5-Dec-2016
https://dl.acm.org/doi/10.1145/2991079.2991114
Banescu SOchoa MPretschner AFalcarin PWyseur B(2015)A framework for measuring software obfuscation resilience against automated attacksProceedings of the 1st International Workshop on Software Protection10.5555/2821429.2821442(45-51)Online publication date: 16-May-2015
https://dl.acm.org/doi/10.5555/2821429.2821442
Preda MMastroeni IGiacobazzi RJagannathan SSewell P(2014)Analyzing program dependencies for malware detectionProceedings of ACM SIGPLAN on Program Protection and Reverse Engineering Workshop 201410.1145/2556464.2556470(1-7)Online publication date: 22-Jan-2014
https://dl.acm.org/doi/10.1145/2556464.2556470
Zhou WZhang XJiang XChen KXie QQiu WLi NTzeng W(2013)AppInkProceedings of the 8th ACM SIGSAC symposium on Information, computer and communications security10.1145/2484313.2484315(1-12)Online publication date: 8-May-2013
https://dl.acm.org/doi/10.1145/2484313.2484315
Preda MMastroeni IGiacobazzi R(2013)A formal framework for property-driven obfuscation strategiesProceedings of the 19th international conference on Fundamentals of Computation Theory10.1007/978-3-642-40164-0_15(133-144)Online publication date: 19-Aug-2013
https://dl.acm.org/doi/10.1007/978-3-642-40164-0_15
Dalla Preda MGiacobazzi R(2009)Semantics-based code obfuscation by abstract interpretationJournal of Computer Security10.5555/1662641.166264417:6(855-908)Online publication date: 1-Dec-2009
https://dl.acm.org/doi/10.5555/1662641.1662644
Martel MPuebla GVidal G(2009)Program transformation for numerical precisionProceedings of the 2009 ACM SIGPLAN workshop on Partial evaluation and program manipulation10.1145/1480945.1480960(101-110)Online publication date: 19-Jan-2009
https://dl.acm.org/doi/10.1145/1480945.1480960
Tsai HHuang YWagner D(2009)A graph approach to quantitative analysis of control-flow obfuscating transformationsIEEE Transactions on Information Forensics and Security10.1109/TIFS.2008.20110774:2(257-267)Online publication date: 1-Jun-2009
https://dl.acm.org/doi/10.1109/TIFS.2008.2011077
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents