Fiabilité étendue grâce à la vérification binaire du micro-noyau seL4® sur l'architecture du processeur RISC-V
**Taufkirchen, Allemagne,5
mai 2021** - La société allemande de cybersécurité HENSOLDT Cyber, en partenariat avec le CSIRO, a annoncé la sortie d'un outil automatisé pour la vérification binaire du micro-noyau seL4 en ce qui concerne l'architecture de processeur RISC-V 64 bits.
"Le micro-noyau seL4 vérifié constitue la base de TRENTOS®
, le système d'exploitation sécurisé pour MiG-V, un processeur RISC-V avec sécurité de la chaîne d'approvisionnement. Cette combinaison unique de sécurité matérielle et logicielle peut protéger les systèmes informatiques critiques contre les APT", a déclaré Sascha Kegreiß, directeur technique de HENSOLDT Cyber.
HENSOLDT Cyber renforce la fiabilité de cette combinaison matérielle et logicielle en collaborant avec Data61 du CSIRO pour prouver mathématiquement que le code binaire du micro-noyau seL4 est la traduction correcte de son code source. Cette fiabilité a été obtenue en transposant le code binaire et le code source dans un langage intermédiaire commun, avant de vérifier l'équivalence à l'aide de prouveurs de théorèmes automatisés.
La vérification binaire élimine la nécessité de faire confiance au compilateur déployé. Les compilateurs peuvent introduire des erreurs ou des comportements involontaires, qui peuvent à leur tour être exploités par des attaquants. Ces erreurs ne sont pas identifiables par la vérification formelle du code source ; le processus doit donc s'étendre au code binaire pour exclure les fautes dans le logiciel déployé. Avec la vérification binaire, nous avons la preuve que tout ce qui est garanti par le code source s'applique également au code binaire, puisque les prouveurs de théorèmes automatiques ont vérifié qu'ils sont effectivement équivalents.
RISC-V est la première architecture 64 bits pour laquelle la vérification binaire d'un système d'exploitation a été réalisée. Cela fait de seL4 le premier noyau entièrement vérifié formellement pour un processeur 64 bits. En combinant une architecture de processeur ouvertement disponible et testable avec un noyau de système d'exploitation formellement vérifié, seL4 sur RISC-V offre l'approche de sécurité la plus complète jamais atteinte par un processeur. Le processus garantit que le code de programme écrit et prouvé correct par la communauté seL4 (organisée au sein de la Fondation seL4) a été compilé sans erreur pour l'architecture RISC-V et est donc disponible en tant que binaire vérifié.
"Il s'agit d'une étape importante, qui renforce la position de seL4 dans la définition de l'état de l'art en matière de systèmes d'exploitation sécurisés", a déclaré le professeur Gernot Heiser, président de la fondation seL4.
Zoltan Kocsis, ingénieur de vérification au CSIRO, a déclaré : "La validation de la traduction relie tous nos efforts de vérification. L'adaptation de la validation de la traduction à un processeur moderne de 64 bits a posé d'importants problèmes d'évolutivité, mais nous avons finalement réussi à les surmonter.
La fiabilité est la valeur fondamentale de HENSOLDT Cyber, qui se manifeste dans la vision de l'entreprise "Secure IT instead of IT security" (l'informatique sécurisée plutôt que la sécurité informatique). La sécurité informatique doit être vérifiable ; à cet égard, la vérification binaire de seL4 sur RISC-V représente une étape importante. HENSOLDT Cyber travaille continuellement avec ses partenaires pour élever les composants individuels de ses solutions à des niveaux de sécurité sans précédent, afin de pouvoir facilement fournir à ses clients les caractéristiques de sécurité qui en résultent.
Pour plus d'informations sur le MiG-V de HENSOLDT Cyber : https://hensoldt-cyber.com/mig-v
À propos de HENSOLDT Cyber
Fondée en 2018, HENSOLDT Cyber GmbH est une start-up allemande basée à Taufkirchen, près de Munich, qui développe des produits informatiques embarqués répondant aux exigences de sécurité les plus élevées. Ceux-ci intègrent un système d'exploitation hautement sécurisé avec du matériel durci pour la sécurité, créant ainsi une informatique sécurisée à la place de la sécurité informatique pour le marché mondial de l'informatique. L'entreprise combine plus de 50 ans d'expérience dans le domaine de l'électronique de défense et de sécurité du groupe HENSOLDT avec une expertise universitaire de niveau mondial dans le développement de matériel et de logiciels. HENSOLDT Cyber emploie actuellement plus de 50 personnes sur différents sites.
De plus amples informations sur l'entreprise sont disponibles à l'adresse suivante : www.hensoldt-cyber.com
Contact pour les questions de presse, les photos et les demandes d'articles
Simone Rudow
Responsable du marketing et des relations publiques
Tél : +49 (0) 174 218 8102