SERMA SAFETY & SECURITY a acquis SafeRiver en juillet 2023 afin de compléter son expertise en méthodes formelles et ainsi de consolider son positionnement historique en Sûreté de Fonctionnement et en Cybersécurité.
Depuis près de 20 ans, SafeRiver a développé une expertise dans la mise en œuvre des méthodes formelles appliquées aux systèmes et logiciels critiques pour les secteurs ferroviaires, automobile et défense.
Les docteurs et ingénieurs de SafeRiver interviennent, au plus tôt dans le cycle de développement (de la définition des propriétés de comportement à la détection de faiblesses et de vulnérabilités), sur des projets à haut niveau de sûreté de fonctionnement ou de cybersécurité.
En support de ses activités de conseil et d’expertise, Saferiver a développé le logiciel SafeProver – outil de Model-Checking qualifié T2 pour le domaine du ferroviaire et le logiciel IFFREE utilisé pour évaluer l’absence d’impact entre des modules/logiciels de niveaux de criticité différents.
Les services et outils proposés par SafeRiver apportent une confiance accrue dans :
- les choix d’architecture,
- l’exhaustivité des scénarios de tests,
- la reproductibilité de la vérification,
- l’absence d’impact entre les flux de criticité différents (safety/non safety)
- la maintenabilité en vie série.
En quoi consiste les méthodes formelles ?
Les méthodes formelles désignent un ensemble de techniques mathématiques utilisées pour spécifier, concevoir, et vérifier les systèmes à forte composante logicielle et électroniques. Contrairement aux méthodes de vérification traditionnelles basées sur des tests empiriques, les méthodes formelles permettent de prouver mathématiquement que le système satisfait certaines propriétés spécifiées.
Plusieurs études ont montré que l’utilisation des méthodes formelles conduit à une réduction significative du coût global (coûts de développement, coûts de vérification, coûts de maintenance) pour des systèmes critiques.
Les méthodes formelles sont déployées pour répondre à des problématiques :
de Sûreté de Fonctionnement
- Les méthodes formelles permettent de définir précisément les exigences de sûreté de fonctionnement à l’aide de modèles mathématiques.
- Elles permettent de démontrer formellement que le système respecte les propriétés de sûreté spécifiées,
- En modélisant et en analysant le système dès les premières étapes du développement, les erreurs de conception pouvant affecter la sûreté peuvent être détectées et corrigées avant même que le système ne soit implémenté.
- Dans de nombreux secteurs, tels que l’aéronautique, l’automobile ou le ferroviaire, les normes de sûreté de fonctionnement (CEI 61508, EN 50128, ISO 26262, …) préconisent l’utilisation de méthodes formelles pour certaines catégories de systèmes critiques.
de Cybersécurité
- Les méthodes formelles sont recommandées voire exigées par exemple dans le cadre de la certification Critères Communs pour les hauts niveaux de sécurité (à partir de EAL 4+).
- Les démarches mathématiques sous-jacentes (typage, interprétation abstraite ou Model Checking) permettent de garantir l’absence de certaines catégories d’erreurs. L’utilisation des démarches formelles peuvent être mises en œuvres lors des phases de spécification, de conception, d’implémentation et de tests.
- Des méthodes reconnues telles que B, COQ peuvent être utilisées.
Services
SafeRiver a développé une offre spécifique pour évaluer la sécurité des systèmes et logiciels intégrant la mise en œuvre de méthodes formelles
Offre en lien avec la Sûreté de fonctionnement
Analyse de sécurité (FHA)
- Identification des critères de sécurité
- Élaboration de propriétés de sécurité observables
- Couverture des mesures de mitigation du système
Vérification formelle des modèles
- Conformité avec les propriétés de sécurité
- Absence d’erreurs d’exécution
- Vérification de modèle ou démonstration de théorème
Analyse statique du code source
- Détection des erreurs d’exécution
- Détection de code mort et de blocage
- Vérification des règles de codage
Co-simulation
- Équivalence entre le modèle et le code
Génération de tests
- Génération automatique de cas de test à partir des propriétés de sécurité
Offre en lien avec la Cybersécurité
Kits méthodologiques pour la sécurité des langages
- Règles de conception pour une utilisation sécurisée des langages
- Recommandations pour la production de code
Analyse statique pour la sécurité
- Profils de configuration des outils d’analyse statique (par exemple Polyspace, Coverity, Klocwork, …) avec CWE
- Détection des vulnérabilités
- Évaluation des risques liés aux vulnérabilités et aux failles
- Flux de contrôle, flux de données et exactitude de l’utilisation de l’interface (c’est-à-dire absence d’interférences)
Évaluation des outils d’analyse statique pour la sécurité
- Kit d’évaluation Juliet-based
- Projet ANSSI/DGA (LaboSSec, AMOEASU)
Produits
Outil SAFEPROVER
SAFEPROVER est un outil automatique de vérification de modèles (Model Checking) basé sur un algorithme d’induction temporelle.
Outil IFFREE
L’outil IFFREE est un outil d’analyse statique qui identifie automatiquement, au niveau du code source, toutes les interférences spatiales susceptibles de mettre la mémoire en danger.