SPARK 2014

Projects that follow the best practices below can voluntarily self-certify and show that they've achieved an Open Source Security Foundation (OpenSSF) best practices badge.

If this is your project, please show your badge status on your project page! The badge status looks like this: Badge level for project 959 is passing Here is how to embed it:

These are the Silver level criteria. You can also view the Passing or Gold level criteria.

        

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

  • Prerequisites


    Enough for a badge!

    The project MUST achieve a passing level badge. [achieve_passing]

  • Basic project website content


    Enough for a badge!

    The information on how to contribute MUST include the requirements for acceptable contributions (e.g., a reference to any required coding standard). (URL required) [contribution_requirements]

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


  • Project oversight


    Enough for a badge!

    The project SHOULD have a legal mechanism where all developers of non-trivial amounts of project software assert that they are legally authorized to make these contributions. The most common and easily-implemented approach for doing this is by using a Developer Certificate of Origin (DCO), where users add "signed-off-by" in their commits and the project links to the DCO website. However, this MAY be implemented as a Contributor License Agreement (CLA), or other legal mechanism. (URL required) [dco]

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


    Enough for a badge!

    The project MUST clearly define and document its project governance model (the way it makes decisions, including key roles). (URL required) [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


    Enough for a badge!

    The project MUST adopt a code of conduct and post it in a standard location. (URL required) [code_of_conduct]

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


    Enough for a badge!

    The project MUST clearly define and publicly document the key roles in the project and their responsibilities, including any tasks those roles must perform. It MUST be clear who has which role(s), though this might not be documented in the same way. (URL required) [roles_responsibilities]

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


    Enough for a badge!

    The project MUST be able to continue with minimal interruption if any one person dies, is incapacitated, or is otherwise unable or unwilling to continue support of the project. In particular, the project MUST be able to create and close issues, accept proposed changes, and release versions of software, within a week of confirmation of the loss of support from any one individual. This MAY be done by ensuring someone else has any necessary keys, passwords, and legal rights to continue the project. Individuals who run a FLOSS project MAY do this by providing keys in a lockbox and a will providing any needed legal rights (e.g., for DNS names). (URL required) [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


    Enough for a badge!

    The project SHOULD have a "bus factor" of 2 or more. (URL required) [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


    Enough for a badge!

    The project MUST have a documented roadmap that describes what the project intends to do and not do for at least the next year. (URL required) [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)


    Enough for a badge!

    The project MUST include documentation of the architecture (aka high-level design) of the software produced by the project. If the project does not produce software, select "not applicable" (N/A). (URL required) [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


    Enough for a badge!

    The project MUST document what the user can and cannot expect in terms of security from the software produced by the project (its "security requirements"). (URL required) [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)


    Enough for a badge!

    The project MUST provide a "quick start" guide for new users to help them quickly do something with the software. (URL required) [documentation_quick_start]

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


    Enough for a badge!

    The project MUST make an effort to keep the documentation consistent with the current version of the project results (including software produced by the project). Any known documentation defects making it inconsistent MUST be fixed. If the documentation is generally current, but erroneously includes some older information that is no longer true, just treat that as a defect, then track and fix as usual. [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


    Enough for a badge!

    The project repository front page and/or website MUST identify and hyperlink to any achievements, including this best practices badge, within 48 hours of public recognition that the achievement has been attained. (URL required) [documentation_achievements]

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


  • Accessibility and internationalization


    Enough for a badge!

    The project (both project sites and project results) SHOULD follow accessibility best practices so that persons with disabilities can still participate in the project and use the project results where it is reasonable to do so. [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).


    Barely enough for a badge.

    The software produced by the project SHOULD be internationalized to enable easy localization for the target audience's culture, region, or language. If internationalization (i18n) does not apply (e.g., the software doesn't generate text intended for end-users and doesn't sort human-readable text), select "not 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


  • Other


    Enough for a badge!

    If the project sites (website, repository, and download URLs) store passwords for authentication of external users, the passwords MUST be stored as iterated hashes with a per-user salt by using a key stretching (iterated) algorithm (e.g., Argon2id, Bcrypt, Scrypt, or PBKDF2). If the project sites do not store passwords for this purpose, select "not applicable" (N/A). [sites_password_security]

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


  • Previous versions


    Enough for a badge!

    The project MUST maintain the most often used older versions of the product or provide an upgrade path to newer versions. If the upgrade path is difficult, the project MUST document how to perform the upgrade (e.g., the interfaces that have changed and detailed suggested steps to help upgrade). [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.


  • Bug-reporting process


    Enough for a badge!

    The project MUST use an issue tracker for tracking individual issues. [report_tracker]

    Yes, GitHub issue tracker.


  • Vulnerability report process


    Enough for a badge!

    The project MUST give credit to the reporter(s) of all vulnerability reports resolved in the last 12 months, except for the reporter(s) who request anonymity. If there have been no vulnerabilities resolved in the last 12 months, select "not applicable" (N/A). (URL required) [vulnerability_report_credit]

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


    Enough for a badge!

    The project MUST have a documented process for responding to vulnerability reports. (URL required) [vulnerability_response_process]

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


  • Coding standards


    Enough for a badge!

    The project MUST identify the specific coding style guides for the primary languages it uses, and require that contributions generally comply with it. (URL required) [coding_standards]

    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)


    Enough for a badge!

    The project MUST automatically enforce its selected coding style(s) if there is at least one FLOSS tool that can do so in the selected language(s). [coding_standards_enforced]

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


  • Working build system


    Enough for a badge!

    Build systems for native binaries MUST honor the relevant compiler and linker (environment) variables passed in to them (e.g., CC, CFLAGS, CXX, CXXFLAGS, and LDFLAGS) and pass them to compiler and linker invocations. A build system MAY extend them with additional flags; it MUST NOT simply replace provided values with its own. If no native binaries are being generated, select "not applicable" (N/A). [build_standard_variables]

    The Makefiles do use environment variables which can be overwritten.


    Enough for a badge!

    The build and installation system SHOULD preserve debugging information if they are requested in the relevant flags (e.g., "install -s" is not used). If there is no build or installation system (e.g., typical JavaScript libraries), select "not 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).


    Enough for a badge!

    The build system for the software produced by the project MUST NOT recursively build subdirectories if there are cross-dependencies in the subdirectories. If there is no build or installation system (e.g., typical JavaScript libraries), select "not 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.


    Enough for a badge!

    The project MUST be able to repeat the process of generating information from source files and get exactly the same bit-for-bit result. If no building occurs (e.g., scripting languages where the source code is used directly instead of being compiled), select "not applicable" (N/A). [build_repeatable]

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


  • Installation system


    Enough for a badge!

    The project MUST provide a way to easily install and uninstall the software produced by the project using a commonly-used convention. [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.


    Enough for a badge!

    The installation system for end-users MUST honor standard conventions for selecting the location where built artifacts are written to at installation time. For example, if it installs files on a POSIX system it MUST honor the DESTDIR environment variable. If there is no installation system or no standard convention, select "not applicable" (N/A). [installation_standard_variables]

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


    Enough for a badge!

    The project MUST provide a way for potential developers to quickly install all the project results and support environment necessary to make changes, including the tests and test environment. This MUST be performed with a commonly-used convention. [installation_development_quick]

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


  • Externally-maintained components


    Not enough for a badge.

    The project MUST list external dependencies in a computer-processable way. (URL required) [external_dependencies]

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


    Enough for a badge!

    Projects MUST monitor or periodically check their external dependencies (including convenience copies) to detect known vulnerabilities, and fix exploitable vulnerabilities or verify them as unexploitable. [dependency_monitoring]

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


    Enough for a badge!

    The project MUST either:
    1. make it easy to identify and update reused externally-maintained components; or
    2. use the standard components provided by the system or programming language.
    Then, if a vulnerability is found in a reused component, it will be easy to update that component. [updateable_reused_components]

    The components used by GNATprove should be separately built.


    Enough for a badge!

    The project SHOULD avoid using deprecated or obsolete functions and APIs where FLOSS alternatives are available in the set of technology it uses (its "technology stack") and to a supermajority of the users the project supports (so that users have ready access to the alternative). [interfaces_current]

    This is met to the best of our knowledge.


  • Automated test suite


    Enough for a badge!

    An automated test suite MUST be applied on each check-in to a shared repository for at least one branch. This test suite MUST produce a report on test success or failure. [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.


    Enough for a badge!

    The project MUST add regression tests to an automated test suite for at least 50% of the bugs fixed within the last six months. [regression_tests_added50]

    A test is added for all bugs fixed.


    Enough for a badge!

    The project MUST have FLOSS automated test suite(s) that provide at least 80% statement coverage if there is at least one FLOSS tool that can measure this criterion in the selected language. [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.


  • New functionality testing


    Enough for a badge!

    The project MUST have a formal written policy that as major new functionality is added, tests for the new functionality MUST be added to an automated test suite. [test_policy_mandated]

    This is part of quality assurance at AdaCore.


    Enough for a badge!

    The project MUST include, in its documented instructions for change proposals, the policy that tests are to be added for major new functionality. [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.


  • Warning flags


    Enough for a badge!

    Projects MUST be maximally strict with warnings in the software produced by the project, where practical. [warnings_strict]

    Warnings are considered as errors and stop the build.


  • Secure development knowledge


    Enough for a badge!

    The project MUST implement secure design principles (from "know_secure_design"), where applicable. If the project is not producing software, select "not applicable" (N/A). [implement_secure_design]

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


  • Use basic good cryptographic practices

    Note that some software does not need to use cryptographic mechanisms. If your project produces software that (1) includes, activates, or enables encryption functionality, and (2) might be released from the United States (US) to outside the US or to a non-US-citizen, you may be legally required to take a few extra steps. Typically this just involves sending an email. For more information, see the encryption section of Understanding Open Source Technology & US Export Controls.

    Enough for a badge!

    The default security mechanisms within the software produced by the project MUST NOT depend on cryptographic algorithms or modes with known serious weaknesses (e.g., the SHA-1 cryptographic hash algorithm or the CBC mode in SSH). [crypto_weaknesses]

    Enough for a badge!

    The project SHOULD support multiple cryptographic algorithms, so users can quickly switch if one is broken. Common symmetric key algorithms include AES, Twofish, and Serpent. Common cryptographic hash algorithm alternatives include SHA-2 (including SHA-224, SHA-256, SHA-384 AND SHA-512) and SHA-3. [crypto_algorithm_agility]

    Enough for a badge!

    The project MUST support storing authentication credentials (such as passwords and dynamic tokens) and private cryptographic keys in files that are separate from other information (such as configuration files, databases, and logs), and permit users to update and replace them without code recompilation. If the project never processes authentication credentials and private cryptographic keys, select "not applicable" (N/A). [crypto_credential_agility]

    Enough for a badge!

    The software produced by the project SHOULD support secure protocols for all of its network communications, such as SSHv2 or later, TLS1.2 or later (HTTPS), IPsec, SFTP, and SNMPv3. Insecure protocols such as FTP, HTTP, telnet, SSLv3 or earlier, and SSHv1 SHOULD be disabled by default, and only enabled if the user specifically configures it. If the software produced by the project does not support network communications, select "not applicable" (N/A). [crypto_used_network]

    Enough for a badge!

    The software produced by the project SHOULD, if it supports or uses TLS, support at least TLS version 1.2. Note that the predecessor of TLS was called SSL. If the software does not use TLS, select "not applicable" (N/A). [crypto_tls12]

    Enough for a badge!

    The software produced by the project MUST, if it supports TLS, perform TLS certificate verification by default when using TLS, including on subresources. If the software does not use TLS, select "not applicable" (N/A). [crypto_certificate_verification]

    Enough for a badge!

    The software produced by the project MUST, if it supports TLS, perform certificate verification before sending HTTP headers with private information (such as secure cookies). If the software does not use TLS, select "not applicable" (N/A). [crypto_verification_private]

  • Secure release


    Not enough for a badge.

    The project MUST cryptographically sign releases of the project results intended for widespread use, and there MUST be a documented process explaining to users how they can obtain the public signing keys and verify the signature(s). The private key for these signature(s) MUST NOT be on site(s) used to directly distribute the software to the public. If releases are not intended for widespread use, select "not applicable" (N/A). [signed_releases]

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


    Barely enough for a badge.

    It is SUGGESTED that in the version control system, each important version tag (a tag that is part of a major release, minor release, or fixes publicly noted vulnerabilities) be cryptographically signed and verifiable as described in signed_releases. [version_tags_signed]

  • Other security issues


    Enough for a badge!

    The project results MUST check all inputs from potentially untrusted sources to ensure they are valid (an *allowlist*), and reject invalid inputs, if there are any restrictions on the data at all. [input_validation]

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


    Enough for a badge!

    Hardening mechanisms SHOULD be used in the software produced by the project so that software defects are less likely to result in security vulnerabilities. [hardening]

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


    Not enough for a badge.

    The project MUST provide an assurance case that justifies why its security requirements are met. The assurance case MUST include: a description of the threat model, clear identification of trust boundaries, an argument that secure design principles have been applied, and an argument that common implementation security weaknesses have been countered. (URL required) [assurance_case]

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


  • Static code analysis


    Enough for a badge!

    The project MUST use at least one static analysis tool with rules or approaches to look for common vulnerabilities in the analyzed language or environment, if there is at least one FLOSS tool that can implement this criterion in the selected language. [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


  • Dynamic code analysis


    Enough for a badge!

    If the software produced by the project includes software written using a memory-unsafe language (e.g., C or C++), then at least one dynamic tool (e.g., a fuzzer or web application scanner) MUST be routinely used in combination with a mechanism to detect memory safety problems such as buffer overwrites. If the project does not produce software written in a memory-unsafe language, choose "not applicable" (N/A). [dynamic_analysis_unsafe]

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



This data is available under the Creative Commons Attribution version 3.0 or later license (CC-BY-3.0+). All are free to share and adapt the data, but must give appropriate credit. Please credit Yannick Moy and the OpenSSF Best Practices badge contributors.

Project badge entry owned by: Yannick Moy.
Entry created on 2017-05-11 04:54:51 UTC, last updated on 2021-05-11 07:46:17 UTC. Last achieved passing badge on 2018-07-02 09:39:05 UTC.

Back