Francesco Dagnino

Francesco Gavazzo

A Fibrational Tale of Operational Logical Relations

Keywords: 2012 ACM Subject Classification Theory of computation → Operational semantics logical relations, operational semantics, fibrations, generic effects, program distance Digital Object Identifier 10.4230/LIPIcs.FSCD.2022.3

Logical relations built on top of an operational semantics are one of the most successful proof methods in programming language semantics. In recent years, more and more expressive notions of operationally-based logical relations have been designed and applied to specific families of languages. However, a unifying abstract framework for operationally-based logical relations is still missing. We show how fibrations can provide a uniform treatment of operational logical relations, using as reference example a λ-calculus with generic effects endowed with a novel, abstract operational semantics defined on a large class of categories. Moreover, this abstract perspective allows us to give a solid mathematical ground also to differential logical relations -a recently introduced notion of higher-order distance between programs -both pure and effectful, bringing them back to a common picture with traditional ones.

Introduction

Logical relations [START_REF] Reynolds | Types, abstraction and parametric polymorphism[END_REF] are one of the most successful proof techniques in logic and programming language semantics. Introduced in proof theory [START_REF] Tait | Intensional interpretations of functionals of finite type I[END_REF][START_REF] Girard | Proofs and Types[END_REF] in their unary form, logical relations have soon became a main tool in programming language semantics. In fact, starting with the seminal work by Reynolds [START_REF] Reynolds | Types, abstraction and parametric polymorphism[END_REF], Plotkin [START_REF] Plotkin | Lambda-definability and logical relations[END_REF], and Statman [START_REF] Statman | Logical relations and the typed lambda-calculus[END_REF], logical relations have been extensively used to study both the denotational and operational behaviour of programs. 1 Logical relations (and predicates) mostly come in two flavours, depending on whether they are defined relying on the operational or denotational semantics of a language. We refer to logical relations of the first kind as operational logical relations and to logical relations of the second kind as denotational logical relations. Due to their link with denotational semantics, denotational logical relations have been extensively studied in the last decades, both for specific programming languages and in the abstract, this way leading to beautiful general theories of (logical) predicates and relations on program denotations. In particular, starting with the work by Reynolds and Ma [START_REF] Ma | Types, abstractions, and parametric polymorphism, part 2[END_REF], Mitchell and Scedrov [START_REF] Mitchell | Notes on sconing and relators[END_REF], and Hermida [START_REF] Hermida | Fibrations, logical predicates and indeterminates[END_REF], researchers have started to investigate notions of (logical) predicates and relations in a general categorical setting, this way giving rise to an abstract understanding of relations over (the denotational semantics of) programs centred around the notions of fibrations [START_REF] Hermida | Fibrations, logical predicates and indeterminates[END_REF][START_REF] Ghani | Bifibrational functorial semantics of parametric polymorphism[END_REF][START_REF] Sojakova | A general framework for relational parametricity[END_REF][START_REF] Katsumata | Codensity lifting of monads and its dual[END_REF][START_REF] Katsumata | Relating computational effects by ⊤⊤-lifting[END_REF][START_REF] Katsumata | Parametric effect monads and semantics of effect systems[END_REF][START_REF] Katsumata | A semantic formulation of tt-lifting and logical predicates for computational metalanguage[END_REF] reflexive graphs [START_REF] O'hearn | Parametricity and local variables[END_REF][START_REF] Robinson | Reflexive graphs and parametric polymorphism[END_REF][START_REF] Dunphy | Parametric limits[END_REF][START_REF] Hermida | Logical relations and parametricity -A reynolds programme for category theory and programming languages[END_REF], and factorisation systems [START_REF] Kammar | Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics[END_REF][START_REF] Hughes | Factorization systems and fibrations: Toward a fibred birkhoff variety theorem[END_REF][START_REF] Goubault-Larrecq | Logical relations for monadic types[END_REF]. The byproduct of all of that is a general, highly modular theory of denotational logical relations that has been successfully applied to a large array of language features, ranging from parametricty and polymorphism [START_REF] Ghani | Bifibrational functorial semantics of parametric polymorphism[END_REF][START_REF] Sojakova | A general framework for relational parametricity[END_REF][START_REF] Dunphy | Parametric limits[END_REF] to computational effects [START_REF] Katsumata | Codensity lifting of monads and its dual[END_REF][START_REF] Katsumata | Relating computational effects by ⊤⊤-lifting[END_REF][START_REF] Katsumata | Parametric effect monads and semantics of effect systems[END_REF][START_REF] Katsumata | A semantic formulation of tt-lifting and logical predicates for computational metalanguage[END_REF][START_REF] Leijen | Implementing algebraic effects in c[END_REF][START_REF] Kammar | Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics[END_REF][START_REF] Goubault-Larrecq | Logical relations for monadic types[END_REF].

On the operational side, researchers have focused more on the development and applications of expressive notions of logical relations for specific (families of) languages, rather than on their underlying theory. In fact, operational logical relations being based on operational semantics, they can be easily defined for languages for which finding the right denotational model is difficult, this way making operational logical relations a handy and lightweight technique, especially when compared to its denotational counterpart. As a paradigmatic example, consider the case of stochastic λ-calculi and their operational techniques [START_REF] Borgström | A lambdacalculus foundation for universal probabilistic programming[END_REF][START_REF] Dal | On bisimilarity in lambda calculi with continuous probabilistic choice[END_REF][START_REF] Wand | Contextual equivalence for a probabilistic language with continuous random variables and recursion[END_REF] which can be (easily) defined relying on the category of measurable spaces and measurable functions, but whose denotational semantics have required the introduction of highly nontrivial mathematical structures [START_REF] Staton | Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints[END_REF][START_REF] Staton | Commutative semantics for probabilistic programming[END_REF][START_REF] Vákár | A domain theory for statistical probabilistic programming[END_REF][START_REF] Ehrhard | Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming[END_REF], since the category measurable spaces (and measurable functions) is not closed [START_REF] Aumann | Borel structures for function spaces[END_REF].

The wide applicability of operational logical relations, however, has also prevented the latter to organise as a uniform corpus of techniques with a common underlying theory. Operational logical relations result in a mosaic of powerful techniques applied to a variety of languages -including higher-order, functional, imperative, and concurrent languages [START_REF] Dreyer | Logical step-indexed logical relations[END_REF][START_REF] Ahmed | Step-indexed syntactic logical relations for recursive and quantified types[END_REF][START_REF] Joseph Turon | Logical relations for fine-grained concurrency[END_REF][START_REF] Appel | An indexed model of recursive types for foundational proof-carrying code[END_REF][START_REF] Crary | Syntactic logical relations for polymorphic and recursive types[END_REF][START_REF] Dreyer | The impact of higher-order state and control effects on local relational reasoning[END_REF]; both pure and (co)effectful [START_REF] Johann | A generic operational metatheory for algebraic effects[END_REF][START_REF] Dal | Effectful program distancing[END_REF][START_REF] Abel | A unified view of modalities in type systems[END_REF][START_REF] Birkedal | A kripke logical relation for effect-based program transformations[END_REF][START_REF] Hofmann | Logical relations and nondeterminism[END_REF][START_REF] Benton | Abstract effects and proof-relevant logical relations[END_REF][START_REF] Biernacki | Handle with care: relational interpretation of algebraic effects and handlers[END_REF][START_REF] Bizjak | Step-indexed logical relations for probability[END_REF] -whose relationship, however, is unclear. This situation creates a peculiar scenario where, on the one hand, the effectiveness of operational logical relations has been proved by their many applications but, on the other hand, a foundational understanding of operational logical relations is still missing, the main consequence of that being the lack of modularity in their development. All of that becomes even worst if one also takes into account more recent forms of logical relations, such as metric [START_REF] Reed | Distance makes the types grow stronger: a calculus for differential privacy[END_REF][START_REF] Pistone | On generalized metric spaces for the simply typed lambda-calculus[END_REF] and differential [START_REF] Dal Lago | Differential logical relations, part I: the simply-typed case[END_REF][START_REF] Dal | Differential logical relations part II: increments and derivatives[END_REF][START_REF] Dal | Differential logical relations, part II increments and derivatives[END_REF][START_REF] Dal | Effectful program distancing[END_REF] ones, that go beyond traditional relational reasoning.

In this paper, we show that much in the same way denotational logical relations can be uniformly understood in terms of fibrations, it is possible to give a uniform account of operational logical relations relying on the language of fibrations. In this respect, our contribution is twofold.

Operational Logical Relations, Fibrationally. Our first contribution is the development of a general, abstract notion of an operational logical relation in terms of fibrations for a λcalculus with generic effects. Fibrations are a mainstream formalism for general, categorical notions of predicates/relations. More precisely, a fibration is a suitable functor from a category of (abstract) predicates -the domain of the fibration -to a category of argumentsusually called the base category. In denotational logical relations, predicates usually apply to program denotations rather than on program themselves, with the main consequence that the base category is usually required to be cartesian closed. In this paper, we follow a different path and work with base categories describing the operational (and interactive) behaviour of programs, rather than their denotations. To do so, we introduce the novel notion of an operational structure, the latter being a cartesian category with arrows describing (monadic) evaluation semantics [START_REF] Plotkin | Adequacy for algebraic effects[END_REF][START_REF] Dal Lago | Effectful applicative bisimilarity: Monads, relators, and howe's method[END_REF] and satisfying suitable coherence conditions encoding the base dynamics of program evaluation. This way, we give not only an abstract account to traditional set-based evaluation semantics, but also of evaluation semantics going beyond the category of sets and functions, the prime example being the evaluation semantics of stochastic λ-calculi, which is defined as a stochastic kernel [START_REF] Dal | On bisimilarity in lambda calculi with continuous probabilistic choice[END_REF][START_REF] Wand | Contextual equivalence for a probabilistic language with continuous random variables and recursion[END_REF].

On top of our abstract operational semantics, we give a general notion of an operational logical relation in terms of (logical) fibrations and prove a general result (which we call the fundamental lemma of logical relations, following standard nomenclature of concrete, operational logical relations) stating that programs behave as arrows in the domain of the fibration. Remarkably, our general fundamental lemma subsumes several concrete instances of the fundamental lemma of logical relations appearing in the literature. Additionally, the operational nature of our framework immediately results in a wide applicability of our results, especially if compared with fibrational accounts of denotational logical relations. In particular, since our logical relations builds upon operational structures, they can be instantiated to non-cartesian-closed categories, this way reflecting at a general level the wider applicability of operational techniques with respect to denotational ones. As a prime example of that, we obtain operational logical relations (and their fundamental lemma) for stochastic λ-calculi for free, something that is simply not achievable denotationally, due to the failure of cartesian closedness of the category of measurable spaces.

