En octobre 2018 et mars 2019, deux Boeing 737 MAX se sont écrasés entrainant des centaines de morts. Après de nombreuses investigations, le logiciel anti-décrochage développé spécialement pour la série 737 MAX de Boeing semble être la principale cause de ces 2 catastrophes. Quelle méthode de vérification doit-on effectuer sur un logiciel aussi critique afin d’éviter de telles tragédies ?
[A] Revue de code (Code review)
[B] Test de régression (Regression testing)
[C] Inspection formelle (Formal inspection)
[D] Test d’intégration (Integration testing)
Les méthodes formelles d’analyse (preuve, model-checking) sont généralement utilisées pour obtenir le plus haut niveau de confiance dans le logiciel mais elles ne peuvent être utilisées que si le logiciel a fait l’objet d’une spécification formelle.
Pour réaliser une spécification formelle il faut effectuer une analyse approfondie du système afin de révéler des défauts, anomalies, incohérences,…
Les méthodes formelles (spécification / analyse) sont particulièrement coûteuses et réservées aux logiciels les plus critiques. Par exemple la certification critères communs EAL7 (norme ISO 15408) permet d’attester la conception et la vérification de façon formelle du système. Mais son coût est si élevé que seuls des systèmes hautement critiques (militaire, nucléaire, aéronautique) seront certifiés à un tel niveau.
La bonne réponse est la proposition [C] Inspection formelle
Pour en savoir plus sur l’intégration de la sécurité dans le développement des logiciels nous vous recommandons de suivre les modules n°20 et 21 de la formation CISSP de VERISAFE.
Questions et réponses rédigées par VERISAFE selon le programme officiel du CISSP actuellement en vigueur
© VERISAFE – Utilisation ou reproduction (même partielle) strictement interdite sans l’accord écrit de VERISAFE
