Common Weakness Enumeration

CWE Glossary Definition

Name of Your Organization:

AdaCore

Web Site:

www.adacore.com

Compatible Capability:

SPARK Pro

Capability home page:

http://www.adacore.com/sparkpro

Product Accessibility <CR_2.4>

Provide a short description of how and where your capability is made available to your customers and the public (required):

SPARK Pro is available for an annual subscription fee from AdaCore, and can be hosted on Windows, Linux OS or Mac OS, targeted to any target architecture of interest. For more information, contact sales@adacore.com

Map Currency Indication <CR_6.1>

Describe how and where your capability indicates the most recent CWE content used to create or update its mappings (required):

The user documentation on CWE features indicates the version of CWE used to label CWE check-boxes and other CWE indicators.

http://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_view_gnatprove_output.html#description-of-messages

Map Currency Update Approach <CR_6.2>

Indicate how often you plan on updating the mappings to reflect the current CWE content and describe your approach to keeping reasonably current with the CWE content when mapping them to your repository (recommended):

AdaCore makes annual major releases of all products, and a mid-year bug-fix release. At these times we will ensure the documentation of CWE capabilities are up to date.

We will also update documentation as we update individual messages to match new CWE revisions.

MAP CURRENCY UPDATE TIME <CR_6.3>

Describe how and where you explain to your customers the timeframe they should expect an update of your capability’s mappings to reflect newly available CWE content (required):

Our customer support tool GNATTracker is the primary means of communication between AdaCore and our customers:

http://www.adacore.com/frontline-support/gnattracker/

Through GNATTracker customers receive semi-annual updates, as well as "wavefront" releases during the year when a specific bug-fix is requested.

CWE AND COMPATIBILITY DOCUMENTATION <CR_5.1>

Provide a copy, or directions to its location, of where your documentation describes CWE and CWE compatibility for your customers (required):

http://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_view_gnatprove_output.html#description-of-messages

as well as the pages pointed from the above:

http://docs.adacore.com/spark2014-docs/html/ug/en/source/proof_checks_table.html
http://docs.adacore.com/spark2014-docs/html/ug/en/source/flow_checks_table.html

DOCUMENTATION OF FINDING ELEMENTS USING CWE IDENTIFIERS <CR_5.2>

Provide a copy, or directions to its location, of where your documentation describes the specific details of how your customers can use CWE identifiers to find the individual security elements within your capability’s repository (required):

http://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_view_gnatprove_output.html#description-of-messages

DOCUMENTATION OF FINDING CWE IDENTIFIERS USING ELEMENTS <CR_5.3>

Provide a copy, or directions to its location, of where your documentation describes the process a user would follow to find the CWE identifiers associated with individual security elements within your capability’s repository (required):

http://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_view_gnatprove_output.html#description-of-messages

DOCUMENTATION INDEXING OF CWE-RELATED MATERIAL <CR_5.4>

If your documentation includes an index, provide a copy of the items and resources that you have listed under "CWE" in your index. Alternately, provide directions to where these "CWE" items are posted on your web site (recommended):

The online documentation system supports search by keyword. This is the URL produced by typing "cwe" into the search box:

http://docs.adacore.com/spark2014-docs/html/ug/search.html?q=cwe

Type-Specific Capability Questions

FINDING TASKS USING CWE IDENTIFIERS <CR_A.2.1>

Give detailed examples and explanations of how a user can locate tasks in the tool by looking for their associated CWE identifier (required):

The user can select which particular CWE identifiers are of interest by using the search bar in the Locations panel in GPS. Here we have a screen shot where a specific CWE is searched, namely CWE 120 (classic buffer overflow). We can drill down to the actual source code by clicking on the message of interest.

In this second example, we search for all CWE, and the Locations panel shows the actual messages, organized by source file:

FINDING CWE IDENTIFIERS USING ELEMENTS IN REPORTS <CR_A.2.2>

Give detailed examples and explanations of how, for reports that identify individual security elements, the tool allows the user to determine the associated CWE identifier for the individual security elements in the report (required):

As seen in the above example, CWE identifiers are included in square brackets after any message in SPARK, provided switch --cwe has been selected when running the tool, either from the command line or in the project file.

GETTING A LIST OF CLAIMED CWE IDENTIFIER COVERAGE <CR_A.2.3>

Give detailed examples and explanations of how a user can obtain a listing of all of the CWE identifiers that the owner claims the tool is effective at locating in software (required):

