Semantics of non-methods in the object system

Protocol Design
1

This post contains some thoughts on the relationship between object behaviour and resource behaviour and in particular the semantics of non-method calls.

An example situation in the RM realm

Let’s consider the following situation: imagine we have an action with a bunch of resources. We go through all resources in the action and prove their logics one by one. The logic of resource R only approves the transition if there is a corresponding resource Q in the same action. The question is: can it happen that two same kind resources Q and Q' are in the same action and only one of them is used to verify constraints of multiple resources instead of each corresponding to the designated case?

It shouldn’t be, but it isn’t clearly specified right now how to prevent this. So far it has only been done “manually”.

  • Often it isn’t possible because this is wrong on the application logic level, like in the example of the counter.
    • If a specific resource Q is intended to be the counterparty for a certain constraint about R, we might want to have an additional logic that ensures the correspondence (if we don’t want to encode the relationship between R and Q in either R or Q explicitly).
  • If the resources don’t influence each other, they can be in different actions.
  • The third case would be that some resources should be in the same action and they have the same kind, so the ordering question happens. I cannot think of an example when this is needed, but I cannot guarantee it is never the case.
    • In this case though, we don’t really care about the order as long as the same resource is not assumed to correspond to multiple consumed ones. So the question reduces to: how to prevent the resolution in which the same resource corresponds to different ones (and who performs this)? Can the user cheat and create wrong bindings when creating the proofs?

How it relates to non-method calls

First, by non-method calls here we mean the functions that do not directly compile into resource logics. This differentiation is helpful on the RM level, even though it might be meaningless on the object language level.

In some sense, if two objects are in the same non-method, these values are related and share some scope and it might make sense to compile them into a single action. But then we might end up in the situation described in the example above. On the other hand, languages allows us calling functions from other functions as many times as we want, and obviously higher level ones cannot be actions if the lower-level ones are. So to say that non-method functions always compile to actions is wrong.

The result of this post is a bunch of questions to answer:

  • what should compile to actions and what should compile to transactions?
  • how to determine what should go in the same action and what can / should be in different actions?
  • what high-level application properties signal that something has to be unique (like counter), different kinds with different labels, what requires an extra logic to ensure some explicit correspondence?
2 Likes
2

I will recapitulate here the concrete (but artificial) example of mutual counter increment, in the context of the compilation strategy @mariari proposed.

Consider:

mutualIncrement (c1 : Counter) (c2 : Counter) := 
  c1.incrementBy(value c2);
  c2.incrementBy(value c1);

Disregarding the artificiality of it, suppose we want this function compiled to a single transaction with a single action. The consumed resources are [c1, c2], created resources are [c1', c2'], and they satisfy value c1' = value c1 + value c2 and value c2' = value c2 + value c1. The resources c1', c2' have the same kind.

The problem is that the RLs for the method calls of c1.incrementBy and c2.incrementBy need to know which created resources (objects) correspond to which method call. Jeremy’s idea was to store indicators in app data that would signify that c1' is the created resource for c1.incrementBy and c2' is the created resource for c2.incrementBy. So in the app data of each (consumed) resource R in the action, we store a list of indices into the list of created resources, which indicate which created resources should be considered by the RL of R.

The problem I see is that this allows for maliciously circumventing the interface of counter objects. I’d like to understand whether my reasoning below is correct, or otherwise what I misunderstand exactly.

Nobody can tamper the app data you submit (as far as I understand), but the problem seems to be that somebody else can use this mechanism to themselves submit a transaction that would manipulate counter objects in a way that circumvents their intended interface.

Concretely, suppose someone submits a transaction with consumed resources [c1, c2] and created resources [c1', c] such that value c1' = value c1 + value c2 and value c = 0. Assume additionally that it so happens that value c1 = value c2 > 0. In app data for both c1 and c2 we indicate that c1' is the relevant created resource. The RLs for c1 and c2 will succeed because c1' is the correct increment of c1 (and of c2) by value c2 = value c1. The transaction balances: we’re consuming two resources and creating two resources of the same kind.

So we can create c with some arbitrary value in a way that is not allowed by the interface. The point is that we can prepare a transaction to consume two objects and create an unrelated object with arbitrary (legal) state in a way not intended by the object interface. Essentially, we’ve reset one of the counters to 0. This seems wrong if the interface of counter objects doesn’t allow counter destruction or decrement. In general, it seems one could use a similar trick to do an arbitrary state change, e.g., if counters had associated “colors” that were required to be preserved, one could arbitrarily change a counter’s color.

Is this a real problem or I’m misunderstanding something? Upon closer consideration, I don’t understand @mariari’s assurances why this is not possible / a problem.

I was thinking for a while that this can be solved by:

  • instead of storing a single indicator in resource’s app data, store a map from a resource to the set of indices in the created resources list,
  • check in every RL that the sets of indices define a disjoint partition of the entire list of created resources.

But this doesn’t seem to work because (with the current RM data structures at least) the RL has access only to the app data of the self resource, so it cannot ensure the consistency (equality) of the partitions (the maps provided in the app data) among different RLs for different resources. So one could do the same trick by providing different partitions for different resources.

3

Yes the really issue in this strategy is argument reuse. I.E. Pinning objects to be the argument twice over on actions you compose yourself.

The problem you noted in the call was about violating a single objects, which always runs their check.This was the sense that I meant it was fine since you were worried about that detail (I could have misunderstood you in the call though). I belive I noted on the call that there could be argument double use from the user pinning it in the action, which is an issue that you can’t really guarantee here without more check scaffoldings like the map structure and then general resource check.

4

Thanks for the reply. This makes things clearer for me. So this is indeed a problem without extra checks concerning app data across different RLs, which I don’t know how to implement in the current RM model.

I was concerned about any possible attacks that might result from putting indicators in app data, not only limited to fixed supply or related properties (though this might’ve been the example we discussed most, don’t remember exactly now). I didn’t have any specific examples at the time.