BrittSec - The Brittany Security Agenda

Séminaire méthodes formelles et sécurité - 2 mars 2012 - 11h

2012-02-21T08:47:00.002+01:00

INRIA / IRISA - Rennes - salle Turing. inscription lydie(.)mabil(@)irisa(.)fr

Roberto Giacobazzi, Université de Vérone : Obfuscation by Partial Evaluation of Distorted Interpreters

How to construct a general program obfuscator? We present a novel approach to automatically generating obfuscated code P' from any program P with source clear code. Start with a (program-executing) interpreter Interp for the language in which P is written. Then “distort” Interp so it is still correct, but its specialization P' with respect to P is transformed code that is equivalent to the original program, but harder to understand or analyze. Potency of the obfuscator is proved with respect to a general model of the attacker, modeled as an approximate (abstract) interpreter. A systematic approach to distortion is to make program P obscure by transforming it to P' on which (abstract) interpretation is incomplete. Interpreter distortion can be done by making residual in the specialization process sufficiently many interpreter operations to defeat an attacker in extracting sensible information from transformed code.

Our method is applied to: code flattening, data-type obfuscation, and opaque predicate insertion. The technique is language independent and can be exploited for designing obfuscating compilers.

Joint work with Neil D. Jones and Isabella Mastroeni

Séminaire méthodes formelles et sécurité - 20 janvier 2012 - 11h

2012-01-20T11:00:00.001+01:00

INRIA / IRISA - Rennes - salle Turing. inscription lydie(.)mabil(@)irisa(.)fr

David Basin (ETH Zurich): Policy Monitoring in First-order Temporal Logic

In security and compliance, it is often necessary to ensure that agents and systems comply to complex policies. An example from financial reporting is the requirement that every transaction of a customer, who has within the last 30 days been involved in a suspicious transaction, must be reported as suspicious within 2 days.
We present an approach to monitoring such policies formulated in an expressive fragment of metric first-order temporal logic. We also report on case studies in security and compliance monitoring and use these to evaluate both the suitability of this fragment for expressing complex, realistic policies and the efficiency of our monitoring algorithm.

Thèse - Arnaud Jobin - 16/01/2012 - 10h30

2012-01-16T09:07:00.002+01:00

Arnaud Jobin : Dioïdes et idéaux de polynômes en analyse statique

Campus de Cachan - Salle du Conseil - Antenne de Bretagne (Ker Lann)

SSTIC 2012 : encore 6 semaines pour soumettre

2012-01-04T18:54:00.003+01:00

Vous avez encore jusqu'au 17 février pour soumettre une proposition au SSTIC.

http://www.sstic.org/2012/cfp/

Rennes Cryptography Seminar - Nov, 18 2011 - 14:00

2011-11-18T14:00:00.000+01:00

Salle 016, IRMAR (rez de chaussée, bâtiment 22), Université de Rennes 1, Campus de Beaulieu.

Ivica Nikolic Automatic search of related-key differential characteristics: Applicationsto AES and DES

he differential attack is one of the most widely used approaches in cryptanalysis of block ciphers and hash functions. It was used in the attacks on the two encryption standards DES and AES. To launch this attack, the cryptanalyst has to find a differential - an input difference for the cipher that propagates to output difference with a probability higher than in a pseudo-random permutation. The input difference can be only in the plaintext (single-key differential attack) or in both the plaintext and the key (related-key differential attack). The differential can be seen as a collection of differential characteristics - round-by-round differences that lead from the input difference to the output difference. The task of finding single-key differential characteristics usually is the most difficult part of the attack since these characteristics in most of the cases are found manually - an effort that requires days of inspecting the internal structure of the cipher. Moreover, the search of related-key characteristics is always by hand. We present algorithms for automatic search of related-key characteristics by efficiently eliminating the requirement for the full search of the brute-force space of characteristics. The elimination is achieved by counting the number of active S-boxes in each round of the cipher. In the cases of byte-oriented ciphers, a special internal representation of the ciphers additionally reduces the search complexity by reducing the branching. Our approach is applied to several block ciphers including DES and AES. We also show relation between the search problem and the problem of finding a path with minimal weight in a graph.T

Séminaire méthodes formelles et sécurité - 18 novembre 2011 - 11h

2011-11-18T11:00:00.003+01:00

INRIA / IRISA - Rennes - salle Turing. inscription lydie(.)mabil(@)irisa(.)fr

Where is my Vote? - Formal Analysis of Electronic Voting Protocols

Steve Kremer, INRIA

Security protocols are distributed programs which aim at establishing security guarantees, such as confidentiality, authentication or anonymity, while being executed over an untrusted network. Nowadays, security protocols are present in many aspects of our everyday life: electronic commerce, mobile phones, e-banking, etc. Symbolic methods, which often come with automated tool support, have shown extremely useful for finding structural flaws in such protocols or proving their absence.

In this talk we report on our efforts carried out over the last years to apply such techniques to electronic voting protocols. The specificities of electronic voting have raised several challenges: they make use of esoteric cryptographic primitives and need to guarantee complex security properties, such as receipt-freeness or verifiability. We have modelled and analyzed such protocols and their properties in the applied pi calculus, a formal language for expressing security protocols. Formally defining the protocols and properties allowed us to highlight many (hidden) assumptions and has shown to be a non trivial task in itself. Regarding automated analysis, this line of work raised a number of challenges in formal analysis of security protocols, some of which are still the subject of active research.

Workshop Gossple - Nov, 18 2011 - 9:00-12:30

2011-11-18T09:00:00.000+01:00

Diagnosis, Resilience, and Privacy in Tomorrow’s Distributed Systems

Salle Métivier (C024), IRISA, Université de Rennes 1

Talk 1: “Diagnosis in Practice”
Richard D. Schlichting. AT&T Labs, Florham Park, NJ, US

Talk 2: “Whisper: Middleware for Confidential Communication in Large-Scale Networks”
Pascal Felber, Université de Neuchâtel, Neuchâtel, Switzerland

Talk 3: “Architecting Resilient Computing Systems: Overall Approach and Open Issues”
Jean-Charles Fabre, LAAS-CNRS, Toulouse, France

Talk 4: “Generalizing Universaility”
Rachid Guerraoui, Ecole Polytechnique Federale de Lausanne (EPFL), Lausanne, Switzerland

Grafotech Veille - mardi 15 novembre 2011 - 12h30

2011-11-08T17:45:00.002+01:00

à la Cantine Numérique

La veille e-réputation décryptée

Inscriptions

Rennes Cryptography Seminar - Oct, 21 2011 - 14:00

2011-10-21T14:00:00.001+02:00

Salle 016, IRMAR (rez de chaussée, bâtiment 22), Université de Rennes 1, Campus de Beaulieu.

Polynômes d'Eisenstein spéciaux engendrant les extensions totalement ramifiées, identification des extensions et réalisation des corps de classes

Soit $K$ un corps local de corps résiduel fini. On présentera une famille de polynômes d'Eisenstein avec la propriété que chaque extension séparable totalement ramifiée $L/K$ est engendrée par au moins un polynôme dans la famille, tandis que le nombre de polynômes engendrant $L/K$ est plus petit que $\#Aut(L/K)$. On décrira des algorithmes pour retrouver les polynômes spéciaux correspondants à une extension, pour identifier les extensions et pour obtenir le seul polynôme engendrant le corps de classes correspondant à un sous-groupe des normes.

Séminaire méthodes formelles et sécurité - 21 octobre 2011 - 11h

2011-10-21T11:00:00.001+02:00

INRIA / IRISA - Rennes - salle Turing. inscription lydie(.)mabil(@)irisa(.)fr

Keqin Li (SAP Research): Model Checking based Security Testing of Web-based Applications

Model checking and security testing are two verification techniques available to help finding flaws in security sensitive, distributed applications. In this presentation, we present an approach of security testing of web-based applications in which test cases are automatically derived from counterexamples found through model checking. We illustrate our approach by discussing its application against a flawed version of the SAML-based Single Sign-On for Google Apps.

C&ESAR approche, 28-30 novembre 2011

2011-10-19T09:04:00.003+02:00

Thèse - Ana Charpentier - 21/10/2011 - 10h45

2011-10-17T10:04:00.000+02:00

Salle Métivier à l'IRISA (Rennes).

Soutenance de thèse, Ana Charpentier : Identification de copies de documents multimédia grâce aux codes de Tardos.

La plupart des mécanismes de détection des anomalies au niveau applicatif reposent sur la détection de la déviation du flot de contrôle d'un programme. Cependant, ces méthodes ne permettent pas de détecter des attaques qui ciblent les données de calcul utilisées par les processus. Pour compléter ces mécanismes de détection, nous proposons une méthode pour contrôler la corruption de données de calcul. Cette approche repose sur la construction d'un modèle de comportement orienté autour des variables et construit par analyse statique du code source. En utilisant Frama-C, un outil d'analyse statique développé par le CEA, nous avons implémenté notre approche pour les programmes écrits en langage C. Pour évaluer plus en détails notre mécanisme de détection, nous proposons aussi une méthode pour simuler des attaques contre les données de calcul. Cette approche repose sur un modèle de faute qui reproduit l'état interne d'une application après ce type d'attaque. Nous avons implémenté une plateforme d'évaluation en combinant notre modèle de faute avec un mécanisme d'injection en mémoire.

Jury

Sylvain Duquesne (IRMAR, Rennes)
Gaetan Le Guelvouit (Orange Labs, Rennes)
Philippe Gaborit (Université de Limoges), Rapporteur
William Puech (Université de Montpellier), Rapporteur
Caroline Fontaine (STICC-Lab, Brest) directrice de thèse
Teddy Furon (IRISA, Rennes), co-directeur de thèse

SSTIC : Appel À Contributions

2011-10-10T18:37:00.000+02:00

======================================================================
SSTIC 6-7-8 juin 2012
Appel à contributions
======================================================================

* Soumission : 17 février 2012
* Notification aux auteurs : 6 mars 2012
* Versions finales (Word) : 23 mars 2012
* Versions finales (LaTeX) : 30 mars 2012
* Symposium : 6-7-8 juin 2012

Le SSTIC est une conférence francophone qui rassemble chaque année
plus de 400 participants intéressés par la sécurité des systèmes
d'information. Les aspects liés à ce thème y sont abordés de façon
approfondie, didactique et prospective. Si la conférence privilégie
les contributions techniques et/ou scientifiques, celles ayant trait
aux aspects juridiques, réglementaires ou organisationnels sont aussi
considérées. La dixième édition de la conférence aura lieu sur le
campus Beaulieu, à Rennes.

== Soumissions ==
Les auteurs soumettent un document d'au moins 7 pages de texte,
accompagné d'un plan détaillé de l'article final. Ce texte doit
permettre au comité de programme de juger de l'originalité et de
l'intérêt de la proposition. Les auteurs s'attacheront donc à décrire
le coeur de leur contribution, plutôt que de fournir uniquement une
introduction de leur article. Les soumissions se font en ligne sur
www.sstic.org. Un même auteur peut effectuer plusieurs soumissions.
Chaque soumission est évaluée par au moins 3 membres du comité de
programme. En cas d'acceptation, les auteurs rédigent la version
finale de l'article, de 35 pages maximum, en tenant compte des
remarques. Les articles des éditions précédentes sont sur
actes.sstic.org

== Thèmes ==
Tous les aspects liés à la sécurité des systèmes d'information sont
considérés. SSTIC attache en effet beaucoup d'importance à réunir
l'ensemble des acteurs impliqués dans la sécurité et souhaite mêler
les questions scientifiques et les problèmes techniques.
Les démonstrations et les preuves de concepts sont encouragées. Les
propositions présentant une analyse sérieuse et complète d'un produit,
un retour d'expérience ou un comparatif fondé sur des tests
reproductibles sont examinées. Les articles destinés à la promotion
d'un produit ne sont pas acceptés.

== Dix ans ==
À l'occasion du dixième anniversaire de la conférence, les articles
rétrospectifs proposant un point de vue pertinent sur l'évolution
de la sécurité au cours des dix années passées seront
exceptionnellement considérés.

== Formats ==
Les articles retenus sont rassemblés dans un ouvrage constituant les
actes du symposium. Les articles doivent être au format LNCS de
Springer, en LaTeX ou en Word. Les modèles sont disponibles:
* ftp://ftp.springer.de/pub/tex/latex/llncs/latex2e/llncs2e.zip
* ftp://ftp.springer.de/pub/tex/latex/llncs/word/LNCS-Office2007.zip

== Calendrier ==
En soumettant, les auteurs s'engagent à respecter le calendrier. Dans
le cas contraire, le comité de programme se réserve la possibilité
d'annuler et remplacer l'intervention.

== Résumé français/anglais ==
Les auteurs sont encouragés à soumettre un double résumé français et
anglais afin de donner une meilleure visibilité à leur article au
niveau international.

== Durée des présentations ==
Les présentations durent 30 minutes, questions incluses. En cas de
débordement les interventions sont susceptibles d'être coupées afin
de respecter l'emploi du temps.

