Repository navigation
fix(kms-auth)!: make DstackApp allowAnyDevice cover every app epoch - #1568
Merged
Merged
Conversation
Which hosts may run an app is not a property of a key generation, and a per-epoch switch is easy to get wrong: restricting the current epoch leaves any older row that allows any device open to every host, which can still fetch that epoch's keys. Make allowAnyDevice one switch again. - setAllowAnyDevice(bool) replaces setAllowAnyDeviceAtEpoch(s) and the allowAnyDeviceAtEpoch getter. It is the selector apps predating app epochs already have, so Manage.s.sol SetAllowAnyDevice calls it on either kind and takes no epoch. - Device ID rows stay per epoch. The decision is now allowAnyDevice or the selected epoch's device row. - Drop the unreleased _allowAnyDeviceByEpoch slot; the gap grows by one. - IAppEpochManagement swaps the two epoch setters for setAllowAnyDevice; its interface ID becomes 0xc65f31b6. BREAKING CHANGE: unreleased only: setAllowAnyDeviceAtEpoch(s), allowAnyDeviceAtEpoch and the IAppEpochManagement interface ID. Signed-off-by: Kevin Wang <wy721@qq.com>
- Correct the AllowAnyDeviceSet NatSpec and the epoch-zero-only notes in app-key-epochs.md, which allowAnyDevice no longer follows. - SetAllowAnyDevice refuses APP_EPOCH and FROM_/TO_APP_EPOCH instead of ignoring them, since it changes every epoch. - Check the legacy-equals-epoch-0 Halmos property with a symbolic allowAnyDevice, and that an upgraded any-device app stays open to unlisted devices at later epochs. - Tidy spec and formal-verification wording. Signed-off-by: Kevin Wang <wy721@qq.com>
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.
Which hosts may run an app is not a property of a key generation, and a per-epoch switch is easy to misuse: restricting the current epoch leaves any older row that allows any device open to every host, which can still fetch that epoch's keys.
setAllowAnyDevice(bool)replacessetAllowAnyDeviceAtEpoch(s)andallowAnyDeviceAtEpoch. Apps predating app epochs already have that selector, soManage.s.sol:SetAllowAnyDeviceuses it on both kinds and takes no epoch.allowAnyDevice || deviceRow[epoch][deviceId]._allowAnyDeviceByEpochslot (gap +1).IAppEpochManagementswaps the two epoch setters forsetAllowAnyDevice; its interface ID becomes0xc65f31b6.Breaking only for unreleased API. dstack-auth's
allowAnyDeviceis already global.Tests:
forge clean && forge test --ffi(111 passed); Halmos (FOUNDRY_DYNAMIC_TEST_LINKING=false):DstackAppSymbolicTest5/5,DstackAppEpochSymbolicTest9/9,DstackKmsEpochSymbolicTest13/13.