SPARK 2014

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

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

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

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

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

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.

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.

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

There are no publicly known vulnerabillities.

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

Yes, GitHub issue tracker.

Yes, we usually fix quickly all bugs reported publicly.

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

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

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

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

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

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.

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.

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.

https://github.com/AdaCore/spark2014/tree/master/testsuite/gnatprove

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

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.

Continuous integration is provided by AdaCore infrastructure.

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

Tests are added as new functionality is 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.

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.

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

Warnings are considered as errors and stop the build.

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

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

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

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

No such vulnerabilities at this time.

No such vulnerabilities at this time.

No valid private credentials are leaked.

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

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

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

CodePeer analysis is performed daily.

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.

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

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

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