Séminaires
Séminaire du 5 Décembre 2008
Lieu
LIP6, salle 847: comment y aller
Programme
14h00-15h00: Eike Best (Universität Oldenburg)
A Decomposition Theorem for Finite Persistent Transition Systems
Abstract: In this talk, it is shown that if a finite labelled transition system is deterministic, persistent, and weakly periodic, then it can be decomposed in the sense that there exists a finite set of label-disjoint cycles such that any other cycle is Parikh-equivalent to a multiset of cycles from this finite set. At the end of the talk, a few open questions are discussed. This is joint work with Philippe Darondeau from IRISA in Rennes..
15h00-15h30 : Jean-Baptiste Voron (LIP6),
Evinrude, a tool to build intrusion monitor dedicated to a program
Abstract: Designing security software that evolves as quickly as threats is a truthful challenge. In addition, current software becomes increasingly complex and difficult to handle even for experts. While dealing with security concerns, Monitors and Intrusion Detection Systems (IDS) are approaches that can alleviate these concerns.
In such a context, model checking is a suitable formal technique to analyze concurrent programsÕ execution because automated tools can be designed and operated with very limited knowledge of the underlying techniques.
However, the formal specification must be given using dedicated notations that are not always familiar to engineers and experts (so far, model checking on UML raises complex problems that will not be solved immediately). In the main part of this talk, we present an approach and its realization by a tool (Evinrude) to perform transformations of C source code into Petri nets, a suitable formalism for model checking. This can be used to check statically some structural or reachability properties and to warn about potential dangerous states. To overcome the complexity of the resulting specification, we only focus on specific aspects of the program. Hence, we never model the entire processed program, but only parts which are relevant for our analysis.
In the second part, we detail the building blocks of the program's dedicated monitor in order to detect bad (or suspicious) behaviors during the process runtime.