== Financement ==
Le comité d'organisation souhaite encourager et soutenir les
initiatives se rapportant à la sécurité des systèmes d'information.
Les auteurs ayant un article accepté mais ne pouvant subvenir
eux-mêmes aux frais (étudiant, demandeur d'emploi...) peuvent faire
une demande d'aide au financement auprès du comité d'organisation.

== Informations ==
Liste de diffusion : annonces(at)lists.sstic.org
* Inscription : annonces-subscribe(at)lists.sstic.org
* Désinscription : annonces-unsubscribe(at)lists.sstic.org

Comités d'organisation et de programme sur la page du comité.
* Contact : contact(at)sstic.org
* Comité d'organisation : co(at)lists.sstic.org
* Comité de programme : cp(at)lists.sstic.org

SSTIC est une association loi 1901 (n° 0300161442).

Séminaire méthodes formelles et sécurité - 7 octobre 2011 - 11h

2011-10-07T11:00:00.001+02:00

INRIA / IRISA - Rennes - salle Turing. inscription lydie(.)mabil(@)irisa(.)fr

Bruno Blanchet (ENS), Stéphanie Alt (DGA-MI): Automatic verification of security protocols, the tools ProVerif and CryptoVerif

This talk will present two security protocol verification tools:
- The tool ProVerif works in the formal, Dolev-Yao model. It can prove security properties for an unbounded number of sessions of the protocol. It supports cryptographic primitives defined by rewrite rules or by equations, and can prove secrecy, authentication, and some process equivalences.
- The more recent tool CryptoVerif works in the computational model of cryptography. It produces proofs by sequences of games, like the manual proofs of cryptographers. It provides a generic method for speficying the assumptions on many cryptographic primitives, and can prove secrecy and authentication.

OSSIR Bretagne - 4 octobre 2011 - 14h15-17h00

2011-10-04T14:15:00.002+02:00

La séance aura lieu dans les locaux de Télécom Bretagne, à Cesson-Sevigné.

Olivier HEEN (Technicolor) : retour sur la conférence ESORICS 2011

Erwan Abgral (Kereval) : retour sur la conférence hack.lu 2011

Séminaire méthodes formelles et sécurité - 30 septembre 2011 - 11h

2011-09-30T11:00:00.000+02:00

INRIA / IRISA - Rennes - salle Turing. inscription lydie(.)mabil(@)irisa(.)fr

Christèle Faure (Safe River): Software security assessment based on static analysis

Software security evaluation has been largely automated: several hundred of tools are meant to facilitate the elimination of security holes, vulnerabilities or flaws for a large panel of programming languages (C, C++, Java, Ada, Perl, Python, PHP ...). Amongst these tools, one can find: commercial or research tools, focused on various aspects of security, and based on several technologies. This makes the choice of tools with respect to security objectives really difficult for any user.

The main security issues which are addressed by existing tools are the threefold:
- Identification of “dangerous function calls”, by syntactic analysis;
- Detection of dangerous patterns and detection of patterns that do not conform to design and coding rules, based on pattern analysis;
- Proof that an application is “error-free” and “weaknesses-free” by semantic analysis (abstract interpretation), with respect to secure execution and secure behavior.

Existing tools implement different analysis methods: syntactic analysis, pattern analysis, abstract interpretation, each of them enables to detect different errors classes or enables to verify different security rules. They also are different in terms of selectivity, soundness and precision. Static analysis tools do not take into account exploitation and scenarios that can take benefit of implementation errors and weaknesses. The question of weaknesses exploitation is usually addressed by dynamic analysis. SafeRiver is developing the CadRiver tool based on static analysis by abstract interpretation, in order to help in Security Audit of C-written applications. It aims at analyzing and assess exploitability of code weaknesses -found by the tool itself or other static tools.

Grafotech Securité - 13 septembre 2011 - 18:00-20:00

2011-09-13T18:00:00.005+02:00

CCIT de Rennes Bretagne. Inscription ici.

Respect de la vie privée dans le contexte professionnel : risques et défis?

Le droit au respect de la vie privée est un droit fondamental de tout individu. Cependant, ce droit devient de plus en plus difficile à protéger dans notre "Société de l'information" où chaque individu laisse constamment des "traces numériques" qui peuvent être reliées à son identité, parfois même sans en être conscient".
Sebastien Gambs (INRIA) présentera les enjeux liés à la protection de la vie privée dans un contexte numérique professionnel. Il exposera également quelques défis qui attendent les responsables des données dans l'entreprise.... Une discussion ouverte suivra la présentation.

Intervenant : Sébastien GAMBS, chaire de recherche entre l'université de Rennes 1 et l'INRIA spécialiste des questions de vie privée sur Internet.

Animateur : Yannick DERRIEN, consultant, ACE TIMING.

Séminaire méthodes formelles et sécurité - 9 septembre 2011 - 14h

2011-09-09T14:00:00.001+02:00

INRIA / IRISA - Rennes - salle Turing. inscription lydie(.)mabil(@)irisa(.)fr

Attention, horaire inhabituel, 14h

Radu State (université du Luxembourg) : The insulting honeypot

We will present an adaptive and learning honeypot called Heliza. Inspired by the simplistic chatting script from the 70' s, Heliza learns how to interact wit attackers in order to maximize the information about them. Leveraging machine learning techniques and game theory, Heliza evaluates several interaction strategies and permanently improves its behavior. We have implemented and deployed Heliza over an weakly configured SSH server and compared its performance with other high interaction and low interaction honeypots. Based on an underlying Markovian decision process, Heliza is capable to achieve a fast learning capability with few human operated interventions.

OSSIR Bretagne - 1er juillet 2011 - 14h15-17h00

2011-07-01T14:15:00.001+02:00

La séance aura lieu dans les locaux d'Orange, Chene Germain, 6 rue de la touche lambert35510 Cesson-Sevigne (une pièce d'identité est nécessaire).

Pour des raisons de logistique, merci de confirmer votre venue par mail à olivier(.)heen(@)technicolor(.)com

Olivier HEEN (Technicolor) : retour sur la conférence SSTIC

Je ferais un bref survol de l'ensemble des présentations. Puis je détaillerai deux présentation : rainbow tables probabilistes et Tookan.

Nicolas DELHAYE (Neo-Soft) : étude d’un loader pour packer

Je présenterai les concepts et objectifs d’un packer, je ferais une introduction sur la mémoire virtuelle, puis je décrirais le loader comme élément clef d’un packer. J'illustrerai l'évolution des ressources lors du chargement d’un binaire par le loader avant de montrer un exemple d’échec de détection d’un antivirus et de conclure.

Rennes Cryptography Seminar - Jul, 1 2011 - 14:00

2011-07-01T14:00:00.001+02:00

Salle 016, IRMAR (rez de chaussée, bâtiment 22), Université de Rennes 1, Campus de Beaulieu.

Marion Daubrignard (Verimag): Towards Automatic Verification of Security Proofs for Cryptographic Primitives

Providing security proofs instead of arguing lack of existing relevant attacks is a quite new approach when it comes to cryptography. In the last thirty years, a lot of work has been done to formalize security of systems and prove of the achievement of security criteria. It has resulted in the design of a great number of proofs under various hypotheses. Though a step in the right direction, these pencil-and-paper proofs are so numerous, involved and technical that the community has difficulty to carefully check them. The well-known example of the encryption scheme OAEP whose security proof, apparently correct, was corrected seven years after its publication illustrates that security-dedicated verification tools need to be designed.Our work takes place in the so-called computational model, where messages are considered to be bitstrings, and system adversaries are probabilistic Turing machines. A proof of security is then a complexity-theoretic reduction argument: the probability of success of an adversary in solving a security challenge is reduced to its ability to solve a known difficult problem (given a fixed amount of resources). Firstly, we provide some intuition on usual security requirements, and common sketches of security proofs. Then, we present a semantics and a logic to formalize security proofs. One could say there are several levels in automatic proving: computer-aided verification of proofs, computer-aided design of proofs, and automatic generation of proofs. We show how our inference rules can be used to derive proofs and verify them automatically, or sometimes perform a proof search using some additional inputs.

Séminaire méthodes formelles et sécurité - 1 juillet 2011 - 11h

2011-07-01T11:00:00.001+02:00

INRIA / IRISA - Rennes - Salle Turing. inscription lydie(.)mabil(@)irisa(.)fr

Daniel Le Métayer (INRIA Grenoble - Rhône-Alpes): Privacy by design: towards a systematic approach

Privacy by design is often praised by lawyers as an essential step towards a better privacy protection: in a world where privacy is more and more jeopardized by new information and communication technologies, the growing view is that part of the remedy should come from the technologies themselves.
However a precise characterization of privacy by design is still lacking and no method has been proposed so far to help in the design or assessment of privacy compliant systems. The long term goal of the work sketched here is to provide formal foundations for privacy by design that can be used in practice both in the design phase (e.g. to explore the design space when conflicting requirements have to be met) and in the evaluation phase (thus paving the way to rigorous privacy assessment procedures).
In this talk, we shall focus on the data minimization principle. We shall use “pay as you drive” systems as a motivating case study and sketch a formal framework for reasoning about data minimization before drawing some perspectives for further work.

Thèse - J-C. DEMAY - 1er Juillet 2011 - 10h30

2011-07-01T10:30:00.000+02:00

Supélec, campus de Rennes, salle de conférence

Soutenance de thèse, Jonathan-Christofer DEMAY: génération et évaluation de mécanismes de détection des intrusions au niveau applicatif

La plupart des mécanismes de détection des anomalies au niveau applicatif reposent sur la détection de la déviation du flot de contrôle d'un programme. Cependant, ces méthodes ne permettent pas de détecter des attaques qui ciblent les données de calcul utilisées par les processus. Pour compléter ces mécanismes de détection, nous proposons une méthode pour contrôler la corruption de données de calcul. Cette approche repose sur la construction d'un modèle de comportement orienté autour des variables et construit par analyse statique du code source. En utilisant Frama-C, un outil d'analyse statique développé par le CEA, nous avons implémenté notre approche pour les programmes écrits en langage C. Pour évaluer plus en détails notre mécanisme de détection, nous proposons aussi une méthode pour simuler des attaques contre les données de calcul. Cette approche repose sur un modèle de faute qui reproduit l'état interne d'une application après ce type d'attaque. Nous avons implémenté une plateforme d'évaluation en combinant notre modèle de faute avec un mécanisme d'injection en mémoire.

Jury

César Viho (Rennes 1): président du jury
Hervé Debar (Telecom Sud Paris): rapporteur
Vincent Nicomette (LAAS-CNRS): rapporteur
Benjamin Monate (CEA): examinateur
Éric Totel
Frédéric Tronel
Ludovic Mé

Grafotech Securité - (Attention: reporté)

2011-06-28T18:00:00.001+02:00

Attention, la séance est reportée à une date entre à préciser entre le 1er et le 19 septembre 2011.

CCIT de Rennes Bretagne. Inscription ici.

Respect de la vie privée dans le contexte professionnel : risques et défis?

Le droit au respect de la vie privée est un droit fondamental de tout individu. Cependant, ce droit devient de plus en plus difficile à protéger dans notre "Société de l'information" où chaque individu laisse constamment des "traces numériques" qui peuvent être reliées à son identité, parfois même sans en être conscient".
Sebastien Gambs (INRIA) présentera les enjeux liés à la protection de la vie privée dans un contexte numérique professionnel. Il exposera également quelques défis qui attendent les responsables des données dans l'entreprise.... Une discussion ouverte suivra la présentation.

Séminaire méthodes formelles et sécurité - 24 juin 2011 - 11h

2011-06-24T09:13:00.004+02:00

INRIA / IRISA - Rennes - Demander la salle à l'accueil. inscription lydie(.)mabil(@)irisa(.)fr

Eric Totel (Supélec) : Détection d'intrusion au niveau applicatif - approches par invariants

Les systèmes de détection d'intrusion actuels se focalisent sur les interactions entre le système et les applications pour détecter des anomalies dans l'exécution de l'application. Malheureusement, certains types d'attaques contre les données sont quasiment indétectables par ce type d'approche. Dans cette présentation, nous montrerons que l'utilisation d'invariants vérifiés à l'exécution dans l'application permet de détecter ces attaques. Deux approches pour construire ces invariants seront présentées. La première repose sur l'analyse statique de programmes écrits en C, en utilisant le framework Frama-C. La deuxième repose sur une analyse dynamique de l'exécution de l'application. Dans les deux cas, le but est d'instrumenter le programme initial en y insérant des assertions exécutables. Une évaluation des deux approches sur des exemples sera présentée.

Séminaire méthodes formelles et sécurité - 17 juin 2011 - 11h

2011-06-17T11:00:00.000+02:00

INRIA / IRISA - Rennes - Demander la salle à l'accueil
inscription lydie(.)mabil(@)irisa(.)fr

Yohann Thomas (ANSSI). Centre opérationnel de l'ANSSI : présentation générale et limites dans le domaine de la détection

L’agence nationale de la sécurité des systèmes d’information (ANSSI) est rattachée au secrétaire général de la défense et de la sécurité nationale (SGDSN), autorité chargée d'assister le Premier ministre dans l’exercice de ses responsabilités en matière de défense et de sécurité nationale. L’ANSSI est l'autorité nationale en matière de sécurité des systèmes d’information. Elle a pour principales missions d'assurer la sécurité des systèmes d’information de l’État et de veiller à celle des opérateurs nationaux d'importance vitale, de concevoir et déployer les réseaux sécurisés répondant aux besoins des plus hautes autorités de l’État et aux besoins interministériels, et de créer les conditions d’un environnement de confiance et de sécurité propice au développement de la société de l’information en France et en Europe.
Le Centre opérationnel de la sécurité des systèmes d’information (COSSI) a pour mission d’assurer la coordination interministérielle de la prévention et de la protection contre les attaques informatiques au profit des autorités gouvernementales. Il comporte trois métiers principaux : la veille, la conduite et l’expertise technique. Comme prévu par le Livre blanc sur la défense et la sécurité nationale paru en juin2008, il met en place une capacité centralisée de détection et de défense face aux attaques informatiques. La présentation se focalisera en particulier sur les défis techniques qui sont encore à relever dans le domaine.

CANCELLED! Rennes Cryptography Seminar - Jun, 10 2011 - 14:00

2011-06-10T14:00:00.002+02:00

CANCELED!

Salle 016, IRMAR (rez de chaussée, bâtiment 22), Université de Rennes 1, Campus de Beaulieu.

Louise Huot (LIP6): utilisation des symétries pour la résolution du problème dedécomposition de points

Rennes Cryptography Seminar - May, 27 2011 - 14:00

2011-05-27T14:00:00.000+02:00

Salle 016, IRMAR (rez de chaussée, bâtiment 22), Université de Rennes 1, Campus de Beaulieu.

Xavier Pujol ( ENS Lyon ) : Analysis of BKZ

Strong lattice reduction is the key element for most attacks against lattice-based cryptosystems. Between the strongest but impractical HKZ reduction and the weak but fast LLL reduction, there have been several attempts to find efficient trade-offs. Among them, the BKZ algorithm introduced by Schnorr and Euchner in 1991 seems to achieve the best time/quality compromise in practice. However, no reasonable time complexity upper bound was known so far for BKZ. We give a proof that after O~(n^3/k^2) calls to a k-dimensional HKZ reduction subroutine, BKZ_k returns a basis such that the norm of the first vector is at most ~= gamma_k ^ (n/2(k-1)) * det(L)^(1/n). The main ingredient of the proof is the analysis of a linear dynamic system related to the algorithm.

Séminaire méthodes formelles et sécurité - 27 mai 2011 - 11h

2011-05-27T11:00:00.002+02:00

INRIA / IRISA - Rennes - Salle Métivier
inscription lydie(.)mabil(@)irisa(.)fr

Jean Goubault-Larrecq (LSV - ENS Cachan - INRI): Orchids, and bad weeds

