[
https://issues.apache.org/jira/browse/HDDS-16566?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18129139#comment-18129139
]
Siyao Meng commented on HDDS-16566:
-----------------------------------
Verification run complete. The Specula pipeline ran all phases against the
pinned commit: code analysis, TLA+ specification generation, harness and trace
collection, trace validation plus TLC model checking, bug confirmation with the
adversarial Challenger debate, and severity classification.
h3. Run environment
{noformat}
Ozone commit: b94df213f20ec0d675f079b57a4566e4e64e4060
Specula: v1.2.0-34-gcdd19e39 (with local changes)
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 5h 7m agent time, 81.6M tokens, about $53 (estimate)
{noformat}
h3. Result
13 candidate findings came out of model checking (5) and code review (8), and
all 13 were investigated individually. No spec repair request stayed open after
confirmation.
||Disposition||Count||
|Reproduced|7|
|Masked (defect present, harm prevented by another component today)|1|
|False positive|3|
|Dropped (already reported upstream)|2|
Two reproduced findings share one fix, so they are one issue. Each issue was
then validated a second time by hand against the pinned commit: a regression
test was added to an existing suite and shown to fail without the fix and pass
with it, the bug was confirmed still present on apache master (checked on
2026-10-20), and the fix patch, reproduction and report were reviewed
independently before filing.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17177|Major|OM renew delegation token apply can write a canceled token
back and can lower a token's stored expiry|
|HDDS-17176|Major|Delegation token is still accepted after its max date when
the renew interval is longer than the max lifetime|
|HDDS-17179|Major|OM skips the secret key expiry check before symmetric token
signing is finalized, so a runtime finalize issues tokens that fail early|
|HDDS-17175|Minor|Expired delegation token remover can drop a renew applied
during its scan, so the OM rejects the token before its renewed expiry|
|HDDS-17178|Minor|Stopped OM delegation token secret manager stays registered
with the certificate client, so a checkpoint install leaks the replaced manager|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch and a standalone reproduction test attached.
h3. Not filed
* Reproduced, not filed: a leader that has lost its majority but has not yet
stepped down still accepts a delegation token that was canceled through the new
leader. This is the same stale leader window that other OM reads have
(HDDS-16435), and it is bounded by the Ratis leader step down timeout. A
contained fix would add a Ratis round trip to every token authentication.
* Masked: followers do not advance the token sequence number when they apply an
issued token, so a new leader reuses sequence numbers after a failover. Tokens
are compared by the full identifier, and sequence numbers are already reused on
one OM after a restart.
* False positive: the expired token remover calling {{Runtime.exit}} could
block OM shutdown. No reachable unchecked exception was found, and the wait is
bounded by the shutdown hook timeout.
* False positive: an unused local variable in the token issue path.
* False positive: a cancel retried after the Ratis retry cache entry expired
fails with token not found. This is the documented retry cache behaviour shared
by all OM writes.
* Dropped: expired tokens deleted from RocksDB outside Ratis while tokens are
loaded is HDDS-13450 (closed as a duplicate of HDDS-13457).
* Dropped: a token left out of memory when the secret key lookup fails during
load is HDDS-16959.
h3. Reproduce
{code:none}
specula run --agent=claude-code --effort=medium --model='claude-opus-5-5[1m]' \
--max-parallel=2 --enable-reviews --confirm-debate \
--tlc-memory-limit=28G --tlc-worker-limit=8 \
"om-delegation-token|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17177 and HDDS-17175 need a request to be applied while the stored token
state differs from the state it was validated against (HDDS-17177), or during
one remover scan of that token (HDDS-17175). The attached tests reach that
state through internal calls, without Ratis or a second OM.
* HDDS-17177 keeps the record of applied cancels in memory, so an OM that
restarts or installs a checkpoint between two related log entries behaves as
all OMs do today. The issue names a persisted alternative.
* HDDS-17176 needs {{ozone.manager.delegation.token.max-lifetime}} below
{{ozone.manager.delegation.token.renew-interval}}; default configs do not
trigger it.
* HDDS-17179 needs a secure cluster that has not finalized layout version 8 and
an explicit {{hdds.secret.key.expiry.duration}} that breaks the HDDS-13343
rule. With the patch such an OM refuses to start before finalization instead of
failing later.
* HDDS-17178 was reproduced by replaying the secret manager calls of a
checkpoint install, not by a real install on a secure HA cluster.
* The patches were built and tested on the pinned commit and apply to master at
df42f7f60a2. HDDS-17177, HDDS-17176, HDDS-17175 and HDDS-17178 add tests to
{{TestOzoneDelegationTokenSecretManager}}, so after the first one lands the
others need a trivial rebase of that file; their main code changes combine
cleanly. HDDS-17179 and the open HDDS-16958 change the same startup check.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-delegation-token (Apache Ozone master @b94df21)
> -------------------------------------------------------------------
>
> Key: HDDS-16566
> URL: https://issues.apache.org/jira/browse/HDDS-16566
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: om-delegation-token.guidance.md
>
>
> This is a runnable Apache Ozone formal-verification target for the Specula
> pipeline (TLA+ model checking plus trace validation against the real code).
> It has not been run yet. Anyone can pick it up: run Specula against the
> pinned commit, then report findings on this issue. Part of umbrella
> HDDS-15926.
> h3. Target
> {{om-delegation-token}}. Scope and code entry points are in the attached
> guidance file [^om-delegation-token.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: b94df213f20ec0d675f079b57a4566e4e64e4060
> Specula: https://github.com/specula-org/Specula (v1.1.0 or later)
> Toolchain: JDK 21, ~28 GB RAM for TLC, an LLM coding agent
> (claude-code or codex adapter)
> Runtime: hours per target; needs an agent API budget
> {noformat}
> h3. How to run
> # Clone Specula and install per its README; clone apache/ozone and check out
> the pinned commit above.
> # Place the attached guidance file as the target's .prompt-extra.md (see the
> Specula README for target layout).
> # Run:
> {code:none}
> specula run --agent=claude-code --effort=medium --keep-original
> --max-parallel=2 \
> --enable-reviews --confirm-debate --tlc-memory-limit=28G
> --tlc-worker-limit=8 \
> "om-delegation-token|apache/ozone|Java|Use the target-specific
> .prompt-extra.md"
> {code}
> # Deliverables land under the run's {{.specula-output/}}:
> {{confirmed-bugs.md}}, {{bug-severity.md}}, {{summary.md}}, and
> {{confirmation/<id>/investigation.md}}.
> h3. Reporting results
> Comment here with the outcome (0 findings is still useful: it records the
> target as covered at this commit). For each confirmed bug, file a separate
> Ozone Bug and link it to this issue with the "Testing" link type ("Testing
> discovered").
> h3. Notes
> * The attached guidance file names an earlier commit ({{20e6a1c}}); use the
> commit above. Code entry-point line numbers in the guidance were captured at
> an earlier commit and may have shifted on this head; treat them as
> approximate. Specula re-analyzes the source, so the run does not depend on
> them.
> * Recon-building targets need a local Specula patch to skip Maven {{target/}}
> out-of-tree symlinks in {{snapshotlib._validate_source_tree}}, else the run
> crashes at finalize.
> * effort=medium is the tested default for large targets; effort=high can hit
> per-turn timeouts on the biggest ones.
> * Findings are proposals, to be confirmed by human review and testing before
> any fix is merged.
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
