Absence of internal errors

We are currently verifying the absence of internal errors in the protocol of Tezos. We show that no unexpected errors are reachable in the code, such as assert false or critical errors. We describe here what we have done recently towards the verification of such errors.

Specification of the storage

The storage described by Storage.v is composed of around one hundred sub-stores. We create these sub-stores on top of the key-value database of Tezos using the Storage_functors.v. For now we axiomatize the behavior of these sub-stores using a simulation in Raw_context_generated.v. This simulation behaves as the actual store, but uses simpler data structures such as records, OCaml sets and maps. Even if it would be impractical for performance reasons to run this simulation, this alternative implementation of the storage simplifies the reasoning for us.

As the storage contains a lot of repetitive declarations, we use a Ruby script to generate the simulation. When we need to make a change, it is easier to change this script than manually replicate the changes on each of the sub-stores. We also generate a file Storage_generated.v with axioms stating that our simulation is valid. An example of axiom about a read operation is the following:

Axiom get : forall (ctxt : Simulations.Raw_context.t),
  Storage.Block_round
    .(Storage.Simple_single_data_storage.get)
    (Raw_context.to_t ctxt) =
  match Helpers.get ctxt with
  | Some x => Pervasives.Ok x
  | None =>
      Raw_context.storage_error_value
        (Raw_context.Missing_key Helpers.name Raw_context.Get)
  end.

The context ctxt is a simulated storage value. The function Raw_context.to_t converts a simulated store to an actual store. It is not possible to do the reverse, that is to say there are no functions from an actual store to a simulated store. The function Helpers.get is:

Definition get (ctxt : Simulations.Raw_context.t) :=
  ctxt
    .(Raw_context.t.back)
    .(Raw_context.back.context)
    .(Context.t.Storage)
    .(Context_generated.t.Block_round).

reading into a simulated store using standard record field accesses.

An axiom about a write operation is:

Axiom update : forall (ctxt : Simulations.Raw_context.t) value,
  Storage.Block_round
    .(Storage.Simple_single_data_storage.update)
    (Raw_context.to_t ctxt) value =
  match Helpers.get ctxt with
  | Some _ =>
      return? Helpers.set ctxt (Some value)
  | None =>
      Raw_context.storage_error_value
        (Raw_context.Existing_key Helpers.name)
  end.

The helper Helpers.set updates the record of the simulated store and converts the result to an actual store.

We are not verifying our axioms about the storage and intend to do it later.

Validity predicate

A typical statement about the absence of internal errors is the following in Apply.ex_ticket_size_is_valid:

(** The function [ex_ticket_size] is valid. *)
Lemma ex_ticket_size_is_valid ctxt ticket :
  Raw_context.Valid.t ctxt ->
  Ticket_scanner.Ex_ticket.Valid.t ticket ->
  letP? '(ctxt, size) :=
    Apply.ex_ticket_size ctxt ticket in
  Raw_context.Valid.t ctxt /\ Pervasives.Int.Valid.t size.

There we state that the function Apply.ex_ticket_size, when applied to a valid ctxt and ticket, both:

• returns a valid ctxt and size,
• does not contain internal errors

We found that is was generally convenient to state and prove both at the same time. The combinator letP? is a notation for:

Definition bind_prop {a : Set} (x : M? a) (P : a -> Prop) : Prop :=
  match x with
  | Pervasives.Ok x => P x
  | Pervasives.Error err => Error.not_internal err
  end.

stating that the value x in the error monad M? a is either successful verifying the property P, or an error that is not internal.

Example of proof

A function such as Apply.ex_ticket_size verified above is a succession of calls to other functions, separated by the monadic combinator let? of the error monad:

Definition ex_ticket_size
  (ctxt : Alpha_context.context) (function_parameter : Ticket_scanner.ex_ticket)
  : M? (Alpha_context.context * int) :=
  let 'Ticket_scanner.Ex_ticket ty_value ticket := function_parameter in
  let? ty_value := Script_typed_ir.ticket_t Micheline.dummy_location ty_value in
  let? '(ty', ctxt) :=
    Script_ir_unparser.unparse_ty Micheline.dummy_location ctxt ty_value in
  let '(ty_nodes, ty_size) := Script_typed_ir_size.node_size ty' in
  let ty_size := Saturation_repr.to_int ty_size in
  let ty_size_cost := Script_typed_ir_size_costs.nodes_cost ty_nodes in
  let? ctxt := Alpha_context.Gas.consume ctxt ty_size_cost in
  (* ... *)

We split these calls with the lemma split_letP:

Lemma split_letP {a b : Set}
  (x : M? a) (f : a -> M? b) (P : a -> Prop) (Q : b -> Prop) :
  (letP? x := x in P x) ->
  (forall x, P x -> letP? y := f x in Q y) ->
  letP? y := (let? x := x in f x) in Q y.

This states that if we can prove that:

• x is valid with the post-condition P,
• f if valid with the post-condition Q when given a pre-condition P

then let? x := x in f x is valid with the post-condition Q. In practice, Q is given by the lemma statement and P is automatically instantiated as we write the proof. Using existing proofs (or axioms) for the absence of internal errors in the functions called by ex_ticket_size we can then complete the proof of the lemma.

Conclusion

We are still at the beginning of verification for internal errors. One interest of this task is that we can state properties about various parts of the code. It also forces us to express the pre and post-conditions of each definition. We are now focusing on functions with a simple structure (no recursion) and will prove more complex ones later.

An example of difficulty that we faced is verifying the absence of integer overflows, when the limit is hard to reach in practice but not checked in the code.