Fibrational Differential Reasoning. Our second, main contribution is to show that our framework goes beyond traditional relational reasoning, as it gives a novel mathematical account of the recently introduced differential logical relations [START_REF] Dal Lago | Differential logical relations, part I: the simply-typed case[END_REF][START_REF] Dal | Differential logical relations part II: increments and derivatives[END_REF][START_REF] Dal | Differential logical relations, part II increments and derivatives[END_REF][START_REF] Dal | Effectful program distancing[END_REF] (DLRs, for short), both pure and effectful. DLRs are a new form logical relations introduced to define higher-order distances between programs, such distances being abstract notions reflecting the interactive complexity of the programs compared. DLRs have been studied operationally and on specific calculi only, oftentimes introducing new notions -such as the one of a differential extension of a monad [START_REF] Dal | Effectful program distancing[END_REF] -whose mathematical status is still not well understood. The main consequence of that is that a general, structural account of pure and effectful DLRs is still missing. In this paper, we show how DLRs are a specific instance of our abstract operational logical relations and how the fundamental lemma of DLRs is an instance of our general fundamental lemma. We do so by introducing the novel construction of a fibration of differential relations and showing how the latter precisely captures the essence of DLRs, bringing them back to a common framework with traditional logical relations. Additionally, we show how our fibrational account sheds a new light on the mathematical status of effectful DLRs. In particular, we show that differential extensions of monads are precisely liftings of monads to the fibration of differential relations, and that the so-called coupling-based differential extension [START_REF] Dal | Effectful program distancing[END_REF] -whose canonicity has been left as an open problem -is an instance of a general monadic lifting to the fibration of differential relations: remarkably, such a lifting is the extension of the well-known Barr lifting [START_REF] Barr | Relational algebras[END_REF] to a differential setting.

Related Work.

Starting with the seminal work by Hermida [START_REF] Hermida | Fibrations, logical predicates and indeterminates[END_REF], fibrations have been used to give categorical notions of (logical) predicates and relations, and to model denotational logical relations [START_REF] Ghani | Bifibrational functorial semantics of parametric polymorphism[END_REF][START_REF] Sojakova | A general framework for relational parametricity[END_REF][START_REF] Katsumata | Codensity lifting of monads and its dual[END_REF][START_REF] Katsumata | Relating computational effects by ⊤⊤-lifting[END_REF][START_REF] Katsumata | Parametric effect monads and semantics of effect systems[END_REF][START_REF] Katsumata | A semantic formulation of tt-lifting and logical predicates for computational metalanguage[END_REF], as they provide a formal way to relate the denotational semantics of a programming language and a logic for reasoning about it. Other categorical approaches to denotational logical relations have been given in terms of reflexive graphs [START_REF] O'hearn | Parametricity and local variables[END_REF][START_REF] Robinson | Reflexive graphs and parametric polymorphism[END_REF][START_REF] Dunphy | Parametric limits[END_REF][START_REF] Hermida | Logical relations and parametricity -A reynolds programme for category theory and programming languages[END_REF] and factorisation systems [START_REF] Kammar | Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics[END_REF][START_REF] Hughes | Factorization systems and fibrations: Toward a fibred birkhoff variety theorem[END_REF][START_REF] Goubault-Larrecq | Logical relations for monadic types[END_REF].

On the operational side, fibrations have been used to give abstract accounts to induction and coinduction [START_REF] Hermida | Structural induction and coinduction in a fibrational setting[END_REF], both in the setting of initial algebra-final coalgebra semantics [START_REF] Ghani | Indexed induction and coinduction, fibrationally[END_REF][START_REF] Ghani | Generic fibrational induction[END_REF][START_REF] Ghani | Fibrational induction rules for initial algebras[END_REF] and in the setting of up-to techniques [START_REF] Bonchi | Coinduction up-to in a fibrational setting[END_REF][START_REF] Bonchi | Up-to techniques for behavioural metrics via fibrations[END_REF]. To the best of the authors' knowledge, F S C D 2 0 2 2 3:4 A Fibrational Tale of Operational Logical Relations however, none of these approaches has been applied to operational reasoning for higher-order programming languages. Concerning the latter, general operational accounts of logical relations both for effectful [START_REF] Johann | A generic operational metatheory for algebraic effects[END_REF] and combined effectful and coeffectful languages [START_REF] Abel | A unified view of modalities in type systems[END_REF][START_REF] Dal | A relational theory of effects and coeffects[END_REF] have been given in terms of relational reasoning. These approaches, however, are tailored on specific operational semantics and notions of relations, and thus they cannot be considered truly general. Finally, DLRs have been studied mostly operationally [START_REF] Dal Lago | Differential logical relations, part I: the simply-typed case[END_REF][START_REF] Dal | Differential logical relations part II: increments and derivatives[END_REF][START_REF] Dal | Differential logical relations, part II increments and derivatives[END_REF][START_REF] Dal | Effectful program distancing[END_REF], although some general denotational accounts of DLRs have been proposed [START_REF] Dal Lago | Differential logical relations, part I: the simply-typed case[END_REF][START_REF] Pistone | On generalized metric spaces for the simply typed lambda-calculus[END_REF]. Even if not dealing with operational aspects of DLRs, the latter proposals can cope with pure DLRs only, and are too restrictive to incorporate computational effects.

The Anatomy of an Operational Semantics

To define a general notion of an operational logical relation, we first need to define a general notion of an operational semantics. This is precisely the purpose of this section. In particular, we introduce the notion of an operational structure on a category with finite products endowed with a strong monad as an axiomatisation of a general evaluation semantics. Operational structures prescribe the existence of basic interaction arrows (the latter describing basic program interactions as given by the usual reduction rules) and define program execution as a Kleisli arrow (this way giving monadic evaluation) satisfying suitable coherence laws reflecting evaluation dynamics. Remarkably, operational structures turn out to be more liberal -hence widely applicable -than categories used in denotational semantics (the latter being required to be cartesian closed).

A Calculus with Generic Effects

Our target calculus is a simply-typed fine grain call-by-value [START_REF] Levy | Modelling environments in call-by-value programming languages[END_REF] Λ enriched with generic effects [START_REF] Gordon | A tutorial on co-induction and functional programming[END_REF][START_REF] Plotkin | Algebraic operations and generic effects[END_REF]. Recall that for a strong monad2 T = (T, η, >>=) on a cartesian category C , a generic effect [START_REF] Plotkin | Algebraic operations and generic effects[END_REF][START_REF] Plotkin | Adequacy for algebraic effects[END_REF] Other examples of generic effects include primitives for input-output, memory updates, exceptions, etc. Here, we assume to have a collection of generic effect symbols γ with an associated type σ γ , leaving the interpretation of γ as an actual generic effect γ to the operational semantics. The syntax and static semantics of Λ are given in Figure 1, where ζ ranges over base types and c over constants of type ζ (for ease of exposition, we do include operations on base types, although those can be easily added).

Notice that Λ's expressions are divided into two (disjoint) classes: values (notation v, w, . . .) and computations (notation t, s, . . .), the former being the result of a computation, and the latter being an expression that once evaluated may produce a value (the evaluation process might not terminate) as well as side effects. When the distinction between values and computations is not relevant, we generically refer to terms (and still denote them as t, s, . . .). We adopt standard syntactic conventions [START_REF] Barendregt | The lambda calculus: its syntax and semantics[END_REF] and identify terms up to renaming of bound variables: we say that a term is closed if it has no free variables and write V σ , Λ σ for the sets of closed values and computations of type σ, respectively. We write t (and similarly for values) for the capture-avoiding (simultaneous) substitution of the values v 1 , . . . , v n for all free occurrences of x 1 , . . . , x n in t. Oftentimes, we will use the notation -→ ϕ for a sequence ϕ 1 , . . . , ϕ n of symbols ϕ i .

[v 1 , . . . , v n /x 1 , . . . , x n ] Γ ⊢ v : σ × τ Γ ⊢ v.2 : τ Γ ⊢ v : σ Γ ⊢ w : τ Γ ⊢ ⟨v, w⟩ : σ × τ Γ ⊢ ⟨⟩ : 1
When dealing with denotational logical relations, one often organises Λ as a syntactic category having types as objects and (open) terms modulo the usual βη-equations as arrows. Operationally, however, terms are purely syntactic objects and cannot be taken modulo βη-equality. For that reason, we consider a syntactic graph rather than a syntactic category. The definition of Syn reflects the call-by-value nature of Λ: to each type σ we associate two objects, representing the type σ on values and on computations. Moreover, there is no arrow having environments as codomains nor having objects σ as domain: this reflects that in call-by-value calculi variables are placeholders for values, not for computations.

Operational Semantics: The Theoretical Minimum

Having defined the syntax of Λ, we move to its operational semantics. Among the many style of operational semantics (small-step, big-step, etc), evaluation semantics turns out to be a convenient choice for our goals. Evaluation semantics are usually defined as monadic functions e : Λ σ → T (V σ ), with T a monad encoding the possible effects produced during program evaluation (e.g. divergence or nondeterminism) [START_REF] Dal Lago | Effectful applicative bisimilarity: Monads, relators, and howe's method[END_REF][START_REF] Plotkin | Adequacy for algebraic effects[END_REF][START_REF] Johann | A generic operational metatheory for algebraic effects[END_REF]. To clarify the concept, let us consider an example [START_REF] Dal Lago | Effectful applicative bisimilarity: Monads, relators, and howe's method[END_REF].

▶ Example 2.2.
Let T be a monad on Set with a generic effects γ ∈ T (V σγ ) for effect symbols γ in Λ. The (monadic) evaluation (family of) map(s) -: Λ σ → T (V σ ) is defined as follows (notice that Λ being simply-typed, -is well-defined 4 ).

val v = η(v) (λx.t)v = t[v/x] t to x.s = s[•/x] † t ⟨v 1 , v 2 ⟩.i = η(v i ) γ = γ
3 Recall that a graph is defined by removing from the definition of a category the axioms prescribing the existence of identity and composition. A diagram is a map from graphs to graphs ( a diagram being defined by removing from the definition of a functor the clauses on identity and composition). Since any category is a graph, we use the word diagram also to denote maps from graphs to categories. 4 It is worth remarking that termination is not an issue for our general notion of an evaluation semantics (Definition 2.3 below). In fact, the results presented in this paper simply require to have an evaluation Example 2.2 defines evaluation semantics as an arrow in the category Set of sets and functions relying on two main ingredients: the monad T and its algebraic operations; and primitive functions implementing the basic mechanism of β-reductions, viz. application/substitution and projections. The very same recipe has been used to define specific evaluation semantics beyond Set , prime example being kernel-like evaluation semantics for stochastic λ-calculi [START_REF] Dal | On bisimilarity in lambda calculi with continuous probabilistic choice[END_REF][START_REF] Wand | Contextual equivalence for a probabilistic language with continuous random variables and recursion[END_REF][START_REF] Vákár | A domain theory for statistical probabilistic programming[END_REF][START_REF] Ehrhard | Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming[END_REF], where evaluation semantics are defined as Kleisli arrows on suitable categories of measurable spaces (see Example 2.5 below for details). Here, we propose a general notion of an operational semantics for Λ in an arbitrary cartesian category B and with respect to a monad T. We call the resulting notion a (Syn -)operational structure.

