ethereum / consensus-specs

Ethereum Proof-of-Stake Consensus Specifications
Creative Commons Zero v1.0 Universal
3.58k stars 981 forks source link

Use of `assert` to validate method arguments #1797

Open franck44 opened 4 years ago

franck44 commented 4 years ago

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:

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

@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 commented 4 years ago

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

dapplion commented 11 months ago

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.

https://github.com/ethereum/consensus-specs/blob/bf09b9a7c4a7b311e86823235815daf31b117574/specs/phase0/beacon-chain.md?plain=1#L1249

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