A platform-evidence mapping for DAL-B certification planning on an AMD64 multi-core processor with Xen temporal isolation

Les aéronefs modernes deviennent de plus en plus complexes, s'appuyant sur des ordinateurs puissants pour gérer tout, des commandes de vol à la navigation et à la planification de mission. Pour garantir la sécurité, l'industrie aéronautique utilise des règles strictes qui exigent que chaque logiciel soit testé et vérifié selon un niveau de confiance spécifique. Pour les systèmes les plus critiques, tels que ceux qui maintiennent un avion en l'air, ce niveau de confiance est le plus élevé possible. Cependant, un nouveau défi est apparu alors que ces ordinateurs sont passés de processeurs uniques à des puces multi-cœurs, similaires aux processeurs puissants que l'on trouve dans les ordinateurs portables et les serveurs modernes. Lorsque plusieurs programmes s'exécutent simultanément sur différents cœurs d'une même puce, ils entrent souvent en compétition pour l'accès à des ressources partagées, spécifiquement une zone de mémoire à haute vitesse appelée cache de dernier niveau. Cette compétition peut ralentir un programme de manière imprévisible, créant une incertitude de synchronisation qui est dangereuse pour les logiciels de l'aviation critiques pour la sécurité.

Pour résoudre cela, les chercheurs développent des moyens d'isoler ces programmes afin qu'ils n'interfèrent pas les uns avec les autres. Une approche prometteuse implique un type de gestionnaire de logiciels, connu sous le nom d'hyperviseur, qui se situe entre le matériel et les applications, divisant les ressources de l'ordinateur en compartiments séparés et sécurisés. La question demeure toutefois de savoir si cette isolation est suffisamment robuste pour répondre aux normes rigoureuses de l'aviation commerciale. Une équipe de chercheurs d'Advanced Micro Devices et de l'Université technique de Munich a exploré cette question en élaborant un plan détaillé de la manière de certifier un type spécifique d'ordinateur multi-cœur pour une utilisation dans les aéronefs. Leur travail se concentre sur une configuration qui utilise un hyperviseur appelé Xen sur des processeurs AMD, combiné à une technique appelée coloration de cache, pour garantir que différentes partitions logicielles ne puissent pas accidentellement se marcher sur les pieds.

Les chercheurs ont commencé par identifier le problème spécifique : sur un processeur multi-cœur, le cache de mémoire partagé est le lieu principal où les interférences se produisent. Si un programme remplit le cache, il peut forcer un autre programme à attendre, provoquant des retards qui pourraient manquer une échéance critique. Pour prévenir cela, l'équipe a proposé une méthode où la mémoire de l'ordinateur est divisée en groupes distincts, ou « couleurs », basés sur l'endroit où les données résident. Chaque programme logiciel se voit attribuer son propre ensemble unique de couleurs, et le système est configuré de telle sorte que les données d'un programme ne puissent jamais remplacer les données d'un autre dans le cache. Crucialement, cette règle s'applique également à l'hyperviseur lui-même. Les chercheurs se sont assurés que les propres données du gestionnaire de logiciels sont également verrouillées dans leur propre ensemble de couleurs exclusif, empêchant ainsi l'hyperviseur d'évincer accidentellement les données des programmes critiques pour la sécurité qu'il gère. Cela crée une garantie constructive que l'interférence est bornée, ce qui signifie qu'elle est mathématiquement limitée et prévisible, plutôt que de simplement espérer qu'elle n'arrivera pas.

L'article présente une mise en correspondance de cette configuration technique avec les règles de certification officielles utilisées par les autorités de l'aviation aux États-Unis et en Europe. Ces règles, connues sous les noms de DO-178C et AC 20-193, exigent que les demandeurs prouvent que les ressources partagées sont gérées de manière sûre. Les auteurs démontrent comment leur configuration spécifique répond à ces exigences en montrant que le mécanisme de coloration de cache isole efficacement le cache de dernier niveau. Ils montrent également comment le cas de sécurité de l'hyperviseur lui-même, qui est documenté séparément par la communauté open-source, peut être réutilisé comme preuve pour le fabricant d'aéronefs. Cela permet au fabricant de se concentrer sur la preuve que ses applications spécifiques fonctionnent correctement au sein de cet environnement isolé, plutôt que de devoir prouver la sécurité du matériel informatique sous-jacent à partir de zéro. Les chercheurs décrivent un chemin clair pour qu'un fabricant d'aéronefs puisse utiliser cette configuration pour atteindre une certification de sécurité de niveau intermédiaire, connue sous le nom de DAL-B, qui convient à de nombreuses fonctions importantes mais non critiques pour la vie.

Cependant, les auteurs prennent soin de définir les limites de leur travail. Ils déclarent explicitement que ce plan ne prouve pas encore que le système est assez sûr pour le niveau de certification le plus élevé, appelé DAL-A, qui est requis pour les commandes de vol les plus critiques. Pour atteindre ce niveau supérieur, des étapes supplémentaires seraient nécessaires, telles que la preuve formelle par les mathématiques que l'outil d'allocation de mémoire ne commet jamais d'erreur et la collecte d'une expérience plus étendue en conditions réelles avec le processeur spécifique. L'article précise également qu'il ne couvre pas les charges de travail d'intelligence artificielle ou de traitement graphique, qui sont des domaines émergents nécessitant des solutions différentes. De plus, les auteurs soulignent qu'il s'agit d'un article de méthodologie, et non d'une certification finale ; il fournit un argument structuré et un ensemble d'outils, mais l'approbation réelle doit toujours venir des régulateurs de l'aviation qui examineront les détails spécifiques de chaque programme aéronautique.

Le cœur de la recherche est une démonstration pratique de la manière dont ces règles de sécurité abstraites peuvent être appliquées à une plateforme informatique réelle. L'équipe a décrit une configuration spécifique où un ordinateur à quatre cœurs est divisé en partitions séparées pour différentes tâches, telles que le contrôle de vol, la perception et la gestion de mission. Ils ont montré comment assigner à chaque partition un cœur dédié et une tranche spécifique de la mémoire cache, garantissant que le logiciel de contrôle de vol dispose toujours des ressources dont il a besoin sans être ralenti par les autres tâches. Ils ont également détaillé comment le système vérifie les erreurs lors du démarrage pour s'assurer que l'isolation de la mémoire fonctionne correctement avant même que l'avion ne décolle. Cette approche offre un moyen d'utiliser des puces informatiques puissantes et disponibles commercialement dans l'aviation sans sacrifier la prévisibilité et la sécurité exigées par l'industrie.

En fin de compte, l'article offre un pont entre l'évolution rapide du matériel informatique commercial et le rythme lent et délibéré de la certification de sécurité aéronautique. Il montre qu'avec la bonne configuration, spécifiquement en utilisant la coloration de cache et un hyperviseur à partitionnement statique, il est possible de créer un environnement informatique où l'interférence est contrôlée et prévisible. Bien que le chemin vers les niveaux de certification les plus élevés nécessite encore des travaux, cette recherche fournit une base solide pour que les fabricants commencent à intégrer ces processeurs avancés dans leurs aéronefs. Ce travail sert de modèle, démontant que les mécanismes techniques existent pour soutenir l'intégration multi-cœur sécurisée, à condition que les règles spécifiques et les preuves requises par les régulateurs soient soigneusement suivies et vérifiées.