Abstract FR:

Dans un monde informatique ou les comportements non spécifiés (boggues) sont nombreux, le souci de parvenir à réaliser des programmes plus sûrs est de plus en plus présent. Cette volonté, appuyée par les normes actuelles comme les Critères Communs dans la sécurité, conduit naturellement à l’utilisation de méthode d’ingénierie comme le test et les méthodes formelles qui sont reconnues comme des méthodes éprouvées pour diminuer les erreurs logicielles. C’est dans ce cadre que le département de la sécurité des systèmes d’information de la société Bertin Technologies développe un système d’exploitation. La sécurité mise en oeuvre dans ce système est certifiée par une évaluation de niveau normatif EAL-5 vis-à-vis des Critères Communs. Une telle évaluation nécessite l’utilisation de méthodes formelles pour tout ce qui concerne les politiques de sécurité. Dans ce travail, nous présentons une expérience facilitant le développement de logiciels certifiables dans un cadre industriel en utilisant l’atelier FoCaLize. Cette expérience s’appuie sur les mécanismes de certification proposés par l’atelier mais aussi sur une compilation du source FoCaLize vers du C. Cette traduction est essentielle dans le cadre d’une utilisation industrielle où les langages basés sur C sont majoritairement présents.