The Open Source
Innovation Spring 2019

Qualité logicielle | IoT | Cloud | Big Data | Systèmes d'information

Mars-juin 2019, Paris - Châtillon

Présidence : Roberto Di Cosmo, vice-président du GTLL, directeur de l’Irill, directeur de recherche Inria, Professeur à l’Université Paris-Diderot

Organisé par : logo Systematic & logo IRILL

Retour à l'OSIS

Sécurité, Sûreté et Confidentialité

10 Mai 2016 — Sécurité, Sûreté et Confidentialité

09h-19h

Université Paris 13, Villetaneuse "Qualité logicielle"

Résumé

Le logiciel est devenu partie intégrante de tous les aspects de notre vie et de notre société, et cela pose de nombreux défis : il faut s'assurer qu'un logiciel fait bien ce pour quoi il est prévu (sûreté de fonctionnement), qu'il n'y a pas de comportements non autorisés (sécurité), et qu'il permet le respect de la confidentialité des données. Ce sont autant de défis importants qui sont interconnectés.
 

Lors de cette journée, académiques et industriels feront le point sur l'état de l'art. Ce sera une occasion unique de comprendre ce que font la recherche et l'industrie dans ces domaines critiques pour notre futur.

Direction de programme

Programme dirigé par Laure Petrucci, directrice du Laboratoire d'Informatique de Paris Nord (LIPN), Université Paris 13, et Roberto Di Cosmo, directeur de l'Irill, Inria, professeur à l'Université Paris-Diderot

Programme résumé

  • 09:20: Ouverture de la journée

    Laure Petrucci, LIPN

  • 09:30: Présentation du Groupe Thématique Logiciel Libre

    Roberto Di Cosmo, GTLL

  • 09:45: L'année de la Sécurité au CNRS

    Jean Mairesse, CNRS

  • 10:00: Differential privacy and applications to location privacy

    Catuscia Palamidessi, LIX

  • 11:15: Prise en compte de la sécurité dans la conception et le développement de logiciels

    Benjamin Morin, ANSSI

  • 12:00: Model-checking for efficient malware detection

    Tayssir Touili, LIPN

  • 12:45: Buffet déjeunatoire
  • 14:00: SQLite with a Fine-Toothed Comb

    John Regehr, TrustInSoft

  • 14:45: Building and verifying a quasi-certification entity over Distributed Hash Tables

    Fabrice Kordon, LIP6

  • 15:30: Pause
  • 16:00: Mise en œuvre des méthodes de vérification de modèle et d'analyse statique de code pour la détection de faiblesses et de vulnérabilités

    Véronique Delebarre, SafeRiver

Lieu

Université Paris 13

Ville: Villetaneuse


