Quelles langues sont utilisées pour les logiciels critiques pour la sécurité?

Je recherche le développement de logiciels critiques pour la sécurité, et en particulier les effets du choix du langage de programmation sur ce développement.

Veuillez expliquer en détail quelles langues sont couramment utilisées et pourquoi.

Ada et SPARK (un dialecte d’Ada avec quelques points d’ancrage pour la vérification statique) sont utilisés dans les cercles aérospatiaux pour la construction de logiciels de haute fiabilité tels que les systèmes avioniques. Il existe en quelque sorte un écosystème d’outils de vérification de code pour ces langages , bien que cette technologie existe également pour d’ autres langues grand public .

Erlang a été conçu dès le départ pour écrire du code de télécommunication à haute fiabilité . Il est conçu pour faciliter la séparation des problèmes de récupération d’erreur (le sous-système générant l’erreur est différent du sous-système qui gère l’erreur). Il peut également être soumis à des preuves formelles, bien que cette capacité ne soit pas vraiment sortie des cercles de recherche.

Les langages fonctionnels tels que Haskell peuvent être soumis à des preuves formelles par des systèmes automatisés en raison de la nature déclarative du langage. Cela permet de contenir du code avec des effets secondaires dans les fonctions monadiques. Pour une preuve de correction formelle, on peut supposer que le rest du code ne fait rien d’autre que ce qui est spécifié.

Cependant, ces langages sont récupérés et la récupération de place est transparente au code, il ne peut donc pas être raisonné de cette manière. Les langages collectés ne sont normalement pas assez prévisibles pour les applications en temps réel, bien qu’il existe un ensemble de recherches en cours dans les collecteurs de mémoire incrémentiels limités dans le temps.

Eiffel et ses descendants prennent en charge une technique appelée Design By Contract, qui fournit un mécanisme d’exécution robuste permettant d’intégrer les contrôles préalables et postérieurs aux invariants. Bien qu’Eiffel ne soit jamais vraiment pris en compte, le développement de logiciels à haute fiabilité consiste généralement à écrire des contrôles et des gestionnaires pour les modes de défaillance avant d’écrire les fonctionnalités.

Bien que C et C ++ n’aient pas été spécifiquement conçus pour ce type d’application, ils sont largement utilisés pour les logiciels embarqués et à sécurité critique pour plusieurs raisons. Les principales propriétés à noter sont le contrôle de la gestion de la mémoire (ce qui vous évite d’avoir à collecter des ordures, par exemple), des bibliothèques d’exécution simples, bien déboguées et des outils matures. Une grande partie des chaînes d’outils de développement embarquées utilisées aujourd’hui ont été développées pour la première fois dans les années 1980 et 1990, alors que la technologie Unix prévalait à cette époque. Ces outils restnt donc populaires pour ce type de travail.

Bien que le code de gestion de la mémoire manuelle doive être soigneusement vérifié pour éviter les erreurs, il permet un certain contrôle sur les temps de réponse des applications qui ne sont pas disponibles dans les langues dépendant du nettoyage de la mémoire . Les bibliothèques d’ exécution principales des langages C et C ++ sont relativement simples, matures et bien comsockets. Elles figurent donc parmi les plates-formes les plus stables disponibles. La plupart sinon la totalité des outils d’parsing statique utilisés pour Ada prennent également en charge C et C ++, et de nombreux autres outils de ce type sont disponibles pour C. Il existe également plusieurs chaînes d’ outils basées sur C / C ++ largement utilisées ; La plupart des chaînes d’outils utilisées pour Ada sont également disponibles dans des versions prenant en charge C et / ou C ++.

Des méthodes formelles telles que la sémantique axiomatique (PDF), la notation Z ou les processus séquentiels communicants permettent de vérifier mathématiquement la logique du programme et sont souvent utilisées dans la conception de logiciels critiques pour la sécurité où l’application est assez simple (systèmes de contrôle intégrés) . Par exemple, un de mes anciens professeurs a fait une preuve formelle de correction d’un système de signalisation pour le réseau ferroviaire allemand.