SΓ × Sσ St / / S(λx.t)×id Sσ Sτ S(σ → τ ) × Sσ β 8 8 SΓ S⟨v1,v2⟩ Svi / / Sσ i S(σ 1 × σ 2 ) i 8 8 SΓ S⟨⟩ / / ! S1 1 ι : : SΓ Sc / / ! Sζ 1 c : : SΓ S(val v) / / S(v) Sσ e Sσ η / / T (Sσ) SΓ ! S(γ) / / S(σ) e 1 γ / / T (Sσ) SΓ S(vw) / / ⟨S(v),S(w)⟩ Sτ e S(σ → τ ) × Sσ β / / Sτ e / / T (Sτ ) SΓ S(t to x.s) / / ⟨id,S(t)⟩ Sτ e SΓ × Sσ id×e / / SΓ × T (Sσ) >>=(e•S(s)) / / T (Sτ ) SΓ S(v.i) / / S(v i ) Sσi e S(σ1 × σ2) i / / Sσi η / / T (Sσi)
▶ Definition 2.3. Given a category B with finite products and a strong monad T on it, a (Syn -)operational structure consists of a diagram S : Syn → B satisfying S( --→ x : σ) = -→ Sσ, together with the following (interaction) arrows (notice that γ is a generic effect) and satisfying the coherence laws in Figure 2.

e : Sσ → T (Sσ) ι : 1 → S1 β : S(σ → τ ) × Sσ → Sτ c : 1 → Sζ p 1 : S(σ × τ ) → Sσ p 2 : S(σ × τ ) → Sτ γ : 1 → T (Sσ γ )
Notice how the first four coherence laws in Figure 2 ensure the intended behaviour of the arrows β, ι, p i , c, whereas the remaining laws abstractly describe the main dynamics of program execution. Notice also that Definition 2.3 prescribes the existence of an evaluation arrow e: it would be interesting to find conditions on B (probably a domain-like enrichment [START_REF] Kelly | Basic concepts of enriched category theory[END_REF] or partial additivity [START_REF] Manes | Algebraic Approaches to Program Ssemantics[END_REF]) ensuring the existence of e. We can now instantiate Definition 2.3 to recover standard Set -based evaluation semantics as well as operational semantics on richer categories. In particular, since B need not be closed, we can give Λ an operational semantics in the category Meas of measurable spaces and measurable functions. map satisfying suitable coherence conditions. Consequently, we could rephrase this example ignoring termination by requiring the monad to be enriched in an ω-complete partial order [START_REF] Abramsky | Domain theory[END_REF] and defining evaluation semantics as a least fixed point of a suitable map, as it is customary in monadic evaluation semantics [START_REF] Dal Lago | Effectful applicative bisimilarity: Monads, relators, and howe's method[END_REF].

▶ Example 2.4. Let B = Set and define S : Syn → Set thus:

Sσ = V σ Sσ = Λ σ S( --→ x : σ) = -→ Sσ S(Γ ⊢ t : σ)( - → v ) = t[ - → v / - → x ]
We obtain an operational structure by defining the maps β, p 1 , p 2 , and ι in the obvious way (e.g.

β(λx.t, v) = t[v/x] and p i ⟨v 1 , v 2 ⟩ = v i ).
Finally, given a monad T with generic effects γ ∈ T V σγ for each effect symbol γ, we define e as the evaluation map of Example 2.2.

▶ Example 2.5 (Stochastic λ-calculus). Let us consider the instance of Λ with a base type R for real numbers, constants c r for each real number r, and the generic effect symbol U standing for the uniform distribution over the unit interval. Recall that Meas has countable products and coproducts (but not exponentials [START_REF] Aumann | Borel structures for function spaces[END_REF]). To define the diagram S : Syn → Meas,

we rely on the well-known fact [START_REF] Ehrhard | Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming[END_REF][START_REF] Staton | Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints[END_REF][START_REF] Borgström | A lambdacalculus foundation for universal probabilistic programming[END_REF]] that both V σ and Λ σ can be endowed with a σ-algebra making them measurable (actually Polish) spaces in such a way that V R ∼ = R and that the substitution map is measurable. We write Σ σ and Σ σ for the σ-algebras associated to V σ and Λ σ , respectively. We thus define S : Syn → Meas as follows:

Sσ = (V σ , Σ σ ) Sσ = (Λ σ , Σ σ ) S( --→ x : σ) = -→ Sσ S(Γ ⊢ t : σ)( - → v ) = t[ - → v / - → x ]
We obtain an operational structure by observing that the maps β, p 1 , p 2 , and ι of previous example extend to Meas, in the sense that they are all measurable functions. Next, we consider the Giry monad [START_REF] Giry | A categorical approach to probability theory[END_REF] G : Meas → Meas which associates to each measurable space the space of probability measures on it. By Fubini-Tonelli theorem, G is strong. Let U be the Lebesgue measure on [0, 1], which we regard as an arrow U : 1 → G(SV Real ), and thus as a generic effect in Meas. We then define [START_REF] Dal | On bisimilarity in lambda calculi with continuous probabilistic choice[END_REF] e : Λ σ → G(V σ ) as in Example 2.2.

Operational Logical Relations, Fibrationally

Having defined what an operational semantics for Λ is, we now focus on operational reasoning.

In this section, we propose a general notion of an operational logical relation in terms of fibrations over (the underlying category of) an operational structure and prove that a general version of the fundamental lemma of logical relations holds for our operational logical relations. But before that, let us recall some preliminary notions on (bi)fibrations (we refer to [START_REF] Hermida | Fibrations, logical predicates and indeterminates[END_REF][START_REF] Bart | Categorical Logic and Type Theory, volume 141 of Studies in logic and the foundations of mathematics[END_REF][START_REF] Streicher | Fibered categories a la jean benabou[END_REF] for more details).

Preliminaries on Fibrations

Let p : E → B be a functor and f :

X → Y an arrow in E with p(f ) = u. We say that f is cartesian over u if, for every arrow h : Z → Y in E such that p(h) = u • v, there is a unique arrow g : Z → X such that p(g) = v and h = f • g. Dually, f is cocartesian over u if, for every arrow h : X → Z in E such that p(h) = v • u, there is a unique arrow g : Y → Z such that p(g) = v and h = g • f . We say that f is vertical if u is an identity.
A fibration is a functor p : E → B such that, for every object X in E and every arrow u : I → p(X) in B, the exists a cartesian arrow over u with codomain X. Dually, an opfibration is a functor p : E → B such that for every object X in E and every arrow f : p(X) → I in B, the exists a cocartesian arrow over u with domain X. A bifibration is a functor which is both a fibration and an opfibration. We refer to E and B as the domain and the base of the (bi/op)fibration. A (op)fibration is cloven if it comes together with a choice of (co)cartesian liftings: for an object X in E, we denote by u X : u * X → X the

α : A → X in C . An arrow f : (X, [α]) → (Y, [β]) is an arrow f : X → Y in C such that f • α = β • g for some arrow g in C . Composition and identities in ws(C ) are those of C . The functor Ψ C maps (X, R)
to X and is the identity on arrows. It is easy to check that, for every arrow

f : X → Y in C and every object (X, [α]), the image along f is f ! (X, [α]) = (Y, [f • α]); and for every object (Y, [β]), the reindexing along f is f * (Y, [β]) = (X, [β ′ ]), where f • β ′ = β • f ′ is a weak pullback square. Therefore, Ψ C is a bifibration.
Note that, given objects (X, [α]) and (X, [β]) in ws(C ), there is at most one vertial arrow between them (the identity on X), hence we will write [α] ≤ X [β] when such arrow exists. Moreover, we have that

[α] ≤ X [β] and [β] ≤ X [α] implies [α] = [β]
, by definition of poset reflection, hence the only vertical isomorphisms are identities. Finally, observe that the bifibrations Ψ Set and Sub Set are equivalent in the sense that there is a functor U : Sub Set → ws(Set ) which is an equivalence satisfying Ψ Set • U = Sub Set and preserving (co)cocartesian arrows. The functor U maps (X, A) to (X, [ι A ]) where ι A : A → X is the inclusion function.

Fibrations nicely carry a logical content: logical operations, in fact, can be described as categorical structures on the fibration. We now define the logical structure underlying logical relations, namely conjunctions, implications, and universal quantifiers. Recall that a fibration p : E → B has finite products if E and B have finite products and p strictly preserves them. We denote by × and 1 finite products in E and recall [START_REF] Bart | Categorical Logic and Type Theory, volume 141 of Studies in logic and the foundations of mathematics[END_REF] that in a fibration with finite products every fibre has finite products ∧ and ⊤ preserved by reindexing functors; additionally, we have the isomorphisms [START_REF] Bart | Categorical Logic and Type Theory, volume 141 of Studies in logic and the foundations of mathematics[END_REF].

A ×B ≃ π * 1 A ∧ π * 2 B
Note that in a fibration with universal quantifiers, we have right adjoints along any tuple of distinct projections ⟨π i1 , . . . , π i k ⟩ : I 1 × . . . × I n → I i1 × . . . × I i k , where i 1 , . . . , i k ∈ {1, . . . , n} are all distinct. We denote such a right adjoint by A ⟨πi 1 ,...,πi k ⟩ . The following proposition shows under which condition the fibration of weak subobjects is a logical fibration.

▶ Proposition 3.4 ([55, 69]). Let C be a category with finite products and weak pullbacks. and Sub Set are logical fibrations. Also Rel Set is a logical fibration, as it can be obtained from Sub Set by pulling back along the product-preserving Set -functor X 2 = X × X.

A 2-category of (bi)fibrations. Fibrations can be organised in a 2-category. This is important because many standard categorical concepts can be internalised in any 2-category, hence we will be able to define them also for fibrations. In particular, we will be interested in (strong) monads on a fibration, as they will allow us to define effectful logical relations. We consider the 2-category Fib of fibrations defined as follows. Objects are fibrations

