REQUIREMENTS.sdoc

[DOCUMENT]
MID: 1ea7bc6af2854a9bbb974d8933158f93
TITLE: OpenSUT Requirements
VERSION: 0.1
CLASSIFICATION: Internal
REQ_PREFIX: TA2-REQ-
ROOT: True
OPTIONS:
  ENABLE_MID: True
  REQUIREMENT_STYLE: Table

[FREETEXT]
This document contains all OpenSUT requirements, and was created with the help of `StrictDocs <https://strictdoc.readthedocs.io/en/stable/>`_. For text formatting, the reStructuredText markup syntax is supported, see `the RST cheatsheet <https://bashtage.github.io/sphinx-material/rst-cheatsheet/rst-cheatsheet.html>`_.

If you are new to requirement writing, we recommend reading first the *21 Top Engineering Tips
for writing an exceptionally clear requirements document* from QRA (available as `PDF here <https://github.com/GaloisInc/VERSE-OpenSUT/blob/main/docs/QRA_Clear_Requirements.pdf>`_)

The OpenSUT requirements are split into different sections and subsections. Each requirement has its section number (e.g. *4.1.1.2 Actuation Logic*) and its Unique Identifier (UID). The section number is used only in this document, the UID guaranteed to be globally unique. On top of UID, we also use StrictDocs' `MID <https://strictdoc.readthedocs.io/en/stable/strictdoc_01_user_guide.html#machine-identifiers-mid>`_. For requirement tracing and coverage measurement, we use primarily the UID.

Requirements that use the word *shall* are binding and must be satisfied, while requirements using the word *should* are non-binding, and can be considered optional or nice-to-have. A *rationale* is provided when appropriate for a given requirement.
[/FREETEXT]

[SECTION]
MID: 19d6225369d047578532ff23b2608b3c
UID: SECTION-OR-SoW-Requirements
TITLE: SoW Requirements

[FREETEXT]
Derived from the Statement of Work for the purpose of tracing the individual tasks and issues back to the SoW.
[/FREETEXT]

[SECTION]
MID: 06d3ceec305e4f60bce19881f23420a1
UID: SECTION-OR-OpenSUT-Platform
TITLE: OpenSUT Platform

[FREETEXT]
Task **TA2.1.1**
[/FREETEXT]

[REQUIREMENT]
MID: 6a87ea8e6db74701a0510b631c99a49a
UID: TA2-REQ-42
TITLE: Task TA2.1.1.A
STATEMENT: >>>
Develop the Open SUT primarily using existing components and specifications, including:

* Flight Controller
* AutoPilot
* Platform Crypto
* Mission Key Management
* Mission Protection System components.


Port a subset of OpenSUT components to run in a pKVM guest VM.
<<<

[REQUIREMENT]
MID: 03160a8cc4544d06b387cb4c2326776d
UID: TA2-REQ-44
TITLE: Task TA2.1.1.B
STATEMENT: >>>
Specify entire OpenSUT architecture with SysML,a subset of components with AADL, and a subset of AADL-specified components to include behavioral specifications.
<<<

[REQUIREMENT]
MID: 4361d44f1b65433e88092bfbb0bc0d41
UID: TA2-REQ-45
TITLE: Task TA2.1.1.C
STATEMENT: >>>
Develop VERSE Toolchain specifications for components with rich code-level specifications.
<<<

[/SECTION]

[SECTION]
MID: 348506bfb1154997a0d3abb6563af528
UID: SECTION-OR-Apply-VERSE-to-Open-SUT
TITLE: Apply VERSE to Open SUT

[FREETEXT]
Task **TA2.1.2**
[/FREETEXT]

[REQUIREMENT]
MID: ce6def11ef074a26a7234816c22264fb
UID: TA2-REQ-46
TITLE: Task TA2.1.2.A
STATEMENT: >>>
Build assurance case for the Open SUT.
<<<

[REQUIREMENT]
MID: 4861ace53a1f417abc04f0002eb775d2
UID: TA2-REQ-47
TITLE: Task TA2.1.2.B
STATEMENT: >>>
Apply Verse Development Environment (VDE) to provide qualitative and quantitative feedback.
<<<