La principale lacune des méthodes formelles est leur tendance à croître de manière exponentielle en termes de complexité par rapport au système sous-jacent prouvé. Cela signifie qu’il existe un risque important d’erreurs dans la preuve, de sorte qu’elles sont pratiquement limitées à des applications assez simples. Les méthodes formelles sont assez largement utilisées pour vérifier l’exactitude du matériel, car les bogues matériels sont très coûteux à résoudre, en particulier sur les produits grand public. Depuis le bogue du Pentium FDIV , les méthodes formelles ont beaucoup attiré l’attention et ont été utilisées pour vérifier l’exactitude du FPU sur tous les processeurs Intel depuis le Pentium Pro.

De nombreuses autres langues ont été utilisées pour développer des logiciels très fiables. De nombreuses recherches ont été effectuées sur le sujet. On peut raisonnablement soutenir que la méthodologie est plus importante que la plate-forme, même s’il existe des principes tels que la simplicité, la sélection et le contrôle des dépendances qui pourraient empêcher l’utilisation de certaines plates-formes .

Comme plusieurs autres l’ont noté, certaines plates-formes O / S ont des fonctionnalités pour promouvoir la fiabilité et le comportement prévisible, telles que les timers de surveillance et les temps de réponse d’interruption garantis. La simplicité est également un facteur de fiabilité important, et de nombreux systèmes RT sont délibérément très simples et compacts. QNX (le seul O / S que je connaisse, ayant déjà travaillé avec un système de traitement par lots concret basé sur celui-ci) est très petit et peut tenir sur une seule disquette. Pour des raisons similaires, les personnes qui créent OpenBSD – réputé pour sa sécurité robuste et son audit approfondi du code – font également en sorte que le système rest simple.

EDIT: Cette publication contient des liens vers de bons articles sur les logiciels critiques pour la sécurité, en particulier ici et ici . Les accessoires à S.Lott et Adam Davis pour la source. L’histoire du THERAC-25 est un peu un travail classique dans ce domaine.

Pour C ++, la norme de codage C ++ de Joint Ssortingke Fighter (F-35) est une bonne lecture:

http://www.stroustrup.com/JSF-AV-rules.pdf

Je crois qu’Ada est toujours utilisé dans certains projets gouvernementaux qui sont essentiels à la sécurité et / ou à la mission. Je n’ai jamais utilisé la langue, mais c’est sur ma liste de “apprendre”, avec Eiffel. Eiffel propose Design By Contract, qui est censé améliorer la fiabilité et la sécurité.

Tout d’abord, les logiciels critiques pour la sécurité respectent les mêmes principes que ceux que vous constateriez dans les domaines classiques de l’ingénierie mécanique et élecsortingque. Redondance, tolérance aux pannes et sécurité en cas de panne.

En passant, et comme l’a fait remarquer l’affiche précédente (et pour une raison quelconque, nous avons voté contre), le facteur le plus important pour atteindre cet objective est que votre équipe comprenne parfaitement tout ce qui se passe. Il va sans dire qu’une bonne conception de logiciel est essentielle. Mais cela implique également un langage accessible, mature, bien supporté, pour lequel il existe beaucoup de connaissances communes et de développeurs expérimentés disponibles.

De nombreuses affiches ont déjà fait remarquer que l’OS est un élément clé à cet égard, ce qui est très vrai parce qu’il doit être déterministe (voir QNX ou VxWorks). Cela exclut la plupart des langages interprétés qui font des choses dans les coulisses pour vous.

ADA est une possibilité mais il y a moins d’outils et de support disponibles, et plus important encore, les personnes stellaires ne sont pas aussi facilement disponibles.

C ++ est une possibilité mais seulement si vous appliquez ssortingctement un sous-ensemble. À cet égard, c’est l’outil du diable, promettant de nous faciliter la vie, mais en faisant souvent trop,