Each message described in the SPARK user manual (Help/SPARK/SPARK 2014 Toolset User's Guide) identifies the associated CWE identifiers, if any.

Here is a portion of the SPARK user manual showing the listing of CWE identifiers associated with the messages reported by proof:

GETTING A LIST OF CWE IDENTIFIERS ASSOCIATED WITH TASKS <CR_A.2.6>

Give detailed examples and explanations of how a user can obtain a listing of all of the CWE identifiers that are associated with the tool’s tasks (recommended):

See section (A.2.3) above.

SELECTING TASKS USING INDIVIDUAL CWE IDENTIFIERS <CR_A.2.8>

Describe the steps that a user would follow to browse, select, and deselect a set of tasks for the tool by using individual CWE identifiers (recommended):

See section (A.2.1) above. By searching for CWE identifiers of interest, GPS will include or exclude messages with the associated CWE identifiers.

NON-SUPPORT NOTIFICATION FOR A REQUESTED CWE IDENTIFIER <CR_A.2.9>

Provide a description of how the tool notifies the user that a task associated with a selected CWE Identifier cannot be performed (recommended):

See section (A.2.1) above. By searching for "CWE", GPS will display all messages related to CWE identifiers.

ELECTRONIC DOCUMENT FORMAT INFO <B.3.1>

Provide details about the different electronic document formats that you provide and describe how they can be searched for specific CWE-related text (required):

SPARK can generate text format. The text file is a simple list of messages prefixed with "filename: line: column:". The text file is produced by invoking "gnatprove" on the command line with the "--cwe" option, to request CWE identifiers to be included after the message kind. For example:

   % gnatprove --cwe -P project_file

See (B.3.2) below for sample output.

ELECTRONIC DOCUMENT LISTING OF CWE IDENTIFIERS <CR_B.3.2>

If one of the capability’s standard electronic documents only lists security elements by their short names or titles provide example documents that demonstrate how the associated CWE identifiers are listed for each individual security element (required):

Below is sample output from "gnatprove --cwe -P project_file". The CWE identifiers are given in brackets after the message kind:

% gnatprove --cwe -P project_file
stack.adb:44:10: medium: exception might be raised
stack.adb:47:46: low: range check might fail [CWE 682]
stack.adb:49:20: medium: range check might fail [CWE 682] (e.g. when Last = 0)
stack.adb:50:12: medium: array index check might fail [CWE 120] (e.g. when Last = 201)
stack.adb:60:10: medium: exception might be raised
stack.adb:63:17: medium: array index check might fail [CWE 120]
stack.adb:66:46: low: range check might fail [CWE 682]
stack.adb:76:10: medium: exception might be raised
stack.adb:79:19: medium: array index check might fail [CWE 120] (e.g. when Last = 0)
stack.adb:89:52: medium: array index check might fail [CWE 120] (e.g. when I = 201)
screen_output.adb:52:46: low: range check might fail [CWE 682]
screen_output.adb:81:46: low: range check might fail [CWE 682]
screen_output.adb:81:53: low: range check might fail [CWE 682] (e.g. when S = (2 => ' ', 3 => ' ', 4 => ' ', others => ':') and S'First = 1 and S'Last = 2147483647)
values-operations.adb:26:10: medium: exception might be raised
instructions.adb:29:07: medium: exception might be raised
instructions.adb:52:13: medium: exception might be raised
values.adb:26:41: warning: unused assignment to "Real_Val"
values.adb:29:10: medium: exception might be raised

FINDING ELEMENTS USING CWE IDENTIFIERS THROUGH THE GUI <CR_B.4.1>

Give detailed examples and explanations of how the GUI provides a "find" or "search" function for the user to identify your capability’s elements by looking for their associated CWE identifier(s) (required):

See Item (A.2.1) above.

GUI ELEMENT TO CWE IDENTIFIER MAPPING <CR_B.4.2>

Briefly describe how the associated CWE identifiers are listed for the individual security elements or discuss how the user can use the mapping between CWE identifiers and the capability’s elements, also describe the format of the mapping (required):

See Item (A.2.2) above.

GUI EXPORT ELECTRONIC DOCUMENT FORMAT INFO <CR_B.4.3>

Provide details about the different electronic document formats that you provide for exporting or accessing CWE-related data and describe how they can be searched for specific CWE-related text (recommended):

The textual output presented in item (B.3.2) can be saved from GPS, selecting the icon to "Save the content of the messages window to a file" from the Messages panel.

STATEMENT OF COMPATIBILITY <CR_2.11>

Have an authorized individual sign and date the following Compatibility Statement (required):

"As an authorized representative of my organization I agree that we will abide by all of the mandatory CWE Compatibility Requirements as well as all of the additional mandatory CWE Compatibility Requirements that are appropriate for our specific type of capability."

Name: Yannick Moy

Title: SPARK Product Manager and Research Directions Lead

STATEMENT OF ACCURACY <CR_3.4>

Have an authorized individual sign and date the following accuracy Statement (recommended):

"As an authorized representative of my organization I agree that we will abide by all of the mandatory CWE Compatibility Requirements as well as all of the additional mandatory CWE Compatibility Requirements that are appropriate for our specific type of capability."

Name: Yannick Moy

Title: SPARK Product Manager and Research Directions Lead

STATEMENT ON FALSE-POSITIVES AND FALSE-NEGATIVES <CR_B.2.10> and/or <CR_B.3.7>

FOR TOOLS AND SERVICES ONLY — Have an authorized individual sign and date the following statement about your tools efficiency in identification of security elements (required):

"As an authorized representative of my organization I agree that we will abide by all of the mandatory CWE Compatibility Requirements as well as all of the additional mandatory CWE Compatibility Requirements that are appropriate for our specific type of capability."

Name: Yannick Moy

Title: SPARK Product Manager and Research Directions Lead