p : E → B. A 1-arrow (F, G) : p → q between fibrations p : E → Band q : D → C is a pair of functors F : B → C and G : E → D such that F • p = q • G. 5 A 2-arrow (ϕ, ψ) : (F, G) ⇒ (H, K) between 1-arrows (F, G), (H, K) : p → q is a pair of natural transformations ϕ : F . → H and ψ : G . → K such that ϕp = qψ.
. Compositions and identities are defined componentwise. The 2-category biFib of bifibrations is defined in the same way. We can define [START_REF] Street | The formal theory of monads[END_REF] strong monads on fibrations as strong monads in the 2-category Fib. That is, a monad T on a fibration p : E → B consists of the following data: a 1-arrow (T, S) : p → p and two 2-arrows (µ T , µ S ) : (T 2 , S 2 ) ⇒ (T, S), (η T , η S ) : (Id E , Id B ) ⇒ (T, S), and (st T , st S ) : (-× T -, -×S-) ⇒ (T (-× -), S(-×-)) such that (T, µ T , η T , st T ) is a strong monad on B and (S, µ S , η S , st S ) is a strong monad on E. In particular, given a strong monad T = (T, µ, η, st) on B, a lifting of T to p : E → B is a tuple Ṫ = ( Ṫ , μ, η, ṡt) such that (T, Ṫ , µ, μ, η, η, st, ṡt) is a strong monad on p : E → B. We write > >= for the lifting of >>=.

Operational Logical Relations and Their Fundamental Lemma

We are now ready to define a general notion of an operational logical relation. Let us consider an operational structure over a cartesian category B with a strong monad T on B, as in Definition 2.3. Let p : E → B be a logical fibration and Ṫ be a lifting of T to p. ▶ Definition 3.6. A logical relation is a mapping R from objects of Syn to objects of E such that p(Rx) = Sx, for any object x of Syn, 6 and the following hold.

R1 = ⊤ S1 R(σ × τ ) = p * 1 (Rσ) ∧ p * 2 (Rτ ) Rσ = e * ( Ṫ (Rσ)) R( --→ x : σ) = ˙ -→ Rσ R(σ → τ ) = A π1 π * 2 (Rσ) ⇒ β * (Rτ )
Notice that giving a logical relation essentially amounts to specify the action of R on basic types, since the action of R on complex types is given by Definition 3.6. The defining clauses of a logical relation exploit both the logic of a (logical) fibration and the operational semantics of Λ. The reader should have recognised in Definition 3.6 the usual definition of a logical relation, properly generalised to rely on the logic of a fibration only. For instance, Rσ intuitively relates computations whose evaluations are related by the lifting of the monad. Notice also that the clause of arrow types has a higher logical complexity than other clauses, as it involves two logical connectives, viz. implication and universal quantification.

Operational logical relations come with their so-called fundamental lemma, which states that (open) terms maps (via substitution) related values to related terms. In our abstract framework that to any term t we can associate a suitable arrow Rt in E lying above St.

To prove our general version of the fundamental theorem, we have to assume it for the parameters of our calculus (constants of basic types and generic effects). Accordingly, we say that a logical relation R is (Λ-)stable if: (i) for every constant c of a base type ζ, we have an arrow ċ : 1 → Rζ above c; (ii) we have an arrow γ : 1 → Ṫ (Rσ) above γ.

▶ Theorem 3.7 (Fundamental Lemma). Let R be a stable logical relation. The map R extends to a diagram R : Syn → E such that p • R = S. In particular, for any term Γ ⊢ t : σ, there is an arrow Rt : RΓ → Rσ in E above St (similarly, for values).

Proof sketch. Given Γ ⊢ t : σ, we construct the desired arrow Rt by induction on t. The case for values lifts commutative triangles in Figure 2 using the universal property of cartesian liftings of interaction arrows and then constructs the desired arrow using the logical structure of p and Rσ. The case of terms, just lifts the commutative diagrams in Figure 2

RΓ >>=(ē•Rs)•⟨id RΓ ,ē•Rt⟩ # # ∃!h Rτ ē / / Ṫ (Rτ )
We choose h as R(t to x.s). ◀

We can now instantiate Theorem 3.7 with the operational structures and fibrations seen so far to recover traditional logical relations (and their fundamental lemmas). For instance, the operational structure of Example 2.5 and the fibraration obtained by pulling back Rel Set along the forgetful from Meas to Set (together with a lifting of the Giry monad [START_REF] Katsumata | Codensity lifting of monads and its dual[END_REF][START_REF] Katsumata | Relating computational effects by ⊤⊤-lifting[END_REF]) give operational logical relations for stochastic λ-calculi. Theorem 3.7 then gives compositionality (i.e. congruence and substitutivity) of the logical relation. But that is not the end of the story. In fact, our general results go beyond the realm of traditional logical relations.

The fibration of differential relations

In this section, we describe the construction of the fibration of differential relations, which can serve as a fibrational foundation of differential logical relations [START_REF] Dal Lago | Differential logical relations, part I: the simply-typed case[END_REF][START_REF] Dal | Differential logical relations part II: increments and derivatives[END_REF][START_REF] Dal | Differential logical relations, part II increments and derivatives[END_REF][START_REF] Dal | Effectful program distancing[END_REF] (DLRs), a recently introduced form of logical relations defining higher-order distances between programs. DLRs are ternary relations relating pairs of terms with elements representing distances between them: such distances, however, need not be numbers. More precisely, with each type σ one associates a set σ of (higher-order) distances between terms of type σ, and then defines DLRs as relating terms of type σ with distances in σ between them. Elements of σ reflect the interactive complexity of programs, the latter being given by the type σ. Semantically, DLRs give rise to generalised distance spaces and differential extensions of monads, the former being relational structures (X, X , δ X ) with δ X ⊆ X × X × X acting as the semantic counterpart of a DLR, and the latter being reminiscent7 of extensions of monads to the category of generalised distance spaces. Here, we show how our general notion of an operational logical relation subsumes the one of a DLR (and, consequently, that the fundamental lemma of DLRs is an instance of Theorem 3.7). Additionally, we show how differential extensions are precisely liftings of monads to the fibration of differential relations and how the so-called coupling-based differential extension [START_REF] Dal | Effectful program distancing[END_REF] is an instance of a general monadic lifting to such a fibration, viz. the well-known Barr lifting properly fitted to a differential setting.

Going Differential, Fibrationally

Let p : E → B be a fibration with finite products. 8 We define the category dr(p) of differential relations in p as follows:

Objects are triples X = (|X|, X , δ X ), where |X| and X are objects in B and δ X is an object in the fibre E |X|× X ×|X| .

Arrows f : X → Y are triples f = (|f |, df, φ f ), where |f | : |X| → |Y| and df : |X| × X → Y are arrows in B, and φ f : δ X → δ Y is an arrow in E over ⟨|f |π 1 , df ⟨π 1 , π 2 ⟩, |f |π 3 ⟩.
Composition of arrows f : X → Y and g : Y → Z is defined thus:

|g • f | = |g| • |f | d(g • f ) = dg • ⟨|f |π 1 , df ⟩ φ g•f = φ g • φ f .
Identity on X is given by id X = (id |X| , π 2 , id δ X ).

▶ Proposition 4.1. dr(p) is a category with finite products.

▶ Remark 4.2. Note that an arrow f : X → Y in dr(p) can be equivalently described as a triple

(|f |, Df, φ f ) where |f | is as before, Df : |X| × X → |Y| × Y is such that |f | • π 1 = π 1 • Df and φ f : δ X → δ Y is above Df × |f | : |X| × X × |X| → |Y| × Y × |Y|.
This presentation is perhaps more in the spirit of fibrations, but we opted for the other one, which follows the original presentation of generalised distance spaces [START_REF] Dal | Effectful program distancing[END_REF].

In the following, we denote by ∇X the object |X| × X × |X| of B and by ∇f the arrow ⟨|f |π 1 , df ⟨π 1 , π 2 ⟩, |f |π 3 ⟩. These data define a functor ∇ : dr(p) → B.

▶ Example 4.3. For the fibration Sub Set : s(Set ) → Set of Example 3.1, the category dr(Sub Set ) is the category of generalised distance spaces [START_REF] Dal | Effectful program distancing[END_REF]. An object in dr(Sub Set ) is essentially a triple (X, V, R) consisting of a set X of points, a set V of distance values, and a ternary relation R ⊆ X × V × X specifying at which distance two elements of X are related: that is, (x, v, y) ∈ R means that x and y are related at distance v. For instance, a metric d : X × X → [0, ∞] on X can be seen as a ternary relation to I × X × I and (u, f ) to ⟨uπ 1 , f ⟨π 1 , π 2 ⟩, uπ 3 ⟩. Therefore, we have p ′ (X) = (|X|, X ) and p ′ (f ) = (|f |, df ). This is somewhat similar to the simple coproduct completion of a fibration [START_REF] Hofstra | The dialectica monad and its cousins. In Models, Logics, and Higher-dimensional Categories: A Tribute to the Work of Mihaly Makkai[END_REF]. We leave a precise comparison between these constructions for future work.

R d ⊆ X × [0, ∞] × X defined by (x, v, y) ∈ R d iff d(x, y) ≤ v. An arrow from (X, V, R) to (Y, U, S) in dr(Sub Set ) consists of a function |f | : X → Y transforming points together with a function df : X × V → U transforming distance values such that, for all x, y ∈ X and v ∈ V , (x, v, y) ∈ R implies (|f |(x), df (x, v), |f |(y)) ∈ S.
We now show under which conditions the fibration DRel p is a logical fibration.

▶ Proposition 4.6. If p : E → B is a logical fibration and B is cartesian closed, then DRel p is a logical fibration.

We report the definition of the logical structure on DRel p : let X, Y, Z objects in dr(p) with |X| = |Y| = I and |Z| = I × J.

⊤ I = (I, 1, ⊤ I×1×I ) X ∧ I Y = (I, X × Y , ⟨π 1 , π 2 , π 4 ⟩ * δ X ∧ ⟨π 1 , π 3 , π 4 ⟩ * δ Y ) X ⇒ I Y = (I, [ X , Y ], A ⟨π1,π2,π4⟩ (⟨π 1 , π 3 , π 4 ⟩ * δ X ⇒ ⟨π 1 , ev X Y ⟨π 2 , π 3 ⟩, π 4 ⟩ * δ Y )) A I J Z = (I, [J, Z ], A ⟨π1,π3,π5⟩ (⟨π 1 , π 2 , ev J Z ⟨π 3 , π 2 ⟩, π 4 , π 5 ⟩ * δ Z ))
▶ Example 4.7. Let us consider the fibration DRel Sub Set : dr(Sub Set ) → Set and instantiate the above constructions to it. We have ⊤ X = (X, 1, X × 1 × X), that is, in ⊤ X there is just one distance value and all elements of X are related. Consider now objects X = (X, V, R) and Y = (X, U, S) in dr(Sub Set ). Then, we have X ∧Y = (X, V × U, R ⊓ S) and X ⇒Y = (X, [V, U ], R → S), where (x, (v, u), y) ∈ R ⊓ S iff (x, v, y) ∈ R and (x, u, y) ∈ S, (x, f, y) ∈ R → S iff, for all v ∈ V , (x, v, y) ∈ R implies (x, f (v), y) ∈ S. That is, two elements x and y are related in R ⊓ S at a distance (v, u) such that x and y are at distance v in R and u in S. Instead, x and y are related in R → S at a distance f transforming distances in V into distances in U , respecting R and S. Finally, if Z = (X × Y, V, R) is an object in dr(Sub C Set ]), then we have