C est idéal. Il est très mature, rapide, dispose d’un ensemble diversifié d’outils et de supports, de nombreux développeurs expérimentés, multi-plateformes et extrêmement flexibles, peuvent travailler au plus près du matériel.

Je me suis développé dans tout, du petit café au rbuy, et j’ai apprécié et apprécié tout ce que les langues supérieures peuvent offrir. Mais quand je fais le développement de systèmes critiques, je mord la balle et je rest fidèle à C. Dans mon expérience (défense et de nombreux dispositifs médicaux de classe II et III), moins c’est plus.

Je prendrais des haskells si c’est la sécurité sur tout le rest. Je propose haskell car il a une vérification de type statique très rigide et il favorise la programmation où vous construisez des pièces de telle manière qu’elles sont très faciles à tester.

Mais je ne me soucierais pas beaucoup de la langue. Vous pouvez obtenir une plus grande sécurité sans compromettre autant le fait que votre projet soit globalement en bon état et fonctionne sans délais. Dans l’ensemble comme en ayant toute la gestion de base du projet en place. Je me concentrerais peut-être sur des tests approfondis pour s’assurer que tout fonctionne comme il se doit, des tests qui couvrent tous les cas de figure + plus.

Le langage et le système d’exploitation sont importants, mais le design l’est aussi. Essayez de garder les choses simples, simples comme bonjour.

Je commencerais par avoir le ssortingct minimum d’informations d’état (données d’exécution) pour minimiser les risques d’incohérence. Ensuite, si vous voulez avoir une redondance dans le but de tolérer les pannes, assurez-vous de disposer de moyens infaillibles pour récupérer les données de manière incohérente. La redondance sans moyen de récupérer de l’incohérence ne demande que des problèmes.

Toujours avoir une solution de rechange lorsque les actions demandées ne se terminent pas dans un délai raisonnable. Comme on dit dans le contrôle de la circulation aérienne, un dédouanement non reconnu n’est pas autorisé.

N’ayez pas peur des méthodes de sondage. Ils sont simples et fiables, même s’ils peuvent perdre quelques cycles. Éloignez-vous du traitement qui repose uniquement sur des événements ou des notifications, car ils peuvent être facilement supprimés, dupliqués ou désordonnés. En complément des sondages, ils vont bien.

Un de mes amis du projet APOLLO a fait une fois remarquer qu’il savait qu’ils devenaient sérieux quand ils ont décidé de se fier aux sondages plutôt qu’aux événements, même si l’ordinateur était terriblement lent.

PS Je viens de lire les normes C ++ Air Vehicle. Ils sont corrects, mais ils semblent supposer qu’il y aura beaucoup de classes, de données, de pointeurs et d’allocation dynamic de mémoire. C’est exactement ce qui ne devrait pas être plus que nécessaire. Il devrait y avoir une structure de données tsar avec une grosse faux.

L’OS est plus important que le langage. Utilisez un kernel en temps réel tel que VxWorks ou QNX. Nous avons examiné les deux pour le contrôle des robots indussortingels et avons décidé d’aller avec VxWorks. Nous utilisons C pour le contrôle réel du robot.

Pour les logiciels véritablement critiques, tels que les systèmes automatiques d’avions, vous voulez que plusieurs processeurs fonctionnent indépendamment pour vérifier les résultats.

Les environnements en temps réel ont généralement des exigences “critiques pour la sécurité”. Pour ce genre de chose, vous pouvez regarder VxWorks , un système d’exploitation en temps réel très populaire. Il est actuellement utilisé dans de nombreux domaines tels que les avions Boeing, les équipements internes BMW iDrive, les contrôleurs RAID et divers engins spatiaux. ( Check it out .)

Le développement de la plate-forme VxWorks peut être réalisé à l’aide de plusieurs outils, parmi lesquels Eclipse , Workbench , SCORE et autres. C, C ++, Ada et Fortran (oui, Fortran) sont supportés, ainsi que d’autres.

