-
Notifications
You must be signed in to change notification settings - Fork 5
Closed
Labels
bugSomething isn't workingSomething isn't working
Description
After moving message logic to object RLs, the RLs of message resources are trivial - always succeed. But this means that there is no check that message recipients are actually present, so they can just be omitted. This makes it possible to circumvent the message logic by not including the recipients.
For example, consider the following AVM program in pseudocode:
class Counter
count : Nat
constructor create
return {count := 0}
method inc (self : Counter)
return {self with count := self.count + 1}
class TwoCounter
cnt1 : Reference Counter
cnt2 : Reference Counter
constructor create
cnt1 := Counter.create
cnt2 := Counter.create
return {cnt1, cnt2}
method inc (self : TwoCounter)
self.cnt1.inc ()
self.cnt2.inc ()
return self
It is possible to create the following valid transaction with all RLs satisfied.
- Top-level action:
- consumed object resources: none
- created object resources: none
- consumed message resources: none
- created message resources:
TwoCounter.inc (recv := self)
- Action for
TwoCounter.inconself:- consumed object resources:
self - created object resources:
self - consumed message resources:
TwoCounter.inc (recv := self) - created message resources:
Counter.inc (recv := self.cnt1),Counter.inc (recv := self.cnt2)
- consumed object resources:
- Action for
Counter.inconself.cnt1:- consumed object resources:
self.cnt1 - created object resources:
self.cnt1withcount := self.cnt1.count + 1 - consumed message resources:
Counter.inc (recv := self.cnt1) - created message resources: none
- consumed object resources:
- Action for "fake"
Counter.inconself.cnt2:- consumed object resources: none
- created object resources: none
- consumed message resources:
Counter.inc (recv := self.cnt2) - created message resources: none
This transaction increments only the first counter, violating the invariant implicit in the definition of TwoCounter.
Action 4 is okay because the RL of the consumed message resource is trivial – it should instead check if the recipient is present in the action.
Metadata
Metadata
Assignees
Labels
bugSomething isn't workingSomething isn't working