Orchids is an intrusion detection tool based on techniques for fast, on-line model-checking. Orchids detects complex, correlated strands of events with very low overhead in practice, although its detection algorithm has worst-case exponential time complexity. We shall explain how it works. The key to efficiency here is solid semantic foundations, plus abstract interpretation. We shall use a few attacks as illustration (mostly host-based), noting that some of them are fairly sophisticated.

Joint work with Julien Olivain (laboratoire LaCime, Montréal, Canada).

Conference - Foundations & Practice of Security - 12 - 13 May 2011

2011-05-12T10:00:00.000+02:00

4th Canada-France MITACS Workshop on Foundations & Practice of Security,
12 — 13 May, 2011, Paris(*), France

(*)The conference is not in Bretagne, but the Organization commitee is 100% in Bretagne.

Rennes Cryptography Seminar - May, 6 2011 - 14:00

2011-05-06T14:00:00.000+02:00

Salle 016, IRMAR (rez de chaussée, bâtiment 22), Université de Rennes 1, Campus de Beaulieu.

Marc Manulis (Technische Universität Darmstadt): Cryptographic Approach to Private Social Clouds

Users increasingly rely on the ``social cloud'' for storing and sharing personal information, for establishing new contacts, and for interacting with their friends and colleagues. Even though social media platforms may differ in the target audience, in the nature of collected and disseminated information, and in services offered to the users, there are several building blocks that enable user's social interactions and are deployed by the majority of these platforms. Designing these building blocks in a secure and privacy-preserving way is of utmost importance, should potential damage from the misuse of user-provided content in the existing ``social cloud'' be averted.

Due to the absence of appropriate models and security/privacy definitions it is, so far, impossible to judge, whether a proposed protection mechanism is suitable or not, whether it can be applied in general, or is tailored to a specific social media platform. Instead of using ``ad-hoc'' and ``best practice'' solutions with questionable guarantees, it is advisable to strive for a more formal treatment of the underlying building blocks by providing sophisticated security/privacy definitions and designing solutions amenable to formal reasoning and security proofs.

In the first part of my talk I will focus on the management of personal user profiles. User profiles serve as a main building block for most social media platforms. I will introduce a formal cryptographic model for \emph{private} user profiles, supporting generation of the digital content owned by the user and its controlled disclosure to other users of the social community. I will present formal definitions of security and privacy that reflect the natural expectations on private profiles. I will further describe two general solutions based on different encryption techniques and highlight their trade-offs from the security/privacy and complexity point of view. These solutions do not require any specific network infrastructure or any trusted third parties. The provided analysis takes into account statistics of several real-world social media platforms. The second part of my talk will address the problem of discovery of common social contacts, for which I will introduce the first privacy-friendly practical solution that lets two users, on input their respective contact lists, learn their common contacts (if any), and nothing else. The proposed protocol prevents arbitrary list manipulation by means of contact certification, and guarantees user authentication and revocability. I will explain why current approaches such as private set intersection or anonymous credentials, although being related, do not provide an appropriate solution to this problem. I will discuss the modeling of contact-hiding security that private contact discovery should provide. I will also highlight efficiency considerations for the proposed protocol that does not require involvement of any trusted third parties and can be deployed in resource-constraint environments.

The content of this talk is based on the recent results from FC 2011/RLCSP, ASIACCS 2011, and ACNS 2011.

Soutenance de thèse - Patrick Battistello - 29 avril 2011 - 10h00

2011-04-29T10:00:00.000+02:00

Télécom Bretagne - campus de Rennes - Amphithéâtre.

Soutenance de thèse de Patrick Battistello : Mécanisme d'établissement d'appels sécurisés limitant les risques de SPIT et de (D)DoS à l'interconnexion entre opérateurs

Cette thèse étudie les risques de sécurité à l'interconnexion VoIP entre opérateurs et propose des mesures de protection. La première partie analyse les risques en partant du contexte intra-domaine qui constitue les déploiements historiques de la VoIP. L'analyse est étendue ensuite au contexte inter-domaines où plusieurs réseaux VoIP, d'opérateurs différents, sont interconnectés avec éventuellement des terminaux en situation de mobilité. Dans ce contexte, les besoins de communications sécurisées sont élevés; il faut être capable d'authentifier les parties en communication, d'assurer l'intégrité et la confidentialité des flux de signalisation et des flux média VoIP.
Les proxys d'interconnexion étant accessibles depuis l'Internet, ils sont exposés à des risques de SPIT (SPam over Ip Telephony) et de (D)Dos. Dans la seconde partie, nous élaborons un protocole d'établissement d'appel sécurisé pour la VoIP, limitant les risques de SPIT et de (D)Dos pour les serveurs d'interconnexion. De plus, ce protocole suppporte la propriété de sécurité PFS (Perfect Forward
Secrecy) et peut s'adapter à différents types d'architectures réseau.
Pour des raisons de performances, il est basé sur des algorithmes cryptographiques symétriques. De ce fait, il est conseillé de le déployer dans des architectures hiérarchiques afin de simplifier les problématiques d'établissement des secrets partagés. Dans la dernière partie de la thèse, nous réalisons une analyse de sécurité incrémentale, nous détaillons l'implémentation du protocole et nous mesurons les performances atomiques du procédé. A partir de ces résultats, nous extrapolons par simulations à un réseau représentatif d'un déploiement opérationnel.
Mots clés : Sécurité informatique, voix sur IP, protocole d'authentification, protocole cryptographique.

Jury

M. Olivier Festor Directeur de recherche INRIA Nancy
M. Josep Domingo-Ferrer Professeur Universitat Rovira i Virgili - Spain
M. Bernard Cousin Professeur Université de Rennes 1
M. André-Luc Beylot Professeur IRIT/ENSEEIHT - Toulouse
M. Frédéric Cuppens Professeur Télécom Bretagne - Rennes
M. Xavier Aghina Responsable de programme Orange Labs - Issy les Moulineaux
M. Henri Gilbert Responsable de Laboratoire ANSSI - Paris
M. Joaquin Garcia-Alfaro Ingénieur de Recherche Télécom Bretagne - Rennes
Mme Nora Cuppens (Invité) Directrice de programmes Swid - Rennes

Séminaire méthodes formelles et sécurité - 22 avril 2011 - 11h

2011-04-22T16:04:00.000+02:00

I N R I A - Rennes - Salle Métivier
inscription lydie(.)mabil(@)irisa(.)fr

Ce séminaire sera une rediffusion du film du séminaire informatique et sciences numériques du Collège de France ayant eu lieu à Paris le 6 avril 2011.

Butler Lampson (Microsoft): Usable Security Through Isolation

Forty years of work on computer security have not led to secure systems. Users don’t know how to set the security policy they want, or how to defend themselves from malware. The first is because users can’t understand their choices, and the second is because systems are complicated and extensible. Isolation can make things much simpler. It also makes systems much less flexible, but with careful design they can be flexible enough.

C&ESAR 2011 - Appel à communications

2011-04-15T16:34:00.005+02:00

Appel à communications

Date limite de soumission: 5 juin 2011

Notification aux auteurs: 30 juillet 2011

Article définitif: 15 octobre 2011

Conférence: 28-29-30 novembre 2011

Rennes Cryptography Seminar - 15 avril 2011 - 14:00

2011-04-15T11:00:00.000+02:00

Salle 016, IRMAR (rez de chaussée, bâtiment 22), Université de Rennes 1, Campus de Beaulieu.

Laila El Aimani (Technicolor) : Design and Analysis of Opaque Signatures

Generic constructions of designated confirmer signatures follow one of the following two strategies; either produce a digital signature on the message to be signed, then encrypt the resulting signature, or produce a commitment on the message, encrypt the string used to generate the commitment, and finally sign the latter. In this talk, we revisit both methods and establish the minimal and sufficient assumptions on the building blocks in order to attain secure confirmer signatures. Our study concludes that both paradigms, when used in their basic form, cannot allow a class of encryption schemes which is vital for the efficiency of the confirmation/denial protocols. Next, we propose a variation of both paradigms which thrives on very cheap encryption and consequently leads to efficient confirmer signatures.

Indeed, the resulting constructions do not only compete with the dedicated realizations of confirmer/undeniable signatures proposed recently, e.g. \citep{LeTrieuKurosawaOgata2009b,SchuldtMatsuura2010},but also serve for analyzing the early schemes that have a speculative security.

The contents of this talk are parts of the speaker's PhD thesis.

Séminaire méthodes formelles et sécurité - 8 avril 2011 - 11h

2011-04-08T11:00:00.000+02:00

I N R I A - Rennes - Métivier
inscription lydie(.)mabil(@)irisa(.)fr

Frédéric Cuppens et Nora Cuppens-Boulahia (ENST Bretagne) : Modèle de dépendances et d’évaluation des risques pour réagir aux intrusions

Les systèmes d’information sont aujourd’hui très étroitement interdépendants à la fois aux niveaux logiciel et matériel. Ces interdépendances se retrouvent dans les couches protocolaires (dépendance verticale) ainsi que dans les imbrications de services (dépendance horizontale). Les attaquants cherchent à exploiter ces dépendances en concevant des intrusions qui se propagent rapidement au travers des services, produisant des réactions en chaîne comparables à un effet domino.
Dans cette présentation nous nous intéressons aux problèmes de dépendances de service dans le cadre de la réaction aux intrusions. Dans ce contexte, nous présentons un modèle pour aider les administrateurs de sécurité dans la gestion, l’activation et la désactivation de politiques de réactions aux intrusions. Nous montrons notamment que l’analyse des dépendances peut être utilisée pour évaluer l'impact des contre-mesures et choisir celles qui ont l'impact le plus faible sur le système et ses utilisateurs.

PhD Thesis - Jean-Marie Borello - 1 Avril 2011 - 14h00

2011-04-01T14:00:00.002+02:00

Jean-Marie Borello soutiendra sa thèse de doctorat intitulée "Étude du métamorphisme viral : modélisation, conception et détection"

La protection contre les codes malveillants représente un enjeu majeur. Il suffit de considérer les exemples récents des vers Conficker et Stuxnet pour constater que tout système d’information peut aujourd’hui être la cible de ce type d’attaques. C’est pourquoi, nous abordons dans cette thèse la menace représentée par les codes malveillants et plus particulièrement le cas du métamorphisme. Ce dernier constitue en effet l’aboutissement des techniques d’évolution de codes (« obfuscation ») permettant à un programme d’éviter sa détection.
Pour aborder le métamorphisme nous adoptons une double problématique : dans une première partie, nous nous attachons à l’élaboration d’un moteur de métamorphisme afin d’en estimer le potentiel offensif. Pour cela, nous proposons une technique d’obscurcissement de code dont la transformation inverse est démontrée NP-complète dans le cadre de l’analyse statique. Ensuite, nous appliquons ce moteur sur une souche malveillante préalablement détectée afin d’évaluer les capacités des outils de détection actuels. Après cette première partie, nous cherchons ensuite à détecter, outre les variantes engendrées par notre moteur de métamorphisme, celles issues de codes malveillants connus. Pour cela, nous proposons une approche de détection dynamique s’appuyant sur la similarité comportementale entre programmes. Nous employons alors la complexité de Kolmogorov afin de définir une nouvelle mesure de similarité obtenue par compression sans perte. Finalement, un prototype de détection de code malveillant est proposé et évalué.

Jury

M. Thomas Jensen, Directeur de recherche à l’INRIA, président
M. Guillaume Bonfante, Maître de conférences à l’institut National Polytechnique de Lorraine, rapporteur
M. Jean-Marc Steyaert, Professeur à l’école Polytechnique, rapporteur
M. Marc Dacier, Senior director in charge of the Collaborative Advanced Research Department (CARD) within Symantec Research Labs, examinateur
M. Loïc Duflot, Ingénieur de recherche à l’Agence Nationale de la Sécurité des Systèmes d’Information (ANSSI), examinateur
M. Frédéric Valette, Ingénieur au centre DGA Maîtrise de l’Information de la Direction Générale de l’Armement (DGA), invité
M. Ludovic Mé, Professeur à Supélec, directeur de thèse
M. Éric Filiol, Professeur à l’ESIEA, co-directeur de thèse

Rennes Cryptography Seminar - 1 avril 2011 - 14:00

2011-04-01T14:00:00.000+02:00

Christiane Peters ( Technische Universiteit Eindhoven ) : Wild McEliece Incognito

The McEliece cryptosystem is based on classical Goppa codes over F_2. Generalizations of the McEliece cryptosystem using Goppa codes over larger fields F_q were investigated but not found to offer advantages for small q. We showed that codes over F_31 offer advantages in key size compared to codes over F_2 while maintaining the same security level against all attacks known. However, codes over smaller fields such as F_3 were still not competitive in key size with binary codes.
The "wild McEliece cryptosystem" uses wild Goppa codes over finite fields to achieve smaller public key sizes compared to the original McEliece cryptosystem. This proposal makes "larger tiny fields" attractive and bridges the gap between F_2 and F_31. We added an extra shield to the wild McEliece cryptosystem, slightly increasing key sizes but drastically increasing the pool of Goppa polynomials to choose from.

OSSIR Bretagne - 29 mars 2010 - 14h15-16h30

2011-03-29T14:00:00.001+02:00

À Technicolor R&D, 1 Avenue de Belle Fontaine à Cesson-Sévigné, salle Vivaldi (se munir d’une pièce d’identité)