Comme vous ne donnez pas de plate-forme, je devrais dire C / C ++. Sur la plupart des plates-formes temps réel, les options sont relativement limitées.

Les inconvénients de la tendance de C à vous laisser prendre en photo sont compensés par le nombre d’outils permettant de valider le code et la stabilité et la correspondance directe du code avec les capacités matérielles de la plate-forme. En outre, pour tout élément critique, vous ne pourrez pas vous fier à des logiciels tiers qui n’ont pas fait l’object d’un examen approfondi, y compris la plupart des bibliothèques, même celles fournies par les fournisseurs de matériel.

Puisque tout sera à votre charge, vous voulez un compilateur stable, un comportement prévisible et une correspondance étroite avec le matériel.

Voici quelques mises à jour pour certains outils dont je n’avais pas encore discuté et avec lesquels je jouais ces derniers temps et qui sont assez bons.

L’infrastructure du compilateur LLVM , un court texte de présentation sur leur page principale (comprend des interfaces pour C et C ++. Des interfaces pour Java, Scheme et d’autres langages sont en cours de développement);

Une infrastructure de compilation – LLVM est également une collection de code source qui implémente la stratégie de langage et de compilation. Les principaux composants de l’infrastructure LLVM sont un frontal C & C ++ basé sur GCC, un cadre d’optimisation de temps de liaison avec un ensemble croissant d’parsings et de transformations globales et interprocédurales, des back-end statiques pour le X86, X86-64, PowerPC. 32/64, architectures ARM, Thumb, IA-64, Alpha, SPARC, MIPS et CellSPU, un back-end qui émet du code C portable et un compilateur Just-In-Time pour X86, X86-64, PowerPC 32/64 processeurs, et un émetteur pour MSIL.

VCC ;

VCC est un outil qui prouve l’exactitude des programmes C concomitants annotés ou trouve des problèmes dans ces derniers. VCC étend C avec la conception par les caractéristiques du contrat, comme la pré- et la post-condition ainsi que les invariants de type. Les programmes annotés sont convertis en formules logiques à l’aide de l’outil Boogie, qui les transmet à un solveur SMT automatisé Z3 pour vérifier leur validité.

VCC utilise l’ infrastructure de compilation commune récemment publiée.

Ces deux outils, LLVM ou VCC, sont conçus pour prendre en charge plusieurs langues et architectures. Je pense qu’il s’agit d’une augmentation du codage par contrat et d’autres méthodes de vérification formelles.