[REQUIREMENT]
MID: ec121241fdc74a5caeae990125257007
UID: TA2-REQ-48
TITLE: Task TA2.1.2.C
STATEMENT: >>>
Define system deltas for program evolution and evaluation.
<<<

[REQUIREMENT]
MID: c7ae3ea9dfce41079532721c4302e349
UID: TA2-REQ-49
TITLE: Task TA2.1.2.D
STATEMENT: >>>
Support two Phase 1 continuous integration events.
<<<

[/SECTION]

[/SECTION]

[SECTION]
MID: 0860f7ea4f254939bec1bfb31c35e2bb
UID: SECTION-OR-Code-requirements
TITLE: OpenSUT Code Requirements

[FREETEXT]
In this section we list requirements about the overall OpenSUT code, its structure, coverage and format.
[/FREETEXT]

[REQUIREMENT]
MID: 6dc8373f5f424128b6d80c430ac19a8b
UID: TA2-REQ-16
TITLE: No undefined behavior
STATEMENT: >>>
OpenSUT shall not contain any C code with undefined behavior, as defined by Cerberus semantics.
<<<
RATIONALE: >>>
An example of undefined behavior include division by zero, out of bounds array access, integer overflow and null pointer dereference.
<<<

[REQUIREMENT]
MID: 64dbfd9b78d2417fa5a05de16ea9c681
UID: TA2-REQ-17
TITLE: MISRA-C compliant code
STATEMENT: >>>
OpenSUT application code should be MISRA-C compliant.
<<<
RATIONALE: >>>
It is acceptable to choose only a subset of MISRA-C, such that it is supported by open-source tools, or regular IDEs (such as `CLion <https://youtrack.jetbrains.com/articles/CPP-A-191430682>`_).
<<<

[/SECTION]

[SECTION]
MID: 117c895561b14ea5a65cec46de14a059
UID: SECTION-OR-OpenSUT-Scenario-Requirements
TITLE: OpenSUT Scenario Requirements

[FREETEXT]
Requirements related to each OpenSUT scenarios.
[/FREETEXT]

[SECTION]
MID: 93337f1b40a44d4faa96a1f5bde4ab20
UID: SECTION-OR-Boot-OpenSUT-to-a-known-initial-state
TITLE: Boot OpenSUT to a known initial state

[FREETEXT]
In this scenario, after a power-on as each OpenSUT component boots, it attests its state to the Mission Key Management (MKM) component. If the attestation of each component passes, the system will be in a known initial state, fully provisioned. The goal is to ensure that only the application code that has been signed by an external authority (e.g. the trusted component manufacturer) is running on the OpenSUT.

For the purpose of this scenario, we assume that each host computer contains a root of trust, a trusted boot that can bring up the hypervisor. In other words, we assume the host OS to be trusted (see the Threat model). Because hardware root of trust, trusted boot and attestation are all complex topics, only the application code will be attested in this scenario.

We expect the code to be signed with eXtended Merkle Signature Scheme (XMSS), as XMSS is commonly used for firmware signing, and is believed to be quantum safe.
[/FREETEXT]

[REQUIREMENT]
MID: d57ba5adcf3a42f1b12453684bae0814
UID: TA2-REQ-20
TITLE: Signature of application code image
STATEMENT: >>>
Each application disk image shall contain a digital signature that can be verified by the secure boot.
<<<
RELATIONS:
- TYPE: Parent
  VALUE: TA2-REQ-19

[REQUIREMENT]
MID: b9356f75b7f444979b97d20d8b504ba1
UID: TA2-REQ-19
TITLE: Secure booting only the application code
STATEMENT: >>>
Secure boot shall be used to boot only the application code, and only on a subset of OpenSUT components.
<<<
RATIONALE: >>>
This simplification is consistent with out threat model. Demonstrating Secure Boot only on a subset of components is sufficient.
<<<
RELATIONS:
- TYPE: Parent
  VALUE: TA2-REQ-18

[REQUIREMENT]
MID: 3143baadd69844e8b5ed4a9d2dd19fe2
UID: TA2-REQ-18
TITLE: Explicit assumptions
STATEMENT: >>>
In the provided documentation, explicitly list the assumptions and limitations of OpenSUT, such as:

