Justement la question est ouverte sur toutes les méthodes formelles, puisque je n'ai pas de visibilité sur ce qu'il se fait actuellement dans le domaine sur ce sujet.
Mais dans le cas de LinuxBoot, ça serait plutôt de savoir si il y a un intérêt quelconque et une plus-value à utiliser des méthodes formelles (lesquelles, comment ?) pour le développement ou la validation, et en particulier vis à vis d'exigences de sécurité, type celles Critères Communs.
[^] # Re: Méthodes formelles ?
Posté par Harvesterify . En réponse à la dépêche Un peu d’Open Hardware pour la rentrée (et beaucoup de LinuxBoot). Évalué à 3.
Justement la question est ouverte sur toutes les méthodes formelles, puisque je n'ai pas de visibilité sur ce qu'il se fait actuellement dans le domaine sur ce sujet.
Ce qui m'intéresse, c'est l'usage possible/avéré des méthodes formelles pour la sécurité des architectures matérielles. Pour donner un exemple, je suis avec attention ce genre de chose : https://www.researchgate.net/publication/327027099_Implementing_a_hardware-assisted_memory_management_mechanism_for_ARM_platforms_using_the_B_method
Mais dans le cas de LinuxBoot, ça serait plutôt de savoir si il y a un intérêt quelconque et une plus-value à utiliser des méthodes formelles (lesquelles, comment ?) pour le développement ou la validation, et en particulier vis à vis d'exigences de sécurité, type celles Critères Communs.
Mes messages engagent qui je veux.