Cinzia Di Giusto (INRIA) ,

The kappa calculus: a study on the expressiveness of rewriting rules

The kappa-calculus is a rewriting-based formalism, originally introduced to describe molecular biology. Here we consider the calculus outside its biological domain and we discuss how the shape of rewriting rules influences the expressive power of the corresponding dialects. We are mainly interested in the verification of kappa models. In particular the restrictions on the shape of the rules give rise to a lattice of dialects where properties such as reachability and coverability become decidable, thus paving the way for (semi)automated verification. We will also outline a novel approach to malware analysis where those result could be applied. The kappa-calculus can indeed be used to model the different actors involved in a malicious code attack. Moreover by simulating their behavior, it is possible to extract important information that can drive in the choice of the defense technique to apply.