Use of assert to validate method arguments

[franck44]

The Eth2 specs frequently use assert statements to validate methods arguments.
This is a known source of security vulnerabilities and may result in insecure implementations:

• CWE-617: Reachable Assertion
• And also MET01-J. Never use assertions to validate method arguments from the The CERT Oracle Secure Coding Standard for Java.

The specs, as guidelines for implementers, may benefit from following standard coding practices to limit the number of security vulnerabilities. After all, the Beacon Chain is a critical component of the Eth2 infrastructure, and critical software components may be coded/specified following the highest coding standards.

Note: this issue is a follow-up of issue 1789.

[dankrad]

I think that is just a misinterpretation of the "assert" statement as used in the spec. When translated into client code, it should just become an exception or a similar thing that flags something invalid has happened during the state transition, and the whole transition should therefore be rejected.

Since the spec is not a program that is run in a production environment, the flagged suggestions don't really apply to it. And if not done using assertions, it would make tracking down bugs while testing the spec itself harder. So I'm not sure if there is a better solution, unless you can suggest one?

[franck44]

Thanks for your feedback @dankrad

I think that is just a misinterpretation of the "assert" statement as used in the spec. When translated into client code, it should just become an exception or a similar thing that flags something invalid has happened during the state transition, and the whole transition should therefore be rejected.

I interpreted the assert as the Python statement as the specs are provided in Python.

Since the spec is not a program that is run in a production environment, the flagged suggestions don't really apply to it.

I am not so sure. Again most of the specs are written in Python, so the only semantics I can see to apply is the semantics of the Python language.

And if not done using assertions, it would make tracking down bugs while testing the spec itself harder.

1. as you rightly mention, assert are useful for debugging and track down glitches. However they are unsafe in production code
2. the semantics of the assert as it is right now seems to enforce a reject of the transition. As I can see in the code, a state_transition is implemented by gradually modifying the state variable so returning to a good state may be harder than it seems, and the state to return to is not specified in the specs
3. the fact that assert statements are used as exception generators may enforce some constraints on the client code: the language should provide an exception mechanism. Our friends using functional programming may prefer more idiomatic and monadic solutions like returning the result of a computation as a Try (which indicates Success or Failure the latter being a sort of exception explanations). Moreover, using assert to generate exception implicitly means that we trust that the client code will properly catch exceptions which is probably optimistic and a thus a source of security vulnerabilities.

So I'm not sure if there is a better solution, unless you can suggest one?

Yes I have a suggestion.

For writing specifications and for instance constraints on the input parameters of a function, it is common to use pre conditions. The semantics is that the function can be called only if the parameters satisfy the pre-condition(s). This allows for a modular reasoning on the validity of functions calls (we can check that a caller satisfies the pre-conditions of a callee for instance using a static analyser).

If you want some examples of the use of pre/post-conditions, we are currently writing a formal specification of the Eth2.0 specs in order to prove that it is sound.
The repo is publicly available.

[protolambda]

@franck44 Maybe you can take a few functions of the beacon spec, and change them how you would like them to look like without asserts? Can you please open a PR to show your approach?

If we can agree on those as example, and share that with client implementers for feedback, we can change the other parts of the spec to not have any asserts.

[franck44]

@protolambda This is what we have done in our Dafny specs.
The repo is public.

[dapplion]

The spec clearly states how to interpret assert in a non ambiguous way.

[..] State transitions that trigger an unhandled exception (e.g. a failed assert or an out-of-range list access) are considered invalid.

consensus-specs/specs/phase0/beacon-chain.md

Line 1249 in bf09b9a

The post-state corresponding to a pre-state `state` and a signed block `signed_block` is defined as `state_transition(state, signed_block)`. State transitions that trigger an unhandled exception (e.g. a failed `assert` or an out-of-range list access) are considered invalid. State transitions that cause a `uint64` overflow or underflow are also considered invalid.

I don't see the added semantic value of switching to something other than assert