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

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/2011 - 10h30

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

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

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

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

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

à la Cantine Numérique

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

Inscriptions

Rennes Cryptography Seminar - Oct, 21 2011 - 14: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

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

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

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

======================================================================
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

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

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

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

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

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

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

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

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

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é)

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.

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é - 24 juin 2011 - 11h

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

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

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

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

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

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

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

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

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

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

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

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

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

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

À 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

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

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

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

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.