Philippe NGuyen de la société Secure-ic (http://www.secure-ic.com) : Evaluation de la sécurité physique des composants

Goulven GUIHEUX et Frédéric Guihery de la société Amossys (http://www.amossys.fr) : Technologies TPM et Intel TXT

Résumé: Le fonctionnement du composant cryptographique TPM et de Intel TXT sera présenté. La présentation sera illustrée à l'aide de produits ou prototypes tirant partie de ces technologies. Les attaques et les contremesures seront également abordées. La présentation se terminera par un bilan sur les menaces couvertes et non couvertes actuellement par les technologies d'informatique de confiance.

Rennes Cryptography Seminar - 25 mars 2011 - 14:00

2011-03-24T11:27:00.004+01:00

14 h 00, Salle 016, IRMAR (rez de chaussée, bâtiment 22), Université de Rennes 1, Campus de Beaulieu.

Christiaan van de Woestijne : deterministic equation solving over finite fields

It is a curious fact that most efficient algorithms for solving algebraic equations over finite fields are probabilistic. In this talk, I will give an overview over deterministic techniques that are applicable. The case of constructing rational points on elliptic curves is especially relevant for cryptographic applications. I will give a detailed exposition of my algorithm for this purpose and also discuss the complexity from various viewpoints.

Séminaire méthodes formelles et sécurité - 25 mars 2011 - 11h

2011-03-17T08:37:00.004+01:00

I N R I A - Rennes - Salle Turing
inscription lydie(.)mabil(@)irisa(.)fr

Emmanuel Gureghian (Bertin) : Méthodes formelles et politiques de sécurité : quel impact dans la fonction d'architecte ?

Rennes Cryptography Seminar - 18 mars 2011 - 14:00

2011-03-17T08:34:00.004+01:00

14 h 00, Salle 016, IRMAR (rez de chaussée, bâtiment 22), Université de Rennes 1, Campus de Beaulieu.

Pierre Castel ( Université de Caen ) : un algorithme de résolution des équations quadratiques

Soit Q une forme quadratique de dimension 5. Le but de cet algorithme est de trouver un vecteur isotrope pour la forme Q. Des algorithmes existent déjà pour résoudre ce type d'équation, cependant la première étape de ces algorithmes consiste à factoriser le déterminant de Q ce qui nuit considérablement à leur efficacité. Dans cet exposé, je proposerai un nouvel algorithme ne factorisant pas le déterminant de Q pour résoudre ce type d'équation.

Séminaire méthodes formelles et sécurité - Mar. 11, 2011 - 11h

2011-03-09T10:52:00.005+01:00

Jean-François Capuron (DGA - MI) : Génération automatique de tests à partir de modèles pour la vérification de composants cryptographiques - mise en oeuvre et expérimentation

La complexité croissante des logiciels rend leur validation et leur vérification de plus en plus problématique. Les méthodes manuelles ne permettent plus de répondre aux exigences fortes de couverture des comportements, en particulier lorsqu'il s'agit de composants critiques pour la sécurité ou la sûreté d'un système.
Suite à ce constat, la génération automatique de tests à partir d'une spécification du comportement attendu est une des solutions possibles au problème. Nous présenterons notre problématique, ici la vérification d'un composant cryptographique logiciel et les objectifs de cette vérification. Ensuite nous décrirons comment nous avons mis en oeuvre la génération automatique de tests à partir d'un modèle UML/OCL et comment elle s'intègre dans le processus de test existant. Nous décrirons également une expérimentation de validation des tests produits, les résultats obtenus et les perspectives du MBT dans le cadre de la vérification de composants à haut niveau d'exigence.

Rennes Cryptography Seminar - Mar. 04, 2011 - 14:00

2011-03-04T13:17:00.006+01:00

14 h 00, Salle 016, IRMAR (rez de chaussée, bâtiment 22), Université de Rennes 1, Campus de Beaulieu.

David Xiao (LRI/LIAFA): Privacy, incentives, and truthfulness

Imagine the government is taking a census, and you as an individual are worried that by participating, private information about you (such as your address, age, ethnicity, etc.) may eventually be revealed when the government publishes the census data. How can the government assure you that by using an appropriate release mechanism that "sanitizes" census data, no individual's privacy will be compromised?
This question has been studied for a long time in the statistics community, and more recently the computer science community has contributed the formal notion of differential privacy, which captures the idea that "no individual's data can have a large effect on the output of the release mechanism". This has been interpreted to mean that individuals should be comfortable revealing their information, since little private information is leaked.
In this talk, we first give an introduction to this fast-developing area of research. We then investigate the above interpretation about the guarantees of differential privacy. We argue that the interpretation is incomplete because unless participation in the database somehow explicitly benefits the individuals, they will always refuse to participate regardless of whether the release mechanism is differentially private or not. We then show that by combining differential privacy with the notion of incentives and truthfulness from game theory, one can take (almost) any release mechanism that motivates individuals to participate and modify it so that in addition
it satisfies differential privacy.

PhD Thesis - Mohamed Ali Ayachi - Feb. 24, 2011 - 14h00

2011-02-24T14:00:00.003+01:00

Jeudi 24 février 2011 à Supélec Rennes.

Mohamed Ali Ayachi soutiendra sa thèse intitulée : contributions à la détection de comportements malhonnêtes dans les réseaux ad hoc AODV par analyse de la confiance implicite.

La constante évolution des technologies de l’information et le penchant vers l’utilisation des machines sans fil qui se sont imposées ces dernières années ont fait émerger un nouveau type de réseaux : les réseaux sans-fil ad hoc, ou MANET (Mobile Ad hoc NETwork). Se souciant de pouvoir communiquer et de partager l’information dans n’importe quelle situation, les réseaux ad hoc sont des systèmes autonomes composés par un ensemble d’entités mobiles libres de se déplacer sans contraintes. Ces entités utilisent le médium radio pour communiquer et forment un réseau n’utilisant aucune infrastructure existante.

Dans cette thèse, nous nous intéressons à sécuriser les protocoles de routage ad hoc en proposant des mécanismes de détection des actions malveillantes pour consolider les protocoles de routage et prévenir les futures attaques. Nous nous basons sur la confiance développée entre les entités pour bâtir un raisonnement sur le comportement des entités voisines. Ceci passe par une comparaison des messages échangés entre les entités du réseau ad hoc ou encore par l’analyse des incohérences dans les annonces et les ouvertures de routes afin de détecter la malhonnêteté ou la compromission d’une entité mobile. Nous choisissons d’appliquer cette approche sur le protocole réactif AODV.

L’évaluation des performances de ce système de détection montre la pertinence du raisonnement sans pour autant influencer les performances du protocole. Une étude portant sur les cas de faux-positifs est aussi effectuée : nous proposons une solution pour les limiter en se basant sur le fait de ne prendre une décision que si l’entité est sûre de l’action malhonnête du voisin.

Jury

Mme Isabelle CHRISMENT, EPFL-Nancy, (rapporteuse)
M. Belhassen ZOUARI, Faculté des Sciences de Tunis, (rapporteur).
M. Bernard COUSIN, IRISA (examinateur)
Mme. Sihem GUEMARA EL FATIMI, Sup'Com Tunis (examinatrice)
M. Adel BOUHOULA, Sup'Com (examinateur)
M. Christophe BIDAN, Supélec (examinateur)
M. Nicolas PRIGENT, Supélec (examinateur).

Séminaire méthodes formelles et sécurité - Feb. 18, 2011 - 11h

2011-02-18T11:00:00.000+01:00

INRIA Rennes, salle Métivier, inscription lydie(.)mabil(@)irisa(.)fr

Jean-Yves Marion (LHS LORIA/INRIA, Nancy) Un point de vue sur la virologie informatique

Cette conférence portera sur la virologie informatique dont le champ d’étude englobe les virus, les ver, les botnets, … Dans un premier temps, un état de l’art en virologie sera présenté. Puis nous nous concentrerons sur l’analyse des programmes malveillants : quelles sont les méthodes de protection ? Comment les contourner ? Enfin, nous explorerons de nouvelles méthodes de détection des codes malveillants.

Ces travaux s’effectuent dans le laboratoire de haute sécurité du LORIA et de l’INRIA Nancy.

SSTIC 2011 - Programme

2011-02-14T14:37:00.004+01:00

Le programme du SSTIC 2011 est publié

SAR-SSI 2011 - still a few day to submit

2011-02-10T09:33:00.005+01:00

Still a few days before submission. Read the c all for papers.

Séminaire méthodes formelles et sécurité - Feb. 04, 2011 - 11h

2011-02-04T11:00:00.001+01:00

INRIA Rennes, salle Métivier, inscription lydie(.)mabil(@)irisa(.)fr

Gilles Barthe, (IMDEA, Madrid) Towards Automated and Independently Verifiable Cryptographic Proofs

CertiCrypt is a fully machine-checked framework that supports the construction and verification of cryptographic proofs within the Coq proof assistant. It was used to formally verify emblematic examples, including a proof of IND-CCA security of OAEP, and a proof of EF-CMA of FDH signatures, and proofs of soundness and completeness for zero-knowledge protocols.

CertiCrypt draws on many areas, such as semantics of programming languages, probability, complexity, and mathematics. In addition, it provides certified tools to reason about the equivalence of probabilistic programs, including a relational Hoare logic, a theory of observational equivalence, a set of verified program transformations, and game-based techniques such as reasoning about failure events.

The presentation will describe CertiCrypt's architecture and main components, describe its applications, and present ongoing work to improve automation using external SMT solvers.

This is joint work with Benjamin Gregoire, Santiago Zanella, Sylvain Heraud, Federico Olmedo, Daniel Hedin, and Anne Pacalet.

CRI'Ouest - Jan. 31, 2011 - 18:00-20:00

2011-01-31T18:00:00.000+01:00

CCI Nantes Saint-Nazaire

Inscription : contact(@)criouest(.)org

Intelligence Economique pour le RSSI : mythe ou réalité ?

Plus d'information sur le site du Cri'Ouest.

Cet événement est aussi sur l'agenda de la sécurité.

Grafotech Security - Jan. 25, 2011 - 18:00-20:00

2011-01-25T18:00:00.001+01:00

CCI de Rennes.

Vulnérabilités dans les logiciels applicatifs : pourquoi, comment?

Suivi d'un bilan des forums Grafotec 2010
Intervenants : Ludovic Me - enseignant chercheur à SUPELEC
Animateurs : Stéphane Goarnisson, ORANGE, Yannick Derrien, ACE TIMING.

Séminaire méthodes formelles et sécurité - Jan. 21, 2011 - 11h

2011-01-21T11:00:00.001+01:00

INRIA Rennes, salle Métivier, inscription lydie(.)mabil(@)irisa(.)fr

Véronique Cortier (LORIA): Can I get my security proof for free?

Security protocols are short programs aiming at securing communications over a network. They are widely used in our everyday life. Their verification using symbolic models has shown its interest for detecting attacks and proving security properties. In particular, several automatic tools have been developed and are used to efficiently detect flaws.
We will present recent results that demonstrate that formal abstract models used for verification are actually sound with respect to much richer models that considers issues of complexity and probability. As a consequence, it is possible to derive strong, clear security guarantees still keeping the simplicity of reasonning in symbolic models.
During this talk, we will also discuss the limitations of the current approaches, which are often hidden in the details of the hypotheses.

Journées "Codes et Stéganographie" - 18 et 19 janvier 2011

2011-01-18T09:00:00.001+01:00

Journées "Codes et Stéganographie" 18 et 19 janvier 2011
Écoles Militaires de Saint-Cyr Coëtquidan
inscriptions : http://www.novetix.fr/recherche/fr/jcs2011.php

Dates Importantes

Soumission : 10 janvier 2011
Notification : 14 janvier 2011
Inscription : 12 janvier 2011
Journées : 18 et 19 janvier 2011

Comité de Programme

Johann Barbier : Novetix
Patrick Bas : CNRS Lagis
Pierre-Louis Cayrel : CASED - Center for Advanced Security Research Darmstadt
Caroline Fontaine : CNRS/Lab-STICC/CID - Télécom Bretagne/ITI
Philippe Gaborit : Université de Limoges
Zoubida Jadda : Écoles Militaires de Saint Cyr Coëtquidan
Emmanuel Mayer : DGA Maîtrise de l'Information - SSI/AMI
Patrice Parraud : Écoles Militaires de Saint Cyr Coëtquidan
Patrick Solé : CNRS/LTCI - Télécom Paristech

Organisateurs

Patrice Parraud : Écoles Militaires de Saint-Cyr Coëtquidan
Johann Barbier : Novetix
Zoubida Jadda : Écoles Militaires de Saint-Cyr Coëtquidan
Morgan Barbier : École Polytechnique - Lix

Rennes Cryptography Seminar - Jan. 14, 2011 - 14:00

2011-01-14T14:00:00.001+01:00

Salle 016, IRMAR (rez de chaussée, bâtiment 22), Université de Rennes 1, Campus de Beaulieu, Rennes.

Peter Bruin (Orsay) : Calculer dans le groupe de Picard d'une courbe projective sur un corps fini

Khuri-Makdisi a développé un cadre algorithmique pour calculer de façon efficace dans le groupe de Picard d'une courbe projective lisse sur un corps $k$. C'est une intéressante approche, par exemple, pour les courbes modulaires, où une représentation convenable de la courbe peut se calculer à partir d'un espace de formes modulaires.
Le but de cet exposé est de montrer que ce cadre algorithmique permet de traiter quelques problèmes intéressants dans le cas où $k$ est fini. Je décrirai des algorithmes efficaces pour trouver des points rationnels au hasard selon la distribution uniforme sur une courbe et sur sa jacobienne, pour calculer le morphisme de Frobenius et l'accouplement de Frey et Rück, et pour trouver une base de la $l$-torsion du groupe de Picard ($l$ un nombre premier différent de la caractéristique de $k$).

Séminaire méthodes formelles et sécurité - Jan. 7, 2011 - 11h

2011-01-07T11:00:00.001+01:00

Salle Métivier, inscription lydie(.)mabil(@)irisa(.)fr

Graham Steel, (LSV, Cachan): Attacking and Fixing PKCS#11 Security Tokens

We show how to extract sensitive cryptographic keys from a variety of commercially available tamper resistant cryptographic security tokens, exploiting vulnerabilities in their RSA PKCS#11 based APIs. The attacks are performed by Tookan, an automated tool we have developed, which reverse-engineers the particular token in use to deduce its functionality, constructs a model of its API for a model checker, and then executes any attack trace found by the model checker directly on the token. We describe the operation of Tookan and give results of testing the tool on 18 commercially available tokens: 10 were vulnerable to attack, while the other 8 had severely restricted functionality. One of the attacks found by the model checker has not previously appeared in the literature. We show how Tookan may be used to verify patches to insecure devices, and give a secure configuration that we have implemented in a patch to a software token simulator.
This is the first such configuration to appear in the literature that does not require any new cryptographic mechanisms to be added to the standard. We comment on lessons for future key management APIs.

Séminaire méthodes formelles et sécurité - Dec. 17, 2010 - 11h

2010-12-17T11:00:00.001+01:00

Inscription lydie(.)mabil(@)irisa(.)fr

Formal analysis of the EMV payment protocol suite, Erik Poll, Radboud University Nijmegen

Joint work Joeri de Ruiter.

EMV is the leading international standard for electronic payments using smartcards. Initially developed by EuroPay, Mastercard and Visa, it has been adopted as the standard across the EU. The EMV standard is extremely complex, involving over 700 pages of documentation describing dozens of options and configurations.

We are working on a formalisation the EMV protocol in the functional programming language F# to then analyse the security using existing tools (in particular the protocol verifier ProVerif with the automated translation from F# to applied pi calculus.)

PhD Thesis, Benoît Boyer - Dec. 13, 2010 - 14h00

2010-12-13T08:52:00.004+01:00

Salle Les Minquiers.

Soutenance de thèse de Benoît BOYER, Réécriture d'automates certifiée pour la vérification de modèle

Cette thèse s'intéresse à la vérification de programmes modélisés sous forme de systèmes de règles de réécriture. La vérification de propriétés est basée sur une analyse statique semi-automatique qui construit une sur-approximation, représentée par un automate d'arbres, de l'ensemble des termes atteignables. L'analyse est paramétrée par une abstraction qui doit être suffisamment précise pour que la propriété attendue puisse être vérifiée. Or, il est difficile de construire une telle abstraction à priori. On propose un mécanisme original de raffinement automatique par élagage de l'automate d'arbres lorsque la sur-approximation calculée, trop imprécise, est susceptible de contenir de fausses alarmes. Non seulement l'analyse s'applique à la vérification de propriétés de sûreté par non-atteignabilité, mais on montre qu'elle peut être adaptée afin de vérifier des propriétés temporelles, notamment sur le graphe des appels de méthodes d'un programme Java. Enfin, les outils réalisant cette analyse reposent sur des implémentations optimisées, clairement éloignées de la spécification originale. Pour accroître la confiance en ces outils, on fournit un vérificateur chargé de la validation de leurs résultats à posteriori. La spécification et la correction de ce validateur sont formulées et démontrées dans l'assistant de preuves Coq.

Jury

Ahmed BOUAJJANI, Professeur LIAFA/Université Paris Diderot, Paris
Pierpaolo DEGANO, Professeur Université de Pise, Italie
Thomas GENET, Maître de Conférences Université de Rennes 1/Irisa Rennes
Jean GOUBAULT-LARRECQ, Professeur LSV/ENS Cachan
Thomas JENSEN, Directeur de Recherche Centre INRIA Rennes Bretagne-Atlantique/Irisa Rennes
Olivier RIDOUX, Professeur Université de Rennes 1/Irisa Rennes

PhD Thesis, Laurent Hubert - Dec. 17, 2010 - 14h30

2010-12-10T10:16:00.002+01:00

Salle Métivier, INRIA / IRISA.

Soutenance de Thèse de Laurent Hubert: Fondations sémantiques et implémentation d'un atelier logiciel pour l'analyse statique de programmes en code objet Java

Dans cette thèse, nous nous intéressons à l’analyse statique du bytecode Java. L’initialisation d’un système d’information est une phase délicate où des propriétés de sécurité sont vérifiées et des invariants installés. L’initialisation en Java pose des difficultés, que ce soit pour les champs, les objets ou les classes. De ces difficultés peuvent résulter des failles de sécurité, des erreurs d’exécution (bugs), ou une plus grande difficulté à valider statiquement ces logiciels. Cette thèse propose des analyses statiques répondant aux problèmes d’initialisation de champs, d’objets et de classes. Ainsi, nous décrivons une analyse de pointeurs nuls qui suit finement l’initialisation des champs et permet de prouver l’absence d’exception de pointeurs nuls (NullPointerException) et de raffiner le graphe de flot de contrôle intra-procédural. Nous proposons aussi une analyse pour raffiner le graphe de flot de contrôle inter-procédural liée à l’initialisation de classe et permettant de modéliser plus finement le contenu des champs statiques. Enfin, nous proposons un système de type permettant de garantir que les objets manipulés sont complètement initialisés, et offrant ainsi une solution formelle et automatique à un problème de sécurité connu. Les fondations sémantiques de ces analyses sont données. Les analyses sont décrites formellement et prouvées correctes. Pour pouvoir adapter ces analyses, formalisées sur de petits langages, au bytecode, nous avons développé une bibliothèque logicielle. Elle nous a permis de produire des prototypes efficaces gérant l’intégralité du bytecode Java.

Jury

Anindya Banerjee , Professeur Fondation IMDEA Software/ Université Polythechnique de Madrid, Espagne
Thomas Jensen, Directeur de Recherche Centre INRIA Rennes Bretagne-Atlantique
Jean-Marc Jézéquel, Professeur Université de Rennes 1
David Pichardie, Chargé de Recherche Centre INRIA Rennes Bretagne-Atlantique
Erik Poll, Maître de Conférences Université de Radboud, Nijmegen, Pays-Bas
Mario Südholt, Professeur École des Mines de Nantes

Rennes Cryptography Seminar - Dec. 10, 2010 - 14:00

2010-12-10T08:37:00.004+01:00

Rennes, campus Beaulieu, IRMAR, bat. 22, Room 016.

Dominique Schröder (universite: TU Darmstadt): History-Free Aggregate Message Authentication Codes

Aggregate message authentication codes, as introduced by Katz and Lindell (CT-RSA 2008), combine several MACs into a single value, which has roughly the same size as an ordinary MAC. These schemes reduce the communication overhead significantly and are therefore a promising approach to achieve authenticated communication in mobile ad-hoc networks, where communication is prohibitively expensive. Here we revisit the unforgeability notion for aggregate MACs and discuss that the definition does not prevent "mix-and-match" attacks in which the adversary turns several aggregates into a "fresh" combination, i.e., into a valid aggregate on a sequence of messages which the attacker has not requested before. In particular, we show concrete attacks on the previous scheme.
To capture the broader class of combination attacks, we provide a stronger security notion of aggregation unforgeability. While we can provide stateful transformations lifting (non-ordered) schemes to meet our stronger security notion, for the statefree case we switch to the new notion of history-free se- quential aggregation. This notion is somewhat between non-ordered and se- quential schemes and basically says that the aggregation algorithm is carried out in a sequential order but must not depend on the preceding messages in the sequence, but only on the shorter input aggregate and the local message. We finally show that we can build an aggregation-unforgeable, history-free sequential MAC scheme based on general assumptions.

PhD Thesis, Nicolas Scouarnec - Dec. 8, 2010 - 10h30

2010-12-09T09:05:00.005+01:00

Salle Métivier, INRIA / IRISA.

Soutenance de thèse de Nicolas Scouarnec: Codage pour l’optimisation de ressources dans les systèmes distribués

Au sein de cette thèse, nous étudions l’utilisation de codes dans les systèmes de diffusion distribuée et dans les systèmes de stockage auto-réparant. La diffusion vise à copier sur tous les composants d’un système une donnée initialement disponible auprès une seule source. Les systèmes de stockage distribués autorisent un stockage fiable (persistent malgré les défaillances) réparti sur plusieurs composants de stockage. Cependant, les différents composants d’un système distribués sont non-fiables et difficilement prévisibles à cause des défaillances possibles et des algorithmes locaux et aléatoires.

Les codes, qui transforment un ensemble de k paquets de données natives en un ensemble de n paquets de données encodées de telle sorte que n’importe quel sous ensemble de k paquets encodés permet de retrouver les paquets natifs, ont été largement utilisés afin de construire des systèmes fiables (transmission ou stockage) à partir de composants non fiables. A ce titre, les codes sont très utiles dans les systèmes distribués et surpassent les approches sans codes (réplication par exemple) grâce à: (i) une diversité plus élevée des paquets diffusés, réduisant ainsi les surcoûts de communication, (ii) une redondance de stockage plus efficace offrant ainsi une meilleure tolérance aux défaillances pour un coût de stockage plus faible. Cependant, dans la pratique, même si les codes sont attirants du fait des grandes améliorations en termes de diffusion et de stockage, ils sont souvent délaissés notamment à cause de leurs coûts de décodage élevés (diffusion) et de leurs coûts de réparation (les coûts réseaux associés à large-création d’un bloc perdu suite à une défaillance) plus élevés (stockage auto-réparant).

Nous étudions la possibilité de réduire les coûts annexes (coûts de décodage et coûts de réparation) afin de rendre les codes plus attrayants. Afin de réduire les coûts de décodages dans les systèmes de diffusion, nous nous intéressons aux codes fontaines basse complexité. Ainsi, nous proposons d’adapter un protocole de diffusion épidémique afin de profiter au plus des codes fontaines basse complexité. Par ailleurs, nous construisons de nouveaux codes réseaux basse complexité en étendant des codes fontaines existants (LT codes). Dans le contexte du stockage auto-réparant, nous étudions l’utilisation de codes réseaux afin de fournir une solution offrant des compromis optimaux entre coûts de stockage et coûts de réparation. Plus précisément, nous étendons les codes régénérants afin de supporter, de façon optimale, des réparations multiples et des systèmes dynamiques. Enfin, nous concluons cette thèse en proposant diverses perspectives concernant les codes réseaux basse complexité et les codes régénérants.

Jury

Claude Jard (Professeur des universités à l’ENS Cachan - Antenne Bretagne)
Philippe Duchon (Professeur des universités à l’Université de bordeaux - LABRI)
Pascal Felber (Professeur à l’Université de Neuchatel)
Pablo Rodriguez (Directeur Scientifique à Telefonica)
Anne-Marie Kermarrec (Directrice de recherche à l’INRIA Rennes)
Mary-Luc Champel (System Project Leader à Technicolor)

GOSSPLE Workshop on Social Networking - Dec. 9 2010

2010-12-09T09:00:00.001+01:00

INRIA Rennes, salle Métivier

Program

9:15 Introduction

9:30 Esther Pacitti, University of Montpellier Large-scale data sharing by exploiting gossiping

10:00 Rachid Guerraoui, EPFL The Social Filtering Problem

10:30 Coffee break

11:00 Pascal Felber, University of Neuchatel Privacy and anonymity in P2P networks

11:30 Eli Gafni, UCLA Oblivious Collaboration

12:00-13:30 Lunch

13:30 Sihem Amer-Yahia, Yahoo! Research NYC Review annotation for better interpretation

14:00 Peter Triantafillou, University of Patras Optimal Ranked Retrieval with tag taxnomies in Social media with TREATS

14:30 Pablo Rodriguez, Telefonica, Barcelona Scaling Online Social Networks

15:00 Coffee break

15:30 Maarten van Steen, Vrije Universiteit, Amsterdam Wireless gossiping for social networking

16:00 Anne-Marie Kermarrec INRIA P2P news recommender

16:30 Wrap up

SSTIC 2011 - Plus qu'un mois pour soumettre

2010-12-09T08:54:00.002+01:00

Lire l'appel à soumission.

Journées Codes et Stéganographie - 18 et 19 janvier 2011

2010-12-07T16:12:00.004+01:00

Écoles Militaires de Saint-Cyr Coëtquidan
http://www.novetix.fr/recherche/fr/jcs2011.php

Soumission : 20 décembre 2010
Notification : 06 janvier 2011
Inscription : 12 janvier 2011
Journées : 18 et 19 janvier 2011

L'objet de ces Journées est de réunir les membres de la communauté scientifique dont les thèmes de recherche sont liés à la Stéganographie et aux Codes Correcteurs d'Erreurs Binaires et/ou quaternaires. Elles ont pour but de créer une dynamique sur ces thèmes en présentant les travaux de chercheurs confirmés et en valorisant ceux des doctorants. Elles proposeront une conférence invitée suivie d'exposés le matin et un après-midi majoritairement dédiés aux doctorants.
Les sujets attendus de ces journées pourront s'étendre de façon non exhaustive autour des thématiques suivantes :
- modèles de sécurité,
- stéganalyse,
- conception d'algorithmes stéganographiques,
- dimensionnement des schémas de stéganographie,
- codage de syndrome et performances,
- codes adaptés l'insertion adaptative,
- théorie de l'information et stéganographie,
- applications,
- ...

Comité de Programme
- Johann Barbier : Novetix
- Patrick Bas : CNRS Lagis
- Pierre-Louis Cayrel : CASED - Center for Advanced Security Research Darmstadt
- Caroline Fontaine : CNRS/Lab-STICC/CID - Télécom Bretagne/ITI
- Philippe Gaborit : Université de Limoges
- Zoubida Jadda : Écoles Militaires de Saint Cyr Coëtquidan
- Emmanuel Mayer : DGA Maîtrise de l'Information - SSI/AMI
- Patrice Parraud : Écoles Militaires de Saint Cyr Coëtquidan
- Patrick Solé : CNRS/LTCI - Télécom Paristech

Organisateurs
- Patrice Parraud : Écoles Militaires de Saint-Cyr Coëtquidan
- Johann Barbier : Novetix
- Zoubida Jadda : Écoles Militaires de Saint-Cyr Coëtquidan
- Morgan Barbier : École Polytechnique - Lix

DGA-INRIA - Dec. 3, 2010 - 11:00

2010-12-03T11:00:00.001+01:00

I N R I A - Rennes, Salle Métivier,
Inscriptions auprès de Lydie Mabil lydie(.)mabil(@)irisa(.)fr

Yassine Lakhnech (Université de Grenoble, CNRS/VERIMAG), Innocuity of Corruption for Key-Exchange Protocols

Key-exchange protocols are among the most important building blocks for the practical deployment of cryptographic solutions; therefore, it is of great importance to guarantee their security under realistic scenarios. Existing provable security frameworks for key-exchange protocols adopt a corruption model that allows the adversary to access some secret information held by the protocol participants; this realism comes at the cost of making security proofs complex and error-prone.
We develop a modular proof method for proving security of a large class of key-exchange protocols in which the session key is obtained by application of a hash function---modeled as a random oracle. Our method captures the intuition that corruption does not provide the adversary with significant benefits if session keys are independent; formally, it provides condition to derive security of a protocol from security in a reduced game in which the adversary has limited corruption capacity. Our method improves and extends an earlier method by Kudla and Paterson. We illustrate the benefits of our results on existing protocols, including HMQV and NAXOS. Moreover, we refine the original security proof of hmqv by providing a finer analysis of the key replication attacks.
Joint work with Cristian Ene and Gilles Barthe

Technicolor Security Newsletter - N°17 Fall 2010

2010-12-01T08:24:00.002+01:00

The Technicolor Security Newsletter #17 is available.

It is published quarterly by the Technicolor Security Lab in Rennes.

CRI'Ouest - Nov. 29, 2010 - 18:00-20:00

2010-11-29T18:00:00.000+01:00

CCI Nantes Saint-Nazaire

Inscription : contact(@)criouest(.)org

Sécurité des applications Web : oui, mais comment ?

Plus d'information sur le site du Cri'Ouest.

Cet événement est aussi sur l'agenda de la sécurité.

Rennes Cryptography Seminar - Nov. 26, 2010 - (rescheduled to) 15:00

2010-11-26T14:00:00.003+01:00

Rescheduled to 15h00.
Rennes, campus Beaulieu, IRMAR, bat. 22, Room 016.

David Roe (Harvard): support for p-adics in Sage: present and future

I will describe the current capabilities within Sage for arithmetic in p-adic rings and fields, as well as support for polynomials, matrices, hyperelliptic curves and p-adic L-functions. I will then discuss plans for improvements to these areas.

C&ESAR 2010 - Nov. 22-23-24, 2010

2010-11-22T09:00:00.002+01:00

Rennes Cryptography Seminar - Nov. 19, 2010 - (rescheduled to) 15:00

2010-11-19T14:00:00.004+01:00

Rescheduled to 15h.

Rennes, campus Beaulieu, IRMAR, bat. 22, Room 016.

Nicolas Estibals (LORIA) : Titre : Accélérateur matériel compact pour le calcul du couplage de Tate sur des courbes supersingulières de 128 bits de sécurité

Read more...

DIWALL Seminar - Nov. 18, 2010 - 14:00-16:00

2010-11-18T14:00:00.000+01:00

At Supelec, Rennes

Gildas Avoine, UCL, Louvain-la-Neuve, Belgique: Security Challenges in RFID

Radio Frequency Identification (RFID) allows to identify and authenticate objects or subjects without any physical nor optical contact, using transponders - micro-circuits with an antenna - queried by readers through a radio frequency channel. This technology is one of the most promising of this decade and is already widely used in applications such as access cards, public transportation, payment cards, and passports. This success is partly due to the steadily decrease in both size and cost of passive transponders called tags.

The shared enthusiasm for RFID makes people think that everything is do-able with any kind of RFID, especially with low-cost tags. Reality is a bit different. In particular, the characteristics of this technology - ubiquity, low-resource, wireless - open a security breach that should be seriously considered.

After a brief introduction about the technology, we will focus in this talk on the security threats. We will propose a classification and show that victims are not only the end-users but they can also be the systems' owners. We will see what is possible today in terms of security and what are the challenges we have to address. Among others, we will consider the following topics: impersonation, privacy, denial of service.

Christoph Neumann and Olivier Heen, Technicolor, Rennes: About Wi-Fi fingerprinting

A Wi-Fi fingerprint is a measurable characteristic of a Wi-Fi system. A good Wi-Fi fingerprint is accurate, easily measurable and hardly forgeable by an attacker. First, we will introduce Wi-Fi fingerprinting and its applications. Then we will detail and discuss two Wi-Fi fingerprinting methods from the literature and known attacks.

HDR Christophe Bidan - Nov. 16, 2010 - 10h15

2010-11-16T10:15:00.002+01:00

Campus de Rennes de Supelec

Soutenance d'habilitation à diriger les recherches de Christophe BIDAN

Contribution à la sécurité des réseaux auto-organisés

Jury

M. Rafael DESOUSA, Université de Brasilia (examinateur)
M. Yves DESWARTE, LAAS-Toulouse (examinateur)
M. Ludovic ME, Supélec (examinateur)
M. Gerardo RUBINO, INRIA Bretagne-Atlantique (examinateur)
Mme Maryline LAURENT, TELECOM SUD Paris (rapporteur)
M. Serge VAUDENAY, EPFL, (rapporteur)

GIPSy 2010 - Nov, 15-16 2010

2010-11-15T09:00:00.000+01:00

Workshop on Games, Logic and Securit, Rennes, France.

The main goal of this workshop is to gather researchers interested in games, logic and security (in a broad sense), and to offer a privileged forum to present their work and exchange ideas on these topics. Read more.

Important dates

Submission deadline: 22nd October 2010
Notification to authors: 1st November 2010
Deadline for registration: 4th November 2010
Workshop: 15th-16th November 2010

Rennes Cryptography Seminar - Nov. 12, 2010 - 14:00

2010-11-12T14:00:00.001+01:00

Rennes, campus Beaulieu, IRMAR, bat. 22, Room 016.

Jan Tuitman (LIX) - Counting points in families of nondegenerate curves

I will talk about an algorithm for computing zeta functions of a quite general class of algebraic curves (so called nondegenerate ones) using deformations in p-adic cohomology. I will give an overview of the mathematics that is involved, talk about my MAGMA implementation, and give some examples.

Appel à soumission SSTIC 2011

2010-11-03T08:52:00.004+01:00

Rennes Cryptography Seminar - Oct. 29, 2010 - 14:00

2010-10-29T14:00:00.004+02:00

Rennes, campus Beaulieu, IRMAR, bat. 22, Room 016.
Méhdi Tibouchi (ENS) : Hachage vers les courbes elliptiques et hyperelliptiques. read more...

Rennes Cryptography Seminar - Oct. 15, 2010 - 14:00

2010-10-15T14:00:00.002+02:00

Rennes, campus Beaulieu, IRMAR, bat. 22, Room 016.
Eimar Byrne (University College Dublin): An Algebraic Decoding of Negacyclic Codes Over the Integers Modulo 4. read more...

DGA-INRIA - Oct. 15, 2010 - 11:00

2010-10-15T11:00:00.004+02:00

Le deuxième séminaire sur le thème des méthodes formelles appliquées à la sécurité des équipements de sécurité aura lieu vendredi 15 octobre à11h, dans la salle Métivier de l'INRIA Rennes.
Il a pour titre "Analyse statique et compilation certifiées pour la sécurité" (read more...) et sera donné par Sandrine Blazy, Laurent Hubert et Thomas Jensen de l'EPI CELTIQUE.

Les séminaires sont ouverts à tous. Afin de faciliter l'accès à la salle du séminaire, les personnes extérieures à l'INRIA et à l'IRISA doivent s'inscrire d'ici le mercredi 13 octobre en donnant leur nom et leur affilia

Analyse statique et compilation certifiées pour la sécurité, Thomas Jensen, Sandrine Blazy, Laurent Hubert, EPI CELTIQUE, IRISA - INRIA Rennes Bretagne Atlantique

Les travaux de l'équipe CELTIQUE portent sur l'amélioration de la sécurité et la sûreté du logiciel en fournissant des certificats logiciels attestant du bon comportement d'un logiciel. Ces certificats sont obtenus suite à des analyses sémantiques. L'emploi de méthodes formelles (analyse statique et méthodes déductives de preuve) pour spécifier ces analyses sémantiques permet de plus de s'assurer de la correction de ces analyses. Les deux domaines d'application principaux sont les logiciels Java utilisés dans les téléphones mobiles, ainsi que les programmes C embarqués dans des équipements sécuritaires. Ce séminaire présente deux exposés portant sur ces deux domaines.

L'exposé de Sandrine Blazy présentera le compilateur CompCert, un compilateur réaliste, modérément optimisant du langage C. CompCert a été développé et prouvé correct à l'aide de l'assistant à la preuve Coq. La preuve de correction établit que le code assembleur engendré se comporte exactement comme prescrit par la sémantique du source C, éradiquant ainsi toute possibilité de bugs introduits par le compilateur et établissant un niveau de confiance sans précédent envers ce compilateur. (Travail commun avec Xavier Leroy - INRIA Paris-Rocquencourt)

L'exposé de Laurent Hubert présentera un système de types dédié à l'initialisation d'objets en Java. Le CERT et Sun recommandent de ne pas autoriser les accès aux objets Java en cours d'initialisation. Cette recommandation n'a pas toujours été suivie et a été source de failles de sécurité importantes. Jusqu'à présent, il n'existait cependant pas de moyen automatique de vérifier qu'un code respecte bien cette politique. Laurent présentera un système de types permettant de spécifier une politique d'initialisation et de la vérifier automatiquement. Le système de types et sa preuve de correction ont été formalisés et vérifiés avec l'assistant à la preuve Coq. (Travail commun avec Thomas Jensen, Vincent Monfort et David Pichardie, présenté cette année à ESORICS)

OSSIR Bretagne - 14 octobre 2010 - 14h00-16h30

2010-10-14T14:00:00.002+02:00

OSSIR Bretagne - 14 octobre - 14h-16h30
à SII, Immeuble Newton, entrée C, 3è étage, 3 bis, avenue Belle Fontaine, 35510 Cesson-Sevigné

14h00 Yvonnick DAVID (IPDIVA) : Sécurité des accès externes au SI

comment développer une large gamme de services tout en préserver la compartimentation étanche des infrastructures ?
Dans le domaine de l'accès distant sécurisé, IPdiva présentera sa plateforme technologique IPdiva Médiation, plateforme de VPN applicatif (VPN SSL). Cette plateforme technologique se caractérise par une topologie de déploiement répartie "à double barrière de contrôle d'accès". Son mode de déploiement non intrusif garanti une compartimentation étanche entre Internet et le réseau interne support des ressources devant être rendues accessibles à distance.Par ailleurs cette plateforme autorise des échanges applicatifs de type Nomade-site central ou de type site-à-site.

15h15 - Olivier HEEN (Technicolor) : Retour sur la conférence ESORICS 2010

ESORICS 2010, pour European Symposium on Research in Computer Security, s'est tenue à Athènes du 20 au 22 septembre 2010. Je ferais un bref retour sur l'ensemble de la conférence avant de présenter les contributions selon moi les plus marquantes.

CRI'Ouest - Oct. 14, 2010 - 8:30-17:00

2010-10-14T08:30:00.002+02:00

Faculté des Métiers - Campus de Ker Lann - Rue des Frères Montgolfier - 35170 BRUZ - tél. 02 99 05 45 00

SÉMINAIRE : LE R.O.I. "ROI" ?,

Dans un contexte économique encore tendu et incertain, les dirigeants d’entreprises recherchent souvent des gains de performance à court terme et privilégient les projets porteurs de développement d’activité et de croissance. Il n’est donc pas surprenant que les DSI soient plus que jamais sollicités sur la justification du R.O.I. (Return On Investment – Retour Sur Investissement) des projets informatiques.
Ce séminaire a été conçu pour les aider à apporter des réponses adaptées aux exigences de la démarche R.O.I. Les approches peuvent en effet varier d’un environnement à l’autre et l’échange d’expériences vécues enrichira cette journée. Le témoignage de dirigeants sera également un temps fort de ce séminaire contribuant à positionner le R.O.I en véritable outil de management et de mesure de performance du système d’information au service d’une stratégie.

INSCRIPTION
Les adhérents GRANIT sont invités à le préciser à l'inscription à : Christine BRETEL - Secrétariat CRI'Ouest - Tel. : 02 40 44 61 06 - contact(@)criouest(.)org

PhD Thesis, Mehdi Talbi - Oct. 8, 2010 - 15h00

2010-10-08T15:00:00.004+02:00

Campus de Rennes de Supelec

Soutenance de thèse de Mehdi Talbi : Spécification et vérification automatique des propriétés des protocoles de vote électronique au moyen de la logique ADM

Les systèmes de vote électronique sont basés sur des protocoles cryptographiques faisant usage de primitives avancées (chiffrement homomorphe, signature en aveugle, etc.) et impliquant des canaux de communication élaborés (anonymes, privés) dans le but de garantir certaines propriétés de sécurité : éligibilité, équité, anonymat, etc. Pour les systèmes critiques tels que celui du vote électronique, l’usage des méthodes formelles, pour prouver que les propriétés prétendues satisfaites par un protocole sont réellement garanties, devrait être incontournable.
Dans cette thèse, nous proposons d’utiliser la logique modale ADM afin de spécifier une sélection de propriétés de sécurité. Ces propriétés sont vérifiables par rapport à un modèle à base de traces représentant des exécutions valides du protocole. Notre modélisation des protocoles tient en compte de la présence d’un intrus actif dont le pouvoir de déduction est ajusté en fonction des spécificités introduites par le vote électronique. La modélisation des protocoles et la spécification des propriétés sont appuyées par une étude de cas portant sur le protocole de vote FOO dont nous proposons une analyse de sa sécurité. En complément, nous proposons d’exploiter le système de preuve qui accompagne la logique ADM, afin d’implémenter un outil permettant d’automatiser le processus de la vérification formelle des propriétés spécifiées par rapport aux traces du protocole analysé.

Jury

Kamel ADI, Rapporteur - Université du Québec en Outaouais
Riadh ROBBANA, Rapporteur - INSAT Tunis
Sophie PINCHINAT, Examinatrice - IRISA
Sihem GUEMARA, Examinatrice - Supcom Tunis
Adel BOUHOULA, Directeur de thèse - Supcom Tunis
Ludovic MÉ, Directeur de thèse - Supélec Rennes
Valérie VIET TRIEM TONG, Co-Directeur de thèse - Supélec Rennes

Rennes Cryptography Seminar - Oct. 8, 2010 - 14:00

2010-10-08T14:00:00.004+02:00

Rennes, campus Beaulieu, IRMAR, bat. 22, Room 016.
Pierre-Jean Spaenlehauer (LIP6) : Systèmes bilinéaires et déterminantiels -algorithmes, complexité etapplications à la cryptanalyse. read more...

Rennes Cryptography Seminar - Oct. 1, 2010 - 14:00

2010-10-01T14:00:00.003+02:00

Rennes, campus Beaulieu, IRMAR, bat. 22, Room 016.
Sorina Ionica (Université de Versailles Saint-Quentin-en-Yvelines) : Couplages et volcans d'isogenies. read more...
Vanessa Vitse (Université de Versailles Saint-Quentin-en-Yvelines) : Calcul d'indices sur courbes elliptiques. read more...

DGA-INRIA - Oct. 1, 2010 - 11:00

2010-10-01T11:00:00.002+02:00

Salle Métivier de l'INRIA Rennes

Quelques problèmes de sécurité informatique en rapport avec les méthodes formelles, par Dominique Chauveau (SPR, DGA-MI) et David Lubicz (CRY, DGA-MI)

Les départements CRY et SPR de la DGA-MI s'occupent principalement de l'implémentation, l'intégration et la validation de la cryptographie dans des produits de sécurité. Dans cet exposé, nous présentons différents problèmes liés à ces activités pour lesquels l'utilisation de techniques découlant des méthodes formelles sont soit déployées, soit envisagées.

Afin de faciliter l'accès à la salle du séminaire, les personnes extérieures à l'INRIA et à l'IRISA doivent s'inscrire d'ici le mercredi 29 septembre en donnant leur nom à Lydie Mabil lydie(.)mabil(@)irisa(.)fr

Grafotech Security - Sep. 29, 2010 - 18:00-20:00

2010-09-29T18:00:00.001+02:00

CCI de Rennes, salle Ouessant.
Retour expérience certification ISO 27001-2005 chez Orange Business Services.
Intervenant : Stéphane Sciacco, Direction de la Sécurité à Orange Business Services.
Introduction et animateur du forum : Stéphane Goarnisson.
Pour des raisons d'organisation, merci d'envoyer vos Prénom/Nom/Fonction/Société à l'adresse grafotech(@)granit(.)org

CRI'Ouest - Sep. 27, 2010 - 17:45-20:30

2010-09-27T17:45:00.001+02:00

CCI Nantes Saint-Nazaire
Inscription : contact(@)criouest(.)org

SENSIBILISER ET FORMER A LA SSI

Qui n’a jamais entendu ou affirmé « Le problème se trouve entre la chaise et le clavier » ? Elle est l’expression couramment utilisée pour évoquer que plus de 80 % des incidents informatiques ont pour cause une négligence d’un utilisateur. (lire la suite)

Cet événement est aussi sur l'agenda de la sécurité.

PhD Thesis, Fuchun Xie - Sep. 23, 2010 - 10h30

2010-09-23T10:30:00.001+02:00

Soutenance de thèse de Fuchun Xie
Salle Metivier, IRISA/INRIA-Rennes

Tatouage sûr et robuste appliqué au traçage de documents multimédia

Cette thèse porte sur la conception d'une technique de tatouage sûr et robuste dans le contexte du traçage de documents multimédia, et propose un système complet du traçage de traîtres. Ces travaux s'appuient sur la technique de tatouage zéro-bit robuste `Broken Arrows', dont nous proposons des améliorations afin de la rendre plus robuste, notamment à l'attaque de débruitage de A. Westfeld, et plus sûre. Sa sécurité est renforcée au regard des attaques connues et publiées, telles que l'attaque de regroupement de A. Westfeld et l'attaque d'estimation de sous-espace de P. Bas. Par ailleurs, nous étendons sa sécurité en considérant des attaques non publiées. Nous proposons ainsi une nouvelle technique de tatouage sûr, basé sur un test de décision `a contrario' et une insertion avec maximisation sous contraintes d'imperceptibilité et de sécurité. Nous proposons dans le dernier chapitre un schéma complet de traçage de documents multimédia, basé sur les codes de Tardos en version q-aire symétrique et les techniques du tatouage améliorées
mentionnées plus haut. Comme les techniques du tatouage sont très robustes, nous pouvons détecter plusieurs symboles en un seul bloc attaqué, ce qui nous permet de proposer deux méthodes d'accusation étendues pour le code de Tardos. Les études expérimentales montrent les bonnes performances de notre schéma de traçage, y compris face à des attaques jusqu’alors mal gérées comme la fusion de documents.

Jury

Patrick BAS Rapporteur
Andreas WESTFELD Rapporteur
Atilla BASKURT Examinateur
William PUECH Examinateur
Caroline FONTAINE Directeur de thèse
Teddy FURON Co-directeur de thèse

Rennes Cryptography Seminar - Sep. 17, 2010 - 14:00

2010-09-17T14:00:00.000+02:00

Rennes, campus Beaulieu, IRMAR, bat. 22, Room 016.

Sébastien Gambs (IRISA): vers une carte d'identité préservant la vie privée

Travail conjoint réalisé avec Yves Deswarte (LAAS-CNRS).

Rennes Cryptography Seminar - Jul. 23, 2010 - 14:00

2010-07-12T16:56:00.001+02:00

Rennes, campus Beaulieu, IRMAR, bat. 22, Room 016.

Oumar Diao (IRMAR) - Quelques aspects de l'arithmétique des courbes hyperelliptiques de genre 2

Dans cet exposé, on s'intéresse aux briques utiles à la cryptographie asymétrique et principalement au problème du logarithme discret. Dans une première partie, nous présentons un survol de différentes notions algorithmiques de couplage sur des jacobiennes de courbes de genre 2 et décrivons les détails d'une implémentation soigneuse. Nous faisons une comparaison à niveau de sécurité équivalent avec les couplages sur les courbes elliptiques.
Une deuxième partie est dévolue à la recherche de modèles efficaces pour les courbes elliptiques et les surfaces de Kummer supersingulières en caractéristique 2. Nous utilisons pour cela des techniques de "déformation" qui consistent à considérer une famille de jacobiennes sur un trait, telle que la fibre générique soit ordinaire et la fibre spéciale soit la jacobienne considérée. Il s'agit alors de montrer que la loi de groupe sur la fibre générique s'étend à tout le modèle. Nous comparons les lois de composition ainsi obtenues avec celles déjà connues.

OSSIR Bretagne - 8 juillet 2010 - 14h15-17h

2010-07-08T14:15:00.007+02:00

OSSIR Bretagne - 8 juillet 2010 - 14h15-17h
à Technicolor, salle Vivaldi (demander Olivier Heen à l'accueil, prévoir pièce d'identité)

Ari Takanen (Codenomicon): Zero day vulnerability management

Codenomicon will explore the process of zero-day vulnerability management from initial threat analysis to automated vulnerability detection and remediation. We will demonstrate how easy it is to detect attack vectors and to quickly assess the reliability and security of those interfaces using general purpose fuzzing solutions. We will also show you how you can complement these solutions with known vulnerability data and do patch verification easily and cost-effectively. Finally, we will discuss how you can tailor your defenses to block zero day attacks, which is a key aspect of vulnerability management. (This talk will be given in english).
Bio: Ari Takanen has worked with information security since 1996 and concentrated on software security as a researcher in Oulu University Secure Programming Group (OUSPG) since 1998. Since 2001, Ari has moved to a spin-off company from the PROTOS project, first as a founder and CEO, and now the CTO of Codenomicon Ltd. He is author of two security books.

Guillaume Prigent (Diateam): Collecte d'information avec Netglub

Le domaine du renseignement d'origine source ouverte (OSINT en anglais pour open source intelligence) n'a aucun rapport avec l'expression open source utilisée dans la communauté du développement logiciel. De par ses enjeux et sa méthodologie, ce domaine n'est que partiellement outillé ou le plus souvent les briques technologiques utilisées sont réservées à quelques privilégiés qui préservent de manière propriétaire leurs plateformes, leurs outils et leurs méthodologies. S'il est pourtant vrai qu'il existe de plus en plus d'outil d'automatisation de recherche et de traitement à base d'information d'origine source ouverte, au travers du projet Netglub nous avons souhaité montrer qu'il était tout à fait possible de concevoir, implémenter et utiliser une plateforme libre ergonomique et fonctionnelle. L'objet de cette présentation, principalement axée sur l'exemple et la démonstration est de montrer quelles sont nos motivations, notre cadre de conception, nos premiers résultats et les pistes que nous souhaitons explorer désormais. Dans un premier temps nous effectuerons un bref rappel de la problématique que nous souhaitons adresser et du contexte dans lequel nous nous plaçons. Nous effectuerons ensuite une présentation méthodique et illustrée des composants principaux de notre architecture avant de conclure par quelques mises en œuvre opérationnelles de l'outil. La synthèse sur les pistes futures et nos travaux actuels permettra de laisser une place significative à des échanges.

Voir aussi sur l'Agenda De La Sécurité.

DIWALL Seminar - Jul. 1, 2010 - 14:00-16:30

2010-07-01T14:00:00.001+02:00

At Supelec, Rennes

Jonathan-Christopher Demay (Supélec) : Génération et évaluation de mécanismes de détection d'intrusion au niveau applicatif

Les systèmes de détection d'intrusion comportementaux reposent sur la construction d'un modèle de comportement normal de l'entité surveillée. Ce modèle est utilisé durant la phase de détection et permet de lever une alerte lorsqu'une déviation est observée. Contrairement à l'approche par scénario, cette méthode permet de détecter des attaques encore inconnues. Pour construire un modèle d'une application, on peut par exemple se baser sur les séquences d'appels système effectuées par le processus. Les arguments des appels système ainsi que leurs contextes d'exécution peuvent être utilisés pour améliorer précision et la complétude du modèle.
Néanmoins, des attaques contre les données de calcul peuvent être manquées et des attaques contre les données de contrôle peuvent être adaptées pour contourner le mécanisme de détection. Dans cette présentation nous nous concentrons essentiellement sur la détection des attaques ciblant les données de calcul. Pour cela, l'approche que nous proposons utilise l'état interne d'un programme pour détecter les corruptions mémoire engendrées par de telles attaques et pouvant mener à un appel système illégal. Pour obtenir ce résultat, nous proposons de construire un modèle de comportement normal orienté autour des données. Ce modèle est obtenu par analyse statique et des contrôles de vraisemblance sont dérivés de ce dernier avant d'être insérés dans le code source. Nous proposons ensuite une méthode d'évaluation de notre approche reposant sur l'injection de fautes.

Yvan Labiche, (Carleton University, Canada) : Software testing applied to intrusion detection engines

An Intrusion Detection System (IDS) protects computer networks against attacks and intrusions. One class of IDS is called signature-based network IDSs as they monitor network traffic, looking for evidence of malicious behaviour as specified in attack descriptions (referred to as signatures). Many studies report that IDSs have problems accurately identifying attacks. Therefore, it is important to precisely understand under which conditions IDSs accurately identify attacks or fail to do so. However, no systematic approach has so far been defined and used to study this problem.
Recognizing that signatures in essence provide the specification of an IDS engine, studying the accuracy of an IDS engine becomes a black-box testing problem. We therefore precisely and systematically evaluate which mature testing techniques can be used (and adapted) to derive tests from IDS signatures.

Preliminary results on applying testing techniques on one widely used and maintained IDS are discussed, showing that software testing techniques are effective at systematically revealing problems in this IDS engine (e.g., problems that prevent the detection of attacks)

Rennes Cryptography Seminar - Jun . 25, 2010 - 14:00

2010-06-25T14:00:00.000+02:00

Rennes, campus Beaulieu, IRMAR, bat. 22, Room 016.

Anne Canteaut (INRIA) : Modes opératoires pour les fonctions de hachage itératives

Dans une fonction de hachage itérative, le choix du mode opératoire est essentiel car il influence à la fois sa sécurité et ses performances. La notion d'indifférentiabilité, introduite par Maurer, Renner et Holenstein en 2004, est particulièrement adaptée au cas des fonctions de hachage. Elle permet de déterminer le nombre de requêtes à la fonction de compression nécessaires pour différencier la fonction de hachage d'un oracle aléatoire. Nous verrons un exemple de ce type de preuve sur la construction chop-MD, puis des résultats similaires sur la construction dite éponge et sur le nouveau mode opératoire utilisé dans Shabal, notre candidat à la compétition SHA-3.
Ceci résulte d'un travail commun avec les membres de l'équipe de Shabal http://www.shabal.com

Anne Canteaut (deuxième exposé) : Preuve d'indifférentiabilité avec distingueurs

(travail commun avec E. Bresson, T. Fuhr, T. Icart, M. Naya-Plasencia, P. Paillier, J-R. Reinhard, M. Videau)
Le principe d'une preuve d'indifférentiabilité est de montrer qu'une fonction de hachage construite selon un mode opératoire donné et utilisant une fonction de compression idéale se comporte comme un oracle aléatoire. Il est donc naturel d'en conclure que l'existence d'un distingueur sur la fonction de compression, si elle ne conduit pas forcément à une attaque sur la fonction de hachage proprement dite, montre que la preuve d'indifférentiabilité ne s'applique pas à la fonction considérée. Un problème crucial est donc de pouvoir déterminer si un distingueur donné affecte ou non la sécurité de la fonction de hachage. Une manière d'y répondre est de se demander s'il est possible d'adapter la preuve d'indifférentiabilité au cas où la fonction de compression est choisie uniformément parmi toutes les fonctions vérifiant la propriété structurelle associée au distingueur. Si une telle modification est possible, on peut alors quantifier la perte de sécurité due à l'existence du distingueur et éventuellement conclure à la sécurité de la fonction de hachage.
Dans cet objectif, nous introduisons une méthode générale pour prendre en compte l'existence de distingueur dans une preuve d'indifférentiabilité et montrons comment cette technique s'applique à chop-MD et au mode opératoire de Shabal. Nous conclurons notamment que la fonction Shabal conserve une sécurité prouvée au-delà du paradoxe des anniversaires, même en tenant compte des distingueurs à clefs liées introduits récemment sur la permutation paramétrée.

SSTIC 2010 Day 2 - a few notes

2010-06-21T10:10:00.002+02:00

Results of the SSTIC 2010 challenge

Raphaël Rigo presented the SSTIC 2010 challenge. This year, the challenge was organized by ANSSI. 1700 unique downloads (5 times more than SSTIC 2009).
Solving the challenge required reconstruction of an archive, edition of link to rebuild virtual memory image (some winners used very advanced tools for this, like grep and excel:), solving riddles or brute forcing, breaking a weak DSA key, … for more details, read the solutions.

Christian Brunette, David Pichardie, Frédéric Guihery, Goulven Guiheux, Guillaume Hiet ,

Security of JAVA's execution platform: limits and improvements
A very broad survey of java security issues. Back to the origin, Java was meant to answer security needs: no pointer, sandbox, clean garbage collection, etc. But now Java is becoming increasingly complex, the security mechanisms are not always used, the integration with the operating system is complex…
There are also vulnerabilities in the standard lib, related to serialization and reflexion, and still some vulnerabilities in the Java Virtual Machine itself. In particular, the confidential data is very remanent: no secure deletion, contamination…
The author then provided several recommendations for improving the security of Java. They also demonstrated an interesting tool to infer the nullness status of variables, for more information see [http://nit.gforge.inria.fr/ NIT].

Eric Lacombe, Fernand LONE SANG, Vincent Nicomette, Yves Deswarte, Efficiency of IOMMU

To make it short, the authors found a way to bypass an IOMMU. Namely it uses the unauthenticated source-id (as usual;) and the bridge between PCI and PCI express (not as usual). I really liked the result, but the talk himself was a bit too technical (for me).

Guillaume Valadon, Loic Duflot, Olivier Levillain, Yves-Alexis Perez, About security of network cards

This talk partly covers what was presented a few month ago at CanSecWest 2010. The presented vulnerability has the potential to allow remote control on a host from the internet (Owned by a ping). The authors first recalled the fundamentals of a networking card: DMA communications, NVRAM, DELS command, internal processor, SMBus for remote admin, PCI configuration space, … Note that the card firmware is loaded at driver start. It may be protected at load time, but it is vulnerable once in memory.
The author then showed the Remote Management and Control Protocol (RCMP) that is implemented on all cards, by specification. RCMP must answer requests even if the host BIOS is down. It also allows remote admin and wake-up on LAN.
This protocol naturally represent a high risk. The exploit is not trivial however. It involves forging a HMAC. This is possible because some fields are under the control of the attacker, and let the card act as an Oracle. Whenever the packet specification is not respected, the card crashes, which lets suspect a buffer overflow. The authors then showed how to instrument the buffer overflow, in particular by using an internal debugger.
The vulnerability is really frightening. Several variants take advantages of unused MAC addresses: up to 4 MAC addresses are allowed in network cards, the first one being preferably used, but the three other ones still answering. As the card can be remotely restarted, the attacker also control the reinitialization to a known state.

Sebastien Tricaud, The Honeynet Project in 2010

The author gave a precise explanation of the goals and the structure of the Honeynet project. The goal is “Improve Internet security at no cost for the public". The Honeynet project is rather research oriented, compared to shadowserver for instance that is more operation oriented. The Honeynet project produced series of papers: Know Your Enemy and Know Your Tools.
The Honeynet project allowed many experiments, like on 1st April 2010 when collecting 2211 binaries containing 32 individual viruses, undetected by ClamAV.
The author then presented some of the numerous research projects, including HonEeeBox, Dionaea…
Also see http://logviz.blogspot.com/

SSTIC 2010 Day 1 - a few notes

2010-06-18T16:46:00.000+02:00

Gouenou Coatrieux (Telecom Bretagne) Medical Image Watermarking, Applications and Methods

The author briefly recalled the global watermarking scheme. He showed various know application of watermarking (including Friedriech’99: repairing part of a picture, like a license plate in a car picture).
In the specific case of medical picture practitioners want:
1) guarantee that an image wasn’t modified (aspect mostly developed in the rest of the talk)
2) proof of origin.
The author provided examples of watermarked medical images. According to the watermarking technique one can find unmodified zones in a picture. These zones are reliable for making a diagnostic. Some techniques provide estimation of the modifications (in the frequency plan).
The watermark can also be used in, conjunction with a cryptographic hash function. I wasn’t convinced at all by the proposed scheme. Maybe it works with reversible watermarking...
For medical images, the standard is DICOM. It provides a Unique Identifier of images. It can be embedded in the picture itself using a watermark. Also, a hash of the medical report can be embedded in the picture. This is useful if the relation picture / report in a database is lost. Another use is retrieving reports of images close to a reference image (using perceptual fingerprint for closeness).
One major issue with medical images is the invisibility of the mark. The author recalled that the perception is very context dependant. He gives the know example of a geometric deformation: on a landscape with trees it is invisible but the same deformation on a coin is highly visible. Moreover, the signal level is very meaningful in medical images. For a same picture, on signal level focus on lungs, another focus on soft tissues and the last one on bones. A watermark could be invisible on some level but not on the other.
State-of-the art regarding this issue is either:
* use non-interest zones for setting the watermark (RONI). I’m really not convinced by this approach: if only non-interesting zones are marked, what is the effective robustness? Meaningful zone can be attacked to mislead a diagnostic, and the watermark won’t reveal it.
* Use reversible watermark. Gouenou quoted B. Macq and J. Friedrich earlier results.
The last issue is the interoperability between several systems. Here again, the non-existence of an acceptable psycho visual model is an obstacle.

Philippe Lagadec (NATO C3 agency) Dynamic risk analysis and visualization

The authors showed two tools: CIAP for the visualization of complex risk situation and DRA for the Dynamic Risk Assessment. He gives the definition of cyber defense: real time defense of systems and networks. This does not covers long term or static topics like crypto, firewalling, access control. On the other hand, this covers all the operational aspects.
The decision cycle is classical: Observe, Analyze, Decide, Act. Nowadays tools mostly correspond to “observe”: logs, ids, antivirus, supervision, forensics, reverse. A few solutions correspond to “analyze” but correlation is still an active research topic (e.g. correlate logs and alerts). The lack of consolidation comes from the absence of a common notation between tools. Moreover, tools outputs are human readable and not program readable (API, normal form data...)
The CIAP tool is developed at NATO since 2007. It tries to overcome the limitations by aggregating the view of several tools. Data from several tools can be queried dynamically. There is no aggregation in a single database: this avoids duplications and expansive state coherency. Instead, the queries are mapped to the original tools. The CIAP demo shows several view of an operational situation:
* Flat database: typically sorted by IP, click to get additional details... very much like supervision.
* Network view: shows topology/subnets. White: OK, yellow: vulnerability detected by one tool, red alert detected by one tool.
* Hierarchical view: supervision style, like HPOV. Useful for large networks.
* Radial graph: same as zenmap graphs.
* Geographical: direct mapping of targets on Google earth. Very nice: The XML data flow is directly converted to KML format. In can be mixed with other geographical flows (like physical security assets, vehicles,...)
* Treemaps: shows both the hierarchal structure and the relevant elements of alerts.
The DRA tool: it is the association of an attack graph tool and a risk assessment tool (PILAR). The demo shows a classical 3/3 architecture with a firewall. According to the change of the vulnerability level of components, the attack graph is recomputed, and the exposure level changes.

Fabien Allard, Mathieu Morel, Paul Gompel, Renaud Dubois: CASTAFIOR: automatic detection of tunnels

In many situations, attacker set HTTPS tunnels (Trojan, evasion, backdoors...) CASTAFIOR tries to automatically detect the protocols in the tunnel, e.g. telnet, SSH, HTTP, POP3, SMTP, SCP, IMAP...
CASTAFIOR is basically the association of two complementary classifiers: random forest and hidden Markov model. To make is short, random forest gives a good classification according to global parameters of a session: average delay between packets, average ratio in/out... on the opposite, Hidden Markov Models are good for the detection of single characteristic like a large packet then only small packets...
The author reach 97% accuracy on a large test set with 20 protocols. 97% is a good research result, although still far from real operational needs, especially for high volumes of encrypted traffic.
On the test cases, the learning stages took 45s per protocols. The detection phase takes less than 5ms.

Eric Freyssinet, Figthing against botnets

There is not enough coordination of defense in this domain. A task force is crated for one year, on the same model that the “virtual worlds” task force and the “Live forensic” task force. The team Cymeru (pronounced Cameri) already joined the task force.

Christophe Devine and Damien Aumaître: VirtDBG: towards a ring -1 debugger for window 7

The initial goal was to run a low-level debugger on Windows 7.
Running a low level debugger on W7 is complicated: how to set the debug mode, how to bypass PatchGuard...
Local ring 0 debugger (like SoftIce, Syser or rr0d) are to close from the architecture and will crash.
The author used a PCI/DMA access (cf. SSTIC 2008 and SSTIC 2009 :) with a FPGA card (COM 1400). This access is used twice: to avoid PatchGuard and then communicate with the stub. Communication through this non synchronized memory channel is still a complex issue.
To avoid PatchGuard during the installation of the (unsigned) stub, the author hooked a pointer that is not often checked in integrity: if check during hooking -> blue screen, otherwise the stub is installed. The stub is “just” an hypervisor à chaud (like bluepill). Mostly undetectable by anti-VM protection. The stub is compatible with gdb, and thus with metasm.
Limitations: bugs of COM 1400 card, only works on Intel (AMD port in progress).

Daniel Reynaud, Jean-Yves Marion, Wadie Guizani: program trace analysis for reverse

Very impressive work from the Nancy team, for improving reverse engineering. There are known cases where static analysis fails: self-modifying code, packed code, self-encrypted... The authors use execution trace to help disassembly. Per se it’s not totally new but their approach is really interesting: generate generic traces, just add them to IDA and use the enriched disassembly. They build their own tool to collect the traces: tracesurfer.
The approach is experimentally validated against a large number of cases: dozen of packers first, and then tens of hundreds of malwares. In more than 80% cases, the trace approach allowed the reverse.

Grafotech Security - Jun. 17, 2010 - 18:00-20:00

2010-06-17T18:00:00.000+02:00

CCI de Rennes, salle Ouessant.

GPL (logiciels libres) – Protection du patrimoine intellectuel et risques juridiques pour l’entreprise.

Intervenant : Maitre Bernard LAMON, avocat au sein du cabinet Avoxa (Rennes).
Animateur : Yannick DERRIEN - Consultant ACE TIMING (Cesson Sévigné).

Pour des raisons d'organisation, merci d'envoyer vos Prénom/Nom/Fonction/Société à l'adresse grafotech(@)granit(.)org

Post SSTIC hangover

2010-06-16T09:34:00.003+02:00

Yet Another SSTIC. Many blogers covered the event.

For the coverage in Brittany, you can read: JoP, N0Secure, GomoR.

For a broader coverage, Sid gives a very comprehensive list of references.

Rennes Cryptography Seminar - Jun . 11, 2010 - 14:00

2010-06-11T14:00:00.001+02:00

Rennes, campus Beaulieu, IRMAR, bat. 22, Room 016.

Tony Ezome ( Université Toulouse I ) : Des algorithmes pour la cryptographie asymétrique

Des algorithmes pour la cryptographie asymétrique
En cryptographie, on souhaite protéger des messages. Et pour ce faire certains cryptosystèmes en cryptographie asymétrique utilisent les nombres premiers. Il est donc très utile de pouvoir déterminer la primalité de grands entiers.
Le test AKS est un algorithme déterministe de preuve de primalité qui a été publié en Août 2002 par Agrawal, Kayal et Saxena ("Primes is in P"). L'algorithme ECPP (Elliptic Curves Primality Proving) est un test de primalité probabiliste. Il a été proposé par A.O.L Atkin en 1988 et c'est l'un des tests de primalité les plus efficaces utilisés en pratique.
Dans cet exposé, nous donnerons un critère de primalité de type AKS utilisant les courbes elliptiques : le critère AKS elliptique. Après avoir rappelé les tests Miller-Rabin, AKS et ECPP, nous généraliserons le critère AKS en termes d'extension étale S de Z/nZ munie d?un automorphisme. L'illustration, sur un exemple simple, du critère AKS elliptique va clôturer l'exposé.

SSTIC 2010 - Jun. 9-10-11, 2010

2010-06-09T09:00:00.000+02:00

Programe

Brittany Researcher - Joaquin Garcia-Alfaro

2010-06-08T06:48:00.006+02:00

Joaquin Garcia-Alfaro is a research engineer at Télécom Bretagne. He received a Bachelor, a Master's and a Ph.D. degree with honors, all in Computer Science, from the Université Autonome de Barcelone (UAB, Catalonia) and the Univesité de Rennes 1. He holds two engineering awards from UAB, a doctoral fellowship award from the Catalan Government and a graduate award from the "la Caixa” savings bank foundation. He recently joined the LUSSI department of Télécom Bretagne, in Rennes, where he is working with the SERES team towards his HDR. Before that, he was working as a lecturer professor for the Computer Science and Multimedia Studies of the Open University of Catalonia (UOC). He closely cooperates with the NRG (Network Research Group, Carleton University, Canada), SENDA (Security of Networks and Distributed Application, UAB), and KISON (K-ryptography and Information Security for Open Networks, UOC) groups (research projects, seminars, Ph.D. advising committees and Master's lectures).
His research interests include a wide range of network security problems, with an emphasis on the management of security policies, analysis of vulnerabilities, and enforcement of countermeasures. He is reviewer for various magazines, journals and symposiums, and has co-authored more than 30 selected peer-reviewed publications related to applied computer security in relevant journals and conference proceedings. He regularly serves on program committees of international security conferences and was the Program Committee Chair of the ESORICS' workshops DPM (Data Privacy Management) 2009 and 2010.

