*salle A. Turing CE4*

5 février 2015 - 14h00

Verimag PhD seminars 1

par Seminaires doctorants 1 de Verimag

Abstract: 14:00-14:35: Josselin Feist

Binary analysis to assist detection and exploitability of

vulnerability related to dynamic memory management

(supervision Parie-Laure Potet)

Vulnerability detection aims to find software bugs that could be

exploited by malicious users to hijack the program execution or to

access sensible data. My work focus on a specific vulnerability

called use-after-free. In this presentation I will introduce the

used of a static analysis developed during my first year, allowing

to detect use-after-free in binary code. Then I will talk about

preliminary results and how to improve it. I will conclude with

some ideas to go further, and how to combine these results with

a symbolic / concolic execution, in order to create a proof of

concept of the vulnerability.

14:45-15:20 Tommaso Dreossi

Parameter Synthesis for Polynomial Dynamical Systems

(supervision Thao Dang)

Parameters are often used to tune mathematical models and capture

nondeterminism and uncertainty in physical and engineering systems.

This presentation is concerned with parametric dynamical systems and

the problem of determining the parameter values that are consistent

with some expected properties. We consider properties specified by

a fragment of STL (Signal Temporal Logic), which allows us to deal

with complex behavioral patterns. We propose an abstract algorithm

for parameter synthesis with respect to a property specified using

the considered logic. It exploits reachable set computations and

forward refinements. We instantiate our algorithm in the case of

polynomial dynamical systems exploiting Bernstein coefficients and

we illustrate it on an epidemic model.

15:30-16:05 Thomas Ferrere

Quantitative Assertion-Based Verification of Mixed-Signal Systems

(supervision Oded Maler)

In this thesis we aim to extend theoretical work in continuous time linear temporal logic, and apply it to practical problems encountered in the design of Analog and Mixed-Signal Systems on Chip. Run-time verification is well established in the discrete domain, and used routinely for the verification of digital circuits modeled as discrete events systems. This is known in the field of electronic system design as Assertion-Based Verification, where an assertion consists in a property formalized in a languages based temporal logic and regular expressions, such assertions being monitored during repeated simulations of a model of the circuit in its design stage.

The systematic verification of systems operating in the continuous domain however is almost limited to academic work. Analog circuit designs are checked for possible failures through various ad-hoc techniques, which make their integration in a digital environment hard to verify. Mixed signal systems emerging from this integration can be modeled as hybrid systems, describing the temporal evolution of states through continuous modes (analog behavior) and switching logic (digital control). Our work aims to address two issues emerging in this framework: the behavior is no longer discrete-time, finite-state but continuous-time, with a continuous state space. This talk will focus on that second issue, which we addressed in two complementary works.

We will first present a generalization of temporal logic to quantitative monitoring. Such an extension allows not only to know if a continuous time behavior satisfies a temporal logic property, but also how far from satisfaction or violation is the observed behavior. Algorithms have been proposed to efficiently estimate such a distance measure, allowing to perform computations with a small overhead as compared to the simpler pass/fail problem.

We will then present a technique to compute other measures that are closely related to the application domain. Analog circuits are characterized by a variety of indicators, measuring some aspect of their transfer function. Examples include: slew rate, duty cycle, rise time, average current consumption, etc. Based on recent work on temporal patterns introduced as a continuous-time extension of regular expressions, we present a unified language to formally define such measurements and covering most of the aforementioned examples. Algorithms are given to repeatedly extract in a simulation trace arbitrary measurements based on this language.