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

• (25/05/2022) I am in Artifact Evaluation Committee of ICFP 2022.
• (21/01/2022) I gave a talk about my PhD dissertation at the Cambridge theory group. Slides.
• (05/10/2021) Ongoing work –Towards Leakage-Resistant Machine Learning in Trusted Execution Environments– accepted in Program Analysis and Verification on Trusted Platforms (PAVeTrust) Workshop.
• (01/10/2021) I joined the University of Cambridge as a senior research associate.
• (06/09/2021) Short paper Machine Checked Properties of the Schulze Method accepted at the HotSpot 2021 (slides).
• (15/07/2021) Now, I am a permanent Australian resident because Australian Home Department has awared me the Global Talent Visa (858), to strengthen the cyber security capability of Australia.
• (21/05/2021) I am in Artifact Evaluation Committee of ICFP 2021.
• (30/03/2021) My PhD thesis is accepted and now I am officially Dr. Mukesh Tiwari!
• (31/01/2021) Poster accepted in NDSS 2021.
• (05/01/2021) I am in Artifact Evaluation Committee of CC Research Artifacts.
• (27/11/2020) Short paper Verifying the Security of a PGP Keyserver accepted at the VerifyThis Long-term Challenge 2020.
• (19/10/2020) Paper Verifpal: Cryptographic Protocol Analysis for the Real World accepted at the INDOCRYPT 2020.
• (09/06/2020) Short paper Verifpal: Cryptographic Protocol Analysis for the Real World accepted at the 2020 ACM SIGSAC Conference on Cloud Computing Security Workshop.
• (10/02/2020) I joined the University of Melbourne as a research associate.
• (04/02/2020) My poster is accepted for the presentation at the Cyber Defence Next Generation Technology & science Conference (CDNG) in Brisbane 24 & 25 March 2020 (cancelled due to COVID pandemic)
• (10/01/2020) PhD thesis submitted (giving my final PhD talk).
• (11/11/2019) Paper Verified Verifiers for Verifying Elections accepted at the CCS 19.
• (31/07/2019) Received travel scholarship to attend Marktoberdorf Summer School 2019. Sadly, I could not attend it because of the visa delay (one of the downsides of having a second world passport).
• (13/07/2019) Paper Verifiable Homomorphic Tallying for the Schulze Vote Counting Scheme accepted at the Verified Software. Theories, Tools, and Experiments 2019 conference.
• (02/10/2018) Paper Modular Formalisation and Verification of STV Algorithms accepted at the E-Vote-ID 2018 conference.
• (16/07/2018) Received travel and accommodation scholarship to attend DeepSpec Summer School, July 16-27, 2018 at the University of Princeton. Thank you DeepSpec!
• (09/07/2018) I am attending 9th International Summer School on Information Security and Protection at the Australian National University, Canberra.
• (24/10/2017) Paper No More Excuses: Automated Synthesis of Practical and Verifiable Vote-Counting Programs for Complex Voting Schemes accepted at the E-Vote-ID 2017 conference.
• (26/09/2017) Paper Schulze Voting as Evidence Carrying Computation accepted at the ITP 2017 (Coq formalisation).
• (21/06/2016) I started my PhD at the Australian National University.

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.