* this is a contrived example
* true secure boot is not possible unless a *chain of trust* going all the way down to *Hardware Root of Trust* is maintained
* in real system a true *Hardware Security Module* (HSM) - such as the one developed on SEASHIP needs to be deployed on each Host computer, and shared with the guests
<<<

[/SECTION]

[/SECTION]

[SECTION]
MID: c4d23c336cf84d91902952b15b5d2afb
UID: SECTION-OR-Component-Requirements
TITLE: Component Requirements

[FREETEXT]
Component specific requirements are located in this section
[/FREETEXT]

[SECTION]
MID: e75433cf837f41648e0ef00231f04e47
UID: SECTION-OR-Mission-Protection-System-Requirements
TITLE: Mission Protection System (MPS) Requirements

[FREETEXT]
An engine protection system, that is redundant, measures engine temperature, and fuel pressure, and shuts down the engine if unsafe values are detected.

The system is connected to two temperature sensors and two fuel pressure sensors. The system has a control interface that allows the user to enter the maintenance mode, and adjust setpoints and trip channels. This control interface is available via a serial console (UART), and as such can be accessed only when the platform is not in operation (imagine the UART port being hidden behind a body panel).
[/FREETEXT]

[SECTION]
MID: e2b63c2068ac441590893f4f05fbeddc
UID: SECTION-OR-MPS-Architectural-Requirements
TITLE: MPS Architectural Requirements

[REQUIREMENT]
MID: eb6359cef9f646f1a9649864dc2a04e4
UID: TA2-REQ-40
TITLE: Four instrumentation channels
STATEMENT: >>>
MPS shall have four redundant divisions of instrumentation, each containing identical designs, with two instrumentation channels (Fuel Pressure and Temperature), each channel containing:

A. Sensor
B. Data acquisition and filtering
C. Setpoint comparison for trip generation
D. Trip output signal generation
<<<

[REQUIREMENT]
MID: c89d1058ea9e4712b244d51d4640f4b3
UID: TA2-REQ-41
TITLE: Actuation logic
STATEMENT: >>>
MPS shall have two trains of actuation logic, each containing identical designs:

A. Two-out-of-four coincidence logic of like trip signals
B. Logic to actuate a first device based on an OR of two instrumentation coincidence signals
C. Logic to actuate a second device based on the remaining instrumentation coincidence signal
<<<

[/SECTION]

[SECTION]
MID: 79296dba042c4553a4e519dad0324902
UID: SECTION-OR-MPS-Functional-Requirements
TITLE: MPS Functional Requirements

[REQUIREMENT]
MID: 882cd65129a343269be014ecc0593d95
UID: TA2-REQ-27
TITLE: High pressure trip
STATEMENT: >>>
MPS shall Trip on high fuel pressure (sensor to actuation)
<<<

[REQUIREMENT]
MID: 0b5deb00ffcd459a90b3ba7de2c3bb06
UID: TA2-REQ-28
TITLE: High temperature trip
STATEMENT: >>>
MPS shall Trip on high temperature (sensor to actuation)
<<<

[REQUIREMENT]
MID: 1df6243806884f23b976d477682d1915
UID: TA2-REQ-29
TITLE: Voting logic
STATEMENT: >>>
MPS shall Vote on like trips using two-out-of-four coincidence
<<<

[REQUIREMENT]
MID: 2f566450029b497fb1f8b6b4894e84f0
UID: TA2-REQ-30
TITLE: Automatic actuation
STATEMENT: >>>
MPS shall Automatically actuate devices.
<<<

[REQUIREMENT]
MID: 71a9b50dba854f0796dd3016eb1f6f2a
UID: TA2-REQ-31
TITLE: Manual actuation
STATEMENT: >>>
MPS shall Manually actuate each device upon receiving a user command.
<<<

[REQUIREMENT]
MID: 67949bc47e6d42988aa2c169a59085b0
UID: TA2-REQ-32
TITLE: Operating modes
STATEMENT: >>>
MPS shall Select mutually exclusive maintenance and normal operating modes on a per division basis.
<<<

