Many proofs of interactive cryptographic protocols (e.g., as in Universal Composability) operate by proving the protocol to be observationally equivalent to an idealized specification. Formal tool support for proving observational equivalence of cryptographic protocols is a nascent area of research. Current tools either support only certain forms of observational equivalence or require an amount of proof effort that makes large-scale verification infeasible. To bridge this gap, we introduce equational techniques for cryptography in the computational model. Our core calculus, the Interactive Probabilistic Dependency Logic (IPDL), is simple, expressive, and addresses technical issues such as probabilistic behaviors, distributed message-passing, and resource-bounded adversaries and simulators. We demonstrate our techniques on a number of case studies, including a distributed coin toss protocol, Oblivious Transfer, and the GMW multi-party computation protocol. All proofs of our case studies are mechanized.

The continuously increasing interest in intelligent autonomous systems underlines the need for new developments in cyber-physical systems that can learn, adapt, and reason. Towards this direction, we will formally analyze the properties of learning for inference, verification, and control of general systems, when time and computational resources are limited, and robustness and interpretability are prioritized. We will focus on the notion of progressive learning: an adaptive process that hierarchically approximates the solution of an optimal decision-making problem given real-time observations of a system and its environment. We will introduce the Online Deterministic Annealing (ODA) approach as a gradient-free stochastic optimization method to construct a learning model that progressively increases its complexity as needed, through an intuitive bifurcation phenomenon. We will study the properties of robustness and interpretability, and the importance of being able to control the performance-complexity trade-off in real time. Finally, we will discuss how these properties can be incorporated in the development of system identification and verification algorithms with a wide range of applications, from robotics and multi-agent systems to automatic theorem proving and software debugging.

Computer systems and software play a vital role in the functioning of our society. Ensuring their security is of utmost importance and is more relevant now than ever before. Although various security measures have made it more challenging, adversaries keep finding innovative ways to exploit vulnerabilities around them. In this talk, I will share my vision for establishing trustworthy software and systems by showcasing examples of my work in the field. I will also address new security challenges at the intersection of software and microarchitectural vulnerabilities. Specifically, I will present our groundbreaking research on BlindSide, a new exploitation technique that relies on a single memory corruption vulnerability to hack the Linux kernel without causing any crashes. Finally, I will conclude by highlighting ongoing efforts and future research directions in the realm of systems and software security.

Autonomous Systems offer hope towards moving away from mechanized, unsafe, manual, often inefficient practices. Last decade has seen several small, but important, steps towards making this dream into reality. These advancements have helped us to achieve limited autonomy in several places, such as, driving, factory floors, surgeries, wearables and home assistants, etc. Nevertheless, autonomous systems are required to operate in a wide range of environment with uncertainties (viz., sensor errors, timing errors, dynamic nature of the environment, etc.). Such environmental uncertainties, even when present in small amount, can have drastic impact on the safety of the system—thus hampering the goal of achieving higher degree of autonomy, especially in safety critical domains. To this end, I shall discuss formal techniques that are able to verify and design autonomous systems for safety, even under the presence of such uncertainties, allowing for their trustworthy deployment in the real world. Specifically, I shall discuss monitoring techniques for autonomous systems from available (noisy) logs, and safety-verification techniques of autonomous system controllers under timing uncertainties. Secondly, using heterogeneous learning-based cloud computing models that can balance uncertainty in output and computation cost, I will present techniques for designing safe and performance-optimal autonomous systems. I will conclude this talk by outlining a number of future research directions on how we can build a network/environment where several autonomous systems coordinate among themselves and achieve their goals in a safe and performance optimal manner even in presence of uncertainties.