Programme détaillé

  • 09:20 - Ouverture de la journée

    Laure Petrucci, LIPN

  • 09:30 - Présentation du Groupe Thématique Logiciel Libre

    Roberto Di Cosmo, GTLL

  • 09:45 - L'année de la Sécurité au CNRS

    Jean Mairesse, CNRS

  • 10:00 - Differential privacy and applications to location privacy

    Catuscia Palamidessi, LIX

    Differential privacy is one of the most successful approaches to prevent disclosure of private information in statistical databases. It provides a formal privacy guarantee, ensuring that sensitive information relative to individuals cannot be easily inferred by disclosing answers to aggregate queries. Most importantly, and in contrast to other previous notions of privacy, it is robust under composition attacks. In this talk we present a generalized version of differential privacy, that is suitable to protect secrets in any metric domain. Then, we explore an application of this generalized version to the case of location privacy, where domain consists of the locations on a map and the distance is the geographical distance. This instance of the property, that we call geo-indistinguishability, is a formal notion of privacy for location-based systems that protects the user's exact location, while allowing approximate information - typically needed to obtain a certain desired service - to be released.
    We describe how to use our mechanism to enhance Location Based Services (LBS) with geo-indistinguishability guarantees without compromising the quality of the service, and we describe an implementation based on a planar Laplacian noise. It turns out that, among the “universal” mechanisms (i.e., those which do not depend on a prior distribution), ours is the one that offers the best privacy guarantees. Finally we present a tool, Location Guard, based on our framework, which allows to use LBS’s on browsers without revealing the exact location of the user.

  • 11:15 - Prise en compte de la sécurité dans la conception et le développement de logiciels

    Benjamin Morin, ANSSI

  • 12:00 - Model-checking for efficient malware detection

    Tayssir Touili, LIPN

    The number of malware is growing extraordinarily fast. Therefore, it is important to have efficient malware detectors. Malware writers try to obfuscate their code by different techniques. Many of these well-known obfuscation techniques rely on operations on the stack such as inserting dead code by adding useless push and pop instructions, or hiding calls to the operating system, etc. Thus, it is important for malware detectors to be able to deal with the program's stack. In this talk, we propose a new model-checking approach for malware detection that takes into account the behavior of the stack. We implemented our techniques in a tool, and we applied it to detect several viruses. Our results are encouraging. In particular, our tool was able to detect more than 800 viruses. Several of these viruses could not be detected by well-known anti-viruses such as Avira, Avast, Norton, Kaspersky and McAfee.

  • 12:45 - Buffet déjeunatoire
  • 14:00 - SQLite with a Fine-Toothed Comb

    John Regehr, TrustInSoft

    What should we do about security-critical software that is too large to be formally verified? This talk explores the practical approach of repurposing a C verifier as an interpreter, sacrificing soundness but gaining scalability and eliminating overapproximation-related alarms. This mode of analysis works best for systems that have very thorough test suites, whether manually constructed or generated by a tool such as afl-fuzz. Using Frama-C as an interpreter we have analyzed widely-used, security-critical libraries such as SQLite, libpng, and libwebp, finding a number of issues in each and also paving the way for future verification efforts.

  • 14:45 - Building and verifying a quasi-certification entity over Distributed Hash Tables

    Fabrice Kordon, LIP6

    Building a certification authority (CA) that is both decentralized and fully reliable is impossible. However, the limitation thus imposed on scalability is unacceptable for many types of information systems, such as e-government services. This talk explores a solution based on a Distributed Hash Table (DHT) and has been formally verified to prove that we get close to full reliability: a CA with a probability of arbitrary failure so low that, in practice, false positives should never occur. The verification of this protocol was performed with several tools among which some are integrated in the CosyVerif platform.

  • 15:30 - Pause
  • 16:00 - Mise en œuvre des méthodes de vérification de modèle et d'analyse statique de code pour la détection de faiblesses et de vulnérabilités

    Véronique Delebarre, SafeRiver

    La réduction des coûts des activités de validation et de vérification est une opportunité pour les méthodes formelles à différentes étapes du cycle de développement. D’une part les référentiels normatifs en admettent le principe, mais d’autre part le développement de composants génériques voire de plates-formes qui doivent ensuite être déployées avec un coût optimisé de revalidation incite fortement à utiliser des moyens de vérification automatisés. Mais, les utilisateurs ou promoteurs de ces méthodes ont besoin de chiffres : « Que font gagner les méthodes formelles » ? « quels sont les coûts de mise en œuvre » ?, « combien de faux positifs » ? « quel est le positionnement par rapport aux tests » ? etc. Une grande partie des réponses réside dans la capacité à montrer que les résultats obtenus sont complets et robustes. Notre retour d’expérience résulte de 10 ans d’expérimentations sur des cas industriels et sera illustré sur trois cas d’utilisation de méthodes statiques : la preuve d’exigences fonctionnelles de sécurité dans le contexte d’un développement « model based design » de système complexe, la vérification d’absence d’interférence dans le cas d’un système embarquant des composants logiciels de différents niveaux, et enfin, la détection de vulnérabilités dans un logiciel.

Organisateurs et/ou sponsors

  • CNRS

    Le Centre national de la recherche scientifique est un organisme public de recherche (Établissement public à caractère scientifique et technologique, placé sous la tutelle du Ministère de l'Éducation nationale, de l'Enseignement supérieur et de la Recherche). Il produit du savoir et met ce savoir au service de la société.

  • Inria

    Inria a pour mission d’avoir un impact économique et sociétal s’appuyant sur ses succès scientifiques. C’est une mission centrale d’Inria, qui se décline à l’échelle de l’institut, de ses centres et de chaque équipe projet. Dans notre domaine du numérique, pour concrétiser ce transfert, nous avons décidé de privilégier la voie de la création d’entreprises.

  • LIPN