ba-cybersecurity.comResearch by Nobuo Otoi

The problem

Section 4.4 of the draft compares the version asserted by a component with an array of integers in the manifest, integer by integer, and stops "after all integers in the array defined by the manifest have been consumed". Section 4.4.1 encodes a pre-release with a negative indicator, for example 1.2.3-alpha.4 = [1,2,3,-3,4], and says this lets pre-releases "compare correctly with final releases".

Put together: for the condition Equal [1,2,3] and a component at 1.2.3-alpha.4, the comparison finds 1 = 1, 2 = 2, 3 = 3, the manifest's array is consumed, and the condition matches. A condition meant for release 1.2.3 also accepts its alpha; Greater or Equal [1,2,3] accepts it the same way, and Lesser [1,2,3] does not, although Semantic Versioning 2.0.0 (a normative reference of the draft) ranks 1.2.3-alpha.4 below 1.2.3.

How it was shown

The case above needs only the draft text. Further cases, a possible wording for a fix, and two checks accompany it: in Lean 4 the rule as written is modelled, the cases are checked by decide, and the proposed wording is proved to agree with SemVer precedence for arrays of any length and any values; in Python, every pair of 858 arrays under the five operators (3,680,820 combinations) is compared, and the draft text differs from SemVer in 49,365 of them, the proposed wording in none.

No cryptographic mechanism is broken, no attack on a deployed device was tried, and implementations were not tested.

Check it by hand

Draft -16 §4.4 · SemVer §11 · Minimal.lean

Response

The case was posted to the SUIT working group list on 1 Nov 2026. The same day (UTC) an author of the draft replied that the reading is correct, that the current encoding together with the stopping rule allows a condition intended for a final release to accept its pre-releases, and that this is an error in the draft. Rather than changing the comparison rule, the author proposed changing the encoding: three release integers are always present, a fourth integer gives the release stage (0 for a final release, negative for a pre-release), and a pre-release ends with the marker −24, so that 1.2.3 becomes [1,2,3,0] and 1.2.3-alpha.4 becomes [1,2,3,-3,4,-24].

That proposal was checked the next day: a model of 1,728 complete versions, every pair under the five operators (14,929,920 combinations), gives no disagreement with SemVer precedence, and a Lean 4 theorem shows the same for complete versions with any values and any number of identifiers. Two remaining edge cases were noted on the list (short selectors still match pre-releases by design; a component shorter than the manifest has no defined outcome).

Revision -17 of the draft, dated 2 Nov 2026, contains the new encoding rules in Section 4.4.1.

Links