Completeness and incompleteness in Abstract Interpretation: A model for information concealment in code protection


January 17, 2014


Roberto Giacobazzi


University of Verona


We will consider completeness and incompleteness of abstract interpretation as models for understanding the phenomenon of hiding information in code protecting transformations and white-box cryptography in a MATE (Man-At-The-End) attack scenario. This is the case in software watermarks and code obfuscation. These code transformations will be are devoted to force incompleteness with respect to an attacker which is modeled as an abstract interpreter. The potency of an attacker consist here in its ability to extract a complete view of program’s execution. The model is general enough to include generic static and dynamic attacks. Known protecting transformations will be systematically derived and implemented by specializing a “distorted” interpreter with respect to the source code to protect. Interestingly the distortion required to protect the code corresponds precisely (and systematically) to the potency of the expected attacker in a clean mathematical correspondence.


Roberto Giacobazzi

Roberto Giacobazzi received the Laurea degree in Computer Science in 1988 from the University of Pisa, and in 1993 he received the Ph.D. in Computer Science from the same university, with a Ph.D. thesis on Semantic aspects of logic program analysis, under the supervision of Prof. Giorgio Levi. From 1993 to 1995 he had a Post Doctoral Research position at Laboratoire d’Informatique (LIX), Ecole Polytechnique (Paris) in the equipe Cousot. From 1995 to 1998 he was (tenured) Assistant Professor in Computer Science at the University of Pisa. From May 2000 until now he is Full Professor in Computer Science at the University of Verona. The research interests of Roberto Giacobazzi include abstract interpretation, static program analysis, semantics of programming languages, program verification, abstract model-checking, program transformation and optimization, digital asset protection, code obfuscation, malware detection, software watermarking and lattice theory. He has been Program Chair of SAS, VMCAI, of workshops in programming languages and language based security, and General Chair of POPL2013. He is currently in the Steering committee of SAS and POPL. From 2006 to 2012 he has been Dean of the College of Science of the University of Verona.