monkey king

Olivier Ly
Associate Professor
[ research - publications - patent - pre-prints - selected conferences - projects - teaching]

LaBRI
Bordeaux 1 university - IUT A

ly@labri.fr

LaBRI - Université BORDEAUX 1
351, cours de la Libération

33405 Talence CEDEX - FRANCE

office 314 / phone: +33.5.40.00.35.27 / fax: +33.5.40.00.66.69



Research Team: Logic, Automata, Algorithms and Applications - LaBRI.

CRYSCOE Project (ANR SSIA).

Students:
  • P. Andouard
  • C. Thuillet
  • R. Tabary
Past Students:
red wooman (Nicolas Ly - 1999)



Robotics

As a hobby, I am the main architect of the RhoBan project. This consists in designing and realising a biped humanoid robot from scratch as a computer science challenge, like these ones. It started as challenge between friends, and finaly I am very proud to announce that the robot, called RhoBan, is now operational, he can walk, get up, go upstairs ... and even dance! Humanoid Robot RhoBan



Software Security

Nicolas Ly - 1998
My work regarding software security concerns smart card technology. I am interested in two particular aspects of security:

Verification of Security Properties using Formal Methods

In collaboration with J. Andronick  (LRI - AXALTO) and B. Chetali  (AXALTO), I investigate the use of the Coq proof assistant for the formal verification of applet isolation properties in Java Card technology. We focus on the confidentiality property. Our work aims at showing how this property is verified by the embedded Java Card virtual machine card manager and the APIs. We also aim at setting up a verification method which allows to complete specifications and to enhance the secure design of the platform. For instance, we describe how the proof of the integrity puts the light on a known bug. Some
more information about this work can be found in this paper.

Software Counter-Measures against Physical Attacks of Smart Cards

I have been the main architect of the CFED project (Control Flow Error Detection - AXALTO copyright).
This work is developed in collaboration with Louis Goubin from AXALTO company. AXALTO (formerly Schlumberger Systems) is
the smart card and terminal division of Schlumberger Limited.

This technology aims at enforcing semi-automatically counter-measures against fault injection attacks of smart cards. It addresses in a generic way the whole software embedded on the card. In particular, it addresses threats going beyond cryptography-related parts of the embedded software, like threats against the firewall of the Java Card embedded virtual machine, the PIN code verification, etc. Counter-measures are automatically integrated to the source code during the pre-compilation step, according to a guideline defined by the programmer under the form of a set of directives included into the source code. All this technology is developed with  the OCAML language. 

Some more information about this work can be found in this paper; this technology is protected by a patent belonging to AXALTO company.


Infinite Model Theory

My current work in this area concerns the problem of compositionality of specifications of sequential programs.
This consists in deciding in an effective way whether or not a given set of local structural properties of the functions of a program implies a given global behavioural property of the program.

I focus on properties expressed in monadic second-order logic dealing with the control flow of the program and the function calls occuring during its execution. This problem has been investigated in relation with the security of open multi-application smart cards.

I proved that the compositionality is a decidable problem for sequential programs whose control-flow graphs are of tree-width less than a fixed integer value, which includes in particular structured programs.

More information about this work can be found in this paper.
people (Nicolas Ly - 1998)


Publications

