Garbage collection greatly simplifies the life of the programmer, removing the need for manually deallocating memory. However, heap space usage of garbage-collected programs can be tricky to understand: to argue that the garbage collector can reclaim the space associated with a heap object, one has to prove that this object…
We consider a certain dynamic system, that is, a system with a certain internal state whose evolution is ruled by a known state update function. At regular interval, a measurement is performed. Based on this series of measurements, our objective is obtaining a good estimation of the current state of…
Static analyses aim at inferring semantic properties of programs. We distinguish two important classes of static analyses: state analyses and relational analyses. While state analyses aim at computing an over-approximation of reachable states of programs, relational analyses aim at computing functional properties over the input-output states of programs. Relational analyses…
Modern programming languages often provide functions to manipulate regular expressions in standard libraries.If they offer support for advanced features, the matching algorithm has an exponential worst-case time complexity: for some so-called vulnerable regular expressions, an attacker can craft ad hoc strings to force the matcher to exhibit an exponential behaviour…
In the second part of the talk, we tackle the setting of dynamic networks and present a quite different approach for the distributed computation of functions, which is based on popular algorithms in statistical physics, namely the Metropolis algorithm and the Push-Sum algorithm. When an upper bound on the network…
In this talk, we present several results on distributed function computation in anonymous network with broadcast communications. First, we recall the characterization, given by Boldi and Vigna, of the computable functions when agents have no information on their outgoing neighborhoods. Then we characterize the class of computable functions in networks…
When studying categories in homotopy type theory, it turns out that the well-behaved definition is that of univalent categories, that is, categories such that isomorphisms between objects are equivalent to identities between them. It has been shown that any category is weakly equivalent to a univalent one; this operation is…
Violations of program properties pose significant risks, particularly when they can be triggered by attackers. Multiple approaches has been proposed recently to detect these vulnerabilities. In this seminar, we will present a new abstract interpretation-based static analysis for this problem. By leveraging a static analysis by abstract interpretation for CTL…
For performance and scalability reasons, most cloud providers start using Field-Programmable Gate Arrays (FPGAs) to provide FPGA-based acceleration services. FPGA virtualization becomes then necessary to optimize hardware resources utilization, but raises security and privacy concerns.In this work we consider a temporal multi-tenancy environment, where a single FPGA instance running a…
In this presentation, we are interested in the Computationally Complete Symbolic Attack (CCSA) approach to security protocol verification, and its implementation in the proof assistant SQUIRREL. The proof of a protocol relies on assumptions on the security provided by its primitives (e.g. hash, encryption, etc.), which are generally formulated in…
Conversion to Static Single Assignment (SSA) form is usually viewed as a syntactic transformation algorithm that gives unique names to program variables, and reconciles these names using “phi” functions based on a notion of domination. We instead propose a semantic approach, where SSA translation is performed using a simple dataflow…
I will present the work I did during my M1 internship in Dresden on two-variable logics (especially C², the two variable first-order logic with counting quantifiers), trying to show that every satisfiable sentence admits a model of finite cliquewidth.
One of the most important results in distributed computing was published in April 1985 by Fischer, Lynch and Paterson. Their short paper “Impossibility of Distributed Consensus with One Faulty Process” definitively placed an upper bound on what it is possible to achieve with distributed processes in an asynchronous environment. The problem of…
Probabilistic programming is a method for Bayesian statistics in which statistical models are encoded as programs. In this talk I will introduce probabilistic programming and the problem of inference. I will then present two kinds of semantics for probabilistic programs: one based on measures and probability kernels, and one based…
It is widely known that the precision of a program analyzer is closely related to intensional program properties, namely, properties concerning how the program is written. This explains, for instance, the interest in code obfuscation techniques, namely, tools explicitly designed to degrade the results of program analysis by operating syntactic…
We present an abstract interpretation framework for proving liveness properties of imperative programs, to ensure that some event happens once or infinitely many times during program execution. A further abstraction based on piecewise-defined ranking functions yields a static analysis that automatically infers sufficient conditions for these liveness properties as well as upper…
Fundamental concerns exist on the trustworthiness of deep learning systems, with examples including robustness, fairness, privacy and explainability. Phenomena like adversarial examples prompt the need to train robust networks and to provide formal guarantees on their behaviour. In this talk, we will first introduce the neural network verification problem. Then,…
We present the article “Shape analysis by means of bi-abduction” by Cristiano Calcagno, Dino Distefano, Peter O’Hearn, Hongseok Yang published at POPL in 2009. This article addresses the problem of pre- & post-condition generation and verification for function analysis. In order to resolve this problem, the authors introduce the notion…
Modeling paradigms for Systems Biology plays an important role in investigating the orchestrated function of various biological systems. Additionally, they permit one to study a system in-silico in order to gain mechanistic insights from the trajectories resulting from the model. A common battle to derive an ideal representation for a…
We present an approach to language design aimed at enforcing modular security, where a security architect can define specific object capabilities that enforce custom security properties. Unlike traditional models that assume an uncompromised system (‘clean garden’), this model (‘dark forest’) assumes local machines are already compromised but anchored by a…
Runtime errors that can be triggered by an attacker are sensibly more dangerous than others, as they not only result in program failure, but can also be exploited and lead to security breaches such as Denial-of-Service attacks or remote code execution. Proving the absence of exploitable runtime errors is challenging,…
In this talk, we will present an overview of the abstract domains that drive the Flambda 2 optimizer for In this talk, we will present an overview of the abstract domains that drive the Flambda 2 optimizer for OCaml programs. Like most optimizing compilers, Flambda 2 relies on static analysis…
Probabilistic programming languages aim at designing and implementing algorithms that compute over probability distributions rather than states. They feature dedicated primitives for sampling and conditioning. Moreover, the evaluation of probabilistic programs relies on general purpose inference engines. In the last few years, several languages such as Pyro, Edward or Stan…
I present two impossibility proofs for consensus in the presence of byzantine failures based on graph coverings.
Event structures, trace automata, and Petri nets are fundamental models in concurrency theory. There exist nice interpretations of these structures as combinatorial and geometric objects and both conjectures can be reformulated in this framework. Namely, from a graph theoretical point of view, the domains of prime event structures correspond exactly…
We tackle the problem of testing and verifying “incomplete” programs—that contain components whose source code is either unavailable (like third-party libraries and cloud-based APIs), or too complex to model formally (like large machine learning models). We show how classical techniques like symbolic execution, deductive verification and SMT solving can be…
In this work, we propose a static analysis by abstract interpretation for Robust CTL properties by taking advantage of our static analyzer FuncTion. A CTL property robustly hold if a controlled input imply it whatever the value of the uncontrolled input. Furthermore, we enhance Conflict Driven Analysis (CDA), an extension…
The remarkable success stories of deep learning systems give the impression that large advanced neural networks are all we need, and they will eventually make all the symbolic techniques obsolete. This predicted death of symbolic techniques might or might not happen in the end. But I believe that at least in the…
Reinforcement learning (RL) presents a promising approach to solving highly non-linear control tasks that are often challenging for classical control methods. In this talk, we present a learner-verifier framework for solving control tasks in stochastic systems with formal guarantees on reachability, safety or reach-avoidance specifications. Given a specification and a…
The goal of the PhD is to design, prove correct, implement, and experiment on static program analyses to discover executions that are formally guaranteed to be erroneous and, dually, infer sufficient conditions for program correctness. The error is only reported due to over-approximations (so-called false alarm). Backward analyses have been…
The Bakery algorithm is a landmark algorithm for ensuring mutual exclusion among N processes that communicate via shared variables. Starting from existing TLA+ specifications, we use the recently developed IC3PO parameterized model checker to automatically compute inductive invariants for two versions of the algorithm. We compare the machine-generated invariants with…
Traditional separation logic-based shape analyses utilize inductive summarizing predicates so as to capture general properties of the layout of data-structures, to verify accurate manipulations of, e.g., various forms of lists or trees. However, they also usually abstract away contents properties, so that they may only verify memory safety and invariance…
We consider a distributed system in which agents communicate by sending messages and operate in synchronous rounds (roughly, all nodes update their internal state at the same frequency). There are many ways to model the communications on a distributed systems using a probabilistic approach. For example, in the PUSH model,…
We investigate the impact of potential symmetries in site-graph rewriting rules on the overall behavior of the system which are induced by these rules. For this purpose, we introduce a categorical framework in which rules are seen as pairs of embeddings, the application of a rule as a universal construction…
In this talk, I present several computability results in anonymous networks with broadcast communications. First, I recall the characterization, given by Hendrickx and Tsitsiklis, of the computable functions when agents have no information on their outgoing neighborhoods. Then I give the characterization of computable functions in networks with either (a)…
Proving that programs cannot crash is important, especially in embedded programs that are critical. The abstract interpretation framework gives tools to prove such properties at scale. Expressing complex properties on program states (the possible values of variables at given program points) can be very costly. This is why symbolic methods…
We present communication closed Distal protocol in two steps: 1) We introduce synchronization tags that capture the round numbers in synchronous protocols, 2) We show how to use this synchronization tag to reduce an asynchronous execution into a sequential one.
Much discussion exists about what is computation, but less about what is a computational problem. In the sequential setting, Turing’s definition of computational problem was based on functions. In a concurrent setting, various notions of distributed problems have been used, under different models of computation, ranging from models equivalent to…
In the last decades, logical or discrete models have emerged as a successful paradigm for capturing and predicting the behaviors of systems of molecular interactions. Intuitively, they consist in sampling the abundance of each kind of biochemical entity within finite sets of intervals and deriving transitions accordingly. On one hand,…
In recent years, the importance of data science applications to analyse phenomena in different areas of knowledge has increased, so it has become essential to verify the correctness of this type of programs. One of the ways in which a data science application can be verified is through the analysis…
Data science plays a crucial role in critical decision making in a variety of fields, including healthcare, finance, and avionics. Therefore, disastrous outcomes may result from programming errors in these safety-critical settings, especially when they do not result in software failures but instead produce a plausible yet erroneous outcome. Such…
Data dissemination is a fundamental task in distributed computing. This talk will explore broadcast problems in various innovative models where the communication network connecting n processes is dynamic (e.g., due to mobility or failures) and controlled by an adversary. In the main model, the processes transitively communicate their ids in…
Imprecision is inherent in any decidable (sound) approximation of undecidable program properties. In abstract interpretation this corresponds to the release of false alarms, e.g., when it is used for program analysis and program verification. As all alarming systems, a program analysis tool is credible when few false alarms are reported.…
Formally describing the specification of a programming language is a challenging task. Specifications that use imperative features, such as state or exceptions, or that manipulate continuations are very difficult to describe in usual operational semantics, such as natural semantics or SOS.In addition, these descriptions are not objects that can be…
Symbolic execution is a program analysis technique commonly utilized to determine whether programs violate properties and, in case violations are found, to generate inputs that can trigger them. Used in the context of security properties such as noninterference, symbolic execution is precise when looking for counter-example pairs of traces when insecure information…
We propose a systematic approach to approximate the behavior of models of polymers synthesis/degradation, described in Kappa. Our abstraction consists in focusing on the behavior of all the patterns of size less than a given parameter. We infer symbolic equalities and inequalities which intentionally may be understood as algebraic constructions…
In this talk, we will discuss a symbolic representation for support vector machines (SVMs) by means of abstract interpretation. We leverage this abstraction in two ways: (1) to enhance the interpretability of SVMs by deriving a novel feature importance measure called abstract feature importance (AFI), that does not depend in any way on a given dataset of…
Separation logic-based shape analyses aim to infer properties of heap manipulating programs. These analyses abstract the heap using separation logic including inductive summarizing predicates. Whereas they have been successfully applied to prove properties of data structures layout, they usually abstract away some properties of the data structures contents. As a…
Probabilistic programming languages aim at designing and implementing algorithms that compute over probability distributions rather than states. They feature dedicated primitives for sampling and conditioning. Moreover, the evaluation of probabilistic programs relies on general purpose inference engines. In the last few years, several languages such as Pyro, Edward or Stan…
Asynchronous code is remarkably hard to get right, making it a common source of errors in TypeScript code. However, we would not be able to write TypeScript applications without it, because it enables long-running actions without freezing the current view. Developers usually rely on manual inspection to understand it, which is quite…
