Repository navigation
Conversation
…ess seed walk.Seed.access names an instruction offset and an access, by operand or by its position in the footprint, with whether what it reads is secret. an access the walk places off no symbol and in no frame slot takes it in place of may-alias with every held extent, for loads, pushed values and atomic results alike, and a secret stored where it states none is refused.
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.
Closes #563
What
The constant-time walk takes the producer's statement of what an unplaced memory access reads, in place of may-alias with every held extent.
walk.Seed.access: walk.Accessis the new seed.Access{at, access, secret}names the instruction offset and the access, with whether what it reads may hold a secret.walk.Accessornames the access asoperand{u8}on register machines (the operand the footprint states the access through, or the memory operand) or asindex{u32}, its position infp.memory, for an access no operand names, as on wasm.reads_secret, which answers the seed for a seeded touch. So a load's written register, a wasm load's pushed value, and the old value an atomic rmw or cmpxchg returns take the seed's secrecy, joined with the rest of what the instruction reads.ct.STORED.UNSEEDABLE. One within an instruction, or naming an access its instruction does not make, is the newUNACCESSED.masc walkgains--access <offset>:<n>=secret|public(operand n) and--access <offset>:@<n>=secret|public(footprint position n). Offsets read decimal or0xhex.Decisions
ct.STORED("secret value stored to memory stated public"). This checks the producer's claim where it could be broken, so a public seed never hides a secret the walk saw stored. A secret stored through a seeded-secret access is placed as any other store is today (held, oreverywherewhen unlocated), because unseeded and placed accesses still read through the extents. A public store does nothing, as today, so a public-seeded access never marks memoryeverywhere.Seed.memoryoff a register and an access off it gets the access seed for that access.ct.STOREDis a newct.Reason(5,REASONS= 6). It is additive. mirl reports refusals throughct.message/ct.spell, which word it.Consumer changes
mirl builds, per unplaced access whose secrecy its types state:
and on wasm, where the address is popped:
Notes
machd check . -a '*'andmachd fmt .. No artifact builds, no gen, no new unit tests and no tool comparison, per the v7 rules.