Controlled Model Deformation

By: Roberto Giacobazzi, Isabella Mastroeni and Durica Nikolic

Roberto Giacobazzi
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
roberto.giacobazzi@univr.it

Isabella Mastroeni
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
isabella.mastroeni@univr.it

Durica Nikolic
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
durica.nikolic@univr.it

Abstract:

Reliable and secure system design require an increasing number of methods, algorithms, and tools for automatic manipulation, where some aspects of the semantics of the modified code is not necessarily preserved. In contrast to program transformations, we call these techniques program deformations. Relevant examples include program obfuscation, watermarking, repairing, diversifying and in ultimate analysis, automatic program synthesis. In this paper we propose a mathematical foundation and a practical methodology for the systematic design of model deformations. The idea is that the controlled deformation of a system is a change in the way a possibly abstract interpreter observes the resulting behavior. We prove that model deformation can be specified and controlled by making models complete with respect to some fixed abstractions. The resulting theory provides new practical methodologies and algorithms for abstraction interpretation-driven synthesis, which are illustrated in abstract model checking, program synthesis and fingerprinting.