saead/downlink: replay gate disarms itself on session start and high-…

[fderepas]

…water mark can move down

Summary

The SAEAD downlink replay protection can be disarmed and rolled backward by an
unauthenticated network attacker in the shipped default configuration. Two
mechanisms combine:

1. is_valid_downlink() accepts unconditionally whenever the SESSION_VALID
   bit is clear (src/saead/downlink.c:41-45), and
2. every session start clears SESSION_VALID (downlink.c:122), which is
   re-armed only after a block successfully decrypts (downlink.c:169), while
3. the replay high-water advance at downlink.c:176 is unconditional —
   server.seqnum = seqnum — so a decrypt with a stale seqnum moves the mark
   down, and server.seqnum is never reset anywhere.

A passive-recorder + active-dropper attacker can therefore lower server.seqnum
and re-open a replay window it had already closed. This PR guards the advance to
be monotonic (the necessary local fix) and describes the additional change needed
to keep the gate armed (the root cause).

Severity: High — replay of authenticated downlink sessions by an unauthenticated
network attacker, in the default CONFIG_POUCH_ENCRYPTION_SAEAD build.

The three facts (current tree, HEAD 0d749f5)

(1) The gate short-circuits to ACCEPT when disarmed — src/saead/downlink.c:

static bool is_valid_downlink(const struct session_id *id, psa_algorithm_t algorithm)
{
    if (!pouch_atomic_test_bit(&downlink.flags, SESSION_VALID))
    {
        // No previous session to invalidate the incoming session
        return true;                                   /* :41-45  accept, gate disarmed */
    }
    ...
    if (id->initiator == POUCH_ROLE_SERVER)
    {
        if (id->type == SESSION_ID_TYPE_SEQUENTIAL && id->value.sequential.seqnum <= server.seqnum)
        {
            return false;                              /* :58  armed reject */
        }
    }
    return true;
}

(2) Every session start disarms the gate — downlink.c:122:

downlink.flags = POUCH_ATOMIC_INIT(0);                 /* clears SESSION_VALID (and SESSION_HAS_POUCH) */

SESSION_VALID is re-set only after a block decrypts (downlink.c:169); session_end
clears only SESSION_ACTIVE, not re-arming the gate. So any session start whose
blocks never decrypt leaves the gate disarmed.

(3) The advance is unconditional and never reset — saead_downlink_block_decrypt,
downlink.c:173-177:

if (downlink.id.initiator == POUCH_ROLE_SERVER
    && downlink.id.type == SESSION_ID_TYPE_SEQUENTIAL)
{
    server.seqnum = downlink.id.value.sequential.seqnum;   /* :176  UNCONDITIONAL — can move DOWN */
}

server.seqnum has exactly this one writer and no reset in the tree. seqnum
arrives in the cleartext, unauthenticated CBOR pouch header.

The attack

Device booted (server.seqnum = 0); attacker recorded genuine sessions at seq=50
and seq=100:

#	event	result	server.seqnum / VALID
1	genuine seq=50, block decrypts	accept	50 / 1
2	genuine seq=100, block decrypts	accept	100 / 1
3	genuine seq=101 header passes the gate; attacker drops the block	header ok, decrypt fails	100 / 0 ← :122 disarmed
4	replay recorded seq=50	:41-45 accept; recorded ct verifies; :176 writes	50 / 1 ← DOWNGRADE
5	replay recorded seq=100 (already consumed at step 2)	100 > 50 → ACCEPTED	100 / 1

Step 3 needs no key material — a fabricated header with any seq > server.seqnum
is accepted (session-key generation never fails on an attacker-chosen id), and
simply dropping one genuine block suffices. The value written at :176 is
constrained to seqnums for which the attacker holds genuine recorded ciphertext
(the write is downstream of psa_aead_decrypt succeeding) — i.e. exactly a replay,
which is what the counter exists to stop.

Collateral: the pouch-id replay guard is dead code

saead_downlink_pouch_start (downlink.c:140) guards on
SESSION_HAS_POUCH && id <= server.pouch_id. Its only caller (crypto_saead.c:91)
runs immediately after saead_downlink_session_start (crypto_saead.c:80), which
cleared SESSION_HAS_POUCH at downlink.c:122. The guard's SESSION_HAS_POUCH
term is therefore always false, so the pouch-id replay protection never fires on
any path. Same root cause (state cleared at session start, checked before any
decrypt re-arms it).

