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.