Modularise the attack language about cooked-validators HOT 8 CLOSED

I just had a very interesting discussion with @mmontin, which yielded some ideas relevant to this issue. The gist is this: An attack is a computation onTxSkels, and so far, we've tried out the following approaches to make that notion more concrete:

• The simplest case would just be type Attack = TxSkel -> TxSkel. This is not satisfactory, because we want the modification to depend on the current state of the world.
• So, we consider type Attack = MockChainSt -> TxSkel -> TxSkel, which is not satisfactory because we want attacks that can signal failure.
• This in turn leads us to consider type Attack = MockChainSt -> TxSkel -> Maybe TxSkel, which we don't like because there might be more than one possible way to perform the attack.
• This is the justification of the current typeAttack = MockChainSt -> TxSkel -> [TxSkel].

Unfortunately, the current attack type makes it not too easy to chain attacks in non-trivial ways (there's only the Monoid instance of Attack or, kind of equivalently, LtlAnd). Say you want to write an attack that goes through all SpendsScript constraints of a transaction and somehow changes the redeemers used. In a second step, you want to change the transaction outputs depending on how you changed the redeemers of the inputs. It's possible to write this attack at the moment, using mkAccumLAttack, but it would be much nicer, and more modular, if these two modification steps were reusable building blocks, i.e. independent attacks.

As the four points above illustrate, for every monad we've considered so far as the codomain of Attacks It has some shortcoming (no state awareness, no failure signalling, only one possible return value, no non-trivial chaining of attacks). So it's to be expected that whatever option we chose next will have some shortcomings as well. (Compare also this comment at the discussion that led us to chose the list monad.)

The question is: Can we somehow make the most general option, namely something like

type Attack m = Monad m => TxSkel -> m TxSkel

work?

from cooked-validators.

About the type

type Attack m = Monad m => TxSkel -> m TxSkel

Would that work if m is a state monad ?
More precisely, what would be the relevance of the TxSkel input in that case ?

In addition, what semantics would have the combination of several attacks living in different monads ?

from cooked-validators.

Maybe going to an arbitrary monad is a bit too generic.

How about something of the like

type Attack m a = MonadMockChain m => StateT TxSkel m a

A few remarks / questions on this proposition (in a very unorganized manner):

• MonadMockChain allows us to rely on the outside world.
• We build a computation, which makes it easily composable with respect to >==.
• How do we branch though, if there are several possible outcomes?
• Is that even relevant to wanting to branch ?
• How do we handle cases where the modification is unsuccessful ?
• Do we just return the id computation, or do we just make a call to fail ?
• Each unary computation can then return a value.
• Each unary computation can be developed using optics on the inner TxSkel.
• Should we change the TxSkel type to have the sub constraints types builtin ?
• In that case, how do we ensure ordering of the outputs ?
• These attacks could be both used for large spectrum attempts or single step modifications.
• In practice for audits, endpoints could be computations aimed at being run on empty skeletons.
• Or, they could be functions that return a TxSkel coupled with whatever value needs to be returned.
• The former has the benefit of providing both the skeleton as well as the return value for free.

Of course, this is something I was to propose at some point since this more or less corresponds to the original vision I had on single step attacks during my latest audit. This vision has improved a lot since then though, since this version can possibly successfuly take the best out of optics, attacks and temporal modalities while using state computations. Feel free to challenge my assumptions, and discuss the implications.

from cooked-validators.

I'm not yet convinced that we have found a good approach. Here are a few thoughts I have about the two Ideas in this discussion.

My idea with type Attack m = TxSkel -> m TxSkel would probably only become really usable if we write functions like mkAttack polymorphically in m. A simple (I don't know how useful) example would be

mkAttack :: Traversal' TxSkel a -> (a -> m a) -> Attack m
mkAttack = Optics.Core.traverseOf

• For m == Maybe, this builds an attack that returns Just the modified TxSkel iff all the foci of the travesal were successfully modified.
• For m == [], we would get an attack that returns a list of modified TxSkels, containing every possible combination of modifications for each of the foci.
• For m == StateT a n, we could work with a state while traversing the foci from the left to the right.
• ...

Chaining attacks with different ms would not be possible straightforwardly, but since mkAttack and siblings are polymorphic, one could just specialise attacks written in terms of them to any monad that's convenient at the moment.

My main problem with this approach is that it feels like an underspecified ad-hoc effect system to construct attacks.

Concerning @mmontin's idea type Attack m = MonadMockChain m => StateT TxSkel m a:

• It's true that such an approach makes chaining very easy, since one can write modifications that return arbitrary values, and use these return values as parameters for subsequent modifications.
• I'm a bit wary of the MonadMockChain constraint. I think it is too powerful: What should for example the meaning of a validateTxSkel be in a computation whose intended purpose it is to build a TxSkel? In a way, we want read-only access to the state of the blockchain. That's what the current type Attack = MockChainSt -> ... allows.

Generally speaking,

• I still think that my remark above holds: For each specific choice of type Attack = ... we'll at some point find a reason why it's not good enough. I'd really either like to have very good reasons to choose one specific type, or be as general as reasonably possible.
• I also (newly) think that something like type Attack = MockChainSt -> TxSkel -> [TxSkel] or type Attack = MockChainSt -> TxSkel -> Maybe TxSkel is correct. An attack should be a function that modifies a transaction in a context-dependent way. At some point all of the monad ideas (like my and @mmontin's) will have to be run with the appropriate function (runStateT etc.), and the result will be something like these types anyway. It's just that we haven't found a really good mechanism to chain attacks.

So, I think that if we can come up with a way that allow us to pass information from one attack to the next, without specialising too much how one should construct attacks, that'd be a solution I'd be happy with.

from cooked-validators.

If we just go from the requirements,

• We need the ability to depend on the state, hence there has to be at least a MockChainSt argument.
• We need the ability to signal failure, so the return type must be at least a Maybe.
• We do not need the ability to return multiple modified transactions, since LtlOr can take care of that.
• We need the ability to return some extra information together with the modified TxSkel.

This suggests

newtype Attack a = Attack (MockChainSt -> TxSkel -> Maybe (TxSkel, a))

and we can define Monad Attack to behave in essentially the same way as the StateT construction you proposed, @mmontin, with all the nice chaining behaviour. I think I'll play around with this idea a bit.

from cooked-validators.

A very short comment before I try to dive more into details.
Why should the attack only have read-only access to the outside world?
I understand why it makes sense at first glance, but is it really a requirement?

from cooked-validators.

I don't think it's a requirement to have read-only access to the outside world, I just wanted to point out that it means quite a substantial change of what we mean by an "attack". At the moment, attacks are about modifying TxSkels; with the whole MonadBlockChain generality, we'd also have attacks that, say, exchange one validateTxSkel for a whole sequence of transactions.

from cooked-validators.

I've given the idea newtype Attack a = Attack (MockChainSt -> TxSkel -> Maybe (TxSkel, a)) from above a shot, and have written a prototype of the dupTokenAttack implemented in this way. I quite like it, and will definitely continue this exploration tomorrow. Comments are welcome!

from cooked-validators.