AstréeS

AstréeA est un analyseur statique qui vise à prouver l’absence d’erreur d’exécution dans du code embarqué. Mais, pour prouver la correction d’un système logiciel, il faut prouver plus que le logiciel final: il y a beaucoup de couches en dessous, des bibliothèques jusqu’au matériel. En particulier, quand on regarde le système d’exploitation, on a besoin de prouver plus que des propriétés de sûreté: il nous faut un analyseur pour la sécurité.

De la même façon qu’AstréeA est construit au dessus Astrée, on écrit AstréeS (Astrée pour la Securité) comme une extension d’AstréeA. Comme Astrée et AstréeA, AstréeS est correct, automatique and a pour vocation de passer à l’échelle d’applications réelles. Les fondements théoriques sont aussi les mêmes: AstréeS est basé sur l’interprétation abstraite.

AstréeS a commencé dans le contexte du projet ANR AnaStaSec.

Pour pouvoir analyser les logiciels bas niveau, tel que les systèmes d’exploitations, AstréeS a reçu diverses extensions. La nouvelle fonctionnalité la plus notable est le support de code mélangeant le C et l’assembleur x86. Une autre amélioration importante est l’ajout d’un nouveau cadre pour la collaboration de domaines abstraits qui permet aux domaines de partagés des variables fantômes dont la gestion est décentralisée. Ce nouveau système peut être utilisé pour prouver aisément des propriétés qu’on peut exprimer avec des variables fantômes.