Track: unsound tracked token manipulation

[rikosellic]

This list tracks some tracked token manipulations, which can be unsound (keep updating). @SNoAnd @hiroki-chen @Marsman1996, I do not perceive any immediate threat to the soundness proof of executable codes, but these should be solved to make the verification solid.

• tracked_mint_frame_obligation duplicates a tracked token (which obviously violates the tracked mode semantics) to track leaked frames. This should be solved by authoritative resource algebra.
• tracked_from_unused_owner creates an M::owner out of thin air in UniqueFrame::from_unused. I think there is an overlap between the M:OwnerOf trait bound and the M:Repr<MetaSlotStorage>, because both of them represent the permission to access the metadata. We should find a unified way to represent it to make migration easier when trait objects are better supported in Verus.

[hiroki-chen]

For the second point, my understanding is that the purposes of M: Repr<MetaSlotStorage> and OwnerOf are indeed different because the first says how you can put M into a MetaSlotStorage while the second says what kind of tracked owner you'll need to properly access the thing guarded by it. They happen to be the same thing for Frames though.

[rikosellic]

For the second point, my understanding is that the purposes of M: Repr<MetaSlotStorage> and OwnerOf are indeed different because the first says how you can put M into a MetaSlotStorage while the second says what kind of tracked owner you'll need to properly access the thing guarded by it. They happen to be the same thing for Frames though.

Thanks! I understand your point now. Taking PageTablePageMeta for example, MetaSlotStorage permits us to access the nr_children field, but we still need the PCell::PointsTo in PageMetaOwner to obtain the actual value.

But this does not explain why UniqueFrame has this OwnerOf while Frame does not. If we need OwnerOf to track the specific owner of the MetaData, and UniqueFrame can take it out because of exclusive ownership, then Frame should also have the OwnerOf bound to allow at least some shared read access. This is inconsistent, and I discovered several soundness issues:

• During creation of Frame or UniqueFrame, the owner of the metadata should be passed in along with the metadata value itself. Now UniqueFrame magically creates one, while Frame just ignores this part.
• This special owner is not stored in MetaRegionOwners, so we just lost them for Frames.
• MetaSlotStorage design is outdated because it follows the enum-based metadata design before 0.16.0.

[rikosellic]

@SNoAnd what do you think about this? Currently, the special owner of PageTablePageMeta is collected in PageMetaOwner and wrapped in NodeOwner, but the special owner for other kinds of metadata just vanishes because it is not considered in the MetaSlotRegion system in the first place (only UniqueFrame considers this). Ideally, I think these owners should also be recorded in MetaSlotRegion, then we can have a unified permission struct that can be used anywhere, making the single-threaded verification perfectly sound and elegant.

[hiroki-chen]

For the second point, my understanding is that the purposes of M: Repr<MetaSlotStorage> and OwnerOf are indeed different because the first says how you can put M into a MetaSlotStorage while the second says what kind of tracked owner you'll need to properly access the thing guarded by it. They happen to be the same thing for Frames though.

Thanks! I understand your point now. Taking PageTablePageMeta for example, MetaSlotStorage permits us to access the nr_children field, but we still need the PCell::PointsTo in PageMetaOwner to obtain the actual value.

But this does not explain why UniqueFrame has this OwnerOf while Frame does not. If we need OwnerOf to track the specific owner of the MetaData, and UniqueFrame can take it out because of exclusive ownership, then Frame should also have the OwnerOf bound to allow at least some shared read access. This is inconsistent, and I discovered several soundness issues:

• During creation of Frame or UniqueFrame, the owner of the metadata should be passed in along with the metadata value itself. Now UniqueFrame magically creates one, while Frame just ignores this part.
• This special owner is not stored in MetaRegionOwners, so we just lost them for Frames.
• MetaSlotStorage design is outdated because it follows the enum-based metadata design before 0.16.0.

I do agree with you. The most unsound part of it is that M::Owner is being created out of nowhere.