Entrusting Remote Software Executed in an Untrusted Computation Helper
with F. Krief and M. Ben MBarka
To appear in proceedings of "Network and Service Security" (N2S'2009), Paris (2009)


A smartcard power analysis simulator
with P. Andouard and C. Thuillet
To appear in proceedings of "IEEE International Symposium on Trusted Computing and Communication", Canada (2009)


Context-free Categorical Grammars
with Michel Bauderon and Rui Chen
To appear in proceedings of "3rd International  Conference on Algebraic Informatics" (CAI'09), Thessaloniki (2009).

Sûreté de fonctionnement et sécurité des algorithmes cryptographiques
with Louis Goubin.
Multi-system & Internet Security Cookbook (MISC) no 42 (2009).

Pullback Grammars are Context-Free
with Michel Bauderon and Rui Chen
proceedings of "4th International Conference on Graph Transformation" (ICGT'08), Leicaster (2008).
LNCS 5214, p366-378. Springer, December 2008.

VisAA: Visual Analyzer for Assembler
with Philippe Andouard, Davy Rouillard
to appear in proceedings of "International Conference on Risks and Security of Internet and Systems"
(CRISIS'08), IEEE, Tozeur (2008)

A constructive solution of the language inequation XA ⊆ BX

proceedings of  "Theory and Applications of Language Equations", Turku.
(TALE'07)
General Publications series
of Turku Centre for Computer Science, 44 p 76-84 (2007). [pdf]

Distance Labeling in Hyperbolic Graphs
with Cyril Gavoille
proceedings of "16th Annual International Symposium on Algorithms and Computation" Sanya China
(ISAAC'05) LNCS 3827, p1071-1081, December 2005. To appear. [pdf]

Compositional Verification: Decidability Issues Using Graph Substitutions
proceedings of  "29th Mathematical Foundations of Computer Science", Prague
(MFCS'2004) LNCS 3153, p 537-549 (2004). [pdf]

Automatic Graph and D0L-Sequences of Finite Graphs
Journal of Computer and System Sciences - JCSS 67:3, p 497-545
(2003). [pdf]

 
Construction of Pseudo-Isometries for Tree-Like Non-Compact 3-Manifolds
Comptes Rendus de l'Académie des Sciences - CRAS 337:7, p 457-460
(2003).[pdf]

Using Coq to Verify Java Card Applet Isolation Properties
with J. Andronick and B. Chetali
proceedings of "16th Theorem Proving in Higher Order Logic", Roma
(TPHOL'2003) LNCS 2758
, p335-351 (2003).
[pdf]

Automatic Graph and Graph D0L-Systems
proceedings of  "25th Mathematical Foundations of Computer Science", Bratislava
(MFCS'2000) LNCS 1893, p 539-548 (2000).


The Weak Monadic Quantifier Alternation Hierarchy of Equationnal Graphs is Infinite
proceedings of "20th Foundations of Software Technology and Theoretical Computer Science", New Delhi
(FST-TCS'2000) LNCS 1974; p188-200 (2000).
[pdf]


On Effective Decidability of the Homeomorphism Problem for Non-Compact Surfaces
Contemporary Mathematics 250, p89-112. AMS (1998).
[pdf]

Etude Algorithmique de Complexes Simpliciaux Infinis
PhD Thesis - Bordeaux 1 University (2000).
[supervisors: G. Sénizergues & Ph. Narbel]



Patent


Procédé de sécurisation d'un dispositif électronique exécutant un algorithme quelconque
contre les attaques
par introduction d'erreur.
with M.-L. Akkar and L. Goubin
European Patent 03290688
5 (Schlumberger, 2003)



Pre-Prints

About the Language Inequation XA subseteq BX
LaBRI
(2007) [pdf]

A Note about Compositional Verification of Sequential Programs.
LaBRI
(2004) [pdf]

Automatic Integration of Counter-Measures against Fault Injection Attacks.
with M.-L. Akkar and L. Goubin
(2003) [pdf]

Classification des surfaces non-compactes planaires à bord
LaBRI (1998)
[pdf]



Selected Conferences

Formal Verification of the Integrity Property in Java Card Technology
with J. Andronick and B. Chetali
E-SMART - Nice 2003

About an Automatic Fault Injection Protection System
with
M.-L. Akkar and L. Goubin
E-SMART - Nice 2003

An Interpretation of the Common Criteria EAL 7 Level:
Formal Modelling of the JavaCard Virtual Machine.
with B. Chetali, E. Giménéz and C. Loiseaux
International Common Criteria Conference (ICCC'2002) - Otawa 2002.

Formal Verification of the Confidentiality Property in Java Card Technology
with B. Chetali
E-SMART
- Nice 2002

Formal Modelling and Verification of the JavaCard Security Architecture:
From Static Checkings to Embedded Applet Execution
with E. Giménéz
VERIFICARD annual meeting - Marseilles 2002.


Programming Project Supervisions

Smv2Java


Teaching

last update: august 2004