Seminar details

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.