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 Passing level criteria. You can also view the Silver or Gold level criteria.

        

 Basics 13/13

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

    What programming language(s) are used to implement the project?
  • Basic project website content


    The project website MUST succinctly describe what the software does (what problem does it solve?). [description_good]

    The project website MUST provide information on how to: obtain, provide feedback (as bug reports or enhancements), and contribute to the software. [interact]

    The information on how to contribute MUST explain the contribution process (e.g., are pull requests used?) (URL required) [contribution]

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

    What license(s) is the project released under?



    The software produced by the project MUST be released as FLOSS. [floss_license]

    The GPL-3.0 license is approved by the Open Source Initiative (OSI).



    It is SUGGESTED that any required license(s) for the software produced by the project be approved by the Open Source Initiative (OSI). [floss_license_osi]

    The GPL-3.0 license is approved by the Open Source Initiative (OSI).



    The project MUST post the license(s) of its results in a standard location in their source repository. (URL required) [license_location]
  • Documentation


    The project MUST provide basic documentation for the software produced by the project. [documentation_basics]

    The SPARK User's Guide is online at http://docs.adacore.com/spark2014-docs/html/ug/

    Sources for it are in the project repository under https://github.com/AdaCore/spark2014/tree/master/docs/ug



    The project MUST provide reference documentation that describes the external interface (both input and output) of the software produced by the project. [documentation_interface]

    The SPARK Reference Manual describing the input SPARK programming language is online at http://docs.adacore.com/spark2014-docs/html/lrm/

    Sources for it are in the project repository under https://github.com/AdaCore/spark2014/tree/master/docs/lrm

    The output format(s) are described in the SPARK User's Guide at http://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_view_gnatprove_output.html


  • Other


    The project sites (website, repository, and download URLs) MUST support HTTPS using TLS. [sites_https]

    The project repo uses GitHub, which supports HTTPS using TLS. The download URL https://www.adacore.com/download supports HTTPS using TLS.



    The project MUST have one or more mechanisms for discussion (including proposed changes and issues) that are searchable, allow messages and topics to be addressed by URL, enable new people to participate in some of the discussions, and do not require client-side installation of proprietary software. [discussion]

    GitHub supports discussions on issues and pull requests. Discussions about SPARK occur on a public mailing list https://lists.adacore.com/mailman/listinfo/spark2014-discuss



    The project SHOULD provide documentation in English and be able to accept bug reports and comments about code in English. [english]

    All documentation is in English, and the project accepts bug reports and comments in English.



    The project MUST be maintained. [maintained]


