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).

Il n'existe aucun ensemble de pratiques qui garantissent que ce logiciel n'aura jamais de défauts ou de vulnérabilités ; même les méthodes formelles peuvent échouer si les spécifications ou les hypothèses sont fausses. Il n'y a pas non plus de pratiques qui peuvent garantir qu'un projet permettra de maintenir une communauté de développement saine et qui fonctionne bien. Toutefois, suivre les meilleures pratiques peut contribuer à améliorer les résultats des projets. Par exemple, certaines pratiques permettent la revue par plusieurs personnes avant publication, ce qui peut aider à trouver des vulnérabilités techniques difficiles à trouver autrement et à renforcer la confiance et un désir d'interaction répétée entre les développeurs de différentes entreprises. Pour gagner un badge, tous les critères DOIT et NE DOIT PAS doivent être satisfaits, tous les critères DEVRAIT doivent être satisfaits OU non satisfaits avec justification, et tous les critères PROPOSÉ doivent être satisfaits OU non satisfaits (nous voulons au moins qu'ils soient considérés). Si vous voulez entrer un texte de justification pour un commentaire générique, au lieu d'une raison justifiant que la situation est acceptable, commencez le bloc de texte avec '//' suivi d'un espace. Les commentaires sont les bienvenus via le site GitHub en tant que problèmes ou pull requests. Il existe également une liste de diffusion pour discussion générale.

