This project will investigate the use of formal methods in providing high-assurance, high-performance privacy-preserving data analytics solutions, and in ensuring their secure use.

In particular, we will focus on new protocols proposed by an industry partner, Oblivious AI, that leverage novel approaches to multi-party computation to support high-performance data analytics in settings where the model owner does not wish to share its parameters, and the data controller does not wish to share the data.

We will develop a high-assurance and high-performance implementation of the proposed primitive, also producing machine-checked proofs of its correctness, security and privacy properties under clearly identified trust assumptions. Further, we will investigate the adequacy of these trust assumptions, of the proposed protocol, and of blind computation in general, for specific applications of interest, likely related to the use of data analytics in government or law enforcement.