Confirmation

This is a protocol-logic defect, not a memory-safety bug — so AddressSanitizer is
not the detector. The confirmation is a behavioral witness (W7a-witness.c) that
transcribes the gate state machine (is_valid_downlink, the :122 disarm, the
:176 advance) and replays the sequence above. It is compiled under
-fsanitize=address specifically to demonstrate that the attack produces no
memory error — which is precisely why fuzzers and sanitizer-based tests do not
catch it:

cc -g -fsanitize=address W7a-witness.c -o w7a && ./w7a          # shipped logic
[W7-a witness | shipped src/saead/downlink.c]
  1| genuine seq=50 ...                      -> accept   server.seqnum= 50 VALID=1
  2| genuine seq=100 ...                     -> accept   server.seqnum=100 VALID=1
  3| seq=101 hdr; attacker DROPS the block   -> hdr-ok/dec-fail server.seqnum=100 VALID=0
  4| REPLAY recorded seq=50 ...              -> accept   server.seqnum= 50 VALID=1  <== DOWNGRADE
  5| REPLAY recorded seq=100 (consumed @2)   -> accept   server.seqnum=100 VALID=1
  W7A-REPLAY-CONFIRMED (mark moved DOWN 100->50; consumed replay re-accepted)

ASan reports nothing (memory-clean); the violation is the non-monotone high-water
mark and the re-accepted replay. Rebuilt with -DFIX (the §1 guard below) the same
run reports W7A-NO-DOWNGRADE and step 5 becomes REJECT.

The fix

Primary — make the advance monotonic (necessary, local, behaviour-preserving on
the armed path):

--- a/src/saead/downlink.c
+++ b/src/saead/downlink.c
@@ saead_downlink_block_decrypt @@
     if (downlink.id.initiator == POUCH_ROLE_SERVER
         && downlink.id.type == SESSION_ID_TYPE_SEQUENTIAL)
     {
-        server.seqnum = downlink.id.value.sequential.seqnum;
+        /* Advance the replay high-water mark only upward, so a decrypt with a
+         * stale (<= current) seqnum can never lower it and re-open the window. */
+        if (downlink.id.value.sequential.seqnum > server.seqnum)
+        {
+            server.seqnum = downlink.id.value.sequential.seqnum;
+        }
     }

On the intended armed-gate path the is_valid_downlink check already forced
seq > server.seqnum, so this is behaviour-preserving there; off it, a
stale/replayed id can no longer roll the mark backward.

This guard is necessary but NOT sufficient. With it, step 4's replay is still
accepted and delivered to the application — only the persistent widening (step 5)
is prevented. The root cause is (1)+(2): the gate is disarmed on every session
start. A complete fix must additionally stop clearing SESSION_VALID on session
start, or make the sequential-seqnum check in is_valid_downlink consult
server.seqnum unconditionally rather than only when a prior session was
validated — so that seq <= server.seqnum is rejected even on the
"no previous session" branch. The pouch-id guard (collateral above) should likewise
be evaluated before the session-start clear, not after.

How this was found

Deductive proof of src/saead/downlink.c against a Lean model of the
replay direction (Direction.advance = if highWater < seq then seq else highWater).
The pristine C advance is unconditional, so it matches the model only on the domain
seq > server.seqnum — a call-graph assumption (that decrypt runs only after an
armed accept gate) that the witness refutes: session start disarms the gate on
the ordinary path, so decrypt can run with seq <= server.seqnum. The primary guard
above turns the write into server.seqnum = max(server.seqnum, seq), matching the
model on the whole domain and making the monotonicity property a local,
single-function post-condition (no cross-function assumption).

[trond-snekvik]

The issue identified in this PR is correct, but the fix only addresses one consequence of the bug, and not the bug itself.

I'm working on a fix to the core issue itself, but there are a few corner cases to cover here. I'll make a separate PR, and we can decide whether we want to do this as an additional safe guard or whether the issue can be closed.