CELTIQUE :

L'objectif global du projet Celtique est d'améliorer la sécurité et la fiabilité des logiciels grâce à des techniques de modélisation, d'analyse et de certification basées sur la sémantique.

Pour atteindre cet objectif, le projet mène des travaux sur l'amélioration des techniques de description et d'analyse sémantique, ainsi que des travaux sur l'utilisation d'assistants de preuve (notamment Coq) pour développer et prouver les propriétés de ces techniques. Nous appliquons ces techniques à une variété de langages sources, dont Java, C et JavaScript.
Nous étudions également comment ces techniques s'appliquent aux langages de bas niveau et comment elles peuvent être combinées avec une compilation certifiée. Le compilateur certifié CompCert et ses représentations intermédiaires sont utilisés pour la plupart de nos travaux sur la modélisation sémantique et l'analyse des représentations C et de niveau inférieur. Les analyses sémantiques extraient des descriptions approximatives mais correctes du comportement des logiciels à partir desquelles une preuve de sûreté ou de sécurité peut être construite. Les analyses d'intérêt incluent l'analyse de flux de données numériques, l'analyse de flux de contrôle pour les langages d'ordre supérieur, l'alias et l'analyse de points vers la manipulation de la structure de tas. En particulier, nous avons conçu plusieurs analyses pour le contrôle du flux d'informations, visant à calculer les connaissances des attaquants et à détecter les canaux auxiliaires.