Le projet B4L4 s’inscrit dans le contexte des travaux liés à la définition des architectures de plateformes sécurisées.

Les partenaires sont :

  • ST Microelectronics : équipe R&D de AST à Rousset
  • CEA
  • ENST : LabSoc
  • ClearSy

Les travaux portent sur la modélisation formelle d’un système d’exploitation sécurisé et sur la validation de son développement.

La méthode formelle B est utilisée pour modéliser le système ainsi que les APIs des différents serveurs consistuant l’OS. Des études pour utiliser ces modèles comme oracle de test sont aussi menées. Le CEA étudie l’applicabilité de l’outil Caveat dans le contexte des systèmes d’exploitation.