Turing PhD student David Butler interns with NASA, analysing the safety of unmanned aircraft
David took three months out of his PhD to work at the NASA Ames...
Monday 17 Dec 2018
Bio
About
David is a Postdoc at The Alan Turing Institute working on developing trustworthy ID systems under Professor Jon Crowcroft. His current work focusses on using Privacy Enhancing Technologies (PETS) to ensure the security and privacy of digital identity systems.
David was previously a Doctoral Student at the Turing, affiliated with the University of Edinburgh. He was supervised by David Aspinall and Adria Gascon. His PhD research lay at the intersection of cryptography and formal methods. In particular in computer aided security proofs. He worked on providing machine checked proofs for proofs of security of low level primitives and Multi Party Computation (MPC) protocols.
Before The Alan Turing Institute he completed his masters (First Class Honours, MMath) at Durham University.
For more details on his research, see his publications page or his Google Scholar profile, or feel free to contact him directly.
In 2018 he spent time working at the NASA Ames Research Center in California. You can read about what he got up to here.
Recent publications
Sept 2020: Paper accepted to NDSS CoronaDef workshop 2021. We develop the idea of a differentially private health token, allowing for aggregated statistics regarding risk from COVID-19 to be computed while maintaining user privacy.
Sept 2020: Journal paper accepted (September 2020) to Journal of Automated Reasoning. An extension of work on formalising Sigma Protocols and Commitment Schemes.
May 2020: New paper on antibody certificates for CVID -19. We present SecureABC, a privacy preserving antibody certificate system.
March 2020: New paper looking at centralised contact tracing systems for Covid-19.
December 2019: Paper accepted at CPP 2020. This work extends formalisation of MPC to the malicious setting.
November 2019: New paper out, extending work from POST 2019 on Sigma Protocols and Commitment Schemes.
Research interests
David is mainly interested in low level cryptographic primitives. Presently he interested in how PETS can be used to increase the security and privacy and thus trustworthiness of digital ID systems in developing economies. Previously, in his PhD this interest manifested itself in using formal methods to put high guarantees of correctness of foundational proofs of security. In particular he worked with the proof assistant Isabelle/HOL to formalise proofs of security of Multi-Party Computation protocols as well as primitives such as commitment schemes and Sigma protocols.
In the summer of 2018 David took some time off to work at NASA at the Ames research centre in California.
While working at NASA Ames in the Intelligent Systems Divison, David worked on formalising (in Isabelle) safety cases for unmanned aircraft. The notion of a safety case is a broad one; in this instance the focus was on formalising the reasoning behind preventing collisions between unmanned aircraft and intruder (not necessarily malicious intruder aircraft but other aircraft in the airspace) aircraft. In general little work has been done to formalise such safety cases, however it is likely that such formalised proofs will be a legal requirement in the future, consequently it is an exciting area to work in. This is work he continues to be interested in when time allows.