![]() |
Olivier
Ly Associate Professor LaBRI Bordeaux 1 university - IUT A ly@labri.fr LaBRI - Université BORDEAUX 1 351, cours de la Libération 33405 Talence CEDEX - FRANCE LaBRI: Office 275 / phone: (+33).5.40.00.84.28 / fax: +33.5.40.00.66.69 [ research - publications - teaching] |
| Research Interests
Team: Formal Methods / Rhoban Project - LaBRI Projects:
Past projects: Students: Past Students:
Habilitation à Diriger des Recherche |
![]() |
| I am
the main architect and designer of the Acroban Humanoid robot. Acroban was born from the RhoBan project supported by the LaBRI, in collaboration with the Inria Flowers project. The project groups some people (academic but not only) interested in the design of autonomous robots (look at it here). The Rhoban project started by the design from scratch of a small humanoid robot called Rhoban able to walk, get up, go upstairs ... and even dance ! Look at him here. News: at the moment, we show ours robots at the international expo in Korea (8 millions visitors). Look at our robots here. |
![]() |
![]() |
My work regarding
software security concerns smart card technology. I am interested
in particular in these 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. |
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. |
![]() |
Exploring robust,
intuitive and emergent physical human-robot interaction with the
humanoid robot Acroban
with Pierre-Yves Oudeyer and Pierre Rouanet.
To appear in 11th IEEE-RAS International Conference on Humanoid Robots (Humanoid'2011) -
2011 (Bled)
Maturational
constraints for motor learning in high-dimensions: the case of biped
walking
with Matthieu Lapeyre and Pierre-Yves Oudeyer.
To appear in 11th IEEE-RAS International Conference on Humanoid Robots (Humanoid'2011) -
2011 (Bled)
Bio-Inspired
Vertebral Column, Compliance and Semi-Passive Dynamics in a Lightweight
Humanoid Robot
with Matthieu Lapeyre and Pierre-Yves
Oudeyer
To appear in proc. of IEEE/RSJ International Conference on Intelligent
Robots and Systems (IROS'2011)
- 2011 (San Francisco) [pdf]
(also selected for
IROS'2011 Special Demonstration Symposium)
Modeling
Maturational Constrains for Learning Biped Humanoid Locomotion
with Matthieu Lapeyre and Pierre-Yves
Oudeyer
To appear in Proc of Int. Conf. on Development and Learning (ICDL)
- Poster session - IEEE 2011 (Frankfurt)
Automated Extraction of Polymorphic Virus
Signatures using Abstract Interpretation
with Renaud Tabary and Serge Chaumette
To appear in proc. of 5th Int. Conf. on Network and System Security (NSS'2011)
- IEEE - 2011 (Milan) [pdf]
The BINCOA Framework for Binary Code Analysis
with Sebastien Bardin, Philippe Herrmann,
Jérôme Leroux, Aymeric Vincent and Renaud Tabary
To appear in proc. of 23rd Int. Conf. on Computer Aided Verification (CAV'2011)
- 2011 (SnowBird, Utah)
Modeling Long Term Signature Validation for
Resolution of Dispute.
with M. Ben MBarka and F. Krief
In proc. of Theory of Security and Applications, TOSCA'2011 (ETAPS
joint event) 2011. To appear in LNCS
Automated Software Protection through Program
Externalization on Memory-Limited Secure Devices.
with S. Chaumette and R. Tabary.
In proc. of IEEE Int.
Symp. on Trusted Computing and Communication (TRUSTCOM'10)
(Hong Kong).
Acroban the Humanoid: Compliance for
Stabilization and Human Interaction.
with P.-Y. Oudeyer.
In IEEE/RSJ Int. Conference on Intelligent Robots and Systems
(IROS'2010) – Video Session (Taipei 2010).
Acroban the Humanoid: Playful and Compliant Physical
Child-Robot Interaction.
with P.-Y. Oudeyer.
In ACM
SIGGRAPH'2010 Emerging Technologies (Los Angeles 2010)
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 Int.
Symp. on Trusted Computing and Communication, (TRUSTCOM'09)
Vancouver.
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
In proc. of "Int. Conf. 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. [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] |