[
https://issues.apache.org/jira/browse/HDDS-17230?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18131260#comment-18131260
]
Siyao Meng commented on HDDS-17230:
-----------------------------------
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: 5f7111a27ea07ce6b7bf5284a4213ebacb65f2ae
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: 2h 48m agent time, 57.7M tokens, about $39 (estimate)
{noformat}
h3. Result
9 candidate findings came out of model checking (4) and code review (5), and
all 9 were investigated individually. No spec repair requests were raised by
confirmation.
||Disposition||Count||
|Reproduced|4|
|Masked (defect present, harm prevented by another component today)|1|
|False positive|4|
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-23), and the fix patch and report were reviewed
independently before filing. The masked finding shares the fix of one
reproduced finding and is part of that issue. One more defect of the same kind
was found during review and is filed as well.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17406|Major|Revoked STS token purge deletes cutoffs without checking
their current value and leaves purged entries in the table cache|
|HDDS-17408|Major|STS revocation cutoff is overwritten on apply, so a revoke
applied with a lower stamp lowers the stored cutoff|
|HDDS-17409|Major|Revoking an S3 secret should record an STS revocation cutoff
for the access id|
|HDDS-17410|Major|Revoking a tenant access id should record an STS revocation
cutoff for the access id|
|HDDS-17407|Minor|Revoked STS token cleanup threshold equals the maximum token
lifetime and leaves no margin for clock differences between OMs|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch with its regression tests attached; no
standalone reproduction is attached. HDDS-17410 was found during review of
HDDS-17409, not by the pipeline.
h3. Not filed
* False positive: a request validated against the revocation state before a
revocation is applied completes after it. That matches the documented
revocation contract.
* False positive: a token created in the same millisecond as the cutoff, or by
an OM whose clock is ahead, survives the strict {{creationTime < cutoff}}
comparison. The comparison is the documented contract, and the wider window
needs clock skew beyond the deployment's time sync requirement.
* False positive: a deposed leader that is not yet aware of it can serve
validation from stale revocation state under the DEFAULT read option. That is
the documented behaviour of non linearizable reads.
* False positive: STS tokens without an issue date are rejected. Only an
unreleased build could have issued them.
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-sts-token-lifecycle|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* STS is not part of any Ozone release yet (the release tags up to 2.2.1 have
no STS revocation code), so all five issues affect 2.3.0 only. HDDS-17406 adds
a field to an unreleased request type and should land before the first release
with STS.
* Landing order: HDDS-17407 before or with HDDS-17406. HDDS-17408 with or after
HDDS-17406; both change the test setup of {{TestS3RevokeSTSTokenRequest}}, so
the second one to land needs a rebase. HDDS-17409 and HDDS-17408 add the same
"keep the larger cutoff" step and the second one should share one helper.
HDDS-17410 applies on top of HDDS-17409.
* The multi OM effects were reproduced with the real request, response, cleanup
and validation classes on separate {{OmMetadataManagerImpl}} instances, with
Ratis and the double buffer simulated and the commit, apply and flush order and
the per OM clocks set by the test. Nothing was run on a mini cluster with
several OMs.
* The patches were built and tested on the pinned commit and apply to master at
65320362775.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-sts-token-lifecycle (Apache Ozone master @5f7111a)
> ----------------------------------------------------------------------
>
> Key: HDDS-17230
> URL: https://issues.apache.org/jira/browse/HDDS-17230
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: om-sts-token-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
> {{om-sts-token-lifecycle}}. Scope and code entry points are in the attached
> guidance file [^om-sts-token-lifecycle.guidance.md]. Added after the S3 STS
> feature branch (HDDS-13323) was merged; no earlier target covers STS tokens
> or their revocation.
> h3. Run environment
> {noformat}
> Apache Ozone commit: 5f7111a27ea07ce6b7bf5284a4213ebacb65f2ae
> 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-sts-token-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 ({{20d95ed}}); 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
(v10.3.26#10030026)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
