BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//GREYC UMR CNRS 6072 - Groupe de Recherche en Informatique, Image, et Instrumentation de Caen - ECPv5.7.0//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:GREYC UMR CNRS 6072 - Groupe de Recherche en Informatique, Image, et Instrumentation de Caen
X-ORIGINAL-URL:https://www.greyc.fr
X-WR-CALDESC:évènements pour GREYC UMR CNRS 6072 - Groupe de Recherche en Informatique, Image, et Instrumentation de Caen
BEGIN:VTIMEZONE
TZID:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20240331T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20241027T010000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20240702T100000
DTEND;TZID=Europe/Paris:20240702T110000
DTSTAMP:20260504T024155
CREATED:20240606T114646Z
LAST-MODIFIED:20240628T073330Z
UID:11597-1719914400-1719918000@www.greyc.fr
SUMMARY:Séminaire Algorithmique :  « StarMalloc : un allocateur de mémoire moderne renforcé formellement vérifié »\, Antonin Reitz (équipe Prosecco\, INRIA Paris)
DESCRIPTION:Malgré la popularisation de langages modernes qui permettent une gestion sûre de la mémoire\, C et C++ restent des langages de choix pour le développement de nombreux logiciels très couramment utilisés. Si ces langages permettent d’obtenir de bonnes performances\, ils sont particulièrement vulnérables aux attaques par corruption mémoire.  Des études récentes estiment que des erreurs de gestion de la mémoire\, telles que des dépassements de tampon\, sont la cause principale de 70% des vulnérabilités dans des logiciels très utilisés comme Android ou Google Chrome. \nPour contrer ces attaques\, les allocateurs mémoire modernes adoptent généralement un design orienté pour la sécurité\, qui permet de limiter le risque de corruption mémoire.  Dans cet exposé\, nous présentons StarMalloc\, un allocateur moderne orienté pour la sécurité vérifié formellement en utilisant l’assistant de preuve F* et la logique de séparation concurrente Steel. Nous montrons comment spécifier et vérifier les invariants de cet allocateur\, dont l’architecture est inspirée de celle de hardened_malloc\, ainsi que la correction des mécanismes de sécurité implémentés. Enfin\, nous présentons des résultats expérimentaux comparant StarMalloc à d’autre allocateurs\, en évaluant leur performance sur différentes applications\, dont le navigateur Firefox.
URL:https://www.greyc.fr/event/seminaire-algorithmique-titre-a-venir-antonin-reitz-equipe-prosecco-inria-paris/
LOCATION:Sciences 3- S3 351
CATEGORIES:Amacc,General,News,Séminaire Algo
END:VEVENT
END:VCALENDAR