Mukesh Tiwari

Mukesh Tiwari

Research Fellow at University of Cambridge

Sitemap

A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.

Pages

Posts

Formal Verification Hello World

7 minute read

Published:

Goal: what is the meaning of formal verification ?

As a beginner, we often come across this word formally verified software, and we ponder what does it mean? In this post, we are going find out the answer of this question with the help of Coq theorem prover. Imagine you are a software developer and your project leader asks you to write a list library with an append function, which can be used in other projects, that takes two lists and returns a list, concatenation of the two input lists. In addition, the project leader also gives some specification (concrete test cases) to ensure that what they expect from your library. Given that you already have some functional programming experience under your belt, it is not a very difficult task for you. You come up with the following Coq data type to model list data structure.

Inductive List (A : Type) : Type :=
| Nil : List A
| Cons : A -> List A -> List A.

List has two constructors: (i) Nil and (ii) Cons. Nil represents (models) empty list and Cons represents a list having at least one element. For example, Cons 1 (Cons 2 (Cons 3 Nil)) represent a list of natural numbers containing 1, 2, and 3. Furthermore, we write the append function, shown below, that concatenates the two input lists as:

Fixpoint append {A : Type} (lsa lsb : List A) : List A :=
  match lsa with
  | Nil => lsb
  | Cons hlsa tlsa => Cons hlsa (append tlsa lsb)
  end.

At this point, if we were using Haskell, OCaml, Scala, or any other language, but not a theorem prover, we would have written some test cases, in addition to the test cases given by the project leader, to ensure that our append function behaves according to the expectations of the project leader. As you can see, this is not rigorous and formal because your project leader may state the requirements vaguely, may miss the corner test cases, etc. But, in this project, we are using the Coq theorem prover, so we don’t need to write test case because we can prove that the append function follows some specifications for all the possible test cases! (you would often see the word correct in the context of formal verification, but I am trying to avoid the usage of word correct and I believe the right word is specification).

Now, you have a difficult and challenging job: finding specifications for the append function! Below are the few specifications that you have come up after a long discussion with your team:

  1. If you append an empty list Nil in the beginning of a list u, the result should be u, i.e., (append Nil u = u).
  2. If you append an empty list Nil in the end of a list u, the result should be u, i.e., (append u Nil = u)
  3. If you have three lists u, v, and w, first appending u and v and then appending the resulting list with w should be the same as appending u with the resulting list of appending v and w, i.e., (append (append u v) w = append u (append v w)).

You write these informal specifications more formally in Coq as:

  1. Theorem append_nil_l {A : Type} : forall (u : List A), append Nil u = u.

  2. Theorem append_nil_r {A : Type} : forall (u : List A), append u Nil = u.

  3. Theorem append_associative {A : Type} : forall (u v w : List A), 
 append (append u v) w = append u (append v w).

Let me explain what do these formal statements mean: the append_nil_l theorem states that for any arbitrary list u, append Nil u is equal to u (if you are not familiar with quantifier, I highly recommend you getting some introductory logic book. In the mean time, you can have a look at this introduction), and same for append_nil_r. However, append_associative is an interesting case. It says that for any three arbitrary lists u, v, and w, if you first append u and v, represented as (append u v), and then you append w to it, is same as first you append v and w and then you append u to it (by the way, I just told you that list append is a monoid where the set S is A, the binary operator is append, and the identity element is Nil). Finally, if you can prove these three theorems, then you can be confident that the append function follows all the three specifications (I want to reiterate that I am avoiding the the usage of correct and using the word specification).

Conclusion:

The astute reader by now is hopefully familiar, or at least some high level idea, with formal verification. Basically, we write our programs, data structures and functions to manipulate these data structures, in Coq (or pick your any favourite theorem prover Isabelle, Lean, HOL4, PVS, etc.). Finally, we come up with some specification, which intuitively captures the notion of correctness. If we can successfully prove all the specification, then we know that our implementation follows all the specification. It is often this proof step, in my experience, that exposes many corner cases which we have never considered.

Appendix:

