Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use of assert to validate method arguments #1797

Open
franck44 opened this issue May 8, 2020 · 4 comments · May be fixed by #2366
Open

Use of assert to validate method arguments #1797

franck44 opened this issue May 8, 2020 · 4 comments · May be fixed by #2366
Labels
general:enhancement New feature or request

Comments

@franck44
Copy link

franck44 commented May 8, 2020

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
Copy link
Contributor

dankrad commented May 12, 2020

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
Copy link
Author

franck44 commented May 14, 2020

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
Copy link
Collaborator

protolambda commented Jun 17, 2020

@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
Copy link
Author

franck44 commented Jun 17, 2020

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
general:enhancement New feature or request
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants