Project Formalization CVE case file

Public evidence / CVE-2026-6679

Case study of the harness in action

CVE-2026-6679 being reproduced independently by Project Formalization

01
Exact boundary
02
Independent replays
03
Evidence layers
ProjectwolfSSL 5.9.0
SubsystemDTLS 1.3 ACK
IdentifierCVE-2026-6679
Source pin922d04b3

CVE-2026-6679 / wolfSSL 5.9.0 / DTLS 1.3

ACK length crosses the word16 boundary

Capacity is reserved from a narrowed length. The writer then traverses the full record list.

Reproduced Heap buffer overflow Open case files

Mechanism

Boundary model
Record count4,095
x 16 bytes
Mathematical body65,520 B
to word16
Reserved body65,520 B

Representable: written bytes equal reserved bytes.

Witness anatomy

What changes at 4,096

  1. 01Mathematical body4,096 x 1665,536 bytes
  2. 02Narrowed reservation(word16) 65,5360 bytes
  3. 03Writer behaviorTraverse every nodeOut-of-bounds writes

Sealed exchange / selected excerpts

The finding, in the agents' own words

Selected excerpts are lightly edited for length and public safety. Raw session files and undisclosed experiments remain local.

T+07m
Investigator Bto Coordinator
"The narrowing is real: CheckAvailableSize trusts the wrapped length and only allocates for that smaller value, while the loop writes every node."
T+10m
Investigator Ato Coordinator
"The code path has a sharp arithmetic boundary: the serialized body length is accumulated as an unbounded element count, then truncated to 16 bits, while the subsequent writer still walks the full list."
T+15m
Coordinatorto Hostile critic
"The candidate snapshot is now frozen at c54a39e, with a sharp 4095/4096 boundary and ASan plus checker-sanity evidence."
T+23m
Hostile criticto Coordinator
"The mechanism survives. With the independent rerun, the strongest supportable grade is confirmed_violation, scoped to ack-write-capacity at the production ACK serialization boundary."
T+29m
Coordinatorfinal classification
"The blind experiment confirmed a DTLS 1.3 ACK serialization heap overflow at exactly 4,096 pending records. Both investigators and the independent critic reproduced it."

Independent confirmation

The discriminator survived every replay

RunInputOracleProduction boundaryResult
Closest control4,095 entriesAddressSanitizerACK writerClean
Investigator A4,096 entriesMSVC ASanDtls13RecordRecvdOverflow
Investigator B4,096 entriesClang ASanEstablished DTLS stateOverflow
Hostile critic4,096 entriesClean rebuild + ASanSendDtls13AckReproduced

The replay establishes the production serialization defect. It does not claim a complete encrypted peer-to-peer exploit path or code execution.

Codex + GPT-5.6 Sol

How the evidence survived the pipeline

  1. 01FreezeExact source pin and safety property
  2. 02SplitPositive and neutral investigator framings
  3. 03ModelBound the word16 length invariant
  4. 04ReplayIndependent sanitizer witnesses
  5. 05CritiqueClean rebuild and claim challenge
00:00

Evidence is sealed between independent arms until coordinator comparison.

READY

Inspectable artifact

Boundary model

ack_length_boundary.cView raw source

          

          

            
Control outputPASS

            
$ ./ack-length-boundary 4095
records=4095 written=65520 reserved=65520
result=representable

exit=0

            
Closest negative control: the full body remains representable.

          

        

      



    


    

      
Publication rule

      
Evidence, not confidence.

      
A production claim needs a pinned revision, concrete witness, fresh unmodified replay, useful negative control, and checker-sanity evidence. Anything less is labeled accordingly.

      Read the evidence standard