SPARK 2014

Les projets qui suivent les meilleures pratiques ci-dessous peuvent s'auto-certifier et montrer qu'ils ont obtenu le badge de la Open Source Security Foundation (OpenSSF).

Si c'est votre projet, veuillez indiquer votre statut de badge sur votre page de projet ! Le statut du badge ressemble à ceci : Le niveau de badge pour le projet 959 est passing Voici comment l'intégrer :

Ce sont les critères du niveau Argent. Vous pouvez également afficher les critères des niveaux Basique ou Or.

        

 Notions de base 17/17

  • Identification

    SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications. It consists of a programming language, a verification toolset and a design method which, taken together, ensure that ultra-low defect software can be deployed in application domains where high-reliability must be assured, for example where safety and security are key requirements.

  • Conditions préalables


    Le projet DOIT atteindre un badge de niveau basique. [achieve_passing]

  • Contenu basique du site Web du projet


    Les informations sur la façon de contribuer DOIVENT inclure les exigences pour des contributions acceptables (par exemple, une référence à toute règle de codage requise). (URL requise) [contribution_requirements]
  • Supervision du projet


    Le projet DEVRAIT avoir un mécanisme juridique par lequel tous les développeurs de quantités non triviales de logiciel du projet affirment qu'ils sont légalement autorisés à effectuer ces contributions. L'approche la plus commune et facilement mise en œuvre pour ce faire est d'utiliser un Certificat d'origine du développeur (DCO), où les utilisateurs ajoutent une information « sign-off-by » dans leurs commits et le projet pointe vers le site Web du DCO. Cependant, cela PEUT être mis en œuvre en tant que contrat de licence de contributeur (CLA), ou tout autre mécanisme juridique. (URL requise) [dco]

    All contributors outside of AdaCore are required to sign a CLA: https://github.com/AdaCore/contributing-howto/blob/master/adacore-corporation-cla.md



    Le projet DOIT définir et documenter clairement son modèle de gouvernance de projet (la façon dont il prend ses décisions, y compris les rôles clés). (URL requise) [governance]

    The SPARK project is a result of the collaboration of AdaCore, Altran and Inria. The collaboration with the three entities takes the form of a partnership between Altran and AdaCore, and a joint lab between AdaCore and Inria (https://www.adacore.com/proofinuse), with AdaCore in the lead role.

    The governance and key roles are documented in the project README at https://github.com/AdaCore/spark2014



    Le projet DOIT adopter un code de conduite et le publier dans un lieu standard. (URL requise) [code_of_conduct]

    Le projet DOIT clairement définir et documenter publiquement les rôles clés dans le projet et leurs responsabilités, y compris les tâches que ces rôles doivent accomplir. Il DOIT être clairement exprimé qui a quel(s) rôle(s), mais cela pourrait ne pas être documenté de la même manière. (URL requise) [roles_responsibilities]

    The README documents key roles and responsibilities: https://github.com/AdaCore/spark2014



    Le projet DOIT pouvoir continuer avec une interruption minimale si une personne décède, est invalidée ou ne peut/veut plus continuer à maintenir le projet. En particulier, le projet DOIT être en mesure de créer et de fermer des problèmes, d'accepter les modifications proposées et de publier des versions du logiciel, dans un délai d'une semaine après confirmation du retrait d'un individu du projet. Cela PEUT être fait en s'assurant que quelqu'un d'autre possède les clés, les mots de passe et les droits juridiques nécessaires pour poursuivre le projet. Les personnes qui exécutent un projet FLOSS PEUVENT faire cela en fournissant des clés dans un coffre-fort et un testament fournissant les droits légaux nécessaires (par exemple, pour les noms DNS). (URL requise) [access_continuity]

    AdaCore as a commercial entity ensures the project will continue with minimal interruption should a person be incapacitated or killed, as SPARK is a key product of the company: https://www.adacore.com/sparkpro



    Le projet DEVRAIT avoir un « bus factor » de 2 ou plus. (URL requise) [bus_factor]

    AdaCore as a commercial entity ensures the project will continue with minimal interruption should a person be incapacitated or killed, as SPARK is a key product of the company: https://www.adacore.com/sparkpro


  • Documentation


    Le projet DOIT avoir une feuille de route documentée qui décrit ce que le projet a l'intention de faire et ne pas faire pour au moins l'année suivante. (URL requise) [documentation_roadmap]

    The SPARK roadmap is presented every year at the AdaCore Tech Days, for example in 2019: https://events.adacore.com/techdaysparis2019/agenda (follow links to access slides)



    Le projet DOIT inclure la documentation de l'architecture (aussi appelée conception de haut niveau) du logiciel produit par le projet. Si le projet ne produit pas de logiciel, sélectionnez « non applicable » (N/A). (URL requise) [documentation_architecture]

    The tool architecture is described as part of the developer documentation at https://github.com/AdaCore/spark2014/blob/master/docs/develguide/tool_structure.rst



    Le projet DOIT documenter ce à quoi l'utilisateur peut et ne peut pas s'attendre en termes de sécurité à partir du logiciel produit par le projet (ses « exigences de sécurité »). (URL requise) [documentation_security]

    As a verification tool, SPARK is not concerned with security vulnerabilities. The benefits of using SPARK for developing secure software are described in particular in a booklet (https://www.adacore.com/books/adacore-tech-for-cyber-security) and on the MITRE listing of CWE-compatible products (http://cwe.mitre.org/compatible/questionnaires/55.html)



    Le projet DOIT fournir un guide de « démarrage rapide » pour les nouveaux utilisateurs afin de les aider à faire rapidement quelque chose avec le logiciel. (URL requise) [documentation_quick_start]

    The SPARK User's Guide contains a tutorial section at http://docs.adacore.com/spark2014-docs/html/ug/en/tutorial.html



    Le projet DOIT faire un effort pour maintenir la documentation conforme à la version actuelle des résultats du projet (y compris les logiciels produits par le projet). Tous les défauts de la documentation connus la rendant incohérente DOIVENT être corrigés. Si la documentation est généralement à jour, mais inclut de manière erronée certaines informations antérieures qui ne sont plus vraies, considérez cela comme un défaut, puis faites le suivi et corrigez comme d'habitude. [documentation_current]

    All documentation is maintained up-to-date daily with changes to the code, in particular the SPARK User's Guide at http://docs.adacore.com/spark2014-docs/html/ug/index.html



    La page d'accueil et/ou le site Web du dépôt du projet DOIVENT identifier et pointer tous les accomplissements, y compris ce badge sur les meilleures pratiques, dans les 48 heures suivant la reconnaissance publique que l'accomplissement a été atteint. (URL requise) [documentation_achievements]

    The GitHub page uses the CII badge: https://github.com/AdaCore/spark2014


  • Accessibilité et internationalisation


    Le projet (à la fois les sites du projet et les résultats du projet) DEVRAIT suivre les meilleures pratiques d'accessibilité afin que les personnes handicapées puissent encore participer au projet et utiliser les résultats du projet où il est raisonnable de le faire. [accessibility_best_practices]

    All functionalities of GNATprove are available through the command-line tool gnatprove, except for some interactions features specific to working inside an IDE (for example, display of the trace corresponding to a counterexample).



    Le logiciel produit par le projet DEVRAIT être internationalisé pour permettre une localisation facile pour la culture, la région ou la langue du public cible. Si l'internationalisation (i18n) ne s'applique pas (par exemple, le logiciel ne génère pas de texte destiné aux utilisateurs finaux et ne trie pas de texte lisible par les humains), sélectionnez « non applicable » (N/A). [internationalization]

    There has not been requests for internationalization that could justify this effort so far. Part of the documentation has been translated into Japanese: https://www.adacore.com/resources-in-japanese


  • Autre


    Si les sites du projet (site Web, dépôt et URL de téléchargement) entreposent des mots de passe pour l'authentification d'utilisateurs externes, les mots de passe DOIVENT être entreposés comme hachages itérés avec salage par utilisateur en utilisant un algorithme d'étirement des clés (itéré) (par exemple, Argon2id, Bcrypt, Scrypt, ou PBKDF2). Si les sites du projet n'entreposent pas de mots de passe à cette fin, sélectionnez « non applicable » (N/A). [sites_password_security]

    Project website uses GitHub which does not store additional passwords than the one for GitHub itself.


  • Versions précédentes


    Le projet DOIT maintenir les anciennes versions les plus utilisées du produit ou fournir un chemin de mise à niveau vers des versions plus récentes. Si le chemin de mise à niveau est difficile, le projet DOIT documenter comment effectuer la mise à niveau (par exemple, les interfaces qui ont changé et une suggestion d'étapes détaillées pour aider la mise à niveau). [maintenance_or_update]

    Previous versions of SPARK 2014, starting with the first one issued in 2014, can be downloaded at https://www.adacore.com/download/more. We pay extraordinary attention to maintain backwards compatibility between versions, and have not needed to issue migration guidelines so far.


  • Procédure de signalement des bogues


    Le projet DOIT utiliser un suivi des problèmes pour le suivi des problèmes individuels. [report_tracker]

    Yes, GitHub issue tracker.


  • Processus de signalement de vulnérabilité


    Le projet DOIT créditer les auteurs de tous les signalements de vulnérabilité résolus au cours des 12 derniers mois, à l'exception des auteurs qui demandent l'anonymat. S'il n'y a pas eu de vulnérabilité résolue au cours des 12 derniers mois, sélectionnez « non applicable » (N/A). (URL requise) [vulnerability_report_credit]

    As a verification tool, SPARK is not concerned with security vulnerabilities in the tool itself.



    Le projet DOIT avoir un processus documenté pour répondre aux signalements de vulnérabilité. (URL requise) [vulnerability_response_process]

    The GitHub issue tracker is used for all issues: https://github.com/AdaCore/spark2014/issues


  • Normes de codage


    Le projet DOIT identifier les guides de style de codage spécifiques pour les langages principaux qu'il utilise, et exiger que les contributions le respectent en général. (URL requise) [coding_standards]

    Le projet DOIT imposer automatiquement son ou ses styles de codage sélectionnés s'il existe au moins un outil FLOSS qui peut le faire dans le(s) langage(s) sélectionné(s). [coding_standards_enforced]

    Warnings and style checks selected for GNAT development are enforced by the GNAT compiler.


  • Système de construction opérationnel


    Les systèmes de construction pour les binaires natifs DOIVENT honorer les variables (d'environnement) pertinentes du compilateur et du lieur qui leur sont transmises (par exemple, CC, CFLAGS, CXX, CXXFLAGS et LDFLAGS) et les transmettre aux invocations du compilateur et du lieur. Un système de construction PEUT les étendre avec des options supplémentaires ; il NE DOIT PAS simplement remplacer les valeurs fournies par les siennes. Si aucun fichier binaire natif n'est généré, sélectionnez « non applicable » (N/A). [build_standard_variables]

    The Makefiles do use environment variables which can be overwritten.



    Le système de construction et d'installation DEVRAIT préserver les informations de débogage si elles sont demandées dans les options correspondants (par exemple, « install -s » n'est pas utilisé). S'il n'y a pas de système de construction ou d'installation (par exemple, les bibliothèques JavaScript typiques), sélectionnez « non applicable » (N/A). [build_preserve_debug]

    GNATprove can be build in debug mode by passing the value Debug for the Build environment variable (also the default mode).



    Le système de construction pour le logiciel produit par le projet NE DOIT PAS reconstruire de manière récursive des sous-répertoires s'il existe des dépendances croisées dans les sous-répertoires. S'il n'y a pas de système de construction ou d'installation (par exemple, les bibliothèques JavaScript typiques), sélectionnez « non applicable » (N/A). [build_non_recursive]

    Each binary can be built independently using the appropriate builder (GPRbuild for Ada code, OCamlbuild for OCaml code). The Makefiles only provide the scripting around calls to the builders.



    Le projet DOIT pouvoir répéter le processus de génération d'informations à partir de fichiers source et obtenir exactement le même résultat bit-à-bit. Si aucune construction ne se produit (par exemple, dans les langages de script où le code source est utilisé directement au lieu d'être compilé), sélectionnez « non applicable » (N/A). [build_repeatable]

    Internal quality assurance at AdaCore relies on the reproducibility of builds.


  • Système d'installation


    Le projet DOIT fournir un moyen d'installer et de désinstaller facilement le logiciel produit par le projet en utilisant une convention couramment utilisée. [installation_common]

    On Linux/Mac, all artefacts are installed under the target installation directory. Uninstall can be done by deleting the directory. Install is facilitated for the Community release by providing an installer for Windows/Linux/Mac.



    Le système d'installation pour les utilisateurs finaux DOIT honorer les conventions standard pour sélectionner l'emplacement où les artefacts construits sont écrits au moment de l'installation. Par exemple, s'il installe des fichiers sur un système POSIX, il DOIT honorer la variable d'environnement DESTDIR. S'il n'y a pas de système d'installation ou pas de convention standard, sélectionnez « non applicable » (N/A). [installation_standard_variables]

    The installer proposes a candidate location for installation that the user can override.



    Le projet DOIT fournir un moyen pour les développeurs potentiels d'installer rapidement tous les résultats du projet ainsi que l'environnement nécessaire pour apporter des modifications, y compris les tests et l'environnement de test. Cela DOIT être effectué avec une convention couramment utilisée. [installation_development_quick]

    This is described in the README at https://github.com/AdaCore/spark2014#6-building-spark


  • Composants maintenus à l'extérieur


    Le projet DOIT afficher ses dépendances externes de manière analysable par ordinateur. (URL requise) [external_dependencies]

    There are few dependencies that are listed in the README: https://github.com/AdaCore/spark2014#6-building-spark



    Les projets DOIVENT surveiller ou vérifier périodiquement leurs dépendances externes (y compris les copies de commodité) pour détecter les vulnérabilités connues, et corriger les vulnérabilités exploitables ou les vérifier comme inexploitables. [dependency_monitoring]

    As a verification tool, SPARK is not concerned with security vulnerabilities in the tool itself.



    Le projet DOIT :
    1. rendre facile l'identification et la mise à jour des composants maintenus extérieurement au projet ; ou
    2. utiliser des composants standards fournis par le système ou le langage de programmation.
    Ensuite, si une vulnérabilité se trouve dans un composant réutilisé, il sera facile de mettre à jour ce composant. [updateable_reused_components]

    The components used by GNATprove should be separately built.



    Le projet DEVRAIT éviter d'utiliser des fonctions et des API obsolètes quand des alternatives FLOSS sont disponibles dans l'ensemble de technologies qu'il utilise (sa « pile de technologies ») et disponibles à une large majorité des utilisateurs supportés par le projet (afin que les utilisateurs puissent avoir accès à l'alternative). [interfaces_current]

    This is met to the best of our knowledge.


  • Suite de tests automatisée


    Une suite de tests automatisée DOIT être appliquée à chaque commit dans un dépôt partagé pour au moins une branche. Cette suite de tests DOIT produire un rapport sur le succès ou l'échec du test. [automated_integration_testing]

    Internal quality assurance at AdaCore ensures that all commits are included in a Continuous Build and Test. Results are reported to the author.



    Le projet DOIT ajouter des tests de régression à une suite de tests automatisée pour au moins 50% des bogues corrigés au cours des six derniers mois. [regression_tests_added50]

    A test is added for all bugs fixed.



    Le projet DOIT avoir une ou des suites de tests automatisées FLOSS qui fournissent une couverture d'instructions d'au moins 80% s'il existe au moins un outil FLOSS qui peut mesurer ce critère dans le langage sélectionné. [test_statement_coverage80]

    Coverage is over 95% on the public testsuite at https://github.com/AdaCore/spark2014/tree/master/testsuite/gnatprove. Coverage is measured every night using source code instrumentation with GNATcoverage. Files from the GNAT compiler used to build the AST are excluded from coverage analysis, as most of the code in these files is not used in the project.


  • Nouveau test de fonctionnalité


    Le projet DOIT avoir une politique écrite formelle, que dès qu'une nouvelle fonctionnalité majeure est ajoutée, des tests pour la nouvelle fonctionnalité DOIVENT être ajoutés à une suite de tests automatisée. [test_policy_mandated]

    This is part of quality assurance at AdaCore.



    Le projet DOIT inclure, dans ses instructions documentées pour les propositions de changement, la politique selon laquelle des tests doivent être ajoutés pour toute nouvelle fonctionnalité majeure. [tests_documented_added]

    Major new functionality is currently only provided by the entities mentioned in the governance section of the README at https://github.com/AdaCore/spark2014. Tests are in fact part of any change, in particular for new functionality (small or large). This can be checked easily as tests and code are submitted in the same patches in the same repository, and must go through peer review.


  • Options d'avertissement


    Les projets DOIVENT être maximalement stricts avec les avertissements dans le logiciel produit par le projet, quand cela est approprié. [warnings_strict]

    Warnings are considered as errors and stop the build.


  • Connaissance du développement sécurisé


    Le projet DOIT implémenter des principes de conception sécurisés (à partir de « know_secure_design »), quand cela est approprié. Si le projet ne produit pas de logiciel, sélectionnez « non applicable » (N/A). [implement_secure_design]

    As a verification tool, SPARK is not concerned with security vulnerabilities in the tool itself.


  • Utiliser de bonnes pratiques de base de cryptographie

    Notez que certains logiciels n'ont pas besoin d'utiliser des mécanismes cryptographiques. Si votre projet produit un logiciel qui (1) inclut ou active la fonctionnalité de chiffrement, et (2) peut être publié des États-Unis (US) vers l'extérieur des États-Unis ou vers un citoyen autre qu'américain, vous pouvez être légalement obligé à faire quelques étapes supplémentaires. En règle générale, cela implique simplement l'envoi d'un email. Pour plus d'informations, consultez la section sur le chiffrement de Comprendre la technologie Open Source et les contrôles à l'exportation américains .

    Les mécanismes de sécurité par défaut dans le logiciel produit par le projet NE DOIVENT PAS dépendre d'algorithmes ou de modes cryptographiques avec des faiblesses sérieuses connues (par exemple, l'algorithme de hachage cryptographique SHA-1 ou le mode CBC en SSH). [crypto_weaknesses]


    Le projet DEVRAIT supporter plusieurs algorithmes cryptographiques, afin que les utilisateurs puissent rapidement changer si l'un deux est cassé. Les algorithmes à clés symétriques courants incluent AES, Twofish et Serpent. Les alternatives d'algorithme de hachage cryptographique courantes incluent SHA-2 (y compris SHA-224, SHA-256, SHA-384 ET SHA-512) et SHA-3. [crypto_algorithm_agility]


    Le projet DOIT supporter le stockage des informations d'authentification (comme les mots de passe et les jetons dynamiques) et des clés cryptographiques privées dans des fichiers distincts des autres informations (fichiers de configuration, bases de données et journaux) et permettre aux utilisateurs de les mettre à jour et de les remplacer sans recompilation de code. Si le projet ne traite jamais d'informations d'authentification et de clés cryptographiques privées, sélectionnez « non applicable » (N/A). [crypto_credential_agility]


    Le logiciel produit par le projet DEVRAIT supporter des protocoles sécurisés pour toutes ses communications réseau, tels que SSHv2 ou ultérieur, TLS1.2 ou ultérieur (HTTPS), IPsec, SFTP et SNMPv3. Les protocoles non sûrs tels que FTP, HTTP, telnet, SSLv3 ou antérieur, et SSHv1 DEVRAIENT être désactivés par défaut et uniquement activés si l'utilisateur le configure spécifiquement. Si le logiciel produit par le projet ne prend pas en charge les communications réseau, sélectionnez « non applicable » (N/A). [crypto_used_network]


    Le logiciel produit par le projet DEVRAIT, s'il prend en charge ou utilise TLS, prendre en charge au moins TLS version 1.2. Notez que le prédécesseur de TLS s'appelait SSL. Si le logiciel n'utilise pas TLS, sélectionnez « non applicable » (N/A). [crypto_tls12]


    Le logiciel produit par le projet DOIT, s'il prend en charge TLS, effectuer la vérification des certificats TLS par défaut lors de l'utilisation de TLS, y compris sur les sous-ressources. Si le logiciel n'utilise pas TLS, sélectionnez « non applicable » (N/A). [crypto_certificate_verification]


    Le logiciel produit par le projet DOIT, s'il supporte TLS, effectuer une vérification de certificat avant d'envoyer des en-têtes HTTP avec des informations privées (telles que des cookies sécurisés). Si le logiciel n'utilise pas TLS, sélectionnez « non applicable » (N/A). [crypto_verification_private]

  • Livraison sécurisée


    Le projet DOIT signer cryptographiquement les versions des résultats du projet destinées à une utilisation répandue, et il DOIT y avoir un processus documenté expliquant aux utilisateurs comment ils peuvent obtenir les clés de signature publique et vérifier la ou les signatures. La clé privée pour ces signature(s) NE DOIT PAS être sur le(s) site(s) utilisé(s) pour distribuer directement le logiciel au public. Si les versions ne sont pas destinées à une utilisation répandue, sélectionnez « non applicable » (N/A). [signed_releases]

    Currently, we only provide a hash of the installation package at https://www.adacore.com/download/more



    Il est PROPOSÉ que, dans le système de contrôle de la version, chaque tag d'une version importante (un tag faisant partie d'une version majeure, d'une version mineure ou qui corrige des vulnérabilités notées publiquement) soit cryptographiquement signé et vérifiable comme décrit dans signed_releases. [version_tags_signed]

  • Autres problèmes de sécurité


    Les résultats du projet DOIVENT vérifier toutes les entrées provenant de sources potentiellement non fiables pour s'assurer qu'elles sont valides (une liste blanche) et rejeter les entrées non valides, en cas de restrictions sur les données. [input_validation]

    As a verification tool, SPARK is not concerned with security vulnerabilities in the tool itself.



    Les mécanismes de durcissement DOIVENT être utilisés dans le logiciel produit par le projet afin que les défauts du logiciel soient moins susceptibles d'entraîner des vulnérabilités de sécurité. [hardening]

    As a verification tool, SPARK is not concerned with security vulnerabilities in the tool itself.



    Le projet DOIT fournir une analyse de fiabilité qui justifie pourquoi ses exigences de sécurité sont respectées. L'analyse de fiabilité DOIT inclure : une description du modèle de menace, une identification claire des limites de confiance, un argument selon lequel des principes de conception sécurisés ont été appliqués et un argument selon lequel les faiblesses de sécurité courantes de l'implémentation ont été contrées. (URL requise) [assurance_case]

    As a verification tool, SPARK is not concerned with security vulnerabilities in the tool itself.


  • Analyse statique de code


    Le projet DOIT utiliser au moins un outil d'analyse statique avec des règles ou des approches pour rechercher des vulnérabilités courantes dans le langage ou l'environnement analysé, s'il existe au moins un outil FLOSS qui peut mettre en œuvre ce critère dans le langage sélectionné. [static_analysis_common_vulnerabilities]

    CodePeer targets common CWE, as documented in CodePeer User's Guide: http://docs.adacore.com/live/wave/codepeer/html/codepeer_ug/messages_and_annotations.html#support-for-cwe


  • Analyse dynamique de code


    Si le logiciel produit par le projet inclut un logiciel écrit à l'aide d'un langage non sûr pour les accès mémoire (par exemple C ou C++), alors le projet DOIT utiliser au moins un outil dynamique (par exemple, un fuzzer ou un scanneur d'application Web) utilisé de manière routinière en combinaison avec un mécanisme permettant de détecter des problèmes de sécurité mémoire tels que les dépassement mémoire. Si le projet ne produit pas de logiciel écrit dans un langage non sûr pour les accès mémoire, sélectionnez « non applicable » (N/A). [dynamic_analysis_unsafe]

    Ada and OCaml are the two main languages used. Both are memory safe languages.



Ces données sont disponibles sous une licence Creative Commons Attribution version 3.0 ou ultérieure (CC-BY-3.0+). Chacun peut librement partager et adapter les données, à condition de créditer leur origine. Veuillez créditer Yannick Moy et les contributeurs du badge des meilleures pratiques de la OpenSSF.

Soumission du badge du projet appartenant à : Yannick Moy.
Soumission créée le 2017-05-11 04:54:51 UTC, dernière mise à jour le 2021-05-11 07:46:17 UTC. Le dernier badge obtenu l'a été le 2018-07-02 09:39:05 UTC.

Retour