Seminar details
Abstract: PhD students present their work.
- 14:00 Maxime Puys: Cybersecurity in industrial systems, from packet filtering to formal methods
Abstract :
Recently medias are showing an increasing number of attacks against in-
dustrial systems. Such attacks become feasible because these systems
are recently spreading geographically and communicating more and more
through unsafe mediums like Internet. As industrial systems historically
have been isolated from the rest of the world, there cybersecurity does
not meet the level of our daily-life machines which are used to be targeted
by hackers around the world. People are starting to realize that industry
must quickly enhance its cybersecurity level to avoid massive attacks such
as Stuxnet in Iran.
Within this thesis, we look at different ways to increase the security
level of industrial systems and blend in usual formal methods of security.
We first look at applicative filtering of industrial protocols and we pro-
pose rules to detect or block malicious packets relying on the semantics
of the messages. Then we use classic protocol modelization tools such as
Proverif to check the security properties that are claimed by these proto-
cols. Finally, we design a formal model to express the behavior of possible
attackers in a system and to generate attack scenarios.
- 14:40 Alexandre Rocca: Application of Formal Methods to Biological System Modelling
Modelling complex biological systems as differential equations mostly results in non-linear, high-dimensional, and stiff models. The validation of those models according to experimental results is often done with simulation. Moreover, to cope with the uncertainty of real biological systems, and to expand the experimental results to a more robust model, set-based parameters are used.To validate a large set of initial states and parameter values, a large number of simulation runs is needed. However, the result, being non-exhaustive, is not guaranteed. Formal verification techniques allow proving properties, with set-based reachability computation techniques, by replacing simulation runs with conservative sets of trajectories. Applying the Bernstein expansion of polynomials, we developed a reachability tool on polynomial systems with uncertain parameters. This tool takes advantage of the particular forms of the polynomials modelling of biochemical networks to speed up the Bernstein expansion.This allows a faster verification of complex biological systems. The tool is directly applied on a real system (Iron Homeostasis project). It is developed in collaboration with a biological experimentation team (LBFA, Grenoble) to address the needs of biologists.
- 15:20 Alexandre Maréchal: Polyhedral approximation of polynomials for both abstract interpretation and SMT-solving
Abstract :
The Verified Polyhedra Library (VPL), developed by A. Fouilhé, is an abstract domain of convex polyhedra.
It has the particularities to use constraint-only representation of polyhedra and to produce witnesses certifying the result correctness.
Our goal is to extend the VPL to deal with polynomial guards such as -2 + z*(x*x - x*y) <= 0, that appear for instance in crucial computations of tennis ball trajectories.
It means computing a polyhedral over-approximation of the semi-algebraic set {(x,y,z) in Q^3| -2 + z*(x*x - x*y) <= 0}.
For this purpose, we designed an algorithm based on the Handelman's representation of positive polynomials and parametric linear programming.
The solution is obtained using the parametric simplex algorithm, that we are also currently trying to improve.
With this extension, the VPL can now over-approximate sets defined by linear and polynomial constraints.
This gives us plenty of research perspectives: for instance, it makes the VPL usable in SMT-solving, where infeasibility of semi-algebraic sets has to be decided.
When our algorithm is able to show infeasibility, the witness that we generate can be used as a lemma for pruning further explorations.
Otherwise, contrary to many other decision procedure, we still provide a polyhedral over-approximation of the semi-algebraic set, which can also be used as a lemma.
We plan to integrate the VPL as a polyhedral polynomial library in FramaC, where it could be used either in the abstract interpretation plugin Value, or in the SMT one.
- 16:00 Nikos Kekatos: Verification of hybrid systems with set-based and simulation-based methods
Hybrid systems exhibit both continuous and discrete behaviors. They can be modeled by combining finite state automata with continuous variables expressed by a set of differential or algebraic equations. Albeit hybrid systems arise very often in practice (i.e. when a digital controller interacts with a physical plant), analyzing and numerically simulating them remains a difficult task. The applicability of analytical methods is rather limited, whereas traditional model-based methods may fail to detect safety critical behaviors. In this talk, two different verification approaches will be presented. The first one is set-based reachability analysis. The focus will be on flowpipe computation, which combines ideas from time discretization, numerical integration and computational geometry. The second approach is trajectory/simulation based and relies on sensitivity analysis. We test both methods on case studies with the SpaceEx platform and Breach toolbox respectively.
