salle A. Turing CE4
12 February 2015 - 14h00
Verimag PhD seminars 2
by Seminaires doctorants 2 from Verimag
Abstract: 14:00-14:35 Dogan Ulus
Monitoring Timed Regular Expressions
(supervision Oded Maler)
Timed level of abstraction is extremely useful to model systems
with real-time constraints. Once such systems are modeled as timed
systems, properties with timing information can be specified using a
variety of different formalisms such as temporal logics and regular
expressions. In this work we use timed regular expressions (TRE)
as a compact but highly-expressive pattern specification language
in the spirit of discrete case. Then we present techniques to report
all instances of a given pattern over individual behaviors of timed
systems and experiments done with our implementation.
14:45-15:20 Laurent Lemke
Shared self-configuring models and software infrastructures
for Smart City monitoring and control.
(supervision Florence Maraninchi)
Most city-scale ICT applications rely on their own vertically
integrated and dedicated infrastructure, foregoing the benefits
that could result from sharing sensors, networks, software enablers
and, crucially, consolidated data and information originating from
these. The objective of this research project is to evolve to a
shared horizontalized software infrastructure, a shared middleware
platform, providing proxies of physical entities to different smart
city applications. These proxies have to capture the essential timing
and reactivity properties of these entities in order to monitor and
control them. They also have to rely on a hierarchy of models that,
together, are generic enough to be automatically matched to the
corresponding entities.
15:30-16:05 Louis Dureuil
Assessing smartcard robustness against fault injection attacks
(supervision Marie-Laure Potet)
Due to today's world pervasiveness of smartcard products (banking,
telephony, ...), failure to ensure their security properties would
result in massive scale fraud.
In response to this threat, smartcard products undergo a
certification process at a dedicated laboratory that evaluates its
security. In particular, this process includes an evaluation of
robustness against pertubation attacks, which are performed using
a laser or EM probes, and result in fault injection in the code
of the application. The current evaluation of robustness against
fault injection is subdivided in two subprocesses, namely the code
review and the physical tests. The current process is challenged
by several factors: there is no direct correspondance between
the vulnerabilities found during code review and during physical
tests, the code review is performed manually and relies heavily on
the evaluator's expertise, and the evolution in the state of the
art of physical attacks introduces the ability to inject multiple
faults during the course of one execution which further complicates
the evaluation.
To tackle these challenges, we aim at automating the currently manual
code review using dynamic code analysis and specifically designed
oracles able to tell whether the injection of a fault result in a
successful attack. Furthermore, we propose a new approach to rate
the attack potential of a product using the device characteristics
and the code of the application, as opposed to the traditional
methods that require us to perform physical attacks on card for
each application.
16:15-16:50 Hela Guesmi
Validation of specifications in hard real-time applications
(supervision Saddek Bensalem)
In hard real-time embedded systems, design and specification
methods and their associated tools must allow development of
temporally deterministic systems and therefore reproducible,
to ensure their safety. To achieve this goal, we have special
interest in methodologies based on the time-triggered paradigm. In
this context, number of properties, in particular, end-to-end
real-time constraints, are being met by-construction. However,
ensuring correctness and safety of such systems remains a
challenging task. Existing development tools do not guarantee
by-construction specification respect, they must generally be
verified a-posteriori. With the increasing complexity of embedded
applications, that of their validation becomes, at best, a major
factor in the development costs and at worst simply impossible. It is
necessary, therefore, to define a method that allows the development
of correct-by- construction systems while structuring and simplifying
the specification process.
Research work on Rigorous Design Flow present a coherent and
accountable model-based process leading from requirements
to correct-by-construction implementations. We are specially
interested in component-based constructions that allow deriving
progressively an implementable system model by source-to-source
automated transformations.
The goal of this thesis is to define a methodology for the
development of correct-by-construction systems for target
platforms based on time-triggered paradigm. The challenge is to
apply the rigorous design flow to the Time-triggered domain, in
order to provide correctness-by-construction as an alternative
to a-posteriori verification, while taking full advantage of
predictability and determinism provided by the time triggered
paradigm.
