[
https://issues.apache.org/jira/browse/HDDS-16543?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18126555#comment-18126555
]
Siyao Meng commented on HDDS-16543:
-----------------------------------
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: 025266b52a6dcaf39508607cad736799c40907e8
Specula: v1.2.0 with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 7h 58m agent time, 121.6M tokens, about $97 (estimate)
{noformat}
h3. Result
13 candidate findings came out of model checking (4) and code review (9), and
all 13 were investigated individually.
||Disposition||Count||
|Reproduced|9|
|Masked (defect present, harm prevented by another component today)|2|
|Environment limited|1|
|False positive|1|
In every reproduced case the secret key lifecycle fails closed: valid tokens
are rejected, in several cases until a restart or an operator action. No case
was found in which an invalid token is accepted.
Each finding that went forward was 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, and the fix patch, the reproduction and
the report were reviewed independently before filing. Two reproduced findings
share one fix and are one issue. Three further issues were found during
validation and review and are filed as well: HDDS-16961, HDDS-16962 and
HDDS-16964.
h3. Filed
||Issue||Type||Priority||Summary||
|HDDS-16956|Bug|Major|SCM secret key file is rewritten in place without sync: a
crash can leave it empty or cut, and a new leader then drops the keys or cannot
initialize|
|HDDS-16957|Bug|Major|Datanode caches a "no such secret key" answer from a
stale SCM leader and keeps rejecting tokens signed with that key|
|HDDS-16959|Bug|Major|OM drops persisted delegation tokens from memory when the
secret key fetch from SCM fails during token load|
|HDDS-16960|Bug|Major|One failed poll for the current secret key permanently
stops the secret key refresh in OM and datanodes|
|HDDS-16963|Bug|Major|SCMSecurityProtocolServer.checkAndRotate does not call
checkAdminAccess|
|HDDS-16964|Bug|Major|SCMSecurityProtocolServer serves the secret keys without
checking the caller for a service identity|
|HDDS-16962|Improvement|Major|Secret key verifier fetches every key id it does
not hold from SCM on the verifying thread; refresh the key set or bound the
lookup|
|HDDS-16955|Bug|Minor|SCM secret key rotation proposed after a Ratis submit
timeout drops the key of the timed out rotation on all SCMs|
|HDDS-16958|Bug|Minor|OM delegation token and secret key duration guard ignores
hdds.secret.key.rotate.check.duration|
|HDDS-16961|Bug|Minor|ozone admin om fetch-key does not make OM fetch the
current secret key from SCM, it prints the key OM already has|
Priorities follow the manual validation, not the pipeline's severity classes.
HDDS-16955 to HDDS-16961 each have a proposed fix patch and a standalone
reproduction test attached. HDDS-16963 and HDDS-16964 have a fix patch with a
regression test and no standalone reproduction. HDDS-16962 is a proposal
without a patch.
h3. Not filed
* Reproduced: an SCM that is restarted with security switched off on a
previously secure HA group terminates when it applies a replicated key update.
Switching security off on a secure group is not a supported operation, the SCM
stops without losing anything, and the other SCMs keep serving.
* Masked: a new SCM leader can be ready before it has a current secret key, and
in process container token signing fails during that window. It heals with the
pending proposal or the next rotation check, and it was shown only with a
stubbed Raft layer and an injected lost write.
* Masked: the size of the verifier's key cache. The part of it that matters is
covered by the patch of HDDS-16957, and the lookup model is the subject of
HDDS-16962.
* Environment limited: a forced rotation on a leader whose clock is behind the
creation time of the current key reports success and leaves the signing key
unchanged until a later rotation. It needs clock skew between SCM hosts beyond
what a time synchronized deployment has and could only be emulated inside one
JVM.
* False positive: a zero {{hdds.secret.key.rotate.duration}} leads to a
division by zero in the verifier client. That is a refusal to start on an
unsupported value, with a logged stack trace.
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 \
"scm-secret-key-lifecycle|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* The cluster reproductions run on in JVM mini clusters, and most need help
with timing. HDDS-16955 needs two rotation proposals to time out without a
leader change (the reproduction lengthens the Ratis election timeout and holds
back a follower). HDDS-16957 needs a verifier to ask a deposed leader inside a
window that is below one second at default timeouts (the reproduction delays
Raft messages). HDDS-16959 needs an OM restart while a new SCM leader is still
initializing its keys (the reproduction delays that initialization). HDDS-16960
was run with shortened client retries, the default of 10 minutes was not run.
* HDDS-16956: the power loss route was shown only for the first save of the key
file on XFS, with a device image test that is not attached. The process kill
route is in the attached test. Its patch stops new damage and does not change
what a leader does with a key file that is already missing, empty or cut. It
relates to HDDS-16923, and the two patches apply together.
* HDDS-16958 cannot be reached with default settings. Its patch makes OM refuse
to start on configurations that pass the current check and not the corrected
one, which needs a release note.
* HDDS-16961: the command has had no effect since 2.0.0. It is not needed for
normal operation, because OM polls for the current key on its own.
* The patches were built and tested on the pinned commit and apply to master at
4389803780f. All nine apply together. HDDS-16963 and the open HDDS-16936 add a
line at the same place in one test, so the second of those to land needs a
trivial rebase.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5, Claude Fable 5.1).
> [Specula] Verify scm-secret-key-lifecycle (Apache Ozone master @025266b)
> ------------------------------------------------------------------------
>
> Key: HDDS-16543
> URL: https://issues.apache.org/jira/browse/HDDS-16543
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: scm-secret-key-lifecycle.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
> {{scm-secret-key-lifecycle}}. Scope and code entry points are in the attached
> guidance file [^scm-secret-key-lifecycle.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: 025266b52a6dcaf39508607cad736799c40907e8
> 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 \
> "scm-secret-key-lifecycle|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]
