Controlled Model Deformation
Roberto Giacobazzi, Isabella Mastroeni · 2010
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.