Employment
I'm currently an assistant professor in the
Department of Computer Science at
Aalborg University within the
Distributed Systems and
Semantics unit. As a member of the DSS unit, I teach and I do
some research.
Research
My two main topics are Software Verification and Computer
Security. A third topic, Optimum Controller Synthesis,
seems to be promising in the context of
CISS.
- Software Verification:
My main interests lies in model-checking and more precisely in
Timed Automata and Hybrid Systems. I did my
Ph. D. on this topic in collaboration with my advisor
Antoine Petit and
Patricia Bouyer and
Catherine Dufourd. We have extended Timed Automata with more expressive
updates (Updatables Timed Automata). We proved that a big fragment of
this model is still decidable for the reachability problem
[BDFP00a] and that this
extension is non-trivial
[BDFP00b].
I have extended my interests to all software verification techniques,
including static analysis, abstract interpretation, and few theorem
proving techniques. Recently, in collaboration with
Patricia Bouyer,
Kim G. Larsen
and Gerd Behrmann,
we described a method based on location dependent region
graph and we did an implementation of a prototype based on
Uppaal
[BBFL03].
- Computer Security:
I am working on this topic in collaboration with
Mikkel Christiansen. We
are very focused on firewalls for the moment. Actually, there is
plenty of work in this field. The network filtering techniques are
still very basic and not really well founded. We have done some work
on packets classification and on stateful inspection. We might be
interested to look for IDS systems afterward.
Our main contribution is to use decision diagrams in order to
represent the network filter of a firewall
[CF02]. Indeed, this
representation has two main advantages, the first one is that it turn
the filter into a predicate logic formula (soundness) and the second
one is that the complexity of the filtering operation is no more
depending of the number of rules that you have in your filter
(efficiency). Moreover, it appears that this decision diagram
representation of a firewall can be used to modelize networks and
perform some checks on it. Some of my
students did a
very complete preliminary work about it
[NAV02].
- Optimum Controller Synthesis
I've started to do some work on optimum controller synthesis in
hybrid systems. I still have a lot to learn in this topic. I am
working in collaboration with
Franck Cassez
and Kim G. Larsen (and I
am learning a lot from both of them). Patricia Bouyer
(ACI Cortos)
joined the team and we produced this
report.
List of
Publications and Writting.
Teaching
Second Semester 2004
- Course of Test og Verifikation (DAT-8) with Kim Larsen:
I do part of the course of
Test and
Verification this semester
(see also here).
- Algorithm and Architecture II (Datateknik D4):
I also give the course of
Algorithm and Architecture II
about computer architecture and algorithms (mainly
data-structures).
- Umbrella Project (DAT-6):
I am supervising three master students which are working on an
implementation of a Mandatory Access Controlled Linux with
authentication of the binaries on PDA/Mobile phones
(Umbrella Project).
Recent Talks/Courses
Recent Talks and Courses ... Soon available
("Soon" is still undefined :-)).
List of
Talks and Courses.
Code and Hacks
I do some code sometimes:
I am also debugging the Debian
testing/unstable
(active bugs,
archived
bugs) and some other stuff
(Alsa drivers,
Mozilla, ...).
Miscellaneous
- Curriculum-Vitae.
- GPG key.
- The movie "Matrix Reloaded" is
featuring the famous
nmap network scanning software
and a famous
flaw
of SSHv1.
Here are the command lines typed by Trinity
to hack through another computer.
Hollywood should learn from this !!! :-)
|