Authz: create a list of properties to test

[ivan-gavran]

• copy from the existing list of tested properties (from the model used for audit with Atomkraft or the original model used for writing integration tests)
• create interesting properties that were not present in previous models

[ivan-gavran]

Alongside those test scenarios, we discussed a bit more involved scenarios in the meeting today. Let's share them here in the comments first. @hvanz @andrey-kuprianov @rnbguy

[ivan-gavran]

1. A gives a generic grant to B.
2. B, on behalf of A, gives a generic grant to C. (Now C is able to send messages on behalf of A)
3. A revokes its grant to B.
   The question is: is the grant of C still valid? (I would expect so, but would like to check)

[rnbguy]

Trying to double spend by circular nested AuthzExec.

Transaction message from A
┌────────────────────────────────────────┐
│  A on behalf of B                      │
│ ┌────────────────────────────────────┐ │
│ │ B on behalf of A                   │ │
│ │ ┌────────────────────────────────┐ │ │
│ │ │ A on behalf of B               │ │ │
│ │ │ ┌────────────────────────────┐ │ │ │
│ │ │ │ B on behalf of A           │ │ │ │
│ │ │ │ ┌────────────────────────┐ │ │ │ │
│ │ │ │ │ A sends 10 tokens to B │ │ │ │ │
│ │ │ │ └────────────────────────┘ │ │ │ │
│ │ │ │                            │ │ │ │
│ │ │ └────────────────────────────┘ │ │ │
│ │ │                                │ │ │
│ │ └────────────────────────────────┘ │ │
│ │                                    │ │
│ │ ┌────────────────────────┐         │ │
│ │ │ A sends 10 tokens to B │         │ │
│ │ └────────────────────────┘         │ │
│ │                                    │ │
│ └────────────────────────────────────┘ │
│                                        │
└────────────────────────────────────────┘

[hvanz]

I don't quite understand the diagram. Can you write it in TLA+? 😉😁

[rnbguy]

Let me share an actual protobuf msg in YAML.

'@type': /cosmos.authz.v1beta1.MsgExec
grantee: A
msgs:
  - '@type': /cosmos.authz.v1beta1.MsgExec
    grantee: B
    msgs:
      - '@type': /cosmos.authz.v1beta1.MsgExec
        grantee: A
        msgs:
          - '@type': /cosmos.authz.v1beta1.MsgExec
            grantee: B
            msgs:
              - '@type': /cosmos.bank.v1beta1.MsgSend
                from_address: A
                to_address: B
                amount:
                  - denom: token
                    amount: '10'
      - '@type': /cosmos.bank.v1beta1.MsgSend
        from_address: A
        to_address: B
        amount:
          - denom: token
            amount: '10'

[hvanz]

In the spec (I'm not so sure about the code) the field msgs of MsgExec cannot be MsgExec. The type url of the message is defined for each authorization. So for the module bank only messages of type /cosmos.bank.v1beta1.MsgSend are allowed in MsgExec.

[rnbguy]

Sorry if we are only listing the scenarios that work with the current specification.

But yes, this will work with cosmos-sdk. I already tried it with Atomkraft. 🙂 GenericAuthorization allows any kind of transaction message.