Authorization logic of staking module: denyList never used?

[ivan-gavran]

Summary of Bug

When going through the authorization logic of the staking module (staking/types/authz.go, function Accept), I was confused by the parameters allowed and denied of the function NewStakeAuthorization.
Quoting from the documentation:

Additionally, this Msg takes an AllowList and a DenyList, which allows you to select which validators you allow grantees to stake with.

However, it seems that it is never possible to have a non-empty DenyList with a successful authorization.

1. exactly one of allowList and denyList may be given, not both (this follows from the function validateAndBech32fy)
2. delegation will be accepted if the validator is both in the allowList and not in the denyList (this follows from the function Accept of authz.go: the boolean value isValidatorExists has to be set to true, or otherwise an error is raised)

Thus, if the authorization is to ever be successfully used, denyList must always be empty.

Is this intended behavior? If so, why not removing denyList?

Version

e0f812d

---

For Admin Use

• Not duplicate issue
• Appropriate labels applied
• Appropriate contributors tagged
• Contributor assigned/self-assigned

[aaronc]

Seems like the implementation is incorrect and there is not a test case to catch it. If deny list is provided, it should be possible to use any validator not on the deny list. This is a bug

[ivan-gavran]

Great, thanks for following up so quickly. I noticed that the issue was mentioned in the context of discussion on whether or not to use a testing framework: in this context, it is worth saying that I discovered this bug using the model-based testing approach on the code, getting failed tests and investigating the code upon that.

[ivan-gavran]

Adding a bit more details and links on the model that revealed the bug since it was interesting to a couple of people looking into model-based testing, and to remain here as a reference.

• I first created a model of the authz logic here starting from the English spec.
• In my first reading of the English spec, I did not understand that denyList and allowList cannot be non-empty at the same time (and, indeed, it was not emphasized there). Thus, my first model allowed for that. This resulted in tests failing, which were supposed to succeed.
• Then I added the restriction to require that exactly one of two sets is non-empty and mimicked the code more closely (where the English spec was not detailed). Upon inspecting generated tests for the predicate SuccessfulExec, I noticed that, curiously, the denyList was always empty. I created a test to force denyList to be populated (here), which the model checker could not resolve. That led me to realize that the logic of ("exactly one non-empty" && "must be in allowList" && "must not be in denyList") implied that there can be no successful authorization with denyList non-empty.

Looking back to the process, I draw two conclusions:

• it is not clear that I would think of creating the test that revealed the bug to begin with (that is, there still is some input expected from the user in describing what are interesting behaviors to test)
• however, the effort of creating a model and being forced to be precise about what happens under different scenarios brought to light this hidden unexplored terrain
• furthermore, the fact that MBT can generate many tests for a single behavior (abstract test) makes it easier to surface bugs which would not be found when describing a concrete test case.