BEGIN:VCALENDAR VERSION:2.0 PRODID:icalendar-ruby CALSCALE:GREGORIAN METHOD:PUBLISH BEGIN:VTIMEZONE TZID:Europe/Paris BEGIN:DAYLIGHT DTSTART:20160327T030000 TZOFFSETFROM:+0100 TZOFFSETTO:+0200 RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3 TZNAME:CEST END:DAYLIGHT BEGIN:STANDARD DTSTART:20161030T020000 TZOFFSETFROM:+0200 TZOFFSETTO:+0100 RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10 TZNAME:CET END:STANDARD END:VTIMEZONE BEGIN:VEVENT DTSTAMP;TZID=Europe/Paris:20160424T054323 UID:11222@assets3.agendadulibre.org DTSTART;TZID=Europe/Paris:20160510T090000 DTEND;TZID=Europe/Paris:20160510T180000 DESCRIPTION:Deuxième événement du [Printemps de l'innovation Open Source ][1]\, organisé par le GTLL de Systematic et l'Irill\, présidé par Robe rto Di Cosmo[][2]\n\n[Sécurité\, Sûreté et Confidentialité][2]\n\nPro gramme dirigé par **Laure Petrucci**\, directrice du Laboratoire d'Infor matique de Paris Nord (LIPN)\, Université Paris 13\, et **Roberto Di Cosm o**\, directeur de l'Irill\, Inria\, professeur à l'Université Paris-Did erot\n\n* 09:20 - Ouverture de la journée\n **Laure Petrucci\,** LIPN\n\ n* 09:30 - Présentation du Groupe Thématique Logiciel Libre\n **Stéfan e Fermigier**\, GT LL\n\n* 09:45 - L'année de la Sécurité au CNRS\n ** Jean Mairesse**\, CNRS\n\n* 10:00 - Differential privacy and applications to location privacy\n **Catuscia Palamidessi**\, LIX\n\n Differential pr ivacy is one of the most successful approaches to prevent disclosure of pr ivate information in statistical databases. It provides a formal privacy g uarantee\, ensuring that sensitive information relative to individuals can not be easily inferred by disclosing answers to aggregate queries. Most im portantly\, and in contrast to other previous notions of privacy\, it is r obust under composition attacks. In this talk we present a generalized ver sion of differential privacy\, that is suitable to protect secrets in any metric domain. Then\, we explore an application of this generalized versio n 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 locat ion\, while allowing approximate information - typically needed to obtain a certain desired service - to be released.\n We describe how to use our mechanism to enhance Location Based Services (LBS) with geo-indistinguish ability guarantees without compromising the quality of the service\, and w e describe an implementation based on a planar Laplacian noise. It turns o ut that\, among the “universal” mechanisms (i.e.\, those which do not depend on a prior distribution)\, ours is the one that offers the best pri vacy 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.\n\n* 11:15 - Prise en compte de la sécurité dans la conception et le développement de logiciels\n **Benjamin Morin* *\, ANSSI\n\n* 12:00 - Model-checking for efficient malware detection\n * *Tayssir Touili**\, LIPN\n\n The number of malware is growing extraordina rily fast. Therefore\, it is important to have efficient malware detectors . Malware writers try to obfuscate their code by different techniques. Man y of these well-known obfuscation techniques rely on operations on the sta ck such as inserting dead code by adding useless push and pop instructions \, or hiding calls to the operating system\, etc. Thus\, it is important f or 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 techniqu es in a tool\, and we applied it to detect several viruses. Our results ar e encouraging. In particular\, our tool was able to detect more than 800 v iruses. Several of these viruses could not be detected by well-known anti- viruses such as Avira\, Avast\, Norton\, Kaspersky and McAfee.\n\n* 14:00 - SQLite with a Fine-Toothed Comb\n **John Reger**\, TrustInSoft\n\n Wha t should we do about security-critical software that is too large to be fo rmally verified? This talk explores the practical approach of repurposing a C verifier as an interpreter\, sacrificing soundness but gaining scalabi lity and eliminating overapproximation-related alarms. This mode of analys is works best for systems that have very thorough test suites\, whether ma nually constructed or generated by a tool such as afl-fuzz. Using Frama-C as an interpreter we have analyzed widely-used\, security-critical librari es such as SQLite\, libpng\, and libwebp\, finding a number of issues in e ach and also paving the way for future verification efforts.\n\n* 14:45 - Building and verifying a quasi-certification entity over Distributed Hash Tables\n **Fabrice Kordon**\, LIP6\n\n Building a certification authorit y (CA) that is both decentralized and fully reliable is impossible. Howeve r\, the limitation thus imposed on scalability is unacceptable for many ty pes of information systems\, such as e-government services. This talk expl ores a solution based on a Distributed Hash Table (DHT) and has been forma lly verified to prove that we get close to full reliability: a CA with a p robability of arbitrary failure so low that\, in practice\, false positive s should never occur. The verification of this protocol was performed with several tools among which some are integrated in the CosyVerif platform.\ n\n* 15:30 - Pause\n* 16:00 - Mise en œuvre des méthodes de vérificatio n de modèle et d'analyse statique de code pour la détection de faiblesse s et de vulnérabilités\n **Véronique Delebarre**\, SafeRiver\n\n 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 c ycle de développement. D’une part les référentiels normatifs en admet tent 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 ave c un coût optimisé de revalidation incite fortement à utiliser des moye ns 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 rappo rt aux tests » ? etc. Une grande partie des réponses réside dans la c apacité à 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é d ans 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.\n\n**[Ins cription gratuite mais obligatoire][3]**\n\n\n\nAutres journées à venir: \n\n [L'Agenda du Libre \\| Langages et Outils pour la Fiabilité](../1122 3) [L'Agenda du Libre \\| Open Source pour le Cloud et les Conteneurs](../ 11224) [L'Agenda du Libre \\| Frama-C Day - Analyse et vérification de co de ](../11226) [L'Agenda du Libre \\| Techniques de programmation web à l 'état de l'art](../11227)\n\n[1]: http://www.open-source-innovation-sprin g.org/\n[2]: http://www.open-source-innovation-spring.org/securite-surete- et-confidentialite/\n[3]: https://lipn.univ-paris13.fr/~petrucci/OSIS-Secu -2016/registration.php\n LOCATION:99 avenue Jean-Baptiste Clément\, Villetaneuse\, Île-de-France\, France ORGANIZER:mailto:muriel.shanseifan@systematic-paris-region.org SUMMARY:Sécurité\, sûreté et confidentialité URL;VALUE=URI:http://www.open-source-innovation-spring.org/securite-surete- et-confidentialite X-ALT-DESC;FMTTYPE=text/html:
Deuxième événement du Printemps de l'innovation Open Source\, orga nisé par le GTLL de Systematic et l'Irill\, présidé par Roberto Di Cosm o
\nSécurité\, Sûreté et Conf identialité
\nProgramme dirigé par Laure Petrucci\, di rectrice du Laboratoire d'Informatique de Paris Nord (LIPN)\, Université Paris 13\, et Roberto Di Cosmo\, directeur de l'Irill\, Inria\, pro fesseur à l'Université Paris-Diderot
\nLaure Petrucci\, LIPN
\nStéfane Fermigier\, GT LL
\n\n\n< b>Jean Mairesse\, CNRS
\nCatuscia Pal amidessi\, LIX
\nDifferential privacy is one of the most successful approach
es to prevent disclosure of private information in statistical databases.
It provides a formal privacy guarantee\, ensuring that sensitive informati
on relative to individuals cannot be easily inferred by disclosing answers
to aggregate queries. Most importantly\, and in contrast to other previou
s notions of privacy\, it is robust under composition attacks. In this tal
k we present a generalized version of differential privacy\, that is suita
ble to protect secrets in any metric domain. Then\, we explore an applicat
ion of this generalized version to the case of location privacy\, where do
main consists of the locations on a map and the distance is the geographic
al distance. This instance of the property\, that we call geo-indistinguis
hability\, is a formal notion of privacy for location-based systems that p
rotects 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 Serv
ices (LBS) with geo-indistinguishability guarantees without compromising t
he quality of the service\, and we describe an implementation based on a p
lanar Laplacian noise. It turns out that\, among the “universal” mecha
nisms (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 too
l\, Location Guard\, based on our framework\, which allows to use LBS’s
on browsers without revealing the exact location of the user.
Benjamin Morin< /b>\, ANSSI
\nTayssir Touili\, LIPN
\nThe number of ma lware 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 r ely on operations on the stack such as inserting dead code by adding usele ss push and pop instructions\, or hiding calls to the operating system\, e tc. Thus\, it is important for malware detectors to be able to deal with t he program's stack. In this talk\, we propose a new model-checking approac h 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 sev eral viruses. Our results are encouraging. In particular\, our tool was ab le to detect more than 800 viruses. Several of these viruses could not be detected by well-known anti-viruses such as Avira\, Avast\, Norton\, Kaspe rsky and McAfee.
\nJohn Reger\, TrustInSoft
\nWhat should we do about security-critical software that is too large to be formally verif ied? This talk explores the practical approach of repurposing a C verifier as an interpreter\, sacrificing soundness but gaining scalability and eli minating overapproximation-related alarms. This mode of analysis works bes t for systems that have very thorough test suites\, whether manually const ructed or generated by a tool such as afl-fuzz. Using Frama-C as an interp reter we have analyzed widely-used\, security-critical libraries such as S QLite\, libpng\, and libwebp\, finding a number of issues in each and also paving the way for future verification efforts.
\nFabrice Kordon\, LIP6
\n div>\nBuilding a certification authority (CA) that is both decentralized and fully reliable is impossible. However\, the limitation thus imposed on scalability is un acceptable for many types of information systems\, such as e-government se rvices. This talk explores a solution based on a Distributed Hash Table (D HT) and has been formally verified to prove that we get close to full reli ability: a CA with a probability of arbitrary failure so low that\, in pra ctice\, false positives should never occur. The verification of this proto col was performed with several tools among which some are integrated in th e CosyVerif platform.
\nVéronique Delebarre\, SafeRiver
\nLa réduction des coûts de s activités de validation et de vérification est une opportunité pour l es 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 plat es-formes qui doivent ensuite être déployées avec un coût optimisé de revalidation incite fortement à utiliser des moyens de vérification aut omatisés. Mais\, les utilisateurs ou promoteurs de ces méthodes ont beso in de chiffres : « Que font gagner les méthodes formelles » ? « q uels sont les coûts de mise en œuvre » ?\, « combien de faux positi fs » ? « 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éri ence résulte de 10 ans d’expérimentations sur des cas industriels et s era illustré sur trois cas d’utilisation de méthodes statiques : la p reuve d’exigences fonctionnelles de sécurité dans le contexte d’un d éveloppement « model based design » de système complexe\, la vérifi cation d’absence d’interférence dans le cas d’un système embarquan t des composants logiciels de différents niveaux\, et enfin\, la détecti on de vulnérabilités dans un logiciel.
\nInscription gratuite mais obligatoire< /a>
\n\n
Autres journ ées à venir :
\n END:VEVENT END:VCALENDAR