Il pensiero astratto è per molti una fatica - per me, in giorni propizi, una festa ed una ebbrezza.
Nietzsche, Unveroffentlichtes aus der Umwerthungszeit 1882/88


Short CV


Roberto Giacobazzi was born in 1964 in
Modena, Italy. He 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 1998 to 2000 he was Associate Professor at the University of Verona. From May 2000 until now he is Full Professor in Computer Science at the University of Verona. He has been visiting professor at The Ben Gurion University of Negev, KAIST Institute of Technology, Ecole Polytechnique (Paris), Ecole Normale Superieure (Paris), and Universidad Complutense de Madrid. He is the Scientific Leader of the SPY-Lab and co-founder of Julia From October 2006 until October 2012 he was the Dean of the College of Science of 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, software watermarking and lattice theory. He is author of more than 100 publications in international journals and conferences and he is involved in national (italian) and international (european) research projects in the field of static program analysis. His main current research interest is in formal methods for systematic design of domains and transfer functions for abstract interpretation, with application in security, digital asset protection, code obfuscation, watermarking, malware analysis, semantics, program analysis, and abstract model-checking. In the past, he gave a declarative semantics for Prolog control features and he studied new methodologies to design static program analyzers and optimization techniques for logic and constraint-based languages by abstract interpretation. In lattice theory he contributed to understanding of the structure of the lattice of closure operators and complete congruence relations on complete lattices. He is in the Steering Committee of the Static Analysis Symposium and of the ACM Conference on Principles of Programming Languages, POPL.


More in detail

Abstract interpretation theory and applications: This is my main research interest. Abstract interpretation is a general theory for approximating discrete dynamic systems [see Cousot]. A central role in this theory is played by the notion of abstract domain. We defined a number of formal and constructive systematic methods for domain design in abstract interpretation. These can be classified [FGR96,GR98b, GR97a] in terms of domain refinements [GR97b, GS97, GR95, GR98c], domain simplifications [GR97b], and domain compressors [GR98a, CFGPR97]. Of particular importance are the systematic operations to make an abstract interpretation complete [GRS00], providing powerful formal methods to constructively design optimal domains for abstract interpretation. The results are universal, independent from specific programming languages, and can be applied to any abstract interpretation. Some of these operations have been applied in many areas of computer science. In particular in static program analysis [GR97a, GR97b, GS97, GR95, GR98c] GRS03], program manipulation (such as program slicing) [GM02], comparative semantics of programming languages [GR99, GM00, G02], abstract model-checking [GQ01, GR06,GR11], and language-based security [GM04]. We are currently interested in applying these theories in computational complexity of approximate algorithms, computational biology, analysis and verification of hybrid systems, and in program testing of large-scale software systems. As far as the theory is concerned, we are working in the definition of a unifying theory for abstract domain design. This theory is based on standard principles of domain-theory. The idea is to develop a mathematical foundation of abstract domain transformers which is adequate to specify both first and higher-order domain operations for domain refinement, simplification, and compression [GM03]. A theory for semantic deformation to achieve completeness has been developed in the SAS’08 Invited Lecture [GM08]. This is now the main research topic for developing a theory of code transformation and deformation guided by abstract interpretation.

Semantics: We studied semantics for modeling control features of Prolog programs [BCGL93, BCGM95] and the hierarchy of semantics for pure logic programs based on abstract interpretation [G96]. Systematic methods for domain construction have been applied for designing semantics of arbitrary transition systems [GR96,GR95,GM00, GM02]. In [CCG09] we analyzed resolution-based semantics of logic programs as abstractions of grammar-like traces. In [GM11] we characterized the structure of safety properties and semantics as abstract domains of a trace based operational semantics, showing the peculiarity of safety with respect to the algebraic properties of its abstractions.

Static program analysis: We studied deductive [GG94, BGL93], abductive [G98] and compositional [CDG93] methods for static analysis of logic programs. Specific domains have been studied for the analysis of types [BG92], deterministic computations [GR92], query optimization [CCG94], and numeric constraint optimization [BGL93]. Abstract interpretation has been applied also to specify static analyzers for constraint logic programs [GDL95] and concurrent constraint programs [ZGL97]. In [BG07] we developed a fast implementation of the octagon relational static analysis on GPU Graphic Hardware architectures showing the very first efficient program analyzer based on a mixed CPU-GPU architecture.

Language-based security: We are currently interested in weakening non-interference in static program analysis for language-based security. The manifesto of our research in this field appeared in POPL'04 [GM04]. The idea is weakening non-interference by abstract interpretation and considering abstract domain transformers to model attackers. Applications in concurrency and timed automata are available in [GM05a] and [GM05b]. Abstract Non Interference is also a unifying paradigm for modeling both declassification and attack models, as proved in [GM05,BGM07]. A proof system for abstract non-interference is in [GM09].

Digital asset protection: We introduced a semantic-based model for specifying code obfuscation algorithms. The idea is to view code obfuscation, and therefore software watermarking, as an abstraction of the concrete semantics of a program [DG05]. Robust algorithms for code obfuscation can then be derived systematically, e.g. in control code obfuscation by opaque predicate insertion, by abstract interpretation from semantic transformers [DG05b, DMDG06], e.g. by hiding watermarks in loop-based structures [DGV08]. In [G08] we introduced the idea of making a program obscure is making an interpreter incomplete. This provides a general theory for information concealment in programing languages which is still under active development. In [CDGGHW11] we launched DAPA, the Digital Asset Protection Association and its manifesto.

Malware analysis: In malware analysis we studied the problem of modeling metamorphic malware in order to extract metamorphic signatures [DGDCT10]. We introduced a semantics, called phase semantics, for self-modifying code modeling precisely the metamorphic code behavior. We proved that metamorphic signatures can be automatically extracted by abstract interpretation of this semantics, and that regular metamorphism can be modeled as finite state automata abstraction of the phase semantics. In [FPG11], we studied a way to adapt Relock malware to Windows 7, finding an OS vulnerability.

Lattice theory: Standard abstract interpretation theory is based on the isomorphism between the lattice of all abstractions on a given domain and the lattice of all its closure operators. The study of abstract interpretation theory have therefore lead us to have results in the theory of closure operators on complete lattices [GPR96,GR98,GR98b]. We are now interested in complete congruence lattices, currently a hot topic in lattice theory. In [GR98b] we proved an embedding of the lattice of complete congruences on a continuous lattice into the lattice of all its closure operators. This allows us to extend most properties of the lattice of closure operators to the lattice of complete congruences on continuous lattices. This result is a consequence of our research in abstract interpretation completeness [GR97b,GRS00].