You can safely ignore this part because I haven’t told you anything about tactics that I am going to use to write the proofs. I will explain them in the next post, but if you have some functional programming background then check the proofs in mixed mode (program mode and tactic mode). First, I am going to write the proofs, of the above mentioned theorems, using tactics, which may be overwhelming in the beginning but once you wrap your head around it, tactics are one of the best features of Coq because you can write proofs quickly. I will also show you mixed mode (tactic and program) to construct these proofs to demonstrate that these proofs are basically a functional program, that we build internally when we write tactics. Complete Source Code

Tactic Mode

Theorem append_nil_l {A : Type} :
  forall (u : List A), append Nil u = u.
Proof.      
  intros u.
  simpl.
  reflexivity.
Qed.

Theorem append_nil_r {A : Type} :
  forall (u : List A), append u Nil = u.
Proof.
  induction u;
    simpl.
  + reflexivity.
  + rewrite IHu.
    reflexivity.
Qed.

Theorem append_associative {A : Type} :
  forall (u v w : List A),
    append (append u v) w = append u (append v w).
Proof.
  induction u;
    simpl.
  + intros *.
    reflexivity.
  + intros *.
    rewrite IHu.
    reflexivity.
Qed.

Mixed Mode (Tactic and Programming)

Theorem append_nil_l_prog {A : Type} :
  forall (u : List A), append Nil u = u.
Proof.      
 refine (fun u => eq_refl).
Qed.

Theorem append_nil_r_prog {A : Type} :
  forall (u : List A), append u Nil = u.
Proof.
  refine
    (fix Fn u {struct u} :=
       match u with
       | Nil => eq_refl
       | Cons h t => _ 
       end); simpl;
    rewrite Fn;
    exact eq_refl.
Qed.

Theorem append_associative_prog {A : Type} :
  forall (u v w : List A),
    append (append u v) w = append u (append v w).
Proof.
  refine
    (fix Fn u {struct u} :=
       match u with
       | Nil => fun v w => eq_refl
       | Cons h t => fun v w => _ 
       end); simpl;
    rewrite Fn;
    exact eq_refl.
Qed.

portfolio

publications

Schulze voting as evidence carrying computation

Published in International Conference on Interactive Theorem Proving - 2017, 2017

The correctness of vote counting in electronic election is one of the main pillars that engenders trust in electronic elections.

Download here

Modular formalisation and verification of STV algorithms

Published in International Joint Conference on Electronic Voting - 2018, 2018

TWe introduce a formal, modular framework that captures a large number of different instances of the Single Transferable Vote (STV) counting scheme in a uniform way.

Download here

Verifiable Homomorphic Tallying for the Schulze Vote Counting Scheme

Published in Conference on Verified Software: Theories, Tools, and Experiments - 2019, 2019

The encryption of ballots is crucial to maintaining integrity and anonymity in electronic voting schemes. It enables, amongst other things, each voter to verify that their encrypted ballot has been recorded as cast, by checking their ballot against a bulletin board.

Download here

Verified Verifiers for Verifying Elections

Published in ACM SIGSAC Conference on Computer and Communications Security - 2019, 2019

The security and trustworthiness of elections is critical to democracy; alas, securing elections is notoriously hard. Powerful cryptographic techniques for verifying the integrity of electronic voting have been developed and are in increasingly common use.

Download here

talks

Verifiable homomorphic tallying for the schulze vote counting scheme

Published:

The encryption of ballots is crucial to maintaining integrity and anonymity in electronic voting schemes. It enables, amongst other things, each voter to verify that their encrypted ballot has been recorded as cast, by checking their ballot against a bulletin board.

Final PhD Presentation

Published:

This was my final PhD talk, where I discussed the challenges of conducting elections electronically, and their possible solutions.

Machine Checked Properties of the Schulze Method

Published:

The correctness of electronic vote-counting software programs is crucial in establishing the trust of people in electronic voting. However, most of these vote-counting programs, used in various jurisdiction for legally binding election, establish the correctness by means of testing which is not sufficient and leaves much to be desired. Therefore, we propose that legally binding vote-counting software programs should be formally verified and its correctness should be evaluated against some well established framework from social choice theory.

teaching

Teaching experience 1

Undergraduate course, University 1, Department, 2014

This is a description of a teaching experience. You can use markdown like any other post.

Teaching experience 2

Workshop, University 1, Department, 2015

This is a description of a teaching experience. You can use markdown like any other post.