We need cryptography that we can trust. Yet the design, analysis, and implementation of cryptographic libraries is a challenging task, which requires deep insights into mathematics and computer science. Computer-aided cryptography is a nascent research area which aims to provide mathematically rigorous methods based on program synthesis and program verification for building zero-defect cryptographic libraries. The talk will show how computer-aided cryptography can be used for discovering and verifying cryptographic algorithms, and for analyzing their resistance against side channels and physical attacks. No prior knowledge of cryptography will be required.

This talk will introduce the seL4 microkernel, its binary-level correctness proof up to high-level security properties, and the”] application of the seL4 kernel as security foundation for high-assurance autonomous air vehicles. Most of this work is based on the machine-checked interactive proof assistant Isabelle/HOL, and the talk will discuss the role of proof engineering and automated provers in this kind of deep-property software verification at scale.

Constrained sampling and counting are two fundamental problems in data analysis. In constrained sampling the task is to sample randomly, subject to a given weighting function, from the set of solutions to a set of given constraints. This problem has numerous applications, including probabilistic reasoning, machine learning, statistical physics, and constrained-random verification. A related problem is that of constrained counting, where the task is to count the total weight, subject to a given weighting function, of the set of solutions of the given constraints. This problem has applications in machine learning, probabilistic reasoning, and planning, among other areas. Both problems can be viewed as aspects of intelligence, which is to understand the structure of the solution space of a given set of constraints.

This project focuses on the development of new algorithmic techniques for constrained sampling and counting, based on a universal hashing — a classical algorithmic technique in theoretical computer science.  Many of the ideas underlying the proposed approach were go back to the 1980s, but they have never been reduced to practice. Recent progress in Boolean reasoning is enabling us to reduce these algorithmic ideas to practice, and obtain breakthrough results in constrained sampling and counting, providing a new algorithmic toolbox in design verification, machine learning, probabilistic reasoning, and the like.

Joint work with Supratik Chakraborty and Kuldeep S. Meel.