| Internet-Draft | Verification Appraisal | October 2026 |
| Watts | Expires 24 April 2027 | [Page] |
This document maps protocol-verification evidence and the WIVL assurance-stage model onto the RATS architecture. It defines appraisal requirements for SPEC_VALIDATED, LOCAL_CONFORMANT, INDEPENDENTLY_REPRODUCED, and SECURITY_TESTED results while preserving unknown evidence and requiring arithmetic preconditions for mathematical test vectors. An attestation result reports bounded assurance; it is not an authorization grant or production-release decision.¶
This Internet-Draft is submitted in full conformance with the provisions of BCP 78 and BCP 79.¶
Internet-Drafts are working documents of the Internet Engineering Task Force (IETF). Note that other groups may also distribute working documents as Internet-Drafts. The list of current Internet-Drafts is at https://datatracker.ietf.org/drafts/current/.¶
Internet-Drafts are draft documents valid for a maximum of six months and may be updated, replaced, or obsoleted by other documents at any time. It is inappropriate to use Internet-Drafts as reference material or to cite them other than as "work in progress."¶
This Internet-Draft will expire on 24 April 2027.¶
Copyright (c) 2026 IETF Trust and the persons identified as the document authors. All rights reserved.¶
This document is subject to BCP 78 and the IETF Trust's Legal Provisions Relating to IETF Documents (https://trustee.ietf.org/license-info) in effect on the date of publication of this document. Please review these documents carefully, as they describe your rights and restrictions with respect to this document. Code Components extracted from this document must include Revised BSD License text as described in Section 4.e of the Trust Legal Provisions and are provided without warranty as described in the Revised BSD License.¶
The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in BCP 14 [RFC2119] [RFC8174] when, and only when, they appear in all capitals.¶
The RATS architecture [RFC9334] separates Evidence produced by an Attester, appraisal by a Verifier, and trust decisions by a Relying Party. WIVL uses a similar separation for software and protocol assurance stages. This document defines a profile for representing protocol-verification evidence as attestation evidence and for appraising that evidence into a bounded assurance stage.¶
This profile does not claim that passing a software test proves model safety, operational authorization, or production readiness. It standardizes what evidence is required before a Verifier can report a specific verification stage.¶
The characterized build or test environment that emits evidence about the implementation, procedure, vectors, environment, and results.¶
The party that appraises the evidence against an appraisal policy and emits an Attestation Result.¶
The party deciding whether the reported assurance stage is sufficient for a local use.¶
Expected vector digests, procedure digests, approved implementation identifiers, release metadata, or other trusted inputs used by the appraisal policy.¶
The ordered stages are REGISTERED, SPEC_VALIDATED, LOCAL_CONFORMANT, INDEPENDENTLY_REPRODUCED, and SECURITY_TESTED. RELEASE_ELIGIBLE is intentionally not an attestation stage because release approval is a relying-party governance decision.¶
No stage implies a later stage. In particular, LOCAL_CONFORMANT MUST NOT be appraised as INDEPENDENTLY_REPRODUCED unless the evidence identifies an independent reproducing producer and implementation.¶
Evidence for this profile includes: subject digest, implementation digest, verification-procedure digest, vector-set digest, environment digest, toolchain versions, result digest, per-check outcomes, producer identifier, and timestamps or freshness evidence appropriate to the attestation mechanism.¶
Where the procedure includes finite-field or elliptic-curve test vectors, the appraisal policy SHOULD require arithmetic preconditions before considering higher-level metamorphic relations. At minimum, declared curve parameters must be non-singular and each declared affine point must satisfy the curve equation before group-law results are admitted as evidence.¶
Validate evidence integrity and freshness according to the selected RATS mechanism.¶
Confirm the subject, procedure, vector-set, and environment digests against trusted reference inputs.¶
For SPEC_VALIDATED, require all declared specification preconditions to be internally consistent and required vector inputs to be valid.¶
For LOCAL_CONFORMANT, additionally require all mandatory conformance checks to PASS in the characterized environment.¶
For INDEPENDENTLY_REPRODUCED, require a producer distinct from the original producer and evidence that the reproducing implementation is independently controlled. The verifier MUST NOT infer independence from a second run of the same implementation by the same producer.¶
For SECURITY_TESTED, require evidence of the deployment-defined authorized security-testing and fault-injection obligations in addition to independent reproduction.¶
If any required fact is unknown or unverifiable, the verifier MUST report a result that does not exceed the strongest stage actually established.¶
The assurance stage can be carried as an application-specific result alongside the trustworthiness information defined by current RATS work such as AR4SI [I-D.rats-ar4si] or EAT Attestation Results [I-D.rats-ear]. This version does not define a new registered EAT claim.¶
A result SHOULD also identify the appraisal-policy digest, evidence digest, verifier identity, and unresolved conditions. A Relying Party MUST apply its own policy; an Attestation Result is not an authorization credential.¶
Deployments MAY use multiple verifiers, including the interaction patterns explored by [I-D.rats-multi]. Multiple-verifier use does not automatically establish independent reproduction: the underlying evidence producers and implementations must also satisfy the independence policy.¶
An implementation is non-conformant if it promotes a local result to independent reproduction without independent evidence, ignores a failed specification precondition, treats an invalid elliptic point as valid evidence for a group-law test, promotes UNKNOWN evidence, or treats an Attestation Result as permission to execute without a separate authorization decision.¶
Threats include circular evidence generation, self-attestation, reference-value substitution, environment spoofing, stale results, toolchain substitution, selective omission of failed vectors, and independence fraud. Security-critical expected values SHOULD come from a source independent of the implementation under test. The appraisal policy SHOULD bind all evidence to immutable digests and preserve failed or indeterminate outcomes.¶
Verification evidence can expose software versions, deployment configuration, test environments, vulnerability findings, and organizational relationships. Profiles SHOULD minimize evidence disclosure and use digests or controlled references where the Relying Party does not require raw evidence.¶
This document has no IANA actions. A future revision can request claim or media-type registrations if a working-group encoding is selected.¶