A X Y Z = (X, [Y, V ], Y → R), where (x, f, x ′ ) ∈ Y → R,
iff for all y, y ′ ∈ Y , ((x, y), f (y), (x ′ , y ′ )) ∈ R. That is, elements x and x ′ are related by Y → R at a distance f returning for each y ∈ Y a distance in V such that R relates (x, y) and (x ′ , y ′ ) at distance f (y), for each y, y ′ ∈ Y .

We now extend this construction to 1-and 2-arrows. To do so, we work with bifibrations whose bases have finite products. Let p and q be such bifibrations and (F, G) : p → q be a 1-arrow in biFib. We define a functor G : dr(p) → dr(q) thus: for X an object in dr(p), we set

| GX| = F |X| GX = F (|X| × X ) δ GX = pr F X ! Gδ X ,
where pr

F X = ⟨F π 1 , F ⟨π 1 , π 2 ⟩, F π 3 ⟩ : F (|X| × X × |X|) → F |X| × F (|X| × X ) × F |X| is an arrow in B.
For every arrow f : X → Y in dr(p), we set

| Gf | = F |f | d( Gf ) = (F ⟨|f |π 1 , df ⟩)π 2 φ Gf = υ(Gφ f ),
where υ(Gφ f ) is the unique arrow over F |f | × F ⟨|f |π 1 , df ⟩ × F |f | making the diagram on the left commute, which exists as the diagram on the right commutes and pr F X Gδ X is cocartesian.

Gδ X Gφ f pr F X Gδ X / / δ GX υ(Gφ f ) Gδ Y pr F Y Gδ Y / / δ GY F (∇X) F (∇f ) pr F X / / F |X| × F (|X| × X ) × F |X| F |f |×F ⟨|f |π1,df ⟩×F |f | F (∇Y) pr F Y / / F |Y| × F (|Y| × Y ) × F |Y|
Notice that cocartesian liftings are essential to appropriately define G on the relational part of X and f , as we do not assume any compatibility with products for F . ▶ Proposition 4.8. (F, G) : DRel p → DRel q is a 1-arrow in Fib.

Similarly, given a 2-arrow (ϕ, ψ) : (F, G) ⇒ (H, K) in biFib between 1-arrows (F, G) : p → q and (H, K) : p → q, we define a natural transformation ψ : G . → K as follows: for every object X in DRel p , we set:

| ψ X | = ϕ |X| d( ψ X ) = ϕ |X|× X π 2 φ ψ X = υ(ψ δ X ),
where υ(ψ δ X ) is the unique arrow over ϕ |X| × ϕ |X|× X × ϕ |X| making the diagram on the left commute, which exists as the diagram on the right commutes and pr F X Gδ X is cocartesian. We are getting closer to the definition of a 2-functor DR from (certain) bifibrations to fibrations given by the following assignments:

Gδ X ψ δ X pr F X Gδ X / / δ GX υ(ψ δ X ) Kδ X pr H X Kδ X / / δ KX F (∇X) ϕ ∇X pr F X / / F |X| × F (|X| × X ) × F |X| ϕ |X| ×ϕ |X|× X ×ϕ |X| H(∇X)
DR(p) = DRel p DR(F, G) = (F, G) DR(ϕ, ψ) = (ψ, ψ).
However, this is not the case as DR does not preserve identity 1-arrows. Indeed, given the identity (Id B , Id E ) on a bifibration p : E → B, we have that for every object X in dr(p),

Id E (X) = (|X|, |X| × X , pr Id B
X ! δ X ), which is not isomorphic to X, in general. We can recover a form of functoriality by restricting to a 2-subcategory of biFib, notably, considering only 1-arrows which are cocartesian. We say that a 1-arrow (F, G) : p → q in biFib is cocartesian if the functor G preserves cocartesian arrows. This implies that G commutes with cocartesian liftings up to isomorphism. Denote by biFib c the 2-subcategory of biFib where objects have finite products and 1-arrows are cocartesian.

▶ Theorem 4.10. DR : biFib c → Fib is a lax functor.

Note that we just have a lax functor, as identities and composition of 1-arrows are preserved only up to a family of a mediating 2-arrow. Nonetheless, this is enough to get important properties of the construction.

Lifting monads: the differential extension

An important problem when dealing with effectful languages is the lifting of monads from the category where the semantics of the language is expressed to the category used to reason about programs, e.g., the domain of a fibration or a category of relations. The most famous one is perhaps the so-called Barr extension [START_REF] Barr | Relational algebras[END_REF] of a Set -monad to the category of (endo)relations, which is fibred over Set (other notions of lifting include ⊤⊤-and codensity lifting [START_REF] Katsumata | Codensity lifting of monads and its dual[END_REF][START_REF] Katsumata | Relating computational effects by ⊤⊤-lifting[END_REF]). In the differential setting, the notion of a differential extension has been recently proposed [START_REF] Dal | Effectful program distancing[END_REF] as a way to lift monads to generalised distance spaces. To what extent such a construction is canonical and whether it defines an actual monadic lifting, however, have been left as open questions. Here, we answer both questions in the affirmative.

▶ Definition 4.11. Let p : E → B be a fibration with finite products and T = (T, µ, η, st) be a strong monad on B. A differential extension of T along p is a lifting Ṫ = ( Ṫ , μ, η, ṡt) of T along the fibration DRel p : dr(p) → B.