(Advanced) What other users have additional rights to edit this badge entry? Currently: []



  • Public version-controlled source repository


    The project MUST have a version-controlled source repository that is publicly readable and has a URL. [repo_public]

    Repository on GitHub, which provides public git repositories with URLs.



    The project's source repository MUST track what changes were made, who made the changes, and when the changes were made. [repo_track]

    Repository on GitHub, which uses git. git can track the changes, who made them, and when they were made.



    To enable collaborative review, the project's source repository MUST include interim versions for review between releases; it MUST NOT include only final releases. [repo_interim]

    Interim versions are put on git, not just final versions.



    It is SUGGESTED that common distributed version control software be used (e.g., git) for the project's source repository. [repo_distributed]

    Repository on GitHub, which uses git. git is distributed.


  • Unique version numbering


    The project results MUST have a unique version identifier for each release intended to be used by users. [version_unique]

    Professional releases use a versioning scheme MAJOR.MINOR, where MAJOR is the 2-figures year of the main release, and MINOR is 0 for beta version, 1 for main release, 2 for corrective release. For example: 18.2

    Community releases use a versioning scheme YEAR, where year is the 4-figures year of the release. For example: 2018



    It is SUGGESTED that the Semantic Versioning (SemVer) or Calendar Versioning (CalVer) version numbering format be used for releases. It is SUGGESTED that those who use CalVer include a micro level value. [version_semver]

    We were originally using Semantic Versioning, but we have now adopted across AdaCore a simpler versioning scheme: a date-based scheme YYYY-MM-DD for intermediate daily releases, and year-based YY.num for official releases: YY.0 for beta release, YY.1 for main release, YY.2 for first corrective release, followed by further corrective releases YY.3, YY.4 etc. on branches where corrective releases are produced for multiple years.



    It is SUGGESTED that projects identify each release within their version control system. For example, it is SUGGESTED that those using git identify each release using git tags. [version_tags]

    All releases use git branches. Professional releases use the version number as branch name, for example 18.2, and community releases use gpl-YEAR as branch name, for example gpl-2018.


  • Release notes


    The project MUST provide, in each release, release notes that are a human-readable summary of major changes in that release to help users determine if they should upgrade and what the upgrade impact will be. The release notes MUST NOT be the raw output of a version control log (e.g., the "git log" command results are not release notes). Projects whose results are not intended for reuse in multiple locations (such as the software for a single website or service) AND employ continuous delivery MAY select "N/A". (URL required) [release_notes]

    High-level release notes are published in HTML for each major release since 2017: http://docs.adacore.com/live/wave/spark2014-release-notes/html/spark2014_release_note/index.html

    More detailed release notes are also published in textual format, simply update the final year in the URL for getting the release notes of that particular year: http://docs.adacore.com/R/relnotes/features-spark-18



    The release notes MUST identify every publicly known run-time vulnerability fixed in this release that already had a CVE assignment or similar when the release was created. This criterion may be marked as not applicable (N/A) if users typically cannot practically update the software themselves (e.g., as is often true for kernel updates). This criterion applies only to the project results, not to its dependencies. If there are no release notes or there have been no publicly known vulnerabilities, choose N/A. [release_notes_vulns]

    There are no publicly known vulnerabillities.


  • Bug-reporting process


    The project MUST provide a process for users to submit bug reports (e.g., using an issue tracker or a mailing list). (URL required) [report_process]

    Yes, either GitHub issue tracker or SPARK public mailing list https://lists.adacore.com/mailman/listinfo/spark2014-discuss



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

    Yes, GitHub issue tracker.



    The project MUST acknowledge a majority of bug reports submitted in the last 2-12 months (inclusive); the response need not include a fix. [report_responses]

    Yes, we usually fix quickly all bugs reported publicly.



    The project SHOULD respond to a majority (>50%) of enhancement requests in the last 2-12 months (inclusive). [enhancement_responses]

    Yes, we usually answer quickly to all public enhancement requests, although we do not commit to implementing them all.



    The project MUST have a publicly available archive for reports and responses for later searching. (URL required) [report_archive]

    Yes, via GitHub isue tracker: https://github.com/AdaCore/spark2014/issues and SPARK public mailing list archive: https://lists.adacore.com/pipermail/spark2014-discuss/


  • Vulnerability report process


    The project MUST publish the process for reporting vulnerabilities on the project site. (URL required) [vulnerability_report_process]

    Vulnerabilities should be reported like other issues using GitHub issue tracker: https://github.com/AdaCore/spark2014/issues



    If private vulnerability reports are supported, the project MUST include how to send the information in a way that is kept private. (URL required) [vulnerability_report_private]

    Private vulnerability reports are only supported through a support contract with AdaCore.



    The project's initial response time for any vulnerability report received in the last 6 months MUST be less than or equal to 14 days. [vulnerability_report_response]

    No external reports so far, so this is vacuously true.


  • Working build system


    If the software produced by the project requires building for use, the project MUST provide a working build system that can automatically rebuild the software from source code. [build]

    The README at the root of the GitHub repository has a section on Building SPARK. It explains how to get the sources, points to the top-level Makefile and lists the dependencies.



    It is SUGGESTED that common tools be used for building the software. [build_common_tools]

    Standard Unix Makefiles are used to build the project, as well as standard builders for every sub-project, depending on the programming language. For example we use GPRbuild for Ada code and OCamlbuild for OCaml code.



    The project SHOULD be buildable using only FLOSS tools. [build_floss_tools]

    Repo page https://github.com/AdaCore/spark2014 explains how to build SPARK with a GNAT Community or FSF compiler, including the dependencies on other FLOSS software.


  • Automated test suite


    The project MUST use at least one automated test suite that is publicly released as FLOSS (this test suite may be maintained as a separate FLOSS project). The project MUST clearly show or document how to run the test suite(s) (e.g., via a continuous integration (CI) script or via documentation in files such as BUILD.md, README.md, or CONTRIBUTING.md). [test]

    A test suite SHOULD be invocable in a standard way for that language. [test_invocation]

    Testsuite relies on publicly available AdaCore framework E3, available at https://github.com/AdaCore/e3-core



    It is SUGGESTED that the test suite cover most (or ideally all) the code branches, input fields, and functionality. [test_most]

    Code coverage is measured every night over the complete testsuite (including the public testsuite) using GNATcoverage to measure code coverage. Most of the code is currently covered at statement level, and we aim at increasing coverage with time.



    It is SUGGESTED that the project implement continuous integration (where new or changed code is frequently integrated into a central code repository and automated tests are run on the result). [test_continuous_integration]

    Continuous integration is provided by AdaCore infrastructure.


  • New functionality testing


    The project MUST have a general policy (formal or not) that as major new functionality is added to the software produced by the project, tests of that functionality should be added to an automated test suite. [test_policy]

    All changes go through review and require testing, both for new functionalities and bug fixes.



    The project MUST have evidence that the test_policy for adding tests has been adhered to in the most recent major changes to the software produced by the project. [tests_are_added]

    Tests are added as new functionality is added.



    It is SUGGESTED that this policy on adding tests (see test_policy) be documented in the instructions for change proposals. [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


    The project MUST enable one or more compiler warning flags, a "safe" language mode, or use a separate "linter" tool to look for code quality errors or common simple mistakes, if there is at least one FLOSS tool that can implement this criterion in the selected language. [warnings]

    Code is compiled with warning flags -gnatwae (all GNAT warnings enabled and considered as errors) or -gnatg (all GNAT warnings enabled for work on the compiler and considered as errors). We also run nightly the CodePeer static analyzer on all Ada code and maintain a baseline of zero findings from static analysis.



    The project MUST address warnings. [warnings_fixed]

    Warnings are considered as errors and stop the build, so must always be addressed.



    It is SUGGESTED that projects 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


    The project MUST have at least one primary developer who knows how to design secure software. (See ‘details’ for the exact requirements.) [know_secure_design]

    Project developers are formal verification experts who develop security-related checking tools.



    At least one of the project's primary developers MUST know of common kinds of errors that lead to vulnerabilities in this kind of software, as well as at least one method to counter or mitigate each of them. [know_common_errors]

    Project developers are formal verification experts who develop security-related checking tools.


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

    The software produced by the project MUST use, by default, only cryptographic protocols and algorithms that are publicly published and reviewed by experts (if cryptographic protocols and algorithms are used). [crypto_published]


    If the software produced by the project is an application or library, and its primary purpose is not to implement cryptography, then it SHOULD only call on software specifically designed to implement cryptographic functions; it SHOULD NOT re-implement its own. [crypto_call]


    All functionality in the software produced by the project that depends on cryptography MUST be implementable using FLOSS. [crypto_floss]


    The security mechanisms within the software produced by the project MUST use default keylengths that at least meet the NIST minimum requirements through the year 2030 (as stated in 2012). It MUST be possible to configure the software so that smaller keylengths are completely disabled. [crypto_keylength]


    The default security mechanisms within the software produced by the project MUST NOT depend on broken cryptographic algorithms (e.g., MD4, MD5, single DES, RC4, Dual_EC_DRBG), or use cipher modes that are inappropriate to the context, unless they are necessary to implement an interoperable protocol (where the protocol implemented is the most recent version of that standard broadly supported by the network ecosystem, that ecosystem requires the use of such an algorithm or mode, and that ecosystem does not offer any more secure alternative). The documentation MUST describe any relevant security risks and any known mitigations if these broken algorithms or modes are necessary for an interoperable protocol. [crypto_working]


    The default security mechanisms within the software produced by the project SHOULD 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]


    The security mechanisms within the software produced by the project SHOULD implement perfect forward secrecy for key agreement protocols so a session key derived from a set of long-term keys cannot be compromised if one of the long-term keys is compromised in the future. [crypto_pfs]


    If the software produced by the project causes the storing of 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). See also OWASP Password Storage Cheat Sheet. [crypto_password_storage]


    The security mechanisms within the software produced by the project MUST generate all cryptographic keys and nonces using a cryptographically secure random number generator, and MUST NOT do so using generators that are cryptographically insecure. [crypto_random]

  • Secured delivery against man-in-the-middle (MITM) attacks


    The project MUST use a delivery mechanism that counters MITM attacks. Using https or ssh+scp is acceptable. [delivery_mitm]

    Download page https://www.adacore.com/download uses HTTPS.



    A cryptographic hash (e.g., a sha1sum) MUST NOT be retrieved over http and used without checking for a cryptographic signature. [delivery_unsigned]

    Download page https://www.adacore.com/download uses HTTPS.


  • Publicly known vulnerabilities fixed


    There MUST be no unpatched vulnerabilities of medium or higher severity that have been publicly known for more than 60 days. [vulnerabilities_fixed_60_days]

    No such vulnerabilities at this time.



    Projects SHOULD fix all critical vulnerabilities rapidly after they are reported. [vulnerabilities_critical_fixed]

    No such vulnerabilities at this time.


  • Other security issues


    The public repositories MUST NOT leak a valid private credential (e.g., a working password or private key) that is intended to limit public access. [no_leaked_credentials]

    No valid private credentials are leaked.


  • Static code analysis


    At least one static code analysis tool (beyond compiler warnings and "safe" language modes) MUST be applied to any proposed major production release of the software before its release, if there is at least one FLOSS tool that implements this criterion in the selected language. [static_analysis]

    CodePeer static analysis tool (https://www.adacore.com/codepeer) is applied every day to the current Ada codebase for SPARK toolset, which includes both the gnat2why and gnatprove executables (and a few smaller executables produced in gnatprove project). We maintain a baseline of zero findings by static analysis, therefore any new finding must be addressed by developers in the following days in order to either fix the bug, or justify the finding.

    No static analysis is performed today on the external dependencies Why3 and Alt-Ergo (in OCaml) or Z3 and CVC4 (in C++).



    It is SUGGESTED that at least one of the static analysis tools used for the static_analysis criterion include rules or approaches to look for common vulnerabilities in the analyzed language or environment. [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



    All medium and higher severity exploitable vulnerabilities discovered with static code analysis MUST be fixed in a timely way after they are confirmed. [static_analysis_fixed]

    CodePeer messages are reviewed and addressed by developers in the following days in order to either fix the bug, or justify the finding.



    It is SUGGESTED that static source code analysis occur on every commit or at least daily. [static_analysis_often]

    CodePeer analysis is performed daily.


  • Dynamic code analysis


    It is SUGGESTED that at least one dynamic analysis tool be applied to any proposed major production release of the software before its release. [dynamic_analysis]

    Compilation in debug mode for testing is done with all Ada runtime checks, plus assertions (with -gnata) and validity checks (with -gnatVa and pragma Initialize_Scalars). This is stricter than most dynamic checking tools for other languages.



    It is SUGGESTED that 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) 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.



    It is SUGGESTED that the project use a configuration for at least some dynamic analysis (such as testing or fuzzing) which enables many assertions. In many cases these assertions should not be enabled in production builds. [dynamic_analysis_enable_assertions]

    Compilation in debug mode for testing is done with all Ada runtime checks, plus assertions (with -gnata) and validity checks (with -gnatVa and pragma Initialize_Scalars).



    All medium and higher severity exploitable vulnerabilities discovered with dynamic code analysis MUST be fixed in a timely way after they are confirmed. [dynamic_analysis_fixed]

    SPARK is a verification tool, hence does not expose the user to risks of attacks through vulnerabilities. Still, bugs are fixed quickly when discovered.



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