[REQUIREMENT]
MID: 702abcfdbe794017a9b8b9cf52738afa
UID: TA2-REQ-33
TITLE: Setpoint adjustment
STATEMENT: >>>
MPS shall Perform setpoint adjustment in maintenance mode.
<<<

[REQUIREMENT]
MID: 8d92ee3fad9f4cec8d268f3dca839eb1
UID: TA2-REQ-34
TITLE: Maintenance mode bypass
STATEMENT: >>>
MPS shall Configure the system in maintenance mode to bypass an instrument channel (prevent it from generating a corresponding active trip output).
<<<

[REQUIREMENT]
MID: 0ec8d8fd517a4670a2f0f4b3027e464d
UID: TA2-REQ-35
TITLE: Maintenance mode forced trip
STATEMENT: >>>
MPS shall Configure the system in maintenance mode to force an instrument channel to an active trip output state.
<<<

[REQUIREMENT]
MID: 6224096ff4024ff4b6e53aa486a99773
UID: TA2-REQ-36
TITLE: Variables displayed
STATEMENT: >>>
MPS shall Display fuel pressure, and engine temperature.
<<<

[REQUIREMENT]
MID: 6d9f02661eb54714be39b507ba84b005
UID: TA2-REQ-37
TITLE: Trip state displayed
STATEMENT: >>>
MPS shall Display each trip output signal state.
<<<

[REQUIREMENT]
MID: a4fe198bfecc4a3ba4c15abc001c4529
UID: TA2-REQ-38
TITLE: Bypass indication display
STATEMENT: >>>
MPS shall Display indication of each channel in bypass.
<<<

[REQUIREMENT]
MID: 4d9169cb67ef45e8be4bd00ac23cada8
UID: TA2-REQ-39
TITLE: Periodic self-test
STATEMENT: >>>
MPS shall run Periodic continual self-test of safety signal path (e.g., overlapping from sensor input to actuation output).
<<<

[/SECTION]

[SECTION]
MID: 3356cf51d10a4f4b944fa2b0be4a7d57
UID: SECTION-OR-MPS-Testing-Requirements
TITLE: MPS Testing Requirements

[FREETEXT]
Traditionally, this section would be called *Verification Requirements*, but in the context of VERSE *verification* means *providing a formal proof*, thus *testing* is a more appropriate label.
[/FREETEXT]

[REQUIREMENT]
MID: a68b1797067440aeb4161c281c0b257f
UID: TA2-REQ-21
TITLE: Completeness and consistency
STATEMENT: >>>
MPS shall demonstrate the Completeness and consistency of requirements
<<<

[REQUIREMENT]
MID: 3b1a4cf5668642d2a88b9e2804a75fd9
UID: TA2-REQ-22
TITLE: Instrumentation independence
STATEMENT: >>>
MPS shall demonstrate Independence among the four divisions of instrumentation (inability for the behavior of one division to interfere or adversely affect the performance of another)
<<<

[REQUIREMENT]
MID: 8456d72a46a44365a46fbca5a8df5a25
UID: TA2-REQ-23
TITLE: Instrumentation independence within a division
STATEMENT: >>>
MPS shall demonstrate Independence among the two instrumentation channels within a division (inability for the behavior of one channel to interfere or adversely affect the performance of another)
<<<

[REQUIREMENT]
MID: b3e86ecd8ca54d9fae6b65f45ecaf1c7
UID: TA2-REQ-24
TITLE: Actuation logic independence
STATEMENT: >>>
MPS shall demonstrate Independence among the two trains of actuation logic (inability for the behavior of one train to interfere or adversely affect the performance another)
<<<

[REQUIREMENT]
MID: b9d14698739f4d9aafa03542bbd89fad
UID: TA2-REQ-25
TITLE: Actuation on coincidence vote or manual action
STATEMENT: >>>
MPS shall demonstrate Completion of actuation whenever coincidence logic is satisfied or manual actuation is initiated.
<<<

[REQUIREMENT]
MID: af961464d2754e108c544458cd1f0ea3
UID: TA2-REQ-26
TITLE: Self test and trip independence
STATEMENT: >>>
MPS shall demonstrate Independence between periodic self-test functions and trip functions (inability for the behavior of the self-testing to interfere or adversely affect the trip functions)
<<<

[/SECTION]

[/SECTION]

