Skip to content

Messages recipients may be omitted #133

@lukaszcz

Description

@lukaszcz

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.

  1. Top-level action:
    • consumed object resources: none
    • created object resources: none
    • consumed message resources: none
    • created message resources: TwoCounter.inc (recv := self)
  2. Action for TwoCounter.inc on self:
    • 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)
  3. Action for Counter.inc on self.cnt1:
    • consumed object resources: self.cnt1
    • created object resources: self.cnt1 with count := self.cnt1.count + 1
    • consumed message resources: Counter.inc (recv := self.cnt1)
    • created message resources: none
  4. Action for "fake" Counter.inc on self.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

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions