Approximate fully homomorphic encryption (FHE) schemes such as the CKKS scheme (Asiacrypt ’17) are popular in practice due to their efficiency and utility for machine learning applications. Unfortunately, Li and Micciancio (Eurocrypt, ’21) showed that, while achieving standard semantic (or IND-CPA security), the CKKS scheme is broken under a variant security notion known as IND-CPAD. Subsequently, Li, Micciancio, Schultz, and Sorrell (Crypto ’22) proved the security of the CKKS scheme with a noise-flooding countermeasure, which adds Gaussian noise of sufficiently high variance before outputting the decrypted value. However, the variance required for provable security is very high, inducing a large loss in message precision.

In this work, we ask whether there is an intermediate noise-flooding level, which may not be provably secure, but allows to maintain the performance of the scheme, while resisting known attacks. We analyze the security with respect to different adversarial models and various types of attacks. We investigate the effectiveness of lattice reduction attacks, guessing attacks and hybrid attacks with noise-flooding with variance ρ2circ, the variance of the noise already present in the ciphertext as estimated by an average-case analysis, 100 · ρ2circ, and t · ρ2circ, where t is the number of decryption queries. For noise levels of ρ2circ and 100 · ρ2circ, we find that a full guessing attack is feasible for all parameter sets and circuit types. We find that a lattice reduction attack is the most effective attack for noise-flooding level t · ρ2circ, but it only induces at most a several bit reduction in the security level.

Due to the large dimension and modulus in typical FHE parameter sets, previous techniques even for estimating the concrete security of these attacks – such as those in (Dachman-Soled, Ducas, Gong, Rossi, Crypto ’20) – become computationally infeasible, since they involve high dimensional and high precision matrix multiplication and inversion. We therefore develop new techniques that allow us to perform fast security estimation, even for FHE-size parameter sets.

In this talk I will present the work I have done concerning the specification and analysis of normative documents using deontic-based formalisms. I will also discuss challenges in the area and future research directions, including applications in smart contracts.

Short bio: Gerardo Schneider received a PhD degree in Computer Science from the University Joseph Fourier (thesis done at the VERIMAG laboratory), Grenoble (France), in 2002. From 2003 till 2009 he was a researcher at Uppsala University (Sweden), Irisa/INRIA Rennes (France), and the University of Oslo (Norway). He joined the Department of Computer Science and Engineering at the University of Gothenburg (Sweden) in July 2009, where he has been a full professor since July 2014. He acted as Head of the Formal Methods Division since Jan 2017 till Dec 2023, and since Dec 2023 he has been the head of the Data Science and AI division. His research interests include formal verification, combination of verification techniques (e.g., static and runtime verification, controller synthesis and runtime verification), the specification and analysis of normative documents, and privacy. (http://www.cse.chalmers.se/~gersch).

This talk will show some of the recent advances we are doing at Microsoft Research towards agents capable of modeling complex environments and human behaviors, which is a key goal of artificial intelligence research. My team focuses on applications of AI in video games, as this has the potential of empowering game developers to realize new creative visions. The talk is split in two parts. In the first one, I will focus on diffusion models as generative models of human behavior. Previously shown to have impressive image generation capabilities, I present insights that unlock applications to imitation learning for sequential decision making. In the second part of the talk, I will discuss a recent project extending modern language modeling with new modalities to build a world and action model of an Xbox game.

Recent years have been pivotal in the field of Industrial Control Systems (ICS) security, with a large number of high-profile attacks exposing the lack of a design-for-security initiative in ICS. The evolution of ICS abstracting the control logic to a purely software level hosted on a generic OS, combined with hyperconnectivity and the integration of popular open source libraries providing advanced features, have expanded the ICS attack surface by increasing the entry points and by allowing traditional software vulnerabilities to be repurposed to the ICS domain. In this seminar, we will shed light to the security landscape of modern ICS, dissecting firmware from the dominant vendors and motivating the need of employing appropriate vulnerability assessment tools. We will present methodologies for blackbox fuzzing of modern ICS, both directly using the device and by using the development software. We will then proceed with methodologies on hotpatching, since ICS cannot be easily restarted in order to patch any discovered vulnerabilities. We will demonstrate our proposed methodologies on various critical infrastructure testbeds.

Adversaries exploit vulnerabilities to compromise systems. For instance, a vulnerability in a Web browser sandbox may allow an attacker to leak private data. Reducing the number of bugs improves security guarantees. We will discuss two key scenarios of system security: detecting bugs introduced by developers and bugs introduced by compilers. Since software is written by human beings, any program suffers from bugs. Improving testing prevents bugs from reaching production environments. Even for bug-free programs, compilers can still introduce hideous side effects that undermine the security premises. I will first introduce automatic testing, while the second part will discuss security challenges caused by misalignments between compiler optimizations and security assumptions.