[SECTION]
MID: 2735d45cae734d8da005a686d00910a0
UID: SECTION-OR-Secure-Boot-Requirements
TITLE: Secure Boot Requirements

[FREETEXT]
A system boot where aspects of the hardware and firmware are measured and compared against known good values to verify their integrity and thus their trustworthiness.
[/FREETEXT]

[SECTION]
MID: 1e86153539334092b7cbb1d8c8ee8010
UID: SECTION-OR-Secure-Boot-Functional-Requirements
TITLE: Secure Boot Functional Requirements

[REQUIREMENT]
MID: 4686057607184f69bea4536790198a82
UID: TA2-REQ-54
TITLE: Known initial state
STATEMENT: >>>
The Secure Boot shall bring a given component to a known initial state.
<<<
RELATIONS:
- TYPE: Parent
  VALUE: TA2-REQ-19

[REQUIREMENT]
MID: 7e63112a785345c0892f4c247aaea0cb
UID: TA2-REQ-65
TITLE: Code attestation
STATEMENT: >>>
TODO
<<<

[REQUIREMENT]
MID: 0d18b653dfb84db098626c08357e1e66
UID: TA2-REQ-55
TITLE: Boot debug information
STATEMENT: >>>
The Secure Boot shall print information to the console/serial port for debugging purposes.
<<<

[REQUIREMENT]
MID: facc21ec6af54e2c9b1e40ea5dee1043
UID: TA2-REQ-56
TITLE: Secure boot termination
STATEMENT: >>>
The Secure Boot shall always terminate.
<<<

[REQUIREMENT]
MID: 9184caef8aac485bbdd3ed976667f72a
UID: TA2-REQ-57
TITLE: Launch application or terminate
STATEMENT: >>>
The Secure boot shall either launch the application, or if an error occurs, log the error and terminate.
<<<

[REQUIREMENT]
MID: ece9a93c174e4cd0901d1956d2e4cb42
UID: TA2-REQ-58
TITLE: Clear memory
STATEMENT: >>>
The Secure boot shall erase all RAM containing the secure boot data before a handoff to the application code.
<<<
RATIONALE: >>>
This prevents accidental leakage of private information to the potentially compromised application, such as private keys or attestation information.
<<<

[/SECTION]

[SECTION]
MID: 0910fb68d35445a7974d37277f4d15a1
UID: SECTION-OR-Secure-Boot-Security-Requirements
TITLE: Secure Boot Security Requirements

[REQUIREMENT]
MID: 71b4c4561b304056a13dff25920f2fff
UID: TA2-REQ-60
TITLE: Measurement algorithm
STATEMENT: >>>
The Secure Boot shall use high assurance implementation of cryptographic algorithms.
<<<
RATIONALE: >>>
For example an implementation that has been formally verified against a "golden" specification, or an implementation automatically generated from such "golden specification".
<<<

[REQUIREMENT]
MID: 07f7a61510e54d2c8357c08c1ab19166
UID: TA2-REQ-59
TITLE: Binary code measurement
STATEMENT: >>>
The Secure Boot shall measure the application binary and compare it against a stored good known value.
<<<
RELATIONS:
- TYPE: Parent
  VALUE: TA2-REQ-20

[REQUIREMENT]
MID: 72e26ca552b14526b49b8295b255d01a
UID: TA2-REQ-61
TITLE: Secure store of the hash measurement
STATEMENT: >>>
The Secure Boot should store the measured values in a Trusted Platform Module or other secure memory storage.
<<<
RATIONALE: >>>
Normally this requirement would be binding ("shall"), but given the scope of our threat model, this requirement is optional ("should").
<<<

[REQUIREMENT]
MID: aab9582e60fb4f08909e85ed4f29abc5
UID: TA2-REQ-62
TITLE: Abort on mismatched measurements
STATEMENT: >>>
The Secure Boot shall abort the boot process and throw an error, if the expected and measured values do not match.
<<<

[REQUIREMENT]
MID: a137631301704756a9842e8700fa0ae9
UID: TA2-REQ-63
TITLE: Secure Boot stored in read-only memory
STATEMENT: >>>
The Secure Boot executable shall be stored in a read only memory, or with read-only permissions.
<<<
RATIONALE: >>>
This avoids possible modifications to the secure boot executable.
<<<