Nous fournissons volontiers l'information dans plusieurs langues, cependant, s'il existe un conflit ou une contradiction entre les traductions, la version anglaise est la version qui fait autorité.
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 :
Vous pouvez afficher votre statut de badge en incorporant ceci dans votre fichier markdown :
[![OpenSSF Best Practices](https://www.bestpractices.dev/projects/959/badge)](https://www.bestpractices.dev/projects/959)
ou en incorporant ceci dans votre HTML :
<a href="https://www.bestpractices.dev/projects/959"><img src="https://www.bestpractices.dev/projects/959/badge"></a>


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

    Notez que d'autres projets peuvent utiliser le même nom.

    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


    Assez pour un badge !

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

  • Contenu basique du site Web du projet


    Assez pour un badge !

    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]

    https://github.com/AdaCore/spark2014/blob/master/CONTRIBUTING.md


  • Supervision du projet


    Assez pour un badge !

    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]
    Le DCO est le mécanisme recommandé, car il est facile à mettre en œuvre, suivi dans le code source, et git prend directement en charge une fonction « approuvé » en utilisant « commit -s ». Pour être plus efficace, il est préférable que la documentation du projet explique ce que signifie « approuvé » pour ce projet. Un CLA est un accord juridique qui définit les termes en vertu desquels des travaux intellectuels ont été licenciés à une organisation ou un projet. Un accord de cession (CAA) est un accord légal qui transfère les droits dans un travail intellectuel à une autre partie ; il n'est pas exigé d'avoir des CAA pour les projets, car un CAA augmente le risque que les contributeurs potentiels ne contribuent pas, en particulier si le destinataire est un organisme à but lucratif. Les CLA de la Fondation Apache (la licence de contributeur individuel et la CLA d'entreprise) sont des exemples de CLA pour des projets qui déterminent que les risques de ces types de CLA au projet sont inférieurs à leurs avantages.

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


    Assez pour un badge !

    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]
    Il doit y avoir une manière documentée bien établie de prendre des décisions et de résoudre les différends. Dans les petits projets, cela peut être aussi simple que « le propriétaire du projet et dirigeant prend toutes les décisions finales ». Il existe différents modèles de gouvernance, y compris le dictateur bienveillant et la méritocratie formelle ; pour plus de détails, voir Modèles de gouvernance. Les approches centralisées (par exemple, un seul mainteneur) et décentralisées (par exemple, les groupes de mainteneurs) ont été utilisées avec succès dans des projets. L'information sur la gouvernance n'a pas besoin de documenter la possibilité de créer une duplication de projet, car cela est toujours possible pour les projets FLOSS.

    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


    Assez pour un badge !

    Le projet DOIT adopter un code de conduite et le publier dans un lieu standard. (URL requise) [code_of_conduct]
    Les projets peuvent être en mesure d'améliorer la civilité de leur communauté et d'établir des attentes quant à une conduite acceptable en adoptant un code de conduite. Cela peut aider à éviter les problèmes avant leur apparition et faire du projet un lieu plus accueillant pour encourager les contributions. Cela devrait se concentrer uniquement sur le comportement au sein de la communauté / lieu de travail du projet. Des exemples de codes de conduite sont le code de conduite du noyau Linux, le code de conduite du pacte de contributeur, le code de conduite du projet Debian, le code de conduite du projet Ubuntu, le code de conduite du projet Fedora, le code de conduite du projet GNOME, le code de conduite de la communauté KDE", le code de conduite de la communauté Python, le guide de conduite de la communauté Ruby, et le code de conduite du projet Rust.

    https://github.com/AdaCore/spark2014/blob/master/CODE_OF_CONDUCT.md


    Assez pour un badge !

    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]
    La documentation pour la gouvernance et les rôles et responsabilités peut être à un seul endroit.

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


    Assez pour un badge !

    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


    Assez pour un badge !

    Le projet DEVRAIT avoir un « bus factor » de 2 ou plus. (URL requise) [bus_factor]
    Un « bus factor » (aussi connu en tant que « truck factor ») est le nombre minimum de membres du projet qui doivent disparaître soudainement d'un projet (« écrasé par un bus ») avant que le projet ne se bloque en raison du manque de personnel compétent. L'outil truck-factor peut l'estimer pour des projets sur GitHub. Pour plus d'informations, voir Évaluation du « bus factor » des dépôts Git par Cosentino et al.

    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


    Assez pour un badge !

    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]
    Le projet pourrait ne pas atteindre la feuille de route, et c'est acceptable ; le but de la feuille de route est d'aider les utilisateurs et les contributeurs potentiels à comprendre l'orientation prévue du projet. Elle ne doit nécessairement pas être détaillée.

    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)


    Assez pour un badge !

    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]
    Une architecture de logiciel explique les structures fondamentales d'un programme, c'est-à-dire les principaux composants du programme, les relations entre eux et les propriétés clés de ces composants et de ces relations.

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


    Assez pour un badge !

    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]
    Ce sont les exigences de sécurité que le logiciel est supposé remplir.

    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)


    Assez pour un badge !

    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]
    L'idée est de montrer aux utilisateurs comment démarrer et de faire en sorte que le logiciel fasse quelque chose. Ceci est d'une importance cruciale pour les utilisateurs potentiels pour les aider à démarrer.

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


    Assez pour un badge !

    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]
    La documentation PEUT inclure des informations sur les différences ou les modifications entre les versions du logiciel et/ou des liens vers les anciennes versions de la documentation. L'objectif de ce critère est de faire en sorte que la documentation soit cohérente et non pas que la documentation soit parfaite.

    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


    Assez pour un badge !

    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]
    Un accomplissement est un ensemble de critères externes que le projet a spécifiquement cherché à atteindre, y compris certains badges. Cette information ne doit pas nécessairement être sur la page d'accueil du site Web du projet. Un projet utilisant GitHub peut mettre des accomplissements sur la page d'accueil du dépôt en les ajoutant au fichier README.

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


  • Accessibilité et internationalisation


    Assez pour un badge !

    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]
    Pour les applications Web, consultez les Directives d'accessibilité des contenus Web (WCAG 2.0) et son document à l'appui Comprendre WCAG 2.0 ; voir aussi les informations d'accessibilité du W3C. Pour les applications IHM, envisagez d'utiliser les directives d'accessibilité spécifiques à l'environnement (telles que Gnome, KDE, XFCE, Android, IOS, Mac et Windows). Certaines applications IHM textuelles (par exemple, les programmes « ncurses ») peuvent faire certaines choses pour se rendre plus accessibles (par exemple, le paramètre « force-arrow-cursor » de « alpine »). La plupart des applications en ligne de commande sont assez accessibles telles quelles. Ce critère est souvent N/A, par exemple, pour les bibliothèques. Voici quelques exemples d'actions à prendre ou de questions à considérer :
    • Fournir des alternatives de texte pour tout contenu non textuel afin qu'il puisse être changé en d'autres formes dont les gens ont besoin, comme une plus grande taille, le braille, une sortie vocale, des symboles ou une langue plus simple (WCAG 2.0 directive 1.1)
    • La couleur n'est pas utilisée comme le seul moyen visuel de transmettre des informations, d'indiquer une action, de provoquer une réponse ou de distinguer un élément visuel. (WCAG 2.0 directive 1.4.1)
    • La présentation visuelle du texte et des images du texte a un taux de contraste d'au moins 4,5:1, à l'exception du grand texte, du texte incident, et des logotypes (WCAG 2.0 directive 1.4.3)
    • Rendez toutes les fonctionnalités disponibles à partir d'un clavier (WCAG directive 2.1)
    • Une IHM ou un projet basé sur le Web DEVRAIT tester avec au moins un lecteur d'écran sur la (les) plate-forme(s) cible(s) (par exemple NVDA, Jaws ou WindowEyes sur Windows ; VoiceOver sur Mac & iOS ; Orca sous Linux/BSD ; TalkBack sur Android). Les programmes IHM textuels PEUVENT travailler à réduire le retrait excessif pour éviter la lecture redondante par les lecteurs d'écran.

    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).


    À peine suffisant pour un badge.

    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]
    La localisation « réfère à l'adaptation du contenu d'un produit, d'une application ou d'un document pour répondre aux exigences linguistiques, culturelles et autres d'un marché cible spécifique (un lieu). » L'internationalisation est la « conception et le développement du contenu d'un produit, d'une application ou d'un document qui permette une localisation facile pour les publics cibles qui varient en culture, en région ou en langue. » (Voir la page « Localisation ou Internationalisation » du W3C.) Le logiciel répond à ce critère simplement en étant internationalisé. Aucune localisation pour une autre langue spécifique n'est requise, car une fois que le logiciel a été internationalisé, d'autres peuvent travailler sur la localisation.

    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


    Assez pour un badge !

    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]
    Notez que l'utilisation de GitHub répond à ce critère. Ce critère s'applique uniquement aux mots de passe utilisés pour l'authentification d'utilisateurs externes sur les sites du projet (càd l'authentification entrante). Si les sites du projet doivent se connecter à d'autres sites (càd l'authentification sortante), ils devront peut-être entreposer différemment des jetons d'identification à cette fin (puisque conserver un code de hachage serait inutile). Ceci applique le critère crypto_password_storage aux sites du projet, de manière similaire à sites_https.

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


 Contrôle des modifications 1/1 ●

  • Versions précédentes


    Assez pour un badge !

    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.


 Compte-rendu 3/3 ●

  • Procédure de signalement des bogues


    Assez pour un badge !

    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é


    Assez pour un badge !

    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.


    Assez pour un badge !

    Le projet DOIT avoir un processus documenté pour répondre aux signalements de vulnérabilité. (URL requise) [vulnerability_response_process]
    Ceci est fortement lié à vulnerability_report_process, qui exige qu'il existe un moyen documenté de signaler les vulnérabilités. Il a également trait à la vulnerability_report_response, qui nécessite une réponse aux signalements de vulnérabilité dans un certain laps de temps.

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


 Qualité 18/19 ●

  • Normes de codage


    Assez pour un badge !

    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]
    Dans la plupart des cas, cela se fait en se référant à certains guides de style existants, ce qui permet d'énumérer les différences. Ces guides de style peuvent inclure des moyens d'améliorer la lisibilité et les moyens de réduire la probabilité de défauts (y compris les vulnérabilités). Beaucoup de langages de programmation ont un ou plusieurs guides de style largement utilisés. Des exemples de guides de style incluent les guides de style de Google et les Règles de codage du SEI CERT.

    We use the standard warnings and style checks selected for GNAT development, triggered by compilation switches -gnatw.g (see http://docs.adacore.com/live/wave/gnat_ugn/html/gnat_ugn/gnat_ugn/building_executable_programs_with_gnat.html#warning-message-control) and -gnatyg (see http://docs.adacore.com/live/wave/gnat_ugn/html/gnat_ugn/gnat_ugn/building_executable_programs_with_gnat.html#style-checking)


    Assez pour un badge !

    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]
    Cela PEUT être mis en œuvre en utilisant des outils d'analyse statique et/ou en faisant passer le code à travers des outils de remise en forme. Dans de nombreux cas, la configuration de l'outil est incluse dans le dépôt du projet (car différents projets peuvent choisir différentes configurations). Les projets PEUVENT permettre des exceptions de style (et le font habituellement) ; là où les exceptions se produisent, elles DOIVENT être rares et documentées dans le code à leur emplacement, afin que ces exceptions puissent être revues et que les outils puissent les gérer automatiquement à l'avenir. Des exemples de tels outils incluent ESLint (JavaScript), Rubocop (Ruby) et devtools check (R).

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


  • Système de construction opérationnel


    Assez pour un badge !

    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]
    Il devrait être facile d'activer des fonctionnalités de construction spéciales telles que Address Sanitizer (ASAN), ou de se conformer aux meilleures pratiques de durcissement de la distribution (par exemple, en activant facilement les options de compilation pour le faire).

    The Makefiles do use environment variables which can be overwritten.


    Assez pour un badge !

    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]
    Par exemple, la définition de CFLAGS (C) ou CXXFLAGS (C++) devrait créer les informations de débogage pertinentes si ces langages sont utilisés et elles ne devraient pas être retirées pendant l'installation. Des informations de débogage sont nécessaires pour le support et l'analyse, et également utiles pour mesurer la présence de fonctionnalités de durcissement dans les binaires compilés.

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


    Assez pour un badge !

    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]
    Les informations de dépendance internes du système de construction du projet doivent être précises, sinon, les modifications apportées au projet peuvent ne pas s'effectuer correctement. Des constructions incorrectes peuvent entraîner des défauts (y compris des vulnérabilités). Une erreur courante dans les grands systèmes de construction est d'utiliser une « construction récursive », c'est-à-dire une hiérarchie de sous-répertoires contenant des fichiers source, chaque sous-répertoire étant construit de manière indépendante. Sauf si chaque sous-répertoire est entièrement indépendant, ceci est une erreur, car les informations de dépendance sont incorrectes.

    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.


    Assez pour un badge !

    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]
    Les utilisateurs GCC et Clang peuvent trouver l'option -frandom-seed utile ; dans certains cas, cela peut être résolu en forçant un ordre de tri. Plus de suggestions peuvent être trouvées sur le site pour une construction reproductible.

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


  • Système d'installation


    Assez pour un badge !

    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]
    Des exemples comprennent l'utilisation d'un gestionnaire de paquets (au niveau du système ou du langage), « make/install/uninstall » (supportant DESTDIR), un conteneur dans un format standard ou une image de machine virtuelle dans un format standard. Le processus d'installation et de désinstallation (par exemple, son paquetage) PEUT être mis en œuvre par un tiers tant qu'il est FLOSS.

    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.


    Assez pour un badge !

    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.


    Assez pour un badge !

    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]
    Cela PEUT être implémenté à l'aide d'un conteneur généré et/ou d'un script d'installation. Les dépendances externes sont généralement installées en invoquant des gestionnaires de paquets du système et/ou du langage, comme précisé dans external_dependencies.

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


  • Composants maintenus à l'extérieur


    Pas assez pour un badge.

    Le projet DOIT afficher ses dépendances externes de manière analysable par ordinateur. (URL requise) [external_dependencies]
    Généralement, cela se fait en utilisant les conventions du gestionnaire de paquets et/ou du système de construction. Notez que cela permet d'implémenter installation_development_quick.

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


    Assez pour un badge !

    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]
    Cela peut se faire à l'aide d'un outil d'analyse d'origine, de vérification de dépendance ou d'analyse de la composition du logiciel tel que Dependency-Check d'OWASP, Nexus Auditeur de Sonartype, Black Duck Software Composition Analysis de Synopsys, et Bundler-audit (pour Ruby). Certains gestionnaires de paquets comprennent des mécanismes pour le faire. Il est acceptable que la vulnérabilité des composants ne puisse pas être exploitée, mais cette analyse est difficile et il est parfois plus simple de mettre à jour ou de corriger la dépendance.

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


    Assez pour un badge !

    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]
    Une façon typique de respecter ce critère est d'utiliser les systèmes de gestion des paquets du système et du langage de programmation. De nombreux programmes FLOSS sont distribués avec des « bibliothèques de commodité » qui sont des copies locales de bibliothèques standard (éventuellement dupliquées). En soi, c'est acceptable. Cependant, si le programme *doit* utiliser ces copies locales (dupliquées), la mise à jour des bibliothèques « standard » lors de mises à jour de sécurité laissera ces copies supplémentaires encore vulnérables. C'est particulièrement un problème pour les systèmes basés sur le cloud ; si le fournisseur du cloud met à jour ses librairies « standard » mais que le programme ne les utilise pas, les mises à jour ne vous aideront pas. Voir, par exemple, « Chromium : pourquoi il n'est pas encore un vrai paquet dans Fedora » par Tom Callaway.

    The components used by GNATprove should be separately built.


    Assez pour un badge !

    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


    Assez pour un badge !

    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]
    Cette exigence peut être considérée comme un sous-ensemble de test_continuous_integration, mais axée sur le simple test, sans nécessiter une intégration continue.

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


    Assez pour un badge !

    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.


    Assez pour un badge !

    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]
    De nombreux outils FLOSS sont disponibles pour mesurer la couverture des tests, y compris gcov/lcov, Blanket.js, Istanbul, JCov et covr (R). Notez que respecter ce critère n'est pas une garantie que la suite de tests est complète, mais, à l'inverse, ne pas respecter ce critère est un indicateur fort d'une suite de tests insuffisante.

    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é


    Assez pour un badge !

    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.


    Assez pour un badge !

    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]
    Cependant, même une règle informelle est acceptable tant que les tests sont ajoutés dans la pratique.

    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


    Assez pour un badge !

    Les projets DOIVENT être maximalement stricts avec les avertissements dans le logiciel produit par le projet, quand cela est approprié. [warnings_strict]
    Certains avertissements ne peuvent être efficacement activés sur certains projets. Ce qui est nécessaire est la preuve que le projet s'efforce d'activer les options d'avertissements où il peut, de sorte que les erreurs soient détectées tôt.

    Warnings are considered as errors and stop the build.


 Sécurité 11/13 ●

  • Connaissance du développement sécurisé


    Assez pour un badge !

    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]
    Par exemple, les résultats du projet devraient avoir des valeurs sécurisées par défaut (les décisions d'accès devraient être de refuser par défaut et l'installation des projets devrait être sécurisée par défaut). Ils devraient également avoir une médiation complète (tout accès qui pourrait être limité doit être vérifié pour l'autorité et être non contournable). Notez que, dans certains cas, ces principes entrent en conflit, auquel cas un choix doit être fait (par exemple, de nombreux mécanismes peuvent rendre les choses plus complexes, en contravention de « l'économie de mécanisme » / principe KISS).

    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 .

    Assez pour un badge !

    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]
    Les préoccupations concernant le mode CBC en SSH sont discutées dans CERT : vulnérabilité SSH CBC.

    Assez pour un badge !

    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]

    Assez pour un badge !

    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]

    Assez pour un badge !

    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]

    Assez pour un badge !

    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]

    Assez pour un badge !

    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]
    Notez que la vérification incorrecte du certificat TLS est une erreur courante. Pour plus d'informations, voir « Le code le plus dangereux du monde : la validation des certificats SSL dans du logiciel qui ne vient pas d'un navigateur » de Martin Georgiev et al. et « Avez-vous confiance en cette application ? » par Michael Catanzaro.

    Assez pour un badge !

    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


    Pas assez pour un badge.

    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]
    Les résultats du projet incluent à la fois le code source et les produits livrés générés, le cas échéant (par exemple, les exécutables, les paquetages et les conteneurs). Les livrables générés PEUVENT être signés séparément du code source. Ces signatures PEUVENT être mises en œuvre sous forme de tags git signées (utilisant des signatures numériques cryptographiques). Les projets PEUVENT fournir des résultats générés séparément d'outils comme git, mais dans ce cas, les résultats distincts DOIVENT être signés séparément.

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


    À peine suffisant pour un badge.

    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é


    Assez pour un badge !

    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]
    Notez que la comparaison de l'entrée par rapport à une liste de « mauvais formats » (aussi appelée liste noire) n'est normalement pas suffisante, car les attaquants peuvent souvent contourner une liste noire. En particulier, les nombres sont convertis en formats internes puis vérifiés pour s'assurer s'ils se situent entre leur minimum et maximum (inclus), et les chaînes de texte sont vérifiées pour s'assurer qu'elles sont des motifs de texte valides (par exemple, UTF-8 valide, longueur valide, syntaxe valide, etc.). Certaines données peuvent avoir besoin d'être « du tout venant » (par exemple, un téléchargement de fichier), mais celles-ci sont généralement rares.

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


    Assez pour un badge !

    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]
    Les mécanismes de durcissement peuvent inclure des en-têtes HTTP comme Content Security Policy (CSP), des options de compilation pour atténuer les attaques (telles que -fstack-protector) ou des options de compilation pour éliminer les comportements indéfinis. Pour nos besoins, le principe de plus faible privilège n'est pas considéré comme un mécanisme de durcissement (le principe de plus faible privilège est important, mais séparé).

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


    Pas assez pour un badge.

    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]
    Une analyse de fiabilité est « une preuve documentée qui fournit un argumentaire convaincant et correct selon lequel un ensemble spécifié de revendications critiques concernant les propriétés d'un système est adéquatement justifié pour une application donnée dans un environnement donné » (« Software Assurance Using Structured Assurance Case Models », Thomas Rhodes et al, NIST Interagency Report 7608). Les limites de confiance sont des limites où les données ou l'exécution modifient leur niveau de confiance, par exemple, les limites d'un serveur dans une application Web typique. Il est fréquent d'énumérer des principes de conception sécurisés (tels que Saltzer et Schroeer) et des faiblesses de sécurité courantes de l'implémentation (comme le OWASP top 10 ou le CWE/SANS top 25) et de montrer comment chacun est contré. L'analyse de fiabilité de BadgeApp peut être un exemple utile. Ceci est lié à documentation_security, documentation_architecture et implement_secure_design.

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


 Analyse 2/2 ●

  • Analyse statique de code


    Assez pour un badge !

    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]
    Les outils d'analyse statique spécialement conçus pour détecter les vulnérabilités les plus courantes sont plus susceptibles de les détecter. Cela dit, l'utilisation d'outils statiques aidera généralement à trouver des problèmes, nous suggérons donc, sans l'exiger, de le faire pour le badge de niveau « passant ».

    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


    Assez pour un badge !

    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]
    Des exemples de mécanismes pour détecter les problèmes de sécurité de la mémoire comprennent Address Sanitizer (ASAN) (disponible dans GCC et LLVM), Memory Sanitizer et valgrind. D'autres outils potentiellement utilisés incluent thread sanitizer et undefined behavior sanitizer. La généralisation de l'utilisation des assertions fonctionnera également.

    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