CRI'Ouest - May 31, 2010 - 17:45-20:30

2010-05-31T17:45:00.001+02:00

CCI Nantes Saint-Nazaire
Inscription : contact(@)criouest(.)org

Septième Forum Sécurité et Management de l’Information :
RSSI - les outils pour piloter la sécurité

Un précédent Forum avait conclu sur le constat qu'un RSSI devait être à la fois un expert technique, un manager, un communiquant et un vendeur pour exercer correctement sa mission. Véritable pilote de la Sécurité des Systèmes d'Information, il doit agir sur ses différentes composantes (gestion des risques, intégration de la sécurité dans les projets, mise en conformité vis-à-vis de la législation et des règlements, conduite d'actions techniques) tout en partageant avec ses homologues pour mieux s'adapter à l'évolution des menaces...
Quels sont les outils à la disposition du RSSI pour être efficace dans ces différents domaines ?

Rennes Cryptography Seminar - May . 21, 2010 - 14:00

2010-05-21T14:00:00.002+02:00

Rennes, campus Beaulieu, IRMAR, bat. 22, Room 016.

Yannick Seurin, France Telecom : indifférentiabilité et preuves de sécurité dans des modèles idéalisés

Les preuves de sécurité en cryptographie font très souvent appel à des modèles idéalisés consistant à remplacer un certain composant d'un cryptosystème par la primitive idéale correspondante (par exemple une fonction de hachage modélisée par un oracle aléatoire).

Dans cet exposé nous présenterons le concept d'indifférentiabilité introduit par Maurer, Renner et Holenstein et son application aux preuves de sécurité dans des modèles idéalisés. Nous discuterons en particulier le résultat d'équivalence entre le modèle de l'oracle aléatoire et celui du chiffrement par blocs idéal dû à Coron, Patarin et Seurin. Nous évoquerons également d'autres résultats, en particulier sur l'extension du domaine d'un chiffrement par blocs idéal.

Rennes Cryptography Seminar - May . 14, 2010 - 14:00

2010-05-14T14:00:00.001+02:00

Rennes, campus Beaulieu, IRMAR, bat. 22, Room 016.

Pascal Molin, Université Bordeaux : Intégration numérique prouvée pour la théorie des nombres

La théorie des nombres rend nécessaire le calcul de certaines intégrales à des précisions permettant un travail arithmétique. On présentera une méthode à la fois simple, rapide et prouvée pour y parvenir. Il existe depuis une vingtaine d'années un paradigme d'intégration numérique, dit des fonctions doublement exponentielles, qui dans la pratique converge très rapidement pour des fonctions régulières. La fonction intnum sous PARI/gp implante ces idées. On donnera une interprétation de ce paradigme, et une démonstration rigoureuse, avec un terme d'erreur explicite, d'une couvergence quasi-linéaire sousdes hypothèses raisonnables. On discutera l'optimalité de la méthode et l'extension de son champ d'application. Deux applications seront décrites : le calcul de périodes de variétés hyperelliptiques et celui de valeurs de fonctions L, à précision garantie arbitraire.