Accueil

Le projet collaboratif CEEC propose de développer une suite de développement et une méthodologie pour permettre la certification sécuritaire de haut niveau du type Critères Communs pour des produits des technologies de l’information.

Description

Le projet CEEC ambitionne de proposer une nouvelle méthodologie de développement de logiciel qui permet d’accélérer les procédures de certification requises par les produits de haute sécurité.

Durant ce projet, les partenaires ont l’intention de créer un nouvel environnement de développement de logiciels, basé sur les technologies innovantes de Prove & Run, qui inclura une chaîne de génération et de compilation intégralement prouvée. En intégrant les aspects de sécurité dans le processus de développement de systèmes critiques, cet environnement permettra la création de logiciels de qualité dotés de propriétés de sécurités garanties et réduira le coût des évaluations et des certifications de haut niveau, telles que celles effectuées selon la méthodologie des Critères Communs.

L’innovation scientifique et technique

L’objectif du projet CEEC est de rendre disponible cette approche et de valider celle-ci en terme de réduction des coûts de mise sur le marché de produit logiciel sensible aux questions de sécurité. Le projet réalisera pour cela :

  • La conception d’un langage par Prove & Run qui permet aux développeurs de spécifier les propriétés du programme et de sécurité que le programme doit respecter ;
  • L’environnement conçu par Prove & Run, peu vérifier formellement les programmes et générer le code correspondant dans le langage C ;
  • À l’aide du compilateur CompCert (lui aussi formellement prouvé)  un code pour les plateformes ARM est généré ;
  • La connection entre les environnements de Prove & Run et d’Esterel Technologies permet de prendre en compte les aspects de sécurité dans les logiciels et systèmes aéronautiques au niveau des modèles ;
  • À tous les niveaux du processus de développement, la chaine d’outil génère des preuves requises par les Critères Communs pour des évaluations de hauts niveaux.

Principaux résultats

Le projet démontrera l’approche sur deux environnements applicatifs représentatifs de ce besoin :

  • L’environnement d’exécution de confiance (TEE : Trusted execution environnement) de la téléphone mobile,
  • L’environnement aéronautique.