Groupe de Travail Sécurité

Planning

Prochain Exposé

Jeudi 23 Avril 2009 au CTL Alexandre Miquel (ENS Lyon) parlera d'extraction de programmes en logique classique.

Futurs Exposés (prévisionnels pouvant éventuellement changer)

Exposés passés

  1. March 10, 2009 Srdjan Capkun from ETH Zurich,
    Wireless Security gets Physical
    Abstract: This talk is concerned with the impact of the physical layer and physical locations on the security of wireless networks and their applications. We discuss the problem of location verification, and then show how location awareness can enable some basic security primitives like broadcast authentication. We further look at the problem of anti-jamming broadcast communication and show how the limitations of the wireless channel introduce a key-establishment/anti-jamming dependency cycle; we then describe a solution that breaks this cycle.
    Short cv: Srdjan Capkun received the Dipl.Ing. Degree in Electrical Engineering / Computer Science from University of Split, Croatia (1998), and the Ph.D. degree (Docteur es Sciences) in Communication Systems from EPFL (Swiss Federal Institute of Technology - Lausanne) (2004). He was a postdoctoral researcher in the Networked & Embedded Systems Laboratory (NESL), University of California Los Angeles and an Assistant Professor in the Informatics and Mathematical Modeling Department (IMM), Technical University of Denmark (DTU). Since September 2006, he is an Assistant Professor in the Department of Computer Science, ETH Zurich. His main interests are in the design and analysis of security protocols and systems for wireless and wireline networks. http://www.syssec.ethz.ch/people/capkun
  2. February 10, 2009 Cas Cremers from ETH Zurich,
    From Dolev-Yao to Strong Adaptive Corruption: Analyzing Security in the Presence of Compromising Adversaries
    Cas Cremers ETH Zurich, joint work with David Basin
    Abstract: We formalize a hierarchy of adversary models for security protocol analysis, ranging from a Dolev-Yao style adversary to more powerful adversaries who can reveal different parts of principals' states during protocol execution. We define our hierarchy by a modular operational semantics describing adversarial capabilities. We use this to formalize various, practically-relevant notions of key and state compromise. The semantics provide a basis for protocol analysis and we extend an existing symbolic protocol-verification tool, Scyther, to reason about security properties of protocols in the presence of adversaries in our hierarchy. Our tool is the first automated tool that supports notions such as weak perfect forward secrecy, key compromise impersonation, and adversaries capable of so-called strong corruptions and state-reveal queries. As applications, we use our model hierarchy to relate different adversarial notions, gaining new insights on their relative strengths, and we use Scyther find new attacks on protocols that were previously reported to be secure.
  3. Thursday February 12th 2009 : Marc Joye – Thomson Security Labs
    Title: techniques de broadcast encryption, protection de contenu
  4. Jeudi 15 janvier 2009 à 14h00 (report du Jeudi 6 Novembre 2008)

    M2P SCCIS - Industrial Talk
    Thursday November 6th 2008 2pm-5pm : Nicolas Ruff -- EADS-IW
    Title: Windows Security
    Where : amphi D
    Abstract : This session will give an overview of security issues and concepts for Windows :
    • Network and System Administration;
    • Design Principles and Standard Protocols;
    • Vulnerabilities and exploit;
    • Defenses and Protections;
    • Future of Microsoft products : Vista, Windows 2008 and Windows 7.0.
    About : Nicolas Ruff is a French security researcher at EADS-IW (formerly EADS Common Research Center). His main areas of expertise are Microsoft networks security, Windows Mobile security, Computer forensics, Malware protection and analysis, and Wireless security. He published several articles about Windows security in French newspapers, gives trainings on a regular basis, and delivered talks at French & European events such as EuroSec, Microsoft Security Days and SSTIC.
  5. -Embedded System (In)Security Workshop-

    Wednesday 7th of January from 2pm to 6pm in the Amphi H of Ensimag (on Saint Martin d'Heres Campus ).

    This workshop will feature the 3 following talks:
    *2pm-3pm: "Code Injection in Smart Cards" Jean-Louis Lanet, Universite de Limoges, FR.
    *3:15pm-4:15pm: "Practical Attacks on low power microcontroller", Travis Goodspeed, University of Tennessee, Knoxville, USA.
    *4:30pm-5:30pm: "Code Injection in Sensor Networks" Aurelien Francillon, INRIA Rhone-Alpes, projet PLANETE, FR.
    For more information please contact: claude.castelluccia@inria.fr
    Summary of the talks:

    - "Code Injection in Smart Cards" Jean-Louis Lanet:
    We present a method to create an hostile ill-formed applet in Javacard if an attacker has the rights to download applet in the smart card and the card has no bytecode verifier. For this we use two weakness in the Java card specifications 3.0 (the classic edition) : one about static fields not checked by firewall under certain conditions, and another one about the on-board linking process. Once downloaded, our malicious applet is able to search for pattern in other applets (even if they are not in the same package and we have no rights on them) and replace bytecodes to bypass important security checks.

    - "Practical Attacks on low power microcontroller", Travis Goodspeed:
    The Texas Instruments MSP430 low-power microcontroller is used in many medical, industrial, and consumer devices. When its JTAG fuse is blown, the device's firmware is kept private by a serial bootstrap loader (BSL), certain revisions of which are vulnerable to a side-channel timing analysis attack. This lecture concerns the attack in both theory and implementation, including the non-standard serial traffic necessary to expose the password by timing.

    - "Code Injection in Sensor Networks" Aurelien Francillon:
    We will present different code injection attacks on wireless sensors networks. We will see in more details how to exploit program vulnerabilities to permanently inject code into the program memory of an Atmel AVR-based sensor (micaz) . AVR microcontrollers use an Harvard based architecture, it was believed that code injection were impossible on such an architecture. We also show that this attack can be used to inject a worm that can propagate through the wireless sensor network and possibly create a sensor botnet. Our attack combines different techniques such as return oriented programming and fake stack injection. We present implementation details and suggest some counter-measures.
    access information at http://ensimag.grenoble-inp.fr: follow "Plan d'acces" and "Le plan d'acces l'Ensimag sur le campus"
  6. 11/12/2008 - 14:00 - Salle de VERIMAG
    Felix Klaedtke, ETZ Zurich
    http://www.infsec.ethz.ch/people/felixkl
    « Alternation Elimination Constructions with an Application to PSL Extended with Past Operators »
    Abstract :
    Alternating automata have various applications in system verification. In particular, in finite-state model checking when translating declarative specifications into nondeterministic B"uchi automata, the use of alternating automata has led to many practical and theoretical improvements. In this talk, I will first revisit constructions from the literature that translate alternating automata into language-equivalent nondeterministic automata. Here, I will highlight the core ingredient of such alternation-elimination constructions, namely, a reduction to the problem of complementing nondeterministic automata. Then, I will present a novel alternation-elimination construction for so-called loop-free 2-way alternating B"uchi automata. In the last part of the talk, I will utilize this novel construction to improve the automata-theoretic approach for finite-state model checking for the IEEE standardized specification language PSL extended with temporal past operators.
  7. Jeudi 27 Novembre 2008 - 14:00 Wendi Urribarri Verimag "historique"

    Title: Why bother?
    Abstract: Why is a verification tool that generates verification conditions of programs for many systems including Coq, PVS, Isabelle, HOL, Alt-Ergo, Simplify, Z3 and other provers and decision procedures. At the same time, it is an intermediate language for the verification of C programs (using the tool Caduceus) and Java programs (using the tool Krakatoa). Why bother in implementing such a platform? The answer is that implementing a verification condition generator (VCG) for a realistic programming language --- such as C, for instance --- is a lot of work; each construct of the language requires an specific treatment, and usually, there are many of them. So reducing the VCG to a core language seems to be a good approach. Moreover, there are many systems for theorem proving, each having their own language, so if the VCs generated by the tool are to be proved with different systems, then the VCs have to be expressed in those different languages. In this talk, I will present the Why verification platform: a quick introduction to the underlying theory of Why, and some demonstrations of how to work directly in Why to prove programs and how the tool is used with Caduceus and Krakatoa.
  8. Le 2 Octobre Jan Olaf Blech parlera de "Towards Certifying Deadlock-freedom of BIP models"
    Abstract: Verification and validation techniques have become popular in software and hardware development. They increase confidence and potentially provide rich feedback on errors. However, with increasing complexity verification and validation techniques are more likely to contain errors themselves.
    This talk presents ongoing work addressing the problem of guaranteeing the correctness of validation work with respect to a formal notion of correctness: We certify the absence of deadlocks in BIP models that have been checked to be deadlock-free using the D-Finder tool. This means that we establish a certificate for each BIP model considered to be deadlock free. The certificate is a proof script that is used in the Coq theorem prover to prove the absence of deadlocks with respect to a human readable notion of deadlock-freedom and BIP semantics. Certificates are established using information provided by the D-Finder tool. The presented technique allows us to formally prove the absence of deadlocks without having to trust any tools other than Coq.
    It turned out that proving inductive invariants on BIP models in Coq is an important subtask in certifying deadlock-freedom. Apart from this, the talk discusses the overall task of certifying deadlock-freedom, and the Coq formalization of the BIP semantics.

  9. Jeudi 25 Septembre 2008 - 14:00 Iman Narasamdya nous parlera d'EDEN2.

    Abstract: We describe an application of a theory of program properties to the certification of smart-card applications in the framework of Common Criteria. In this framework, a smart-card application is represented consecutively by a model of its specification, a functional specification describing an input-output relationship, a low-level design, and implementation code.
    The certification process consists of the following tasks: (1) prove that the model, the functional specification, the low-level design, and the code satisfy security properties in the smart-card application's specification, and (2) prove that there is a representation correspondence between each two consecutive representations. For each task, a certificate or a collection of certificates are needed to certify the accomplishment of the task.
    The theory of program properties applied to the certification process provides foundations for describing and proving properties of a single program and properties relating two programs. The theory provides a notion of verification condition as a notion of certificate. The theory is applicable to the certification process because all representations of a smart-card application are essentially programs and the representation correspondences are properties relating two programs.
  10. Mardi 2 Septembre 2008 Polyvios Pratikakis
    What: Sound, precise and efficient static race detection for multi-threaded programs.
    Abstract: Multi-threaded programming is increasingly relevant due to the growing prevalence of multi-core processors. Unfortunately, the non-determinism in parallel processing makes it easy to make mistakes but difficult to detect them, so that writing concurrent programs is considered very difficult. A data race, which happens when two threads access the same memory location without synchronization is a common concurrency error, with potentially disastrous consequences.
    We present Locksmith, a tool for automatically finding data races in multi-threaded C programs by analyzing their source code. Locksmith uses a collection of static analysis techniques to reason about program properties, including a novel effect system to compute memory locations that are shared between threads, a system for inferring ``guarded-by'' correlations between locks and memory locations, and a novel analysis of data structures using existential types. We present the main analyses in detail and give formal proofs to support their soundness. We discuss the implementation of each analysis in Locksmith, present the problems that arose when extending it to the full C programming language, and discuss some alternative solutions. We provide extensive measurements for the precision and performance of each analysis and compare alternative techniques to find the best combination.
  11. Mercredi 9 juillet à 14 heures Florent Garnier, nous parlera de deux articles "On Decision Problems for Probabilistic Büchi Automata"[1] de Christel Baier, Nathalie Bertrand et Marcus Grosser (2005) ainsi que "Recognising Omega-regular Languages with Probabilistic Automata"[2]. (2007)
  12. Vendredi 4 Juillet Journée sécurité (programme provioire):
    • 10h30 - 11h Présentation de Jean-Louis Lanet sur le projet Smart Security Devices du laboratoire XLIM
    • 11h - 11H 30 Présentation Vérimag des projets ANR (Pascal)
    • 11h30 - 12h15 exposé vérimag non-interférence computationnelle (Yassine ou Judicaël ou Cristian )
    • 12h15 - 14h : repas
    • 14h - 14h45 : Philippe Gaborit
    • 14h45 - 15h30 : Bruce Kapron
    • 15h30 - 17h : discussions
  13. Jeudi 3 Juillet 2008 - 14:00 Pierre-Louis Aublin : Attaques d'AES par défaut de Cache et Endri Vangjel : Secret Sharing.
  14. Mardi 1er Juillet 2008 - 14:00 - Amphi du CTL
    Mohamad Sawan, Ecole Polytechnique de Montreal (http://www.polystim.polymtl.ca/membres/sawan.html)

    « Wireless multi-channel stimulation and sensing from the cortex: Design, test and validation challenges »

    Abstract: This talk covers biomedical low-power circuits and systems techniques for the construction of smart implantable microstimulators and sensors. High-reliability wireless links are used to power up the implanted devices while bidirectional data are exchanged between implants and external controllers. Such microsystems are dedicated to interface peripheral and central neural systems. Case study of Intracortical dysfunctions monitoring and subsequent treatment will be elaborated. More particularly, monitoring and recording from the primary visual cortex, as well as microstimulation to create vision will be described. Global view of main stimulators/sensors will be given. Special attention will be paid to massively parallel recording and detection of neural signals using flip-chip and multi-chip stacking assembly and packaging techniques. In addition, challenges of test and both in vitro and in vivo validations will be discussed.

  15. Jeudi 26 Juin à 14h0 Laurent Evain (Université d'Angers) nous parlera de Cryptosystèmes basés sur les réseaux.
    Salle à déterminer plus tard (il y a de fortes chaces que ce soit pas à VERIMAG ;-) ).
  16. Jeudi 29 Mai 2008 - 14:00 Iman
  17. Jeudi 22 Mai 2008 - 14:00 Judicael Courant : Isabelle et Coq
  18. Jeudi 15 Mai 2008 - 14:00 Marie-Laure Potet: Presentation du projet POSE
  19. Jeudi 24 Avril 2008 - 14:00 Crisian Ene
  20. Jeudi 10 Avril 2008 - 14:30 au CTL Thèse de Guillaume Salagnac
  21. Jeudi 3 Avril 2008 - 14:00 - Salle de VERIMAG
    Khaled El-Fakih, Visitor at Verimag/American University of Sharjah (UAE) http://www-verimag.imag.fr/~elfakih/
    « Extended Finite State Machine Based Test Derivation Driven By User Defined Faults »
    RÉSUMÉ :
    Test derivation based on user defined faults deals with the generation of tests that check if some parts of a given specification are correctly implemented in a corresponding implementation. In this work, we present a method for test derivation based on user defined faults for Extended FSM (EFSM) specifications. Given an EFSM specification ES and a set of selected transitions of ES, the method returns a test suite that is complete with respect to output and transfer faults at the selected transitions, i.e., checks whether the selected transitions are correctly implemented in a corresponding EFSM implementation. Test derivation is based on a formally defined fault model (conformance relation and types of faults) and is guided by some conditions established for complete test derivation. To reduce test derivation efforts, we propose to use appropriate slices of the specification EFSM. The slices, on one hand, preserve the facilities of the original specification (before slicing) EFSM for traversing the selected transitions and for distinguishing their final states and on the other hand, these slices are much smaller than the given specification. Application examples and a simple case study are provided.
  22. Jeudi 27 Mars 2008 - 14:00 - Salle de VERIMAG
    Susan L. Graham, University of California Berkeley, CA http://www.cs.berkeley.edu/~graham/
    « The Challenge of Programming »
    RÉSUMÉ :
    The history of software development goes back more than 60 years, yet it remains challenging. Some people see better programming languages and better hardware design as the solution. Others emphasize software design methodologies, analysis, testing, and re-use. My own research has focused on tools. In this talk, I will summarize some recent work by my group on the use of speech, on the use of transformations, and on some approaches to parallelism.
  23. Jeudi 12 Mars 2008 Jean-Francois Monin presentattion de F91 à 14h00.
  24. Jeudi 5 Mars 2008 Manuel Granacho prsentation d'un papier sur "paramodulation-based theorem proving"
  25. Mardi 4 Décembre 2007 Philippe Bidinger présentation
  26. Jeudi 29 Novembre 2007 GDT consacré au projet SCALP animé par Judicael Courant.
  27. Jeudi 22 Novembre 2007 Sylvain Boulmé : Calcul de raffinement en Coq.
    Résumé: dans cet exposé, je montrerai comment le calcul du raffinement permet de marrier très finement deux formes de raisonnements sur les programmes: d'une part, les raisonnements "algébriques" (i.e. par "transformation de programmes" sur une congruence) et d'autre part, les raisonnements à la Hoare par pré/post-conditions. Marrier ces deux formes de raisonnements est utile dès qu'on veut mélanger "effets de bords" et ordre sup. Un exemple typique: on peut modéliser un jeu à 2 joueurs comme une fonction paramétrée par 2 joueurs où chaque joueur est vu comme un programme impératif non-déterministe. Le raffinement permet typiquement de raisonner sur une telle fonction de jeu: stratégie optimale, raffinement de joueur, etc. Dans l'exposé, j'illustrerai cela sur le jeu de Nim.
  28. Jeudi 15 Novembre 2007 Pierre Louis Aublin : Attaques par canaux cachés sur AES.
  29. lundi 12 Novembre 2007 à 16h00, grande salle VERIMAG, Boris Köpf ETH Zürich : Formal Models for Side-Channel Attacks.
  30. Jeudi 8 Novembre 2007 Takoua Abdellatif : CIVITAS un systeme de vote electronique réélement implementé.
  31. Jeudi 18 Octobre 2007 Pascal Lafourcade Comparing State Spaces in Automatic Security Protocol Verification. join Wrok with Cas Cremers.
    Abstract: Many tools exist for automatic security protocol verification, and most of them have their own particular language for specifying protocols and properties. Several protocol specification models and security properties have been already formally related to each other. However, there is a further difference between verification tools, which has not been investigated in depth before: the explored state space. Some tools explore all possible behaviors, whereas others explore strict subsets, often by using so-called scenarios. Ignoring such differences can lead to wrong interpretations of the output of a tool. We relate the explored state spaces to each other and find previously unreported differences between the various approaches. We apply our study of state space relations in a performance comparison of several well-known automatic tools for security protocol verification. We model a set of protocols and their properties as homogeneous as possible for each tool. We analyze the performance of the tools over comparable state spaces. This work allows us for the first time to compare these automatic tools fairly, i.e., using the same protocol description and exploring the same state space. We also propose some explanations for our experimental results, leading to a better understanding of the tools.

Divers

Membres