Université Paris 13, Villetaneuse "Qualité logicielle"
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.
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
Laure Petrucci, LIPN
Roberto Di Cosmo, GTLL
Jean Mairesse, CNRS
Catuscia Palamidessi, LIX
Benjamin Morin, ANSSI
Tayssir Touili, LIPN
John Regehr, TrustInSoft
Fabrice Kordon, LIP6
Véronique Delebarre, SafeRiver
Laure Petrucci, LIPN
Roberto Di Cosmo, GTLL
Jean Mairesse, CNRS
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.
Benjamin Morin, ANSSI
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.
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.
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.
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.
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 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.