INRIA a CCSD electronic archive server
Not a member yet
122212 research outputs found
Sort by
Determinacy Checking for Elpi: an Higher-Order Logic Programming language with Cut
No full textInternational audienceElpi is a higher-order logic programming language derivedfrom λProlog and widely used to extend the Rocq interactive theoremprover. Typical users are familiar with types and functional programmingbut often lack experience with backtracking.We introduce a language of signatures to declare that a predicate isoperationally deterministic, meaning that calling the predicate does notleave any choice points. The signature language handles higher-orderprograms and dynamic programs.We present a static analyzer that verifies these signatures and report itsapplication to the majority of public Elpi code in the Rocq ecosystem
Global stabilization of the cubic defocusing nonlinear Schr\"odinger equation on the torus
No full textComments welcome!In this article, we prove the (uniform) global exponential stabilization of the cubic defocusing Schr\"odinger equation on the torus d-dimensional torus, for d=1, 2 or 3, with a linear damping localized in a subset of the torus satisfying some geometrical assumptions. In particular, this answers an open question of Dehman, G\'erard, Lebeau from 2006. Our approach is based on three ingredients. First, we prove the well-posedness of the closed-loop system in Bourgain spaces. Secondly, we derive new Carleman estimates for the nonlinear equation by directly including the cubic term in the conjugated operator. Thirdly, by conjugating with energy estimates and Morawetz multipliers method, we then deduce quantitative observability estimates leading to the uniform exponential decay of the total energy of the system. As a corollary of the global stabilization result, we obtain an upper bound of the minimal time of the global null-controllability of the nonlinear equation by using a stabilization procedure and a local null-controllability result
A Mesoscale Framework for Psychedelic Drug Action in the Human Brain
No full textThe mechanism of psychedelic drug action is a dynamic area of neuroscience, with two major lines of investigation: (1) laboratory studies at the molecular and cellular level, and (2) human neuroimaging studies of functional brain networks. Despite considerable progress, there remains insufficient understanding of the link between molecular/cellular substrates of psychedelics and the whole-brain network effects that result. Here we report a study of psychedelic action that focuses on the intermediate spatial scale of local brain regions (<1cm 3 ). We analyzed the effects .</div
The impact of homeostatic inhibitory plasticity in a generative biophysical model
No full textA main characteristic of biological systems is their capacity to dynamically adapt to environmental changes. In the brain, synaptic plasticity enables the strengthening or weakening of connections between neurons, allowing neural circuits to adapt based on experience, learning, and environmental changes. Yet, it is homeostatically regulated such that it avoids excessive proliferation of synaptic contacts. These mechanisms can be studied with large-scale models of brain activity. Here, we embed a biologically grounded inhibitory-homeostatic plasticity rule into the Dynamic Mean Field (DMF) model, creating a Homeostatic Dynamic Mean Field (HDMF) model that dynamically tunes local excitation–inhibition balance. Convergence of excitatory firing rates is reached by mapping a large range of coupling strength to parameters of inhibitory synapses. The HDMF reproduces statistical observables of brain activity as well as the original DMF, and can sustain neuromodulatory perturbations without overhead computations. The HDMF can generate unprecedented sleep-like slow-wave activity, which can also coexist with wake-like asynchronous dynamics, permitting to model dissociated states of consciousness such as parasomnias. Together, these results show that a single homeostatic rule broadens the stability and expressiveness of the DMF, providing a unified platform for studying how local adaptive processes shape the diverse global dynamics of the human brain
Tamarin Unchained: Handling User-Defined AC Operators
No full textIn symbolic models, equational theories are used to model the algebraic primitives of cryptographic primitives. Automated verification tools however only handle limited classes of equational theories to avoid performance and termination issues. In particular associative and commutative (AC) symbols have often been problematic, although they are common, e.g., to model addition, multiplication, exclusive-or (XOR), multisets, etc. In this paper we extend the Tamarin prover to allow users to specify AC symbols as part of their user-defined equational theory. To avoid termination issues, we propose a novel property that bounds certain deduction chains. We use Tamarin's deduction algorithm to verify whether this bound is indeed correct for a given equational theory, generalizing previous work. We illustrate the effectiveness and efficiency of our approach using different examples, including XOR, multisets, re-encryption, Diffie-Hellman exponentiation, and distributed decryption. It turns out that our property holds for all these examples, and that, compared to Tamarin's built-in support for XOR or multisets, our approach only incurs a small overhead on startup when checking the property, but otherwise has similar performance on most examples. Reencryption and distributed decryption were previously out of scope, and our model for Diffie-Hellman exponentiation, albeit simpler than the built-in, allows for the exponentiation symbol to be reused in further equations, which is not allowed for the built-in one
EWEMrl: A White-Box Secure Cipher with Longevity
No full textInternational audienceWe propose the first updatable white-box secure cipher, EWEMrl (Extended WEM with longevity against non-adaptive read-only adversaries), and its natural extension, EWEMxl (Extended WEM with longevity against executable adversaries), both based on WEM (White-box Even-Mansour), and both achieving longevity against non-adaptive read-only malware. The notion of longevity, introduced by Koike et al., addresses continuous code leakage and is stronger than incompressibility. While Yoroi claimed longevity, but was broken by Isobe and Todo. Given the prevalence of continuous leakage, developing such ciphers is crucial in white-box cryptography. Precisely, we have the following.• We first present EWEMr (Extended WEM against non-adaptive read-only adversaries), a generalization of WEM (White-box Even-Mansour). WEM is the first (and possibly only) white-box cipher based on Even-Mansour (EM), replacing its key addition layer with a secret Sbox. EWEMr achieves a high space-hardness bound in the non-adaptive model, with a new generic proof strategy, but does not provide longevity. Instead, it serves as the base for EWEMrl.• We also present EWEMx (Extended WEM against executable adversaries), which uses EWEMr as subroutines and achieves a high space-hardness bound in the stronger adaptive model. While EWEMx does not achieve longevity, it is the base design for EWEMxl.• We next propose EWEMrl, that achieves longevity against non-adaptive read-only malware. None of the existing ciphers, such as SPNbox and SPACE, are designed for longevity. We show that EWEMrl ensures (against non-adaptive read-only adversaries) (1) longevity, (2) high space-hardness in both known-space and chosen-space settings, and (3) security against hybrid code-lifting attacks.• Finally, we introduce EWEMxl, a natural extension of EWEMrl with a structure similar to EWEMx. EWEMxl achieves (2) and (3) in the stronger adaptive model while maintaining (1) in the same non-adaptive and read-only setting.In summary, our proposals EWEMrl and EWEMxl provide longevity against nonadaptive read-only malware while ensuring security confidence in the black-box setting.</div
VLSF Decoding with Reliability Guarantees over Correlated Noncoherent Fading Channels
No full textThis report studies reliability-guaranteed decoding for variable-length stop-feedback (VLSF) codes over correlated noncoherent fading channels. The decoding rule is based on the evolution of the information density associated with a channel input-output realization. Due to channel memory, exact evaluation of this information density is intractable. To enable a constructive decoding, computable finite-blocklength lower and upper bounds on the information density that hold uniformly over time along each input-output sequence are derived. The lower bound enables a stopping-time analysis for VLSF decoding and has an operational meaning, while the upper bound quantifies the relaxation gap. Moreover, the relaxation gap between the bounds is explicitly characterized. For Gaussian signaling, the stopping-time distribution and the impact of fading correlation on decoding performance are numerically studied
BUBBLE-BLUE a multihop private network based on Bluetooth
No full textThe BUBBLE-BLUE (BB) project aims to create private Bluetooth bubbles on top of smartphones and to create a kind of terrestrial STARLINK network based on users smartphones.. In each private bubble, participants will be able to communicate autonomously, without recourse to private operator networks, neither data nor cellular, relying solely on the Bluetooth technology of smartphones. The routing strategy is based on dynamic Connected Dominant Sets (CDS). We present the specific features of a BB network as well as some simulation results on their routing performance
IA et IRM pour mieux comprendre le cerveau après un AVC - Retour d’expérience
No full textNational audienc
Convergence of weighted branching processes
No full textWe study the long-term behavior of weighted multi-type branching processes, focusing on extending classical laws of large numbers and martingale convergence to settings with infinitely many weighted particles, arbitrary type spaces and non-geometric rescaling. We demonstrate applications to Galton-Watson trees indexed by random weights and by random kernels, convergence in Wasserstein distance of the underlying mean semi-group, and convergence of ergodic averages along lineages