Améliorations autour de PolyORB Kernel
Le but de ce projet est de travailler sur le noyau PolyORB Kernel. Ce noyau minimal est conçu pour construire des systèmes critiques sûrs et sécurisés. Il fournit un ensemble de fonctionnalités qui sont activables/désactivables à la compilation. Quelques lignes de code et la configuration sont générées à partir de modèles AADL. Ainsi, nous pouvons vérifier le modèle puis générer le système à partir du modèle. Nous garantissons alors que l'implémentation du système suit les spécifications et nous réduisons le nombre d'erreurs de conception.
Nous avons repris le concept d'OS partitionnés : l'OS est constitué de partitions contenant des threads. Chaque partition est isolée spatialement (une partition ne peut pas accéder à l'espace d'adressage d'une autre partition) et temporellement (une partition ne peut pas déborder sur le temps d'exécution d'une autre partition). On retrouve ce concept de système partitionné dans les spécifications d'ARINC653.
Nous proposons ici que vous puissiez travailler sur le noyau PolyORB Kernel et y ajouter l'isolation spatiale, c'est à dire d'implémenter un mécanisme qui assure qu'une partition ne peut pas accéder aux données d'autres partitions. Plusieurs approches peuvent être retenus, vous devrez en proposez une et l'implémenter. Les contraintes sont les suivantes :
- Portabilité de l'approche
- Généricité du code
- Coût du mécanisme de protection, overhead introduit
Bien entendu, il faudra également penser à limiter les permissions de chaque partition et à veiller à ce que le code fournit par le développeur soit exécuté en mode utilisateur. Cela est un travail fortement connexe à la protection spatiale des partitions.
Une fois cette première approche réalisée, nous nous pencherons alors sur l'isolation spatiale distribuée, c'est à dire garantir que chaque partition ne peut utiliser que les canaux de communication qui lui sont dédiées. Cela permet de garantir une isolation spatiale pour les communications inter-partitions. Une explication plus longue de ce mécanisme est donnée dans le papier Design and Verification of Secure Systems (cf. liens).
Il faudra donc, au cours du projet, proposez des mécanismes permettant d'isoler les canaux de communications de chaque partition.
Le code du noyau est encore un peu jeune, c'est pour cela qu'il y aura déjà un travail de refactorisation du code et de debug.
