Invited Speakers
-
Adi Shamir, Department of Computer Science, Weizmann Institute of Science, Rehovot, Israel
Bio:
Professor Adi Shamir was born in Israel in 1952, and received his PhD from the Weizmann Institute of Science in 1977. He is one of the founders of modern cryptography, and had made significant contributions to many of its branches. In 1977 he co-invented (together with Ron Rivest and Len Adleman) the RSA cryptosystem, which remains the best known and most commonly used public key encryption and signature scheme. Among his other inventions are secret sharing schemes, identity-based schemes, Zero-knowledge identification and signature schemes, ring signatures, and a variety of both classical and side-channel attacks on cryptosystems including differential cryptanalysis, cache attacks, bug attacks, and acoustic attacks. For these contributions he received the Pius XI Gold Medal in 1992, the Turing Award in 2002, the Israel Prize in 2008, and the Japan Prize in 2017. He is a member of the Israeli Academy, the US National Academy of Science, the Academia Europaea, the French Academy of Science, and the Royal Society.
A New Theory of Adversarial Examples in Machine Learning: The extreme fragility of deep neural networks when presented with tiny perturbations in their inputs was independently discovered by several research groups in 2013. Due to their mysterious properties and major security implications, these adversarial examples had been studied extensively over the last eight years, but in spite of enormous effort they remained a baffling phenomenon with no clear explanation. In particular, it was not clear why a tiny distance away from almost any cat image there are images which are recognized with a very high level of confidence as cars, planes, frogs, horses, or any other desired class, why the adversarial modification which turns a cat into a car does not look like a car at all, and why a network which was adversarially trained with randomly permuted labels (so that it never saw any image which looks like a cat being called a cat) still recognizes most cat images as cats. The goal of this talk is to introduce a new theory of adversarial examples, which we call the Dimpled Manifold Model. It can easily explain in a simple and intuitive way why they exist and why they have all the bizarre properties mentioned above. In addition, it sheds new light on broader issues in machine learning such as what happens to deep neural networks during regular and during adversarial training. Experimental support for this theory, obtained jointly with Odelia Melamed and Oriel BenShmuel, will be presented and discussed in the last part of the talk.
-
Karthikeyan Bhargavan, Inria Paris, France, karthikeyan.bhargavan@inria.fr
Bio:
Karthikeyan Bhargavan is a researcher at INRIA, where he leads a group
called Prosecco (Programming Securely with Cryptography).
He received his B.Tech from IIT Delhi in 1997, his PhD from the
University of Pennsylvania in 2003, and worked as a researcher in
Microsoft Research Cambridge before joining INRIA in 2009.Bhargavan is
interested in the design and implementation of program
verification techniques that enable robust implementations and formal
analyses of real-world security applications.His recent work
focuses on using dependent type systems, such as F*. to investigate the
(in)security of cryptographic protocols, such as Transport Layer
Security (TLS),and to build verified cryptographic libraries, such as HACL*.For more
details on the Prosecco research group and it publications, see
http://prosecco.inria.fr
High-Assurance High-Performance Cryptographic Software:Every year, many new cryptographic algorithms, constructions, and protocols are proposed, standardized, and deployed across a variety of platforms. However, implementing these cryptographic mechanisms remains a challenging and error prone task, typically entrusted to a few specialists who understand both the subtleties of cryptographic design and the intricacies of the target hardware architectures. The resulting code is comprehensively tested, fuzzed, and subject to manual reviews and audits by experts both before and after deployment. Despite all these measures, however, bugs in cryptographic software are regularly uncovered, often resulting in embarrassing attacks. In this talk, we will show how formal verification can be used to bring higher assurance to cryptographic software development [1]. In particular, we will examine the HACL* verified cryptographic library, which implements a full suite of modern crypto algorithms and is used by mainstream software like the Mozilla Firefox web browser, the WireGuard VPN, the Tezos blockchain, and the Election Guard voting software. We will discuss the verification and compilation methodology used by HACL* to generate portable C code for each cryptographic algorithm [5]. We will see how this methodology can be extended to generate verified C code optimized for single-instruction-multiple-data (SIMD) architectures [3]. We will also show how verified C code from HACL* can be safely composed with verified assembly code for improved performance [4]. By combining these techniques, the verified code in HACL* is as fast as (and sometimes faster than) the unverified handoptimized C and assembly code in mainstream cryptographic libraries. Despite its critical importance, the cryptographic library is only one component in a cryptographic software stack that typically also includes communication protocols, key management, and application code. We will conclude by discussing how the formal verification guarantees of the HACL* cryptographic library can be combined with symbolic protocol analysis to build provably secure implementations of modern real-world cryptographic protocols like TLS 1.3, Signal, and ACME [2] -
Maria Naya-Plasencia, Inria Paris, France
Bio:
Maria Naya-Plasencia is a research director at Inria, France. Her main
research topic is symmetric cryptography.She has served in many
program committees of IACR conferences and been the co-editor in chief
of the IACR ToSC journal in 2016 and 2017. In September 2017, she was
awarded an ERC Starting grant for the QUASYModo project on quantum-safe
symmetric cryptography, and in 2019 she was awarded the Inria-Academy of
Sciences Young Researcher Prize.
Quantum Safe Symmetric Cryptography: During this talk we will introduce the context and summarize the state-of-the-art of the main quantum symmetric cryptanalysis results, providing the details of some particularly interesting cases. We will also present the scenario of some related open problems that are yet to be solved or improved.