About

Welcome to my personal website! My name is Mukesh Tiwari, and currently, I am a Senior Research Fellow at the University of Cambridge and working on formal verification of networking protocols, from algebraic point of view, with Timothy Griffin. The goal is to extract a verified OCaml implementation that will help network-protocol designers to verify the property of their protocol. Before joining the University of Cambridge, I was a research fellow at the University of Melbourne where I worked on formally verified information flow security with Toby Murray. Before moving to Melbourne, I was a PhD student at the Australian National University, Canberra where I worked on formal verification of electronic voting algorithms, under the supervision of Dirk Pattinson.

Research

The ultimate goal of my research is to push correct software programs used in public domain. My research focuses on proving the correctness of software programs, particularly used for a very high stake situations involving common citizens, e.g., vote counting software for a legally binding elections to a public office, data processing software for sensitive data, cryptographic software used in elections, etc. Mainly, I use Coq theorem prover to implement a software program and prove them correct. In addition, I am also very passionate about teaching formal verification.

Feel free to get in touch if you have any research project related to theorem proving, particularly if it involves Coq.

News

PhD Abstract

In my PhD, I addressed three main concerns posed by electronic voting, i.e. correctness, privacy, and verifiability. I addressed the correctness concern by using theorem prover to implement the vote counting algorithm, privacy concern by using homomorphic encryption, and verifiability concern by generating a independently checkable scrutiny sheet (certificate). You can read my thesis. Below is the abstract:

Since the introduction of secret ballots in Victoria, Australia in 1855, paper (ballots) are widely used around the world to record the preferences of eligible voters. Paper ballots provide three important ingredients: correctness, privacy, and verifiability. However, the paper ballot election brings various other challenges, e.g. it is slow for large democracies like India, and error prone for complex voting method like single transferable vote, and poses operational challenges for large countries like Australia. In order to solve these problems and various others, many countries are adopting electronic voting. However, electronic voting has a whole new set of problems. In most cases, the software programs used to conduct the election have numerous problems, including, but no limited to, counting bugs, ballot identification, etc. Moreover, these software programs are treated as commercial in confidence and are not allowed to be inspected by general member of general public. As a consequence, the result produced by these software programs can not be substantiated.

In this thesis, we address the three main concerns posed by electronic voting, i.e. correctness, privacy, and verifiability. We address the correctness concern by using theorem prover to implement the vote counting algorithm, privacy concern by using homomorphic encryption, and verifiability concern by generating a independently checkable scrutiny sheet (certificate). Our work has been carried out in Coq theorem prover.