[REQUIREMENT]
MID: 328e8e19d1c84a398b9bb425d8a1091e
UID: TA2-REQ-64
TITLE: Do not compare measurements if expected value is not provided
STATEMENT: >>>
If no expected value of the application binary is provided, the secure boot shall only perform a measurement, save it, and launch the application.
<<<
RATIONALE: >>>
If an application is not signed, the secure boot measurement comparison is disabled.
<<<

[/SECTION]

[/SECTION]

[/SECTION]

[SECTION]
MID: 377a09e7f8fa4c399ea4ae3a9f7c22fd
UID: SECTION-OR-VERSE-Toolchain-Requirements
TITLE: VERSE Toolchain Requirements

[FREETEXT]
VERSE Toolchain specific requirements, driven by the TA2 needs.
[/FREETEXT]

[SECTION]
MID: 1bc49bad6c4f481bad154377f5f7f44e
UID: SECTION-OR-Robustness-requirements
TITLE: VERSE Toolchain Usability Requirements

[FREETEXT]
Requirements related to the user experience with VERSE Toolchain in general.
[/FREETEXT]

[REQUIREMENT]
MID: c89d6255025d4e81ba7fd316d38ffb3f
UID: TA2-REQ-1
STATUS: Active
TITLE: No crashing
STATEMENT: >>>
VERSE Toolchain shall not crash on arbitrary input. Instead, an error message shall be produced.
<<<
RATIONALE: >>>
Even if a specification is incorrect, or the input file is not a valid C code, VERSE Toolchain should gracefully exit.
<<<

[REQUIREMENT]
MID: 7486f9de0f0d4b3fad5529d9b26da3fc
UID: TA2-REQ-2
STATUS: Active
TITLE: Special delimiters
STATEMENT: >>>
VERSE Toolchain should support multiple special delimiters, such as `//@` or `/*@` or `/**@`. Which special delimiter should be used can be either configurable, or VERSE Toolchain should support all of them at the same time (see TA2-REQ-15).
<<<
RATIONALE: >>>
In some codebases, VERSE Toolchain specs need to co-exist with existing specifications (such as Frama-C ACSL), such that adding VERSE Toolchain specs does not break the existing proofs.
<<<
RELATIONS:
- TYPE: Parent
  VALUE: TA2-REQ-7

[REQUIREMENT]
MID: d1c4883fe05149ab94ca644e5e21eb98
UID: TA2-REQ-7
TITLE: Multiple specification languages
STATEMENT: >>>
VERSE Toolchain shall run on codebases with multiple specification languages, such as Frama-C, SAW, and Cryptol.
<<<
RATIONALE: >>>
High assurance code might contain multiple different spec languages. For VERSE program, we expect that only Frama-C ACSL specifications will exist directly in the C source code. Other specs, such as SAW and Cryptol, do not change the C code directly.
<<<

[REQUIREMENT]
MID: ed253cc2440040d8ae16b40d787f8b4f
UID: TA2-REQ-8
TITLE: Continuity of existing proofs
STATEMENT: >>>
Adding VERSE Toolchain specs to a codebase shall not break existing proofs about such codebase.
<<<
RATIONALE: >>>
For example, adding VERSE Toolchain specs into an existing high assurance codebase shall not break the existing Frama-C proofs
<<<
RELATIONS:
- TYPE: Parent
  VALUE: TA2-REQ-7

[REQUIREMENT]
MID: 08aa1eec7c5a4f218d9ceeef73c1b938
UID: TA2-REQ-15
TITLE: Project specific VERSE Toolchain configuration
STATEMENT: >>>
VERSE Toolchain shall support project specific configuration, in the form of a configuration file that will adjust how VERSE Toolchain behaves.
<<<
RATIONALE: >>>
This is a top level requirement, further specified in the child requirements.
<<<

[REQUIREMENT]
MID: 4c8d98c9b64c4cfe83ecbd73d785fc27
UID: TA2-REQ-52
TITLE: Code similarity
STATEMENT: >>>
The code checked by VERSE Toolchain and the code compiled and deployed on the OpenSUT shall be identical.
<<<
RATIONALE: >>>
If the code that can be checked by VERSE Toolchain is substantially different from the code that is compiled and deployed, errors in the production code might not be captured, leading to presence of bugs and vulnerabilities.
<<<

