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

Proposed Verification Approach #20

Open
ehildenb opened this issue Sep 5, 2019 · 2 comments
Open

Proposed Verification Approach #20

ehildenb opened this issue Sep 5, 2019 · 2 comments

Comments

@ehildenb
Copy link
Member

ehildenb commented Sep 5, 2019

The amount of Wasm code to verify here is quite large, so traditional verification approaches we've used for KEVM will not scale while keeping us in our modest budget. As such, we're taking this as the opportunity to develop more scalable/automated techniques.

After several discussions internally, we've landed on what seems like a feasible approach, broken into 3 phases.

  1. Make a high-level executable specification SET-FREE-BALANCE-SPEC of the set_free_balance function, capturing the intended behavior: Executable spec - initial high-level K files describing desired behavior #15.
  2. Generate symbolic descriptions of the execution paths of the set_free_balance function automatically using fuzzing over concrete execution traces + abstraction/broadening ("poor person's" concolic execution). Call this SET-FREE-BALANCE-ACTUAL.
  3. Prove that SET-FREE-BALANCE-SPEC is a refinement of SET-FREE-BALANCE-ACTUAL using KEQ tooling.

In our traditional approach, we would instead express SET-FREE-BALANCE-SPEC directly as a specification over the KWasm state, which is where the majority of the time would be spent. Instead, we'll try using (2) to auto-generate that description and save the human effort needed for that step, allowing us to focus on the high-level spec and the refinement relation.

Optional next step:

  1. Ensure completeness of the generated traces. This would look like ALL_POSSIBLE_INITIAL_STATES == \/ lhs(GENERATED_RULES) (or perhaps the weaker ALL_POSSIBLE_INITIAL_STATES -> \/ lhs(GENERATED_RULES)), and if this formula is bottom, then we are complete.
@ehildenb
Copy link
Member Author

  1. Prove some simple properties about the SET-FREE-BALANCE specification.

@ehildenb
Copy link
Member Author

Update on status:

On the linked issue: #20 we are largely done with (1) other than bug-fixes/improvements. I'm in progress on (2), which is blocking (3). Demi and I have been pairing on (5), which is writing actual high-level properties over the spec developed in (1).

Recall that the summary is that (1) is about making a high-level model of the system, (2) is about generating specifications for the Wasm code that is generated, (3) is about proving that the generated specifications in (2) actually agree with the high-level model from (1), and (5) is about proving that the high-level model from (1) (and thus the low level model from (2)) actually has some desirable properties.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant