Repository navigation
Conversation
A request may select any epoch up to the current one and is decided on that epoch's row, but the epoch-less setters only wrote rows from the current epoch on. After a rotation, removing an OS image, compose hash or device left older rows granting it. - DstackKms: drop the epoch-less add/remove setters for OS images, KMS aggregated MRs and KMS devices. Keep the *AtEpoch setters and add *AtEpochs(fromEpoch, toEpoch, value) range setters, so the caller names the rows and one transaction revokes a value from every row. - DstackApp: the IAppAuthBasicManagement setters and setAllowAnyDevice keep their ABI and interface ID but now write every row from 0 through the next epoch, so a removal is a full revocation. - Key root policy rows by registration instead of chain hash. A popped epoch re-registered with the same keys had the same chain hash and got its old rows back; every registration now starts with empty rows. Epoch 0 still uses the v0.5.x mappings. - Cap kms_serve at the current root epoch. Only the key handover operations may select a pending epoch. - Manage.s.sol KMS scripts take ROOT_EPOCH or FROM_ROOT_EPOCH and TO_ROOT_EPOCH. By default additions write the current through the latest epoch, and removals write every row. - Fix two stale DstackKms comments: evidence report data does not bind the epoch, and KMS authorization does not check the app ID. Signed-off-by: Kevin Wang <wy721@qq.com>
Disk and env migration fetch the keys of the recorded epochs, so an image not allowed in those rows stops boot. Say which root and app epoch it was. Signed-off-by: Kevin Wang <wy721@qq.com>
The symbolic checks cover properties no Forge test covers, such as epoch monotonicity and the legacy entry points refusing after rotation. Run each suite in its own job when dstack/kms/auth-eth changes, with Halmos and Forge pinned. Signed-off-by: Kevin Wang <wy721@qq.com>
kvinwang
added a commit
that referenced
this pull request
Nov 11, 2026
Add the deployment order, the GET /app/:appId backend requirement, the per-epoch setter semantics from #1561, the removed DstackKms setters and legacy KMS info setters, two-step ownership for v0.5.9 proxies, dstack-auth pending-epoch handover, and the reorg caveat of non-finalized block tags. Signed-off-by: Kevin Wang <wy721@qq.com>
Signed-off-by: Kevin Wang <wy721@qq.com>
As in DstackKms, every DstackApp setter now names the app epoch rows it writes: *AtEpoch one row, and new *AtEpochs(fromEpoch, toEpoch, ...) a range up to the next epoch. The epoch-less addComposeHash, removeComposeHash, addDevice, removeDevice and setAllowAnyDevice are gone, and with them IAppAuthBasicManagement (0x8fd37527). The new IAppEpochManagement interface (0x853d2b79) lets tools tell current apps from those predating app epochs. App policies deployed from v0.5.9 and v0.6.0 keep working under the upgraded DstackKms: it authorizes them through isAppAllowed for app epoch 0 only. Manage.s.sol detects them by interface ID and calls their epoch-less setters, accepting only APP_EPOCH=0 or no epoch. For current policies, and for every KMS script, it requires an explicit epoch or range. Upgrading an old app keeps its allowlist as app epoch 0. New tests cover both releases against the upgraded KMS, before and after a root rotation, the interface IDs, and the upgrade. Formal verification: - The Halmos properties now cover symbolic ranges, full-range revocation on both sides, empty rows after pop and re-registration, epoch 0 rows being the legacy mappings, and legacy app policies limited to app epoch 0. - New TLA+ model EpochPolicy covers registration-keyed rows, range writes, pop and re-registration, legacy apps and their upgrade, and key release on the selected rows. Two mutation configs show the chain-hash keying and a legacy fallback that ignores the app epoch each break it. Signed-off-by: Kevin Wang <wy721@qq.com>
kvinwang
added a commit
that referenced
this pull request
Nov 11, 2026
…support Follow #1561: DstackApp loses its epoch-less setters and IAppAuthBasicManagement, reports IAppEpochManagement, and app policies predating app epochs keep working at app epoch 0. Signed-off-by: Kevin Wang <wy721@qq.com>
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Round 2 review of #1533: item 1/4, the contract side of 2/4, and the follow-ups in #122-#124.
A request may select any epoch up to the current one and is decided on that epoch's row. The epoch-less setters only wrote the current row and the ones after it, so after a rotation a removal still left older rows granting the value.
DstackKmsandDstackAppdrop their epoch-less material setters. Every setter now names its rows:*AtEpochwrites one row,*AtEpochs(fromEpoch, toEpoch, value)a range (up to the next epoch for apps). One transaction can revoke a value from every row.DstackAppno longer reportsIAppAuthBasicManagement(0x8fd37527). It reports the newIAppEpochManagement(0x853d2b79) instead, so tools can tell current apps from older ones.DstackKms, at app epoch 0 only.Manage.s.soldetects them and calls their epoch-less setters. Upgrading one keeps its allowlist as app epoch 0. For every other script, an explicit epoch or range is now required.kms_serveis capped at the current root epoch.EpochPolicy, check the new semantics, with two mutation configs as controls.Tests:
LegacyAppCompatandManageScriptsuites.EpochPolicyholds over 6,104,564 states, and both mutation configs fail as expected.