[/SECTION]

[SECTION]
MID: 47b21bb670624559b181b882007035d6
UID: SECTION-OR-Functional-Requirements
TITLE: VERSE Toolchain Functional Requirements

[FREETEXT]
This section lists requirements on the functionality of VERSE Toolchain, and the features it provides.
[/FREETEXT]

[REQUIREMENT]
MID: d7f93f2b664e49778727afb3656b2725
UID: TA2-REQ-3
TITLE: Versioned releases
STATEMENT: >>>
VERSE Toolchain shall provide versioned releases, such that running VERSE Toolchain with `-V` flag shall print out the version of the tool.
<<<

[REQUIREMENT]
MID: 2a0d10e543ec4f279e2f56d092e7e65e
UID: TA2-REQ-5
TITLE: Variadic functions
STATEMENT: >>>
VERSE Toolchain shall support reasoning about variadic functions, such as `printf()`.
<<<

[REQUIREMENT]
MID: 967a8c569dca4e8492d371b030be0f13
UID: TA2-REQ-4
TITLE: Packaged releases
STATEMENT: >>>
VERSE Toolchain shall provide packaged releases using industry standard mechanisms, such as docker, or debian packages.
<<<

[REQUIREMENT]
MID: 2db8fe5f16b247eea953e3c944687e33
UID: TA2-REQ-6
TITLE: C Unions
STATEMENT: >>>
VERSE Toolchain shall support reasoning about C union types.
<<<
RATIONALE: >>>
For example the MPS code relies heavily on unions, and such code needs to be supported.
<<<

[REQUIREMENT]
MID: 38dbcc6d1cc042749c550ff7394513db
UID: TA2-REQ-9
TITLE: Nested types
STATEMENT: >>>
VERSE Toolchain shall support reasoning about structs composed of other structs.
<<<
RATIONALE: >>>
For example VERSE Toolchain shall be able to reason about the following struct and prove that there is no undefined behavior and that any user defined specification holds for such a struct:

.. code-block:: c

    struct S {
        T1 S1;
        T2 *S2;
        T3 S3[];
    }
<<<

[REQUIREMENT]
MID: 9dd60eb2b6b74db2ae06ff42ad0505e2
UID: TA2-REQ-53
TITLE: User defined type invariants
STATEMENT: >>>
VERSE Toolchain should support checking user defined type and data structure invariants. VERSE Toolchain should allow users to annotate types and data structures with invariants, such that the invariant is preserved at every instance of that type.
<<<
RATIONALE: >>>
For example, the user wishes to prove that a pointer of particular type is never NULL. While NULL pointers are allowed under Cerberus C semantics, *dereferencing* a NULL pointer is an undefined behavior. Thus, a user defined invariant that a pointer shall never be NULL should be checkable by VERSE Toolchain.

Or given an array `T3 S3[];` the user wishes to prove that invariants about type T3 are valid for each element of array S3, and this is true for min and max size of S3, with min=0 and max some sensible default value (uint32_MAX?).
<<<

[REQUIREMENT]
MID: 0edc5a82bfa34fe79f46c23eb9af9986
UID: TA2-REQ-10
TITLE: Specs in header of source file allowed
STATEMENT: >>>
VERSE Toolchain shall allow the user to write VERSE Toolchain specifications in either header (function declaration) or source file (function definition). If VERSE Toolchain specs are provided at both function declaration and function definition, VERSE Toolchain shall raise an error.
<<<
RATIONALE: >>>
In some cases, writing specs in the header files is more ergonomic. In other cases, there might be no header files. The user shall have a choice that is the most suitable for a particular codebase. If accidentally the user writes multiple VERSE Toolchain specs for the same function (in the header and in the source file), VERSE Toolchain needs to throw an error an notify the user, as resolving which specs are valid is a complex problem.
<<<