A differential extension of T along the fibration p is thus a monad on the category of differential relations in p which is above T with respect to the fibration DRel p . We describe two techniques to build differential extensions of monads. The first one is an immediate consequence of Theorem 4.10. Indeed, DR : biFib c → Fib being a lax functor, every cocartesian monad on a bifibration p induces a monad on the fibration DRel p , hence a differential extension. This follows from general properties of lax functors [9,[START_REF] Street | Two constructions on lax functors[END_REF].

▶ Corollary 4.12. Let T = (T, S, η T , η S , µ T , µ S ) be a monad on p in biFib c . Then, T = (T, S, η T , η S , µ T , µ S ) is a monad on DRel p in Fib.

To get a lifting of strong monads, we need an additional hypothesis: we have to require that the product functor × on the total category E preserves cocartesian arrows, as often happens when dealing with monoidal bifibrations [START_REF] Michael | Framed bicategories and monoidal fibrations[END_REF][START_REF] Melliès | A bifibrational reconstruction of lawvere's presheaf hyperdoctrine[END_REF].9 This is sensible as the action of DR on 1-arrows is defined using cocartesian liftings.

▶ Theorem 4.13. Let p : E → B be a bifibration with finite products where × preserves cocartesian arrows and T = (T, S, µ T , µ S , η T , η S , st T , st S ) be a strong monad on p. Then, ( S, µ S , η S , st S ) is a differential extension of (T, µ T , η T , st T ).

In other words, this result provides us with a differential extension of a monad (T, µ T , η T ) starting from a usual extension (S, µ S , η S ) along the fibrations p. Therefore, to build a differential extension of (T, µ T , η T ) we can use existing techniques to lift it, obtaining a monad on the fibration p and then apply our construction.

We conclude this section by instantiating this technique to a special class of bifibrations, notably, bifibrations of weak subobjects as defined in Example 3.2. The resulting construction applies to (strong) monads on categories with weak pullbacks and finite products, and provides a differential version of the Barr extension, which we dub a differential Barr extension.

First of all, we show that the construction of the bifibration of weak subobjects extends to a 2-functor. Let us denote by Cat cwp the 2-category of categories with weak pullbacks and finite products, functors, and natural transformations. Given a functor [START_REF] Dal | Effectful program distancing[END_REF] maps an object (X, V, R) to (T X, T (X × V ), τ (R)) where (x, v, y) ∈ τ (R) iff there exists φ ∈ T R such that T π 1 (T ι R (φ)) = x, T ⟨π 1 , π 2 ⟩(T ι R (φ)) = v, and T π 3 (T ι R (φ)) = y. Here, ι R : R → X × V × X denotes the inclusion function and the element φ is called a (ternary) coupling, borrowing the terminology from optimal transport [START_REF] Villani | Optimal Transport: Old and New[END_REF]. Basically, this lifting states that monadic elements x and y are related with monadic distance v iff we can find a coupling φ that projected along the first and third component gives x and y, respectively, and projected along the first two components gives the monadic distance v. Relying on the equivalence between Sub Set and Ψ Set , we get that the above lifting of (T, µ, η) is an instance of the differential Barr extension T : dr(ws(Set )) → dr(ws(Set )). Indeed, for an object (X, V, [α]) in dr(Ψ Set ) we can choose a canonical representative ι R : R → X × V × X such that [α] = [ι R ], where R is the image of α and ι R is the inclusion function.

F : C → D in Cat cwp , define F : ws(C ) → ws(D) as F (X, [α]) = (F X, [F α]) and F f = F f . It is easy to check that this is indeed a functor. Moreover, note that if f : (X, [α]) → (Y, [β]) is cocartesian in Ψ C , that is, [β] = [f α], then F f : (F X, [F α]) → (F Y, [F β]) is cocartesian in Ψ D , as [F β] = [F f • F α]. Consider now a natural transformation ϕ : F . → G in Cat cwp and define ϕ (X,[α]) : F . → G as ϕ (X,[α]) = ϕ X . This is well-defined because, if α : A → X, then we have ϕ X • F α = Gα • ϕ A ,

Conclusion and Future Work

We have shown how fibrations can be used to give a uniform account to operational logical relations for higher-order languages with generic effects and a rather liberal operational semantics. Our framework encompasses both traditional, set-based logical relations and logical relations on non-cartesian-closed categories -such as the one of measurable spaces -as well as the recently introduced differential logical relations. In particular, our analysis sheds Further examples of logical relations that can be described in our framework include classic Kripke logical relations [START_REF] Mitchell | Foundations for programming languages[END_REF] (take fibrations of poset-indexed relations) as well as logical relations for information flow (the latter could be approached both as suitable Kripke logical relations or by considering a shallow semantics on the category of classified sets [START_REF] Kavvos | Modalities, cohesion, and information flow[END_REF]). Additionally, since differential logical relations can be used to reason about nontrivial notions such as program sensitivity and cost analysis [START_REF] Dal | Effectful program distancing[END_REF], our framework can be used for reasoning about the same notions too. Even if general, the vehicle calculus of this work lacks some important programming language features, such as recursive types and polymorphism. Our framework being operational, the authors suspect that the addition of polymorphism should not be problematic, whereas the addition of full recursion may require to come up with abstract notions of step-indexed logical relations [START_REF] Appel | An indexed model of recursive types for foundational proof-carrying code[END_REF][START_REF] Dreyer | Logical step-indexed logical relations[END_REF]. In general, the proposed framework looks easily extensible and adaptable. To reason about a given calculus, one should pick a fibration with a logical structure supporting the kind of analysis one is interested in and whose base category has enough structure to model its interactive behaviour. For instance, in this work we just need products and a monad on the base category but, e.g., to model sum types, we would need also coproducts to describe case analysis. On the logical side, we have just considered standard intuitionistic connectives but, e.g., to support more quantitative analysis, one may need to use fibrations supporting linear connectives and modalities [START_REF] Michael | Framed bicategories and monoidal fibrations[END_REF][START_REF] Melliès | Functors are type refinement systems[END_REF][START_REF] Daniel | A fibrational framework for substructural and modal logics[END_REF][START_REF] Dagnino | Doctrines, modalities and comonads[END_REF][START_REF] Dagnino | Logical foundations of quantitative equality[END_REF].

Besides the extension of our framework to richer languages and features, an interesting direction for future work is to formally relate our results with general theories of denotational logical relations. Particularly relevant for that seems the work by Katsumata [START_REF] Katsumata | A generalisation of pre-logical predicates and its applications[END_REF] who observes that the closed structure of base categories is not necessarily essential. Another interesting direction for future work is the development of fibrational theories of coinductive reasoning for higher-order languages. Fibrational accounts of coinductive techniques have been given in the general setting of coalgebras [START_REF] Bonchi | Coinduction up-to in a fibrational setting[END_REF][START_REF] Bonchi | Up-to techniques for behavioural metrics via fibrations[END_REF], whereas general accounts of coinductive techniques for higher-order languages have been obtained in terms of relational reasoning [START_REF] Dal Lago | Effectful applicative similarity for call-by-name lambda calculi[END_REF][START_REF] Dal Lago | Effectful applicative bisimilarity: Monads, relators, and howe's method[END_REF][START_REF] Gavazzo | Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances[END_REF][START_REF] Dal | On bisimilarity in lambda calculi with continuous probabilistic choice[END_REF][START_REF] Dal | Effectful normal form bisimulation[END_REF][START_REF] Dal Lago | Effectful applicative similarity for call-by-name lambda calculi[END_REF][START_REF] Dal | Resource transition systems and full abstraction for linear higher-order effectful programs[END_REF][START_REF] Gavazzo | Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects[END_REF][START_REF] Dal | A relational theory of effects and coeffects[END_REF]. It would be interesting to see whether these two lines of research could be joined in our fibrational framework. That may also be a promising path to the development of conductive differential reasoning.

Figure 1

 1 Figure 1 Syntax and Static semantics of Λ.

3 ▶ 2 . 1 .

 321 Definition The objects of the syntactic graph Syn are environments Γ, types σ, and expressions σ, for σ a type. Arrows are defined thus: hom(Γ, σ) consists of values Γ ⊢ v : σ, whereas hom(Γ, σ) consists of terms Γ ⊢ t : σ; otherwise, the hom-set is empty.

Figure 2

 2 Figure 2 Coherence laws, where -.i ∈ {-.1, -.2} and i ∈ {p1, p2}.

F 8 A

 8 Fibrational Tale of Operational Logical Relationschosen cartesian arrow over u : I → p(X) and by u X : X → u ! X the chosen cocartesian arrow over u : p(X) → I. A bifibration is cloven if it has choices both for cartesian and cocartesian liftings. From now on, we assume all (bi/op)fibrations to be cloven.Let p : E → B be a functor and I an object in B. The fibre over I is the category E I where objects are objects X in E such that p(X) = I and arrows are arrows f : X → Y in E such that p(f ) = id I , namely, vertical arrows. Then, for every arrow u : I → J, if p is a fibration, we have a functor u * : E J → E I called reindexing along u and, if p is an opfibration, we have a functor u ! : E I → E J called image along u. If p is a bifibration, we have an adjunction u ! ⊣ u * . ▶ Example 3.1. n-ary predicates form a bifibration Pred Set : p(Set ) → Set , with p(Set ) having pairs of sets (X, A) with A ⊆ X n as objects and functions f : X → Y such that A ⊆ ( f ) -1 (B) as arrows f : (X, A) → (Y, B), and Pred Set (X, A) = X. The cartesian and cocartesian liftings of f are given by inverse and direct images along f , respectively. Special bifibrations are obtained for n = 1 (unary predicates) and n = 2 (binary relations). In those cases, we specialise the notation and write Sub Set : s(Set ) → Set and Rel Set : r(Set ) → Set . ▶ Example 3.2 (Weak subobjects). Let C be a category with weak pullbacks. We define the bifibration Ψ C : ws(C ) → C of weak subobjects in C[START_REF] Grandis | Weak subobjects and the epi-monic completion of a category[END_REF][START_REF] Emilia | Elementary quotient completion[END_REF]. Objects of ws(C ) are pairs (X, R) where X is an object of C and R is an object of the poset reflection of the slice C /X, hence it is an equivalence class [α] for an arrow

1 .▶ Example 3 . 5 .

 135 If C is cartesian closed, then Ψ C has universal quantifiers; 2. If C is slicewise weakly cartesian closed, then Ψ C is fibred cartesian closed. Since Set is locally cartesian closed, Proposition 3.4 implies that both Ψ Set

  using the universal property of the cartesian lifting of the e. As a paradigmatic example, we show the case of sequencing. First, let us notice that for any type σ, the evaluation arrow e : Sσ → T (Sσ) gives a cartesian arrow ē : e * ( Ṫ (Rσ)) → Ṫ (Rσ), i.e. ē : Rσ → Ṫ (Rσ) (since Rσ = e * ( Ṫ (Rσ))). Let us now consider the case of Γ ⊢ t to x.s : τ as obtained from Γ ⊢ t : σ and Γ, x : σ ⊢ s : τ . By induction hypothesis, we have arrows Rt : RΓ → Rσ and Rs : RΓ ×Rσ → Rτ . By postcomposing the former with ē, we obtain the arrow ē • Rt : RΓ → Ṫ (Rσ), and thus ⟨id RΓ , ē • Rt⟩ : RΓ → RΓ × Ṫ (Rσ). In a similar fashion, we have ē • Rs : RΓ ×Rσ → Ṫ (Rτ ) and thus, using the extension of the monad, > >=(ē•Rs) : RΓ × Ṫ (Rσ) → Ṫ (Rτ ). Altogether, we obtain the arrow > >=(ē•Rs)•⟨id RΓ , ē•Rt⟩ : RΓ → Ṫ (Rτ ). Using the commutative diagram of sequencing in Figure 2 and the very definition of a fibration, we obtain SΓ >>=(e•Ss)•⟨id Γ ,e•St⟩ # # S(t to x.s) Sτ e / / T (Sτ )

,

  The assignments DRel p (X) = |X| and DRel p (f ) = |f | determine a functor DRel p : dr(p) → B. ▶ Proposition 4.4. The functor DRel p : dr(p) → B is a fibration with finite products. Proof. Define the cartesian lifting along an arrow u : I → J of an object Y with |Y| = J by (u, π 2 , ⟨uπ 1 , π 2 , uπ 3 ⟩ δ Y ) : u * Y → Y, where u * Y = (I, Y , ⟨uπ 1 , π 2 , uπ 3 ⟩ * δ Y ). ◀ ▶ Remark 4.5. The fibration DRel p can be also obtained from the simple fibration [55] s : s(B) → B, where objects of s(B) are pairs (I, X) of objects in B; arrows (u, f ) : (I, X) → (J, Y ) are pairs of arrows u : I → J and f : I × X → Y in B; and s projects both objects and arrows on the first component. Indeed, we have that DRel p = s • p ′ where p ′ : dr(p) → s(B) with the functor s(B) → B mapping (I, X)

F▶

  pr H X / / H|X| × H(|X| × X ) × H|X| Proposition 4.9. (ϕ, ψ) : (F, G) ⇒ (H, K) is a 2-arrow in Fib.

  by naturality of ϕ. We define Ψ F = (F, F ) and Ψ ϕ = (ϕ, ϕ). ▶ Proposition 4.14. Ψ : Cat cwp → biFib c is a strict 2-functor. Therefore, composing Ψ and DR we get a lax functor from Cat cwp to Fib, this way extending Theorem 4.13. ▶ Theorem 4.15. Let T = (T, µ, η, st) be a strong monad on a category C with weak pullbacks and finite products. Then, ( T , µ, η, st) is a differential extension of T along Ψ C . ▶ Example 4.16. Let (T, µ, η) a monad on Set . The coupling-based lifting of (T, µ, η) to dr(Sub Set )

F S C D 2 0 2 2 3: 16 A

 216 Fibrational Tale of Operational Logical Relationsa new light on the mathematical foundation of both pure and effectful differential logical relations.

  and 1 ≃ ⊤ 1 .

▶ Definition 3.3. A fibration p : E → Bwith finite products is a logical fibration if it is fibred cartesian closed and has universal quantifiers, where: 1. p is fibred cartesian closed if every fibre E I has exponentials, denoted by X ⇒ Y , and reindexings preserve them. 2. p has universal quantifiers if for every projection π : I × J → I in B the reindexing functor π * : E I → E I×J has a right adjoint A I J : E I×J → E I satisfying the Beck-Chevalley condition

  Thus, for instance, the main novelty of DLRs is that a distance between two values λx.t, λx.s of type σ → τ is not just a number, but a function dt : V σ × σ → τ mapping a value v and an error/perturbation dv to an error/perturbation dt(v, dv). A DLR then relates λx.t and λx.s to dt if for all values v, w related to dv (meaning that v and w are dv-apart), then

t[v/x] and s[w/x] are related to dt(v, dv).

We use the notions of a strong monad (T, η, µ, st) and of a strong Kleisli triple T = (T, η, >>=) interchangeably, where for an arrow f : X × Y → T Z in a cartesian category C , we denote by >>=f : X × T Y → T Z the strong Kleisli extension of f . We write f † : T X → T Y for the Kleisli extension of f : X → T Y .F. Dagnino and F.Gavazzo

3:5 v, w::= x | c | ⟨⟩ | λx.t | ⟨v, w⟩ t, s ::= val v | vw | v.1 | v.2 | t to x.s | γ x : σ ∈ Γ Γ ⊢ x : σ Γ ⊢ c : ζ Γ ⊢ v : σ Γ ⊢ val v : σ Γ ⊢ γ : σ γ Γ, x : σ ⊢ t : τ Γ ⊢ λx.t : σ → τ Γ ⊢ v : σ → τ Γ ⊢ w : σ Γ ⊢ vw : τ Γ ⊢ t : σ Γ, x : σ ⊢ s : τ Γ ⊢ t to x.s : τ Γ ⊢ v : σ × τ Γ ⊢ v.1 : σ

Note that we do not require G to preserve cartesian arrows.

Actually, it suffices to have p(Rζ) = Sζ for basic types only, as the second part of the definition assures it for other types.F S C D 2 0 2 2

Whether differential extensions indeed define a monadic lifting is left as an open problem in[START_REF] Dal | Effectful program distancing[END_REF].

Actually, to carry out our construction, binary products in the base are enough, but we use a richer structure as we need it in the following part of this paper.

Here the monoidal structure is given just by cartesian product.

Funding This work was partially funded by the MUR project T-LADIES (PRIN 2020TL3X8X).

The second author is supported by the ERC Consolidator Grant DLV-818616 DIAPASoN.

Acknowledgements

The authors would like to thank the anonymous reviewers for the many useful comments, some of which improved of our work.


Abdelhak Hidouri
email: abdelhakhdr@gmail.com

Haifa Touati
email: haifa.touati@cristal.rnu.tn

Mohamed Hadded
email: mohamed.elhadad@irt-systemx.fr

Nasreddine Hajlaoui
email: hajlaoui.ing@gmail.com

Paul Muhlethaler
email: paul.muhlethaler@inria.fr

Abdelhak Hidouri Hatem

Haifa Touati Hatem

Nasreddine Hajlaoui Hatem

A Detection Mechanism for Cache Pollution Attack in Named Data Network Architecture

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The volume of the Internet traffic is constantly increasing and shifting to content distribution. According to CISCO Annual Internet Report [START_REF]Cisco Annual Internet Report -Cisco Annual Internet Report[END_REF], the video content (data, streaming, etc) that represents in 2016, 73% of the traffic consumed on the Internet, increases to 82% in 2021 and is expected to raise to 92% in 2023. However, the TCP/IP architecture is not optimal in terms of resources consumption [START_REF] Yang | An accelerating approach for blockchain information transmission based on NDN[END_REF] and has been always a vulnerable target for most of the security attacks, rather than the issues of not being fully capable of handling most of the new features such as massive content distribution, mobility and security. Named Data Networks (NDN) is one of the most suitable candidates for the future Internet architecture [START_REF] Touati | Named Data Networking-based communication model for Internet of Things using energy aware forwarding strategy and smart sleep mode[END_REF]. In NDN, each content is identified by a URI-like name and can be cached in intermediate NDN routers to serve subsequent requests for the same content [START_REF] Touati | Fair hop-by-hop interest rate control to mitigate congestion in named data networks[END_REF].

Caching in NDN is different from the traditional web caching "Recency-based policies", which is based on the idea that the content has been demanded recently in short period of time in other word "Short time locality" [START_REF] Karami | An ANFIS-based cache replacement method for mitigating cache pollution attacks in Named Data Networking[END_REF]. But, there is a high probability that the content will no longer be requested. NDN has different caching process, policies and metrics also NDN caching is much more optimized in which it manages to minimize both the bandwidth usage and the data retrieval delay all along with congestion avoidance.

NDN reserves three main essential components: (i) the Pending Interest Table (PIT) contains the interest packet entries and the corresponding list of incoming interfaces, (ii) the Forwarding Information Base (FIB) associates the prefix names to one or many output interfaces to which the interest packets should be forwarded and (iii) the Content Store (CS) holds a copy of the data packets that has been passed by the NDN router, this copy will be used to satisfy subsequent interests that request the same content [START_REF] Mejri | Hop-by-hop interest rate notification and adjustment in named data networks[END_REF].

In addition, NDN held a signature field inserted in each data packet where the content and the signature are binded together, to insure the verification of the data along the way of its transmission. When a data packet is received, the requesting consumer verifies the signature field [START_REF] Mejri | Preventing unnecessary interests retransmission in named data networking[END_REF]. Although, the verification by intervening routers is not mandatory because the verification overhead of the signature might be high, and a router needs access to multiple public key certificates to trust the public key that verifies a content signature [START_REF] Zhang | On Certificate Management in Named Data Networking[END_REF].

However, since NDN is not vulnerable to a range of basic attacks that are effective on the TCP/IP model, a number of new attacks have appeared that target NDN's main components. These attacks include the CPA where the attacker tries to deplete the size of the cache presented in the CS and deny other legitimate consumers from getting the desired content from the cache.

Obviously, the CPA attack leads to a considerable deterioration in the NDN architecture's performance in terms of Cache Hit Ratio (CHR) and Average Retrieval Delay (ARD). To mitigate the effect of this attack, we propose a new CPA detection mechanism, named ICAN, that monitors the state of each NDN node using different efficient parameters, namely the Average Cache Hit Ratio (AVG-CHR), the Average Interest Inter-Arrival Time (AVG-IAT), the Hop Count and the Prefix variation. ICAN insures high accuracy of detecting CPA attack, and it outperforms the pre-existed CPA detection mechanisms that present multiple gaps such as the exhaustion of router efficiency, increasing the total bandwidth usage and the intense consumption of the NDN routers resources.

The rest of this paper is organized as follows. Section 2 overviews the security vulnerabilities in named data networking and precisely CPA. The next section details the literature review of CPA detection mechanisms. Our proposed CPA detection mechanism: ICAN is detailed in Section 4 followed by evaluating the efficiency of the proposed CPA detection mechanism in Section 5. And we end up with a conclusion and future work upon section 6.

Cache Pollution Attack in Named Data Networks

In CPA, the attacker tries to cache unpopular content in the CS in an attempt to make the cache not available to legitimate consumers. This attack targets mostly NDN routers cache. More precisely, in CPA the attacker sends interest packets to change the priority of the content stored in the CS of nearby routers. This induces the caching of a large number of malicious packets in the CS. This behaviour changes the priority of the content and increases the popularity of these malicious contents. As a result, this attack reduces the probability of obtaining the legitimate content from the cache by the legitimate consumers. This attack confuses the router from detecting such fake content, so it rather keeps them in the router which results in False Locality Attack (FLA), and that's because the attacker does not follow any specific pattern. Another type of this attack is based on multiple number of attackers with a high frequency of demanding fake content, called Locality Disruption Attack (LDA) [START_REF] Kumar | Security Attacks in Named Data Networking: A Review and Research Directions[END_REF].

In our previous work [START_REF] Hidouri | Cache Pollution Attacks in the NDN Architecture: Impact and Analysis[END_REF], we assessed via extensive simulations the extent of the damage caused by the CPA attack. Our study reveals that when the CPA is launched, the CHR is reduced by around 90%. Even with different caching strategy: LRU (Least Recently Used), LFU (Least Frequently Used), FIFO (First In First Out) and Random, the CHR still decreases which reduces the available bandwidth, overloads the network and could lead, in certain conditions, to congestion. In the same study [START_REF] Hidouri | Cache Pollution Attacks in the NDN Architecture: Impact and Analysis[END_REF], we show that the CPA attack affects also the consumers by increasing the delay needed to obtain a desired content. This behaviour results in reduced bandwidth, increased data retrieval delay and in certain cases it may result in a Time-Out.

Overview of recent CPA detection mechanisms

Recently, several detection mechanisms have been proposed in the literature to capture the presence of a CPA attack in the network. Basically, we can classify these approaches into three main categories: (i) machine learning based approaches, (ii) statistical based solutions and (iii) probabilistic based approach. A brief literature review of these solutions is provided in the following subsections.

Machine Learning Based Approach

Adaptive Neuro-Fuzzy Inference System (ANFIS) [START_REF] Karami | An ANFIS-based cache replacement method for mitigating cache pollution attacks in Named Data Networking[END_REF] is one of the earliest solution that proposes to enhance NDN caching strategy by integrating a CPA detection mechanism based on machine learning. ANFIS works on each router independently by collecting statistics about each data packet cached in the CS and then passing this information through five layers of a fuzzy network to refine the goodness value. The goodness value is defined as the value used by the cache replacement policy for making the caching decision.

However, ANFIS detection algorithm is applied on cached contents (on the data packets present in the CS) and not on all received interests, which means that malicious interests are not detected unless the corresponding data packet is received and even more cached in the CS, i.e. after consuming network resources (bandwidth, caching resources, PIT entries, etc). Moreover, a nearby attacker can affect the router's caching choice. Because the router has access only to local data, it may mistakenly believe the attacker's request is valid and begin caching contents requested by the attacker instead of the actual legitimate content [START_REF] Kumar | Security Attacks in Named Data Networking: A Review and Research Directions[END_REF].

Statistical Based Approaches

To detect the existence of CPA, CacheShield [START_REF] Conti | A lightweight mechanism for detection of cache pollution attacks in Named Data Networking[END_REF] monitors the received contents. When the router receives a content for the first time, it stores its placeholder in the CS. If the router receives a content whose placeholder is already stored in CS, then it computes a shield function to decide whether the content will be cached or not [START_REF] Kumar | Security Attacks in Named Data Networking: A Review and Research Directions[END_REF]. Like ANFIS, CacheShield is applied on cached contents and not on received interests. Moreover, this mechanism can negatively impact the caching process, mainly due to its high space usage, and its high complexity. In fact, as explained in [START_REF] Kumar | Security Attacks in Named Data Networking: A Review and Research Directions[END_REF], this solution induces a large overhead in terms of space to store the placeholder names and in terms of CPU to compute the shield function.

Kamimoto et al. propose in [START_REF] Kamimoto | Cache protection method based on prefix hierarchy for content-oriented network[END_REF] a Prefix Hierarchy solution that includes a CPA detection algorithm. In the first step, this solution calculates the Weighted Request rate Variation per Prefix (WRVP) that helps to create a black-list. This black-list contains each prefix with the Request rate Variation per Prefix (RVP), then the router removes cached content from the black-list in the second step. In the final step, the router does not cache any future unpopular data, because namespace statistics are saved per namespace rather than per content. As the authors claimed, this mechanism uses less memory, but it still contains some gaps, the attacker can use less popular content of the popular prefix to perform the attack. [START_REF] Guo | Exploiting path diversity for thwarting pollution attacks in named data networking[END_REF] a path diversity based approach to detect CPA in NDN using the route of each content stored in each router. The main idea is to trace the route of each content using the information that exist in the CS, such as : the times the content object gets hit, the data structure of each content and the path of each content. Then, it calculates the Bernoulli distribution for each of the contents distinct paths, if the content has higher path value, it will be discarded from the cache otherwise it remains in the cache.

Guo et al. propose in

Lin Yao et al. proposed in [START_REF] Yao | Detection and defense of cache pollution attacks using clustering in named data networks[END_REF] a CPA detection approach based on clustering. This solution starts by computing the number of all interests and the time interval between two consecutive interests demanding the same content in the meanwhile the NDN router computes the interest probability and its time interval then it begins the procedure of clustering by calculating the Euclidean distance between all data points and form the clusters. Based on the results of the clusters, it decides whether CPA has been launched. A CPA attack is detected if the number of requests in the non-popular cluster suddenly drops. This solution may fall in false positive and may result in wrong judgements, where some legitimate consumers can demand low popular contents.

Probabilistic Based Approach

The Randomness Checks [START_REF] Park | Detection of cache pollution attacks using randomness checks[END_REF] solution is based on ranking each content received by the NDN router and calculating the probability of the low rate pollution attack. When a content is received, the NDN router uses this content to construct a binary matrix. Then it analyses this matrix to rank the content. As soon as the low rate content gets captured, i.e. the matrix reaches a pre-defined threshold, the router initiates an "attack warning". Although this method is light weighted, but it is still limited to small topologies, and it can make the caching replacement policy lose its efficiency. In addition, this mechanism cannot be extended to a larger NDN topology and wider scenarios.

After studying different CPA detection approaches and identifying the limits of each one of them, we conclude that, a new efficient CPA detection mechanism should be designed to overcome these limitations. This mechanism has to match the following criteria:

• The detection mechanism needs to take into account the content popularity and should be efficient by choosing the appropriate detection parameters. • The detection mechanism should use low computational time, less storage space usage and less time complexity. • The detection process should not expose the identity of the consumer and the producer. • The detection mechanism needs to be with a high accuracy and with a less detection time. • The detection mechanism needs to be able to manage large topology and more complex environments.

Intrusion detection system for Cache pollution Attack in Ndn (ICAN)

As discussed in the previous section, despite the progress that has been made in developing a method to detect CPA in NDN, this is not sufficient because even if the CPA is detected, these solutions, in return, induces high resources' usage by detecting the CPA on the cached Data and not the interest and may don't respect the NDN philosophy by exposing the identity of the consumers. Therefore, a lightweight interest-based solution is required to detect CPA while respecting the NDN philosophy. In this section, we explain our choice of the CPA detection parameters, then we present the CPA detection process.

CPA detection parameters

To detect if a malicious consumer is trying to pollute the CS, we propose that each router monitors a set of parameters, that we called CPA detection parameters. Based on the study that we conducted in [START_REF] Hidouri | Cache Pollution Attacks in the NDN Architecture: Impact and Analysis[END_REF], to assess the impact of CPA on the NDN network, we analyse the inherent characteristics of the network when the CPA is launched, to efficiently choose which parameters could be used as CPA indicators.

From this analysis, we extract four candidates CPA detection parameters: Average Cache Hit Ratio, Average Interest Inter-Arrival Time, prefix variation and Hop Count. The analysis of the variation of these parameters under CPA, will be detailed in the followings subsections.

Average Cache Hit Ratio (AVG-CHR)

To decide if the AVG-CHR could be chosen as a CPA detection parameter, we analyse the variation of the CHR with and without CPA in different scenarios [START_REF] Hidouri | Cache Pollution Attacks in the NDN Architecture: Impact and Analysis[END_REF]. An example of our analysis is given in Fig. 1. As illustrated in this figure, the AVG-CHR clearly decreases when the CPA is launched, and it drops to 0% in some points. The total difference between the AVG-CHR in Normal State and the AVG-CHR in Attack State reaches 40%. Therefore, we conclude that the AVG-CHR could be a good candidate to detect the appearance of a CPA attack.

Average Interest Inter-Arrival Time (AVG-IAT)

Inspired by previous works in the literature [16] [17], that used packet inter-arrival time to detect DDoS attack in TCP/IP networks, we define a similar parameter that we called the Average Interest Inter-Arrival Time (AVG-IAT) to detect the presence of CPA in NDN networks. This parameter is defined as the average, on each time period, of the time difference between the arrival of two consecutive interests at an NDN router. Fig. 2 traces an example of the variation of the AVG-IAT with and without CPA. We clearly observe that, the AVG-IAT decreases by around 40% when the attack is launched. Thus, this confirms that the Average Interest Inter-Arrival Time could be a good indicator of the presence of a CPA attack.

Prefix Variation

To ensure that the metrics elaborated above not falling into a false positive (i.e. considering a legitimate interest as a malicious request), we added the "Prefix Variation" parameter to ensure that such prefix is the one who is demanding such malicious content. We check the variation of the prefix in each time stamp to identify which prefix caused the decrease of the AVG-CHR and AVG-IAT and to mark it as suspected prefix.

Hop Count

The Hop Count parameter is defined as the number of hops between the consumer and the NDN router. As explained in Table 1, we observed that when the attack is launched, the hop count of the malicious interests stays stable. Hence, when the ratio of interests having the same Hop Count exceeds a pre-set threshold (i = 75%), we suspect a CPA attack.

CPA Detection process

The main steps of the proposed CPA detection algorithm are illustrated in the flowchart of Fig. 3. The detection process involves the following steps:

1. Each router monitors the upcoming interests and collects locally some statistics, like the Hop Count, the time when each interest reaches the router which will help us later to calculate the Average Interest Inter-Arrival Time, the Average of the Cache Hit Ratio and the prefix variation. 2. In each time period, the router verifies the existence of the attack by checking the state of the CPA detection parameters. If, the AVG-CHR decreases, the AVG-IAT decreases and this decrease is associated with the arrival of a new prefix (suspected prefix) and the hop count of the suspected prefix is stable, then the router concludes that it is under CPA and the algorithm marks that state as "Attack detected". 3. At each time the detection parameters suspect an attack, the router checks the new state to a Reference state, where the reference point presents the optimal state of the network before the attack appears. Based on the comparison to the Reference state, the router decides to come back to the "Normal state" or to stay in the "Attack detected" state.

Performance Evaluation

To validate the proposed ICAN solution, we conducted a simulation study as well as a Qualitative Comparative Analysis (QCA). The details of these studies are given in the next subsections.

Simulation based evaluation

In this section we evaluate, through simulations, the performance of ICAN. We used the NDNSim simulator as well as the latest python version 3.10.0 to implement our solution. We used a real-world topology, namely the German Research Network (DFN) shown in Fig. 4, and we varied the CPA attack entry into 8 main ranges. Each range is composed of 7 seconds of attack (Attack State) and 6 seconds of nonattack (Normal State). Table 2 summarizes the simulation settings. We evaluate our ICAN detection mechanism in terms of three metrics: Accuracy, False positive ratio (FP%) and False negative ratio (FN%). Table 3 summarizes the obtained results for Router 6 and Router 10.

The obtained results, show that the accuracy of ICAN reaches 92, 307% for router R6 and 91, 346% on router R10. Moreover, the false positive ratio is limited to 4, 807% for router R6 and 6, 730% on router R10. Finally, the false negative is reduced to 2.884% in router R6 and 1.923% in router R10. These results confirm the efficiency of our CPA detection approach.

Qualitative Comparative Analysis of our Proposed Solution

In Table 4, we elaborate a qualitative comparison based on the space usage in the router in terms of memory overhead, the complexity of the algorithm in terms of computational time and the insurance of the privacy of endpoints. Our qualitative comparison shows that ICAN requires less memory usage, conserves the identity of the consumer and insures high precision compared to state-of-the-art detection algorithms. In fact, our proposed detection algorithm ICAN is applied on interest packets, whereas most of other solutions are applied on cached data, hence our so-lution induces less memory usage since PIT and CS components will not be overloaded with malicious interest and cached data, respectively. Moreover, ICAN is a lightweight and simple solution, hence it induces a reduced computational time. On the other side, our proposal doesn't use the identity of the consumer or the producer to decide whether a CPA is performed or not, hence ICAN preserves a key feature of the NDN architecture, i.e. not using the identity or the addresses of the endpoints during data dissemination.

Conclusion and future works

In this paper, we begin with a literature review of CPA detection solutions in named data networks. We classified these approaches into three main categories, namely machine learning based approaches, statistical based approaches and probabilistic based approaches. We explain their detection algorithms and identify their limitations. This study reveals the need of a new robust and efficient CPA detection mechanism in NDN. Therefore, in a second step, we propose a new CPA detection mechanism called ICAN. Based on the analysis of the behaviour of the network, when the CPA is applied, we defined a set of parameters that will govern the CPA detection process. In our approach, the router continuously monitors the Average Cache Hit Ratio, the Average interest Inter Arrival Time, the Hop count and the variation of the prefix requested by the received interests to detect whether the received interests are sent by a malicious consumer or not. The proposed solution is applied on interest packets, thereby avoiding the need to load the network links as well as the PIT and the CS of intermediate routers by malicious interests. Simulation results conducted in a real-world topology illustrate the accuracy of the proposed solution.

As future work, another direction that could be explored is the design of a distributed detection mechanism where, instead of relaying on local parameters, each router communicates with other nodes to exchange related attack information.

Fig. 1

 1 Fig. 1 Analysis of the variation of the Cache Hit Ratio under CPA.

Fig. 2

 2 Fig. 2 Analysis of the variation of the Average Interest Inter-Arrival Time under CPA.

Fig. 3

 3 Fig. 3 Detection mechanism process.

Fig. 4

 4 Fig.4The German Research Network Topology (DFN).

Table 1

 1 Average Hop Count based Detection.

	Prefix	Hop Count	State
	/com/CPA.lab/xyz	7	i = 25%
	/com/CPA.lab/xyz	7	i = 50%
	/com/legitime.lab/xyz	5	i = 50%
	/com/CPA.lab/xyz	7	i = 75% Attack suspected
	/com/CPA.lab/xyz	7	i = 75% Attack suspected

Table 2

 2 Our CPA Detection Approach Settings

	Parameter	Value
	Simulation time	105s
	Number of legitimate consumers	6
	Number of attackers	1
	Consumer type	ConsumerZipfMandelbrot
	Interest rate	240 Interest/s
	Time of launching the attack
	Routers CS size	50
	Cache policy	LRU
	Topology	DFN *
	* German Research Network Topology (Deutsches Forschungs Netz)

5-12, 18-25, 31-38, 44-51, 57-60, 67-74, 80-87,93-100 s

Table 3

 3 Evaluation of the ICAN detection mechanism through simulation.

	Router	Accuracy (%) False Positive (%)	False Negative (%)
	Router 6	92, 307	4, 807	2, 884
	Router 10	91, 346	6, 730	1, 923

Table 4

 4 Qualitative Comparative Analysis (QCA) of the ICAN detection mechanism.

	Mechanism	Memory	Computational	Privacy Conser-	Accuracy	Topology
		Overhead	Time	vation
	ICAN	Low	Low	No leakage	High	DFN
	ANFIS [5]	Low	Low	No leakage	Medium	DFN
	CacheShield [11] High	High	Leak Consumers	Medium	Self-made
				information
	Prefix	Low	Low	No leakage	Low	DFN
	Hierarchy[12]
	Path Diversity [13] Medium	Low	No leakage	Medium	K-ary Tree
	Clustering [14]	Low	Low	No leakage	Medium	AS-1221
	Randomness	Low	High	-	High	-
	Checks [15]