Secure Multiparty Computation (MPC) allows a set of mutually distrusting parties to jointly perform a computation on their private inputs in a way no information about their inputs is revealed, except the output of the computation. The use of MPC is promising in real-life situations that demand both privacy and computation at the same time. The aim of my research is to advance our understanding of the feasibility of tasks related to MPC, and to construct efficient MPC protocols in various adversarial and network settings. More specifically, I am interested in in the following three research directions: Resource-Efficient MPC. One of the fundamental metrics to analyze efficiency of MPC protocols is communication complexity, that measures the total communication of the protocol across all parties. However, this standard metric ignores the practically important aspect of load-balancing. We explore the notion of Bottleneck Complexity (defined as maximum communication complexity of any party in the protocol) that addresses this issue. Realistic Adversaries in MPC. As per the standard security definition in MPC, a protocol is considered secure if an adversary learns nothing about honest parties’ inputs (other than what can be derived from the output). We observe that this definition permits honest parties to learn other honest parties’ inputs, which is clearly undesirable in real-life. This motivates the notion of ‘friends-and-foes’ (FaF) security, that addresses this issue. You Only Speak Once (YOSO) MPC. The above two research directions — resource efficiency, and modelling realistic adversaries — seem to conflict since achieving security against more powerful adversaries is, intuitively, easier when the protocols use more resources. However, the large-scale distributed setting of YOSO MPC manages to strike a balance between security and efficiency.

Open Access (OA) is a mechanism that allows for free and immediate access to research results and data. It aims to enhance global dissemination, reduce research duplication, and increase the use of scientific contributions in teaching programs, among others. However, a survey has revealed that many researchers need more adequate knowledge about OA and the transition to it. While making research products openly available is a great idea for communicating science and knowledge, shifting the costs from readers to authors induces risks that must be identified, understood, and analyzed. It is worth noting that OA does not eliminate publishing costs. The move to OA can lead to financial bias if publishers take advantage of the opportunity to publish more or engage in unethical practices. This could create an unequal playing field, where some researchers have an advantage over others due to their access to resources. The talk describes the scientific publishing market, the problems emerging from the current transition to OA, and potential countermeasures to mitigate the current difficulties.

The most widely studied language for expressing statements in the context of Zero-Knowledge (ZK) proofs is arithmetic circuit satisfiability. In this talk we present circom, a programming language and a compiler that allows the programmer to provide a low-level description of the arithmetic circuit together with an effective way to execute it. Challenging constraint manipulation and analysis problems will be introduced as well as some safety properties of circom programs that need to be checked. New language features focused on enhancing security will be discussed.

Non-volatile main memory (NVMM) is a new tier in the memory hierarchy that offers jointly the durability of spinning disks, near-DRAM speed and byte addressability. This talk presents J-NVM, a fully-fledged interface to use NVMM in the Java language. J-NVM relies on proxy objects that intermediate direct off-heap access to NVMM. We present the internals of J-NVM and how to use it in the context of a modern distributed data store. This talk is based on a paper in SOSP'21: http://www-public.it-sudparis.eu/~thomas_g/research/biblio/2021/lefort-sosp-jnvm.pdf

Self-adaptation is often defined as the ability of systems to alter at runtime their behaviour in response to changes in their environment, capabilities and goals that were unforseen at design time. I will discuss why I believe one interesting route to achieving self-adaptation is to endow systems with the capability of synthesising at runtime discrete event controllers.I will provide an overview of the work we have done in this direction and some of the challenges that remain, covering software architectures, modelling and learning approaches for defining novel discrete event cotrol problems, and algorithms to solve them.

The context-free language (CFL) reachability problem on graphs (as well as a closely related problem of language emptiness for pushdown automata) is a core problem for interprocedural program analysis and model checking. It can be solved in cubic time but, despite years of efforts, there is no truly sub-cubic algorithm known for it.

We study the related certification task: given a problem instance, are there small and efficiently checkable certificates for the existence and for the non-existence of a path? We show that there exist succinct certificates, of quadratic size, which can be checked in subcubic (matrix multiplication) time.

In this talk, I will introduce CFL reachability and standard algorithms for it and discuss our certification results. I will also discuss the question of whether faster algorithms for CFL reachability could lead to faster algorithms for other combinatorial problems such as SAT (a "fine-grained complexity" question).

Smart contracts are immutable programs deployed on the blockchain that can manage significant assets. Because of this, verification and validation of smart contracts is of vital importance. Indeed, it is industrial practice to hire independent specialized companies to audit smart contracts before deployment. Auditors typically rely on a combination of tools and experience but still fail to identify problems in smart contracts before deployment, causing significant losses. In this talk, I will discuss our experience using predicate abstraction to construct models which can be used by auditors to explore and validate smart contact behaviour at the function call level by proposing predicates that expose different aspects of the contract.