WPF (pas le framework MS 🙂 est un bon sharepoint départ si vous essayez d’évaluer certaines des recherches et des outils récents dans l’espace de validation des programmes.

Le WG23 est la principale ressource pour les détails de langage de développement de systèmes critiques relativement actuels et spécifiques. Ils couvrent tout, depuis Ada, C, C ++, Java, C #, Scripting, etc. et disposent à tout le moins d’un ensemble de références et de directives pour mettre à jour les informations sur les failles et les vulnérabilités spécifiques à la langue.

Un langage qui impose des patrons soigneux peut aider, mais vous pouvez imposer des patrons soigneux en utilisant n’importe quel langage, même un assembleur. Chaque hypothèse sur chaque valeur nécessite un code qui teste l’hypothèse. Par exemple, testez toujours le diviseur pour zéro avant de diviser.

Plus vous pouvez faire confiance aux composants réutilisables, plus la tâche est facile, mais les composants réutilisables sont rarement certifiés pour une utilisation critique et ne vous permettront pas de passer par les processus de sécurité réglementaires. Vous devez utiliser un petit kernel de système d’exploitation, puis construire de petits modules qui sont testés par unité avec une entrée aléatoire. Une langue comme Eiffel pourrait aider, mais il n’y a pas de solution miracle.

Il y a beaucoup de bonnes références sur http://www.dwheeler.com (“logiciel de haute assurance”).

Pour les produits automobiles, voir la norme MISRA C. C mais vous ne pouvez pas utiliser plus de deux niveaux de pointeurs, et d’autres choses comme ça.

adahome.com a de bonnes informations sur Ada. J’ai bien aimé ce tutoriel C ++ to Ada: http://adahome.com/Ammo/cpp2ada.html

Tom Hawkins a fait des choses intéressantes sur Haskell. Voir: ImProve (le langage intègre un solveur SMT pour vérifier les conditions de vérification) et Atom (EDSL pour la programmation simultanée en temps réel) sans utiliser de threads ou de tâches réels.

Tout logiciel peut passer le processus de certificateion DO-178b à l’aide de n’importe quel outil, mais la question est de savoir à quel point cela serait difficile. Si le compilateur n’est pas certifié, vous devrez peut-être démontrer que votre code est traçable au niveau de l’assemblage. Il est donc utile que votre compilateur soit certifié. Nous avons utilisé C sur nos projets mais nous avons dû vérifier au niveau de l’assemblage et utiliser une norme de code incluant la désactivation de l’optimiseur, une utilisation limitée de la stack, une utilisation limitée des interruptions, des bibliothèques certifiables transparentes, etc. Le plan de l’AFPC semble plus réalisable.

À mesure que les applicatons deviennent plus grandes, le code d’assemblage devient un choix moins viable. Le processeur ARM invite juste C ++, mais si vous demandez à des entresockets comme Kiel si leur outil est certifié, elles reviendront avec un “hein?” Et n’oubliez pas que les outils de vérification doivent également être certifiés. Essayez de vérifier un programme de test LabView.

Une nouvelle norme de sécurité pour Java est en cours de développement – JSR 302: technologie Java critique pour la sécurité .

La sécurité Java critique (SCJ) est basée sur un sous-ensemble de RTSJ. L’objective est de disposer d’un cadre adapté au développement et à l’parsing des programmes critiques de sécurité pour la certificateion critique de sécurité (DO-178B, niveau A et autres normes critiques pour la sécurité).

SCJ, par exemple, supprime le tas, qui est toujours présent dans RTSJ, définit également 3 niveaux de conformité auxquels les applications et les mises en œuvre de VM peuvent se conformer, les niveaux de conformité définis pour faciliter la certificateion d’applications diverses.

Ressources :

  • Java pour les applications critiques pour la sécurité.
  • JSR 302: Technologie Java critique pour la sécurité
  • Développement d’applications critiques pour la sécurité avec Java

HAL / S est utilisé pour la navette spatiale.

Je ne sais pas quelle langue j’utiliserais, mais je sais quelle langue je ne voudrais pas:

NOTE SUR LE SUPPORT JAVA. LE PRODUIT LOGICIEL PEUT CONTENIR UN SUPPORT POUR LES PROGRAMMES ÉCRITS EN JAVA. JAVA TECHNOLOGY N’EST PAS TOLÉRANT AUX DÉFAUTS ET N’EST PAS CONÇU, FABRIQUÉ OU DESTINÉ À ÊTRE UTILISÉ OU REVENDU EN TANT QU’ÉQUIPEMENT DE CONTRÔLE EN LIGNE DANS DES ENVIRONNEMENTS DANGEREUX NÉCESSITANT DES PERFORMANCES SANS ÉGARD, TELS QUE LE FONCTIONNEMENT CONTRÔLE DE LA CIRCULATION, APPAREILS DE SOUTIEN À LA VIE DIRECTE OU SYSTÈMES D’ARMES, DANS LESQUELS LA DÉFAUT DE LA TECHNOLOGIE JAVA POURRAIT ENTRAÎNER DIRECTEMENT LA MORT, DES BLESSURES CORPORELLES OU DES DOMMAGES GRAVES PHYSIQUES OU ENVIRONNEMENTAUX.