First version of Authz TLA+ #2

hvanz · 2022-08-16T11:55:05Z

Closes #1

ivan-gavran · 2022-08-16T15:08:42Z

I had a high-level look at the model. Let me write preliminary comments as the basis for the synchronous discussion tomorrow.

First thing to say, I am very impressed by how well structured and easy to read it is. It is also extremely modular.
One clarification question wrt to that is:
how does one check for different authorization logics (AuthzSend, AuthzStake...)? I can see that one could create e.g. AuthzSend_MC.[cfg, tla], but this then only allows checking for a single authorization logic (and not mixing between them)

I also notice that the model very much follows the code structure. I can see an advantage being that the developers of the implementation would have an easier time following along the model.
I can also see some disadvantages:

the model gets fairly complex
if it faithfully follows the implementation, then we should not expect to see mismatches between the code and the model
Does this seem right?

Finally, a very high-level question: when you were looking at the existing model, what made you decide to start from scratch?
(Since I was working on the basis of it, this could be a useful feedback in model-writing for me.)

Test scenarios

models/authz/StakeAuthorization.tla

ivan-gavran · 2022-08-25T08:26:13Z

I just noticed one thing in the Cosmos-SDK codebase: they are also adding the allowList SendAuthorization. This is already merged in main, but is not part of any existing releases (check this PR). Bringing this up here so that we know what to expect when new releases come (I don't think we need to change our model yet).

models/authz/StakeAuthorization.tla

ivan-gavran · 2022-08-25T10:12:57Z

models/authz/Grants.tla

+      [] auth.authorizationType \in Stake!MsgTypeUrls -> 
+        Stake!MsgTypeURL(auth)
+
+Accept(auth, msg) ==


It seems that this way of modelling Accept prevents send or stake messages that rely on a generic authorization. Is that true?

GenericAuthorization accepts any kind of message url, including send or delegate, for instance. The accepted messages are defined in the constant GenericAuthTypes. So one could instantiate this constant with any kind of message (I haven't tried it).

hvanz · 2022-08-25T15:21:56Z

I just noticed one thing in the Cosmos-SDK codebase: they are also adding the allowList SendAuthorization. This is already merged in main, but is not part of any existing releases (check this PR). Bringing this up here so that we know what to expect when new releases come (I don't think we need to change our model yet).

If it's the same as in the Staking module, it should be easy to change. Good to know anyway.

hvanz · 2022-08-29T07:47:35Z

I added to SendAuthorization an allowList field, which is implemented in cosmos-sdk since version 0.47.

andrey-kuprianov

The model is great! Very well structured, and logical. I have made some comments about potential improvements for using the model for test case generation, but those can be addressed separately later.

andrey-kuprianov · 2022-08-31T09:16:27Z

models/authz/Authz.tla

+    /\ IsValid(g)
+    /\ ~ HasGrant(g) \/ IsExpired(g)


My feeling is that the way RequestGrant and other top-level operators from Next are too restrictive for testing purposes. In particular, we want to be able to test inputs where:

granter is the same as grantee

there is already a grant given, and it's not expired

So, in short, we should treat the inputs maximally non-deterministically, and ensure that the implementation fails for incorrect combinations of input parameters.

andrey-kuprianov · 2022-08-31T09:16:51Z

models/authz/Authz.tla

+    /\ IsValid(g)
+    /\ HasGrant(g)


Same as RequestGrant above

andrey-kuprianov · 2022-08-31T09:19:29Z

models/authz/Grants.tla

+\* https://github.com/cosmos/cosmos-sdk/blob/c1b6ace7d542925b526cf3eef6df38a206eab8d8/x/authz/authz.pb.go#L74
+\* @typeAlias: GRANT = [authorization: AUTH, expirationTime: EXPIRATION_TIME];
+\* @type: Set(GRANT);
+Grants == [
+    authorization: Authorization,
+    expirationTime: ExpirationTimes
+]


Type AUTH is defined in each of Generic/Send/Stake Autohrization separately; and then it is used in Grants here. It is unclear which AUTH is used; in fact Apalache's type checker should have complained about having multiple type aliases with the same name

First version of Authz TLA+

d083737

hvanz requested a review from ivan-gavran August 16, 2022 11:55

hvanz added 3 commits August 16, 2022 16:15

TypeOK now holds with TLC

12f40a1

Fix IsActive and IsExpired

29b2292

Restrict domain of grantStore only to active grants

560dff7

hvanz and others added 19 commits August 16, 2022 23:51

Fix type invariant of grantStore

a025ed8

Split main module in two files, and other improvements

110a2f0

Add properties to test

c88699d

Create instances of all auths at once

75d1c31

Fix Apalache types

365ee82

Many small fixes and refactorings

3d78049

Fix spec for TypeOK

4e467c7

More improvements

6d322f9

Add variable numRequests; fix record with EXCEPT

fc94ab7

Fix record with EXCEPT

fc0ec35

Simplify Accept expression in Send

0efdf17

Fix Apalache types

6498935

Update auth without accept

bcba250

Send one msg per Exec call; code styling

d1e8ec6

first version of test scenarios

1ce7c3f

Merge pull request #4 from informalsystems/ivan/list_test_scenarios

13808f1

Test scenarios

Add gitignore

1900790

Formatting

421a126

Rename variable also in properties

39f9855

ivan-gavran reviewed Aug 23, 2022

View reviewed changes

models/authz/StakeAuthorization.tla Outdated Show resolved Hide resolved

hvanz added 3 commits August 23, 2022 12:36

Fix Accept in Send and Stake auths

fc3d59c

Split AuthzGrants into Grants and GrantMessages

c68ae33

Repeated field in Apalache record type

c0fcb72

hvanz marked this pull request as ready for review August 23, 2022 09:48

hvanz self-assigned this Aug 23, 2022

ivan-gavran self-requested a review August 25, 2022 08:23

ivan-gavran reviewed Aug 25, 2022

View reviewed changes

hvanz added 3 commits August 29, 2022 10:24

Allow Coins to include negative numbers

07f2951

Return insufficient-amount error in StakeAuth

a4ed54d

Add allowList to SendAuthorization

a109275

andrey-kuprianov self-requested a review August 29, 2022 15:24

andrey-kuprianov approved these changes Sep 2, 2022

View reviewed changes

andrey-kuprianov merged commit fee85e9 into main Sep 2, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

First version of Authz TLA+ #2

First version of Authz TLA+ #2

hvanz commented Aug 16, 2022 •

edited

Loading

ivan-gavran commented Aug 16, 2022

ivan-gavran commented Aug 25, 2022 •

edited

Loading

ivan-gavran Aug 25, 2022

hvanz Aug 25, 2022 •

edited

Loading

hvanz commented Aug 25, 2022

hvanz commented Aug 29, 2022

andrey-kuprianov left a comment

andrey-kuprianov Aug 31, 2022

andrey-kuprianov Aug 31, 2022

andrey-kuprianov Aug 31, 2022

First version of Authz TLA+ #2

First version of Authz TLA+ #2

Conversation

hvanz commented Aug 16, 2022 • edited Loading

ivan-gavran commented Aug 16, 2022

ivan-gavran commented Aug 25, 2022 • edited Loading

ivan-gavran Aug 25, 2022

Choose a reason for hiding this comment

hvanz Aug 25, 2022 • edited Loading

Choose a reason for hiding this comment

hvanz commented Aug 25, 2022

hvanz commented Aug 29, 2022

andrey-kuprianov left a comment

Choose a reason for hiding this comment

andrey-kuprianov Aug 31, 2022

Choose a reason for hiding this comment

andrey-kuprianov Aug 31, 2022

Choose a reason for hiding this comment

andrey-kuprianov Aug 31, 2022

Choose a reason for hiding this comment

hvanz commented Aug 16, 2022 •

edited

Loading

ivan-gavran commented Aug 25, 2022 •

edited

Loading

hvanz Aug 25, 2022 •

edited

Loading