Events

Private data analytics systems preferably provide required analytic accuracy to analysts and specified privacy to individuals whose data is analyzed. Devising a general system that works for a broad range of datasets and analytic scenarios has proven to be difficult.

Differentially private systems allow for proven formal privacy guarantees. To provide these guarantees, however, differentially private mechanisms often need to add large amounts of noise to statistical results, which impairs their usability. Thus, despite the advent of mechanisms with formal guarantees, industry still uses inferior ad-hoc mechanisms that provide better analytic accuracy.

In my thesis I follow two approaches to improve the usability of private data analytics systems in general and differentially private systems in particular. First, I revisit ad-hoc mechanisms and explore the possibilities of systems that do not provide Differential Privacy or only a weak version thereof. Based on an attack analysis, I devise a set of new protection mechanisms including Query Based Bookkeeping (QBB). In contrast to previous systems, QBB only requires the history of analysts’ queries in order to provide privacy protection, but does NOT require any knowledge about the protected individuals’ data.

In my second approach I use the insights gained with QBB to propose UniTraX, the first differentially private analytics system that allows analysts to analyze part of a protected dataset without affecting the other parts and without giving up on accuracy. I show UniTraX’s usability by way of multiple case studies on real-world datasets across different domains. In all cases I demonstrate that UniTraX allows more queries than previous differentially private data analytics systems at moderate runtime overheads.

Automated reasoning in first-order logic (FOL) is becoming a mature research domain. It has led to the development of powerful tools such as superposition-based theorem provers and SMT solvers (Satisfiability Modulo Theory solvers), that have found and continue to find many applications in industry and research.

One such application is the automation of proofs in interactive theorem proving (ITP), where proof assistants are used to write computer-checked proofs of theorems, generally expressed in a variant of higher-order logic (HOL). This automation is realised via "hammers", that attempt to delegate the proof obligations to first-order automated provers. However, in the translation from HOL to FOL, hammers obfuscate the structure of terms and formulas through the application of a sequence of encodings, although it is this very structure that the provers exploit to find proofs efficiently.

This situation is less than ideal, and if until a few years ago, the ITP and ATP communities were working in parallel, mostly ignoring each other, there is nowadays a trend pushing to bring the two communities closer. The work that I will present in this talk is part of this trend. It includes ongoing research that is either improving higher-order automation with respect to ITP applications or using ITP as a vehicle for ATP research.

Producing reliable systems software is a major challenge, plagued by the ubiquitous problems of shared mutable state, pointer aliasing, dynamic memory management, and subtle concurrency issues such as race conditions; even expert programmers struggle to tame the wide variety of reasons why their programs may not behave as they intended. Formal verification offers potential solutions to many of these problems, but typically at a very high price: the mathematical techniques employed are highly-complex, and difficult for even expert researchers to understand and apply.

The relatively-new Rust programming language is designed to help with the former problem: a powerful ownership type system requires programmers to specify and restrict their discipline for referencing heap locations, providing in return the strong guarantee (almost – the talk, and Rustbelt!) that code type-checked by this system will be free from dangling pointers, unexpected aliasing, race conditions and the like. While this rules out a number of common errors, the question of whether a program behaves as intended remains.

In this talk, I’ll give an overview of the Prusti project, which leverages Rust’s type system and compiler analyses for formal verification. By combining the rich information available about a type-checked Rust program with separate user-specification of intended behaviour, Prusti enables a user to verify functional correctness of their code without interacting with a complex program logic; in particular, specifications and all interactions with our implemented tool are at the level of abstraction of Rust expressions.