SPARK 2014

遵循以下最佳实践的项目将能够自愿的自我认证，并显示他们已经实现了核心基础设施计划（OpenSSF）徽章。

没有一套可以保证软件永远不会有缺陷或漏洞的做法；如果规范或假设是错误的，即使合适的方法也可能失败。也没有哪些做法可以保证一个项目能够维持健康和运作良好的开发者社区。但是，遵循最佳做法可以帮助改善项目的成果。例如，一些做法可以在发布之前进行多人评估，这可以帮助您找到其他难以找到的技术漏洞，并帮助建立信任，并希望不同公司的开发人员之间进行重复的交互。要获得徽章，必须满足所有“必须”和“禁止”的条款，满足所有“应该”条款或有合适的理由，和所有“建议”条款必须满足或未满足（至少希望考虑）。欢迎通过 GitHub网站创建问题或提出请求进行反馈。另外还有一个一般讨论邮件列表。

如果这是您的项目，请在您的项目页面上显示您的徽章状态！徽章状态如下所示： 项目959的徽章级别为passing 这里是如何嵌入它：
您可以通过将其嵌入在您的Markdown文件中：
[![OpenSSF Best Practices](https://www.bestpractices.dev/projects/959/badge)](https://www.bestpractices.dev/projects/959)
或将其嵌入到HTML中来显示您的徽章状态：
<a href="https://www.bestpractices.dev/projects/959"><img src="https://www.bestpractices.dev/projects/959/badge"></a>


这些是白银级别条款。您还可以查看通过或黄金级别条款。

        

 基本 17/17 ●

  • 识别

    请注意，其他项目可能使用相同的名称。

    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.

  • 先决条件


    足够获得徽章！

    项目必须拥有通过徽章。 [achieve_passing]

  • 基本项目网站内容


    足够获得徽章！

    关于如何贡献的信息必须包括对可接受的贡献的要求（例如，引用任何所需的编码标准）。 (需要网址) [contribution_requirements]

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


  • 项目监督


    足够获得徽章！

    该项目应该有一个合法机制，所有对项目软件做出显著贡献的开发人员都声明他们有合法授权作出这些贡献。最常用且易于实施的方法是使用开发者原产地证书（DCO），用户可以在其提交中添加“signed-off-by”，另外，项目链接到DCO网站。本条款也可以使用贡献者许可协议（CLA）或其他法律机制实现。 (需要网址) [dco]
    DCO是推荐的机制，因为它易于实现，在源代码中进行跟踪，并且git使用“commit -s”直接支持“签名”功能。更有效的是，项目文件解释了该项目的“签名”手段。 CLA是一项法律协议，用于定义知识产权许可给组织或项目的条款。捐助者转让协议（CAA）是将知识产权权利转让给另一方的法律协议；项目不必具备CAA，因为CAA增加了潜在贡献者不愿贡献的风险，特别是如果接收者是一个营利性组织。 Apache Software Foundation CLA（个人贡献者许可证和公司CLA）是CLA的示例，用于确定项目的这些CLA的风险对项目的影响小于其获益。

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


    足够获得徽章！

    该项目必须明确定义和记录其项目治理模式（决策方式，包括关键角色）。 (需要网址) [governance]
    需要有一些成熟的书面方式来作出决定和解决争端。在小项目中，这可能就像“项目拥有者和负责人做所有最终决定”一样简单。有各种治理模式，包括仁慈的独裁者和正式的精英统治；有关详细信息，请参阅治理模式。集中式（例如，单一维护者）和分散式（例如，组维护者）方法都已经在项目中成功使用。治理信息不需要记录创建项目分支的可能性，因为对于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


    足够获得徽章！

    该项目必须采取行为守则，并将其发布在标准的位置。 (需要网址) [code_of_conduct]
    项目可能能够提高社区的文明程度，并通过采取行为守则来规定对可接受的行为的期望。这可以帮助在发生问题之前避免问题，并使项目成为更加欢迎的地方来鼓励贡献。这应该只关注项目社区/工作场所的行为。行为规范的示例是贡献者约定行为准则和Linux内核代码冲突。

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


    足够获得徽章！

    该项目必须明确定义和公开记录项目中的关键角色及其职责，包括这些角色必须执行的任务。必须清楚指出谁是什么角色，尽管这可能没有以相同的方式记录下来。 (需要网址) [roles_responsibilities]
    治理和角色和职责的文档可以在一个地方。

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


    足够获得徽章！

    如果任何一个开发者丧失工作能力或丧生，该项目必须能够继续保持最小的中断。特别是，在确认个人无行为能力或死亡的一周内，项目必须能够创建和关闭问题，接受提议的更改和发布软件版本。这可以通过确保其他人有任何必要的密钥，密码和合法权利来继续该项目。运行FLOSS项目的个人可以通过在锁箱中提供密钥，并提供任何所需的合法权利（例如DNS名称）来实现。 (需要网址) [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


    足够获得徽章！

    项目必须具有2个或更多的“公交车因子”。 (需要网址) [bus_factor]
    “公交车系数”（又名“卡车因子”）是指最少数量的项目成员，如果突然离开项目（“被公交车撞了”），项目会由于缺乏具备知识的或有能力的人员而暂停。 卡车因子 工具可以对GitHub上的项目进行估计。有关详细信息，请参阅Cosentino等人的评估Git存储库的卡车因子。

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


    足够获得徽章！

    该项目必须包括项目生成的软件的架构（也称为高级别设计）的文档。如果项目不产生软件，请选择“不适用”（N/A）。 (需要网址) [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


    足够获得徽章！

    该项目必须书面记录用户从项目生成的软件的安全性上可以获得和不能指望的内容（其“安全需求”）。 (需要网址) [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)


    足够获得徽章！

    该项目必须为新用户提供“快速启动”指南，以帮助他们快速使用该软件。 (需要网址) [documentation_quick_start]
    这个想法是向用户展示如何入门，使软件完全可以做事情。这对于潜在用户是至关重要的。

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


    足够获得徽章！

    项目必须努力使文档与当前版本的项目结果（包括项目生成的软件）保持一致。任何已知的文档缺陷使其不一致必须修正。如果文档基本是最新的，但是错误地包括一些不再是真实的旧信息，那么将其视为缺陷，然后像往常一样进行跟踪和修复。 [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


    足够获得徽章！

    项目存储代码库首页和/或网站必须在获得成就的48小时内标识并超链接任何成就，包括此最佳实践徽章。 (需要网址) [documentation_achievements]
    一个成就是项目致力于满足的任何外部条款，包括徽章。该信息不需要在项目网站首页上。使用GitHub的项目可以通过将其添加到README文件中，将成果放在存储代码库首页。

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


  • 无障碍和国际化


    足够获得徽章！

    该项目（项目网站和项目成果）都应遵循无障碍最佳做法，使残疾人仍然可以参与项目，并在合理的情况下使用项目成果。 [accessibility_best_practices]
    对于Web应用程序，请参阅 Web 内容无障碍指导 (WCAG 2.0，英文) 以及其支持文档 理解 WCAG 2.0（英文）；或者 W3C 无障碍信息（英文）. 图形界面（GUI）应用考虑使用环境特定的无障碍指导（例如 Gnome, KDE, XFCE, Android, iOS, Mac, 以及 Windows). 一些TUI应用 (例如，`ncurses` 程序) 可以做一些特定的工作，增强可访问性（例如，`alpine` 的 `force-arrow-cursor` 设置）。多数命令行应用没有特别的无障碍设置。本条款经常是不涉及（N/A），例如，对于组件库。以下是一些要采取的行动或需要考虑的问题的例子：
    • 提供非文字内容的文字替代，以便于转换为其他需要的格式，如大字体、盲文、语音、符号或者简单文字（ WCAG 2.0 指导 1.1 （英文）)
    • 颜色不被用作传达信息，指示动作，提示响应或区分视觉元素的唯一视觉方式。 ( WCAG 2.0 指导 1.4.1（英文）)
    • 文本和文字图像的视觉呈现对比度至少为4.5：1，除了大文本，次要文本和标识符之外。 ( WCAG 2.0 指导 1.4.3（英文）)
    • 使用键盘可访问所有功能 (WCAG 指导 2.1)
    • 图形界面应用（GUI）或者Web应用在目标平台上，应该至少使用一种屏幕阅读器测试（例如，NVDA；Jaws；Windows上的WindowEyes；Mac & iOS上的VoiceOver；Linux/BSD上的Orca；Android上的TalkBack）。TUI程序可以减少过度渲染以防止屏幕阅读器的冗余读取。

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


    勉强够获得徽章。

    该项目产生的软件应该被国际化，以便为目标受众的文化，地区或语言进行简单的本地化。如果国际化（i18n）不适用（例如，该软件不会生成针对最终用户的文本，并且不排序可读文本），请选择“不适用”（N/A）。 [internationalization]
    本地化“是指适应产品，应用或文档内容以满足特定目标市场（语言环境）的语言，文化和其他要求。国际化是“设计和开发产品，应用或文档内容，使不同文化，地区或语言的目标受众更容易本地化”。 （请参阅 W3C的“本地化与国际化”）。软件只需通过国际化即可达到此标准。不需要另一种特定语言的本地化，因为一旦软件已被国际化，其他人就可以从事本地化。

    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


  • 其他


    足够获得徽章！

    如果项目站点（网站，存储库和下载URL）存储用于外部用户认证的密码，则必须使用密钥拉伸（迭代）算法将密码存储为具有每用户盐值的迭代散列（例如，PBKDF2，Bcrypt或Scrypt）。如果项目站点不存储密码，请选择“不适用”（N/A）。 [sites_password_security]
    请注意，使用 GitHub 符合此条款。此条款仅适用于用于外部用户认证到项目站点的密码。如果项目站点必须登录到其他站点，则可能需要为此目的存储密码（因为使用像Bcrypt这样的算法会使这些密码无效）。本条款将 crypto_password_storage 条款应用于项目站点，类似于sites_https条款。

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


 变更控制 1/1 ●

  • 之前的版本


    足够获得徽章！

    该项目必须维护最常用的旧版本的产品或提供较新版本的升级路径。如果升级路径很困难，项目必须记录如何执行升级（例如，给出更改的接口描述和详细的建议步骤以帮助升级）。 [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.


 报告 3/3 ●

  • 错误报告流程


    足够获得徽章！

    项目必须使用问题跟踪器来跟踪每个问题。 [report_tracker]

    Yes, GitHub issue tracker.


  • 漏洞报告流程


    足够获得徽章！

    除了要求匿名的报告者外，该项目必须对过去12个月内解决的所有漏洞报告的报告者表示感谢。如果过去12个月没有修复漏洞，请选择“不适用”（N/A）。 (需要网址) [vulnerability_report_credit]

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


    足够获得徽章！

    该项目必须有一个书面的流程来响应漏洞报告。 (需要网址) [vulnerability_response_process]
    这与security_report_process有很强的相关性，它需要有一个书面的流程来报告漏洞。它还涉及到spam_report_response，它需要在一定时间内响应漏洞报告。

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


 质量 18/19 ●

  • 编码标准


    足够获得徽章！

    该项目必须确定其使用的主要语言的具体编码风格指南，并要求贡献一般情况下符合此要求。 (需要网址) [coding_standards]
    在大多数情况下，这是通过参考一些现有的风格指南来完成的，可能列出差异。这些风格指南可以包括提高可读性的方法和减少缺陷可能性（包括漏洞）的方法。许多编程语言有一个或多个广泛使用的风格指南。样式指南的示例包括 Google风格指南（英文）和 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)


    足够获得徽章！

    如果至少有一个FLOSS工具可以应用于所选择的语言，项目必须自动执行其选定的编码风格。 [coding_standards_enforced]
    这可以使用静态分析工具和/或通过代码重新格式化强制代码实现。在许多情况下，工具配置包含在项目的存储库中（因为不同的项目可能会选择不同的配置）。项目可以允许风格例外（通常会）；在发生例外的情况下（应该很少），它们必须在其位置的代码中记录在案，以便可以对这些例外进行检视，并使工具能够在将来自动处理它们。这些工具的例子包括ESLint（JavaScript）和Rubocop（Ruby）。

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


  • 可工作的构建系统


    足够获得徽章！

    本地二进制文件的构建系统必须遵守传递给它们的相关编译器和链接器（环境）变量（例如CC，CFLAGS，CXX，CXXFLAGS和LDFLAGS），并将它们传递给编译器和链接器。构建系统可以使用附加标志来扩展它们，但不能简单地用自己的替换提供的值。如果没有生成本地二进制文件，请选择“不适用”（N/A）。 [build_standard_variables]
    应该很容易启用特殊的构建功能，如地址消毒剂（Address Sanitizer，ASAN），或符合发布加固最佳实践（例如，通过轻松打开编译器标志来实现）。

    The Makefiles do use environment variables which can be overwritten.


    足够获得徽章！

    构建和安装系统在在相关标志中要求时，应该保留调试信息（例如，“install -s”未被使用）。如果没有构建或安装系统（例如典型的JavaScript库），请选择“不适用”（N/A）。 [build_preserve_debug]
    例如，如果使用这些语言，则应该设置CFLAGS（C）或CXXFLAGS（C ++）创建相关的调试信息，并且在安装过程中不应该剥离它们。支持和分析时，需要调试信息，也可用于测量编译二进制文件中加固特性的存在。

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


    足够获得徽章！

    如果子目录中存在交叉依赖关系，则由项目生成的软件的构建系统必须不能递归地构建子目录。如果没有构建或安装系统（例如典型的JavaScript库），请选择“不适用”（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.


    足够获得徽章！

    该项目必须能够重复从源代码文件生成的过程，并获得完全相同的比特位结果。如果没有发生构建（例如，直接使用源代码而不是编译使用的脚本语言），请选择“不适用”（N/A）。 [build_repeatable]
    GCC和clang用户可能会发现-frandom-seed选项有用；在某些情况下，这可以通过强制某种排序来解决。更多建议可以在可重复构建（英文）站点找到。

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


  • 安装系统


    足够获得徽章！

    该项目必须提供一种使用常用惯例轻松安装和卸载由项目生成的软件的方法。 [installation_common]
    示例包括使用软件包管理器（在系统或语言级别），“make install/uninstall”（支持DESTDIR），标准格式的容器或标准格式的虚拟机映像。安装和卸载过程（例如，打包）可以由第三方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.


    足够获得徽章！

    最终用户的安装系统必须遵守用于在安装时选择构建工件写入位置的标准约定。例如，如果在POSIX系统上安装文件，它必须遵守DESTDIR环境变量。如果没有安装系统或没有标准惯例，请选择“不适用”（N/A）。 [installation_standard_variables]

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


    足够获得徽章！

    该项目必须为潜在开发人员提供一种快速安装所有项目成果和支持环境所必需的环境，包括测试套件和测试环境。必须通过常规惯例执行。 [installation_development_quick]
    可以使用生成的容器和/或安装脚本来实现。外部依赖关系一般通过调用系统和/或语言包管理器（根据 external_dependencies 条款）进行安装。

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


  • 外部维护的组件


    不足以获得徽章。

    项目必须以计算机可处理的方式列出外部依赖关系。 (需要网址) [external_dependencies]
    通常这是使用包管理器和/或构建系统的约定完成的。请注意，这有助于实施 installation_development_quick 。

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


    足够获得徽章！

    项目必须监视或定期检查其外部依赖（包括便利副本）以检测已知的漏洞，并修复可利用的漏洞或将其验证为不可利用的漏洞。 [dependency_monitoring]
    这可以使用源分析器/依赖项检查工具/软件组成分析工具（例如OWASP的Dependency-Check ， Sonatype的Nexus Auditor ， Synopsys的Black Duck软件组成分析和Bundler-audit（针对Ruby））来完成。一些程序包管理器包括执行此操作的机制。如果无法利用组件的漏洞，这是可以接受的，但是这种分析是困难的，有时简单地更新或修复零件就更容易。

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


    足够获得徽章！

    该项目必须满足下述情况之一：
    1. 可以轻松识别和更新重用的外部维护组件; 或
    2. 使用系统或编程语言提供的标准组件。
    这样，如果在重用的组件中发现了一个漏洞，将容易更新该组件。 [updateable_reused_components]
    符合这一条款的典型方法是使用系统和编程语言的包管理系统。许多FLOSS程序与“便利库”一起分发，这些库是标准库的本地副本（可能是分支）。一般没问题。但是，如果程序*必须*使用这些本地（分支）副本，则“标准”库的安全更新将使这些附加副本仍然易受攻击。这对于基于云的系统尤其是一个问题；如果云提供商更新他们的“标准”库，但程序不会使用它们，那么这些更新实际上不会有帮助。参见，例如，“Chromium：为什么它不在Fedora中作为适当的包”（Tom Callaway）。

    The components used by GNATprove should be separately built.


    足够获得徽章！

    该项目应避免使用已弃用或过时的功能和API，如果FLOSS替代品在其使用的技术集合（“技术堆栈”）中以及项目支持的大多数用户中可用（以便用户可以随时访问该替代品）。 [interfaces_current]

    This is met to the best of our knowledge.


  • 自动测试套件


    足够获得徽章！

    必须将自动测试套件应用于至少一个分支的共享代码库的每次签入。该测试套件必须生成关于测试成功或失败的报告。 [automated_integration_testing]
    这个要求可以被视为test_continuous_integration的一个子集，但是仅仅是测试，而不需要持续集成。

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


    足够获得徽章！

    该项目必须为过去六个月内修复的至少50％的错误，在自动化测试套件中添加回归测试。 [regression_tests_added50]

    A test is added for all bugs fixed.


    足够获得徽章！

    如果有至少一个FLOSS工具可以以所选语言度量此条款，该项目的FLOSS自动测试套件必须具有至少80％语句覆盖率。 [test_statement_coverage80]
    许多FLOSS工具可用于度量测试覆盖范围，包括gcov / lcov，Blanket.js，Istanbul和JCov。请注意，满足这个条款并不能保证测试套件是完备的，而不满足该条款则意味着测试套件很差。

    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.


  • 新功能测试


    足够获得徽章！

    该项目必须具有正式的书面策略，一旦添加了主要的新功能，新功能的测试必须被添加到自动测试套件中。 [test_policy_mandated]

    This is part of quality assurance at AdaCore.


    足够获得徽章！

    该项目必须在其关于变更建议的书面指导中包括要为主要新功能添加测试的策略。 [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.


  • 警告标志


    足够获得徽章！

    在实际允许时，项目必须最大限度地严格修复项目生成的软件中的警告。 [warnings_strict]
    某些项目无法有效启用某些警告。需要证明的是，项目正在努力的启用警告标志，以便早期发现错误。

    Warnings are considered as errors and stop the build.


 安全 11/13 ●

  • 安全开发知识


    足够获得徽章！

    该项目必须实施安全设计原则（来自“know_secure_design”）（如适用）。如果项目不生产软件，请选择“不适用”（N/A）。 [implement_secure_design]
    例如，项目结果应该具有故障安全默认值（默认情况下，访问决策应该拒绝，默认情况下项目的安装应该是安全的），也应该有完全的仲裁（每一个可能被限制的访问权限必须被检查，不可绕过）。请注意，在某些情况下，原则会发生冲突，在这种情况下必须做出选择（例如，许多机制使事情更复杂，违反“机制经济”/“保持最简化”的原则）。

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


  • 使用基础的良好加密实践

    请注意，某些软件不需要使用加密机制。

    足够获得徽章！

    由项目产生的软件中的默认安全机制不得取决于具有已知严重弱点（例如，SHA-1密码散列算法或SSH中的CBC模式）的加密算法或模式。 [crypto_weaknesses]
    在 CERT：SSH CBC漏洞中讨论了SSH中CBC模式的问题。

    足够获得徽章！

    该项目应该支持多种加密算法，如果一个被破解，用户可以快速切换。普通的对称密钥算法包括AES，Twofish和Serpent。通用密码散列算法的选择包括SHA-2（包括SHA-224，SHA-256，SHA-384和SHA-512）和SHA-3。 [crypto_algorithm_agility]

    足够获得徽章！

    该项目必须支持在与其他信息（如配置文件，数据库和日志）分离的文件中存储身份验证凭据（如密码和动态令牌）以及私有加密密钥，并允许用户更新和替换它们，而无需重新编译代码。如果项目从不处理身份验证凭据和私有加密密钥，请选择“不适用”（N/A）。 [crypto_credential_agility]

    足够获得徽章！

    该项目产生的软件应该支持所有网络通信的安全协议，如SSHv2或更高版本，TLS1.2或更高版本（HTTPS），IPsec，SFTP和SNMPv3。默认情况下，FTP，HTTP，Telnet，SSLv3或更早版本和SSHv1等不安全协议将被禁用，只有在用户专门配置时才启用。如果项目生成的软件不支持网络通信，请选择“不适用”（N/A）。 [crypto_used_network]

    足够获得徽章！

    项目生成的软件（如果支持或使用TLS）应该至少支持TLS版本1.2。请注意，TLS的前身称为SSL。如果软件不使用TLS，请选择“不适用”（N/A）。 [crypto_tls12]

    足够获得徽章！

    由项目生成的软件必须，如果它支持TLS，则在使用TLS（包括子资源）时默认执行TLS证书验证。如果软件不使用TLS，请选择“不适用”（N / A）。 [crypto_certificate_verification]
    请注意，不正确的TLS证书验证是一个常见的错误。有关详细信息，请参阅“世界上最危险的代码：在非浏览器软件中验证SSL证书“，Martin Georgiev等人和 “你信任这个应用程序吗？”作者Michael Catanzaro

    足够获得徽章！

    项目生成的软件（如果支持TLS）必须在发送具有私有信息（如安全Cookie）的HTTP头之前执行证书验证。如果软件不使用TLS，请选择“不适用”（N/A）。 [crypto_verification_private]

  • 安全发布


    不足以获得徽章。

    该项目必须加密签名旨在广泛使用的项目结果的发布，并且必须有一个书面流程，向用户解释如何获取公共签名密钥并验证签名。这些签名的私钥不得在项目网站上直接向公众发布。如果发行版本不适用于广泛使用，请选择“不适用”（N/A）。 [signed_releases]
    项目结果包括源代码和适用的任何生成的可交付成果（例如，可执行文件，包和容器）。生成的交付项可以单独签名源代码。可以用签名的git标签实现（使用加密数字签名）。项目可以从git类似的工具分别提供生成的结果，但在这些情况下，单独的结果必须单独签署。

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


    勉强够获得徽章。

    建议在版本控制系统中，每个重要版本标签（作为主要版本的一部分的标签，次要版本或修复公开提到的漏洞）都按照signed_releases中的要求进行加密签名，并可验证。 [version_tags_signed]

  • 其他安全问题


    足够获得徽章！

    项目结果必须检查来自潜在不受信任来源的所有输入，以确保它们有效（ *白名单*），如果对数据有限制，则拒绝无效输入。 [input_validation]
    请注意，将输入与“不良格式”（*黑名单*）的列表进行比较通常是不够的，因为攻击者通常可以绕过黑名单。例如，数字被转换成内部格式，然后检查它们是否在最小和最大（包括）之间，并且检查文本字符串以确保它们是有效的文本模式（例如，有效的UTF-8，长度，语法等）。一些数据可能需要是“任何东西”（例如，文件上传器），但这些数据通常是罕见的。

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


    足够获得徽章！

    加固机制应该用于项目生产的软件，以便软件缺陷不太可能导致安全漏洞。 [hardening]
    加固机制可能包括HTTP头，如内容安全策略（CSP），用于减轻攻击的编译器标志（如-fstack-protector）或用以消除未定义行为的编译器标志。对于此条款的目的，最小权限不被认为是一种加固机制（最少权限是重要的，但是另有条款）。

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


    不足以获得徽章。

    该项目必须提供一个保证案例，证明其满足安全要求。保证案例必须包括：对威胁模型的描述，明确确定信任边界，确定设计原则得到适用，以及常见安全弱点已经被消减。 (需要网址) [assurance_case]
    一个保证案例是“一个文献记录的证据体系，提供了一个有说服力和有效的论据，指出一组关于系统属性的关键权利要求在给定环境中给定应用程序是充分合理的”（使用结构化保证案例模型的软件保证，Thomas Rhodes等人，NIST机构间报告7608）。信任边界是数据或执行改变其信任级别的边界，例如，典型Web应用程序中的服务器边界。常见做法是列出安全设计原则（例如Saltzer和Schroeer）和常见的实施安全漏洞（例如OWASP前10名或CWE / SANS前25名），并显示每个方案如何抵御。 BadgeApp保证案例可能是一个有用的例子。本条款与documentation_security，documentation_architecture和implement_secure_design等条款有关。

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


 分析 2/2 ●

  • 静态代码分析


    足够获得徽章！

    如果至少有一个FLOSS工具能够以所选择的语言实现此条款，则该项目必须至少使用一个具有规则或方式的静态分析工具来查找分析语言或环境中的常见漏洞。 [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


  • 动态代码分析


    足够获得徽章！

    如果由项目生成的软件包含使用内存不安全语言编写的软件（例如，C或C ++），则项目必须至少使用一个动态工具（例如，fuzzer或web应用扫描程序）与一种检测缓冲区覆写等内存安全问题的机制组合例行使用。如果项目不生成以内存不安全语言编写的软件，请选择“不适用”（N/A）。 [dynamic_analysis_unsafe]
    检测内存安全问题的机制的示例包括AddressSanitizer（ASAN）（可在GCC和LLVM中使用），“Memory Sanitizer”和 valgrind 。其他可能使用的工具包括ThreadSanitizer和UndefinedBehaviorSanitizer。广泛的断言也将起作用。

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



此数据在知识共享署名3.0或更高版本许可证（CC-BY-3.0 +） 下可用。所有内容都可以自由分享和演绎，但必须给予适当的署名。请署名为Yannick Moy和OpenSSF最佳实践徽章贡献者。

项目徽章条目拥有者： Yannick Moy.
最后更新于 2017-05-11 04:54:51 UTC, 最后更新于 2021-05-11 07:46:17 UTC。 最后在 2018-07-02 09:39:05 UTC 获得通过徽章。

后退