[REQUIREMENT]
MID: ff63483e56744e10a10d5a9467f81231
UID: TA2-REQ-12
TITLE: Explicit assertion checking
STATEMENT: >>>
VERSE Toolchain shall have a configurable option to either ignore inline `assert()` statements, or to statically check them.
<<<
RATIONALE: >>>
In some codebases, assertions are used only for selective runtime testing, so static checking might produce findings that are not interesting for the developers. The assertions are removed in the production code. Hence having the configurable option for VERSE Toolchain is important.
<<<
RELATIONS:
- TYPE: Parent
  VALUE: TA2-REQ-15

[REQUIREMENT]
MID: 239719df3d0746c6be9363179d9c9fa1
UID: TA2-REQ-13
TITLE: Well defined default behavior
STATEMENT: >>>
If a function is not annotated with any VERSE Toolchain specifications, VERSE Toolchain shall explicitly state what are the default (implicit) `require`, `ensure` and `modify` clauses.
<<<
RATIONALE: >>>
It needs to be stated whether by default each function requires and ensures nothing, or if there are some implicit assumptions, important for compositional reasoning. Same for modification - a sensible default behavior could be that a function without specs is assumed to modify everything. However, in that case compositional reasoning is not really possible, so having a configurable option here might be preferred.

The implicit `requires` might encompass e.g. a valid stack frame for the function.
<<<
RELATIONS:
- TYPE: Parent
  VALUE: TA2-REQ-15

[REQUIREMENT]
MID: d0a1826596ee41fcba1230498e92b242
UID: TA2-REQ-14
TITLE: Annotation of pure functions
STATEMENT: >>>
VERSE Toolchain shall have a configurable option to either assume that all functions are `pure` by default, or to require an explicit `pure` annotation.
<<<
RATIONALE: >>>
Pure functions are side-effects free, and don't have any persistent static variables (see https://en.wikipedia.org/wiki/Pure_function). In some cases, explicitly stating which functions should be `pure` is easier, while in other codebases, it is reasonable to assume that the functions are `pure` by default. This should be configurable.
<<<
RELATIONS:
- TYPE: Parent
  VALUE: TA2-REQ-15

[REQUIREMENT]
MID: 99d58897b02743eb9c35b925b1a5bcfc
UID: TA2-REQ-51
TITLE: Check for undefined behavior
STATEMENT: >>>
VERSE Toolchain shall check C code for undefined behavior as defined in Cerberus semantics, and raise an error when undefined behavior is found.
<<<
RATIONALE: >>>
This is a base level functionality of VERSE Toolchain, as code with undefined behavior often leads to errors and unintended results.
<<<
RELATIONS:
- TYPE: Parent
  VALUE: TA2-REQ-16

[/SECTION]

[SECTION]
MID: 8b79d2b352df4ac2af8e9bdbed7bd64c
UID: SECTION-OR-Documentation-requirements
TITLE: VERSE Toolchain Documentation Requirements

[FREETEXT]
Documentation of VERSE Toolchain, including manuals, tutorials, quick-start guides, code and document generation, and hints and error messages.
[/FREETEXT]

[REQUIREMENT]
MID: 82e79a99aa9c4c9ab74c1bbe4535dbda
UID: TA2-REQ-11
TITLE: Generating code documentation with specs
STATEMENT: >>>
TA1 tools shall generate source code documentation that includes VERSE Toolchain specification with VERSE Toolchain syntax highlighted.
<<<
RATIONALE: >>>
Doxygen-like documentation with VERSE Toolchain specs included is ideal. It is important that the specs are not treated like comments, but are lifted and highlighted in the generated documents.
<<<

[REQUIREMENT]
MID: 39e7d83efe9f4073b69ff53f2be42c68
UID: TA2-REQ-50
TITLE: Code coverage measurement
STATEMENT: >>>
VERSE Toolchain should provide means of measuring code coverage, and specifically reporting:

1) percentage or LOC of code/functions that have *any* specs
2) *any* code excluded from VERSE Toolchain checking (maybe hiding behind `#ifdef` or some other directive, excluding the code from being examined)
3) coverage based on types/classes of specifications (see the different classes we mentioned in the proposal)
<<<
RATIONALE: >>>
See https://github.com/GaloisInc/VERSE-Toolchain/issues/93 for more details.
<<<

[/SECTION]

[/SECTION]