search

runtimeverification / polkadot-verification

Verification of Polkadot WASM code
Other
9 stars 6 forks source link

Proposed Verification Approach #20

Open ehildenb opened 5 years ago

ehildenb commented 5 years ago

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: #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 commented 4 years ago
  1. Prove some simple properties about the SET-FREE-BALANCE specification.
ehildenb commented 4 years ago

Update on status:

On the linked issue: https://github.com/runtimeverification/polkadot-verification/issues/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.