Lionel Blatter

Nikolai Kosmatov

Virgile Prevosto

Pascale Le Gall

Certified verification of relational properties

est destinée au dépôt

Introduction

Modular deductive verification [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] allows the user to prove that a function respects its formal specification. More precisely, for a given function f , any individual call to f can be proved to respect the contract of f , that is, basically an implication: if the given precondition is true before the call and the call terminates 5 , the given postcondition is true after it. However, some kinds of properties are not easily reducible to a single function call. Indeed, it is frequently necessary to express a property that involves several functions or relates the results of several calls to the same function for different arguments. Such properties are known as relational properties [START_REF] Benton | Simple relational correctness proofs for static analyses and program transformations[END_REF]. Examples of such relational properties include monotonicity (i.e. x ≤ y ⇒ f (x) ≤ f (y)), involving two calls, or transitivity (cmp(x, y) ≥ 0 ∧ cmp(y, z) ≥ 0 ⇒ cmp(x, z) ≥ 0), involving three calls. In secure information flow [START_REF] Barthe | Secure information flow by self-composition[END_REF], noninterference is also a relational property. Namely, given a partition of program variables between high-security variables and low-security variables, a program is said to be non-interferent if any two executions starting from states in which the low-security variables have the same initial values will end up in a final state where the low-security variables have the same values. In other words, high-security variables cannot interfere with low-security ones.

Relational properties can also relate calls to different functions. For instance, in the verification of voting rules [START_REF] Beckert | Automated verification for functional and relational properties of voting rules[END_REF], relational properties are used for defining specific properties (such as monotonicity, anonymity or consistency). Notably, applying the voting rule to a sequence of ballots and a permutation of the same sequence of ballots must lead to the same result, i.e. the order in which the ballots are passed to the voting function should not have any impact on the outcome.

Motivation. Lack of support for relational properties in verification tools was already faced by industrial users (e.g. in [8] for C programs). The usual way to deal with this limitation is to use self-composition [START_REF] Barthe | Secure information flow by self-composition[END_REF][START_REF] Scheben | Efficient self-composition for weakest precondition calculi[END_REF][START_REF] Blatter | RPP: automatic proof of relational properties by self-composition[END_REF], product program [START_REF] Barthe | Relational verification using product programs[END_REF] or other self-composition optimizations [START_REF] Shemer | Property directed self composition[END_REF]. Those techniques are based on code transformations that are relatively tedious and error-prone. Moreover, they are hardly applicable in practice to real-life programs with pointers like in C. Namely, self-composition requires that the compared executions operate on completely separated (i.e. disjoint) memory areas, which might be extremely difficult to ensure for complex programs with pointers.

Example 1 (Motivating Example). Figure 1 shows an example of two simple C programs performing a swap of the values referred to by pointers x1 and x2 (of type int*). Program C sw1 uses an auxiliary variable x3 (of type int), while C sw2 performs an in-place swap using arithmetic operations. As usual in that case, to work correctly, each of these programs needs some separation hypotheses: pointers x1 and x2 should be separated (that is, point to disjoint memory locations) and must not point to x1, x2 themselves and, for C sw1 , to x3.

Consider a relational property, denoted R sw , stating that both programs, executed from two states in which each of *x1 and *x2 has the same value, will end up in two states also having the same values in these locations. To prove this relational property using self-composition, one typically has to generate a new C program C sw3 (see Fig. 1) composing C sw1 and C sw2 . To avoid name conflicts, we rename their variables by adding, resp., suffixes "_1" and "_2". The relational property R sw is then expressed by a contract of C sw3 with a precondition P and a postcondition Q. Obviously, both P and Q must include the equalities: *x1_1==*x1_2 and *x2_1==*x2_2, and P must also require the aforementioned separation hypotheses necessary for each function. But for programs with pointers and aliasing, this is not sufficient: the user also has to specify additional separation hypotheses 6 between variables coming from the different programs, that is, in our example, that each of x1_1 and x2_1 is separated from each of x1_2 and x2_2. Without such hypotheses, a deductive verification tool cannot show, for example, that a modification of *x1_1 does not impact *x1_2 in the composed program C sw3 , and is thus unable to deduce the required property. For real-life programs, such separation hypotheses can be hard to specify or generate. It can become even more complicated for programs with double or multiple indirections.

⊓ ⊔

Approach. This paper proposes an alternative approach that is not based on code transformation or relational rules. It directly uses a verification condition generator (VCGen) to produce logical formulas to be verified (typically, with an automated prover) to ensure a given relational property. It requires no extra code processing (such as sequential composition of programs or variable renaming). Moreover, no additional separation hypotheses-in addition to those that are anyway needed for each function to work-are required. The locations of each program are separated by construction: each program has its own memory state. The language L considered in this work was chosen as a minimal language representative of the main issues relevant for relational property verification: it is a standard While language enriched with annotations, procedures and pointers (see programs c sw1 and c sw2 in Fig. 1 for examples; we use a lower-case letter c for L programs and a capital letter C for C programs). Notably, the presence of dereferencing and address-of operations makes it representative of various aliasing problems with (possibly, multiple) pointer dereferences of a real-life language like C. We formalize the proposed approach and prove7 its soundness in the Coq proof assistant [START_REF]The Coq Development Team: The Coq Proof Assistant[END_REF]. Our Coq development contains about 3400 lines.

Contributions. The contributions of this paper include:

a Coq formalization and proof of soundness of recursive Hoare triple verification with a verification condition generator on a representative language with procedures and aliasing;

a novel method for verifying relational properties using a verification condition generator, without relying on code transformation (such as self-composition) or making additional separation hypotheses in case of aliasing; a Coq formalization and proof of soundness of the proposed method of relational property verification for the considered language.

Outline. Section 2 introduces an imperative language L used in this work. Functional correctness is defined in Section 3, and relational properties in Section 4.

Then, we prove the soundness of a VCGen in Section 5, and show how it can be soundly extended to verify relational properties in Section 6. Finally, we present related work in Section 7 and concluding remarks in Section 8. Let Σ be the set of functions σ : N → N, called memory states, and let σ, σ ′ , σ 1 , ... denote metavariables ranging over the set. A state σ maps a location to a value using its address: location x i has value σ(i).

We define the update operation of a memory state set(σ, i, n), also denoted by σ[i/n], as the memory state σ ′ mapping each address to the same value as σ, except for i, bound to n. Formally, set(σ, i, n) is defined by the following rules:

∀σ ∈ Σ, x i ∈ X, n ∈ N, x j ∈ X. i = j ⇒ σ[i/n](j) = n, (1)
∀σ ∈ Σ, x i ∈ X, n ∈ N, x j ∈ X. i ̸ = j ⇒ σ[i/n](j) = σ(j). (2)
Let Ψ be the set of functions ψ : Y → C, called procedure environments, mapping program names to commands (defined below), and let ψ, ψ 1 , ... denote metavariables ranging over Ψ . We write body ψ (y) to refer to ψ(y), the commands (or body) of procedure y for a given procedure environment ψ.

Assertions are predicates of arity one, taking as parameter a memory state and returning an equational first-order logic formula. Let metavariables P, Q, ... range over the set A of assertions. For instance, using λ-notation, assertion P assessing that location x 3 is bound to 2 can be defined by P ≜ λσ.σ(3) = 2. This form will be more convenient for relational properties (than e.g. x 3 = 2) as it makes explicit the memory states on which a property is evaluated.

Finally, we define the set Φ of contract environments ϕ : Y → A × A, and metavariables ϕ, ϕ 1 , ... to range over Φ. More precisely, ϕ maps a procedure name y to the associated (procedure) contract ϕ(y) = (pre ϕ (y), post ϕ (y)), composed of a pre-and a postcondition for procedure y. As usual, a procedure contract will allow us to specify the behavior of a single procedure call, that is, if we start executing y in a memory state satisfying pre ϕ (y), and the evaluation terminates, the final state satisfies post ϕ (y).

Syntax for Expressions and Commands

Let E a , E b and C denote respectively the sets of arithmetic expressions, Boolean expressions and commands. We denote by a, a 1 , ...; b, b 1 , ... and c, c 1 , ... metavariables ranging, respectively, over those sets. Syntax of arithmetic and Boolean expressions is given in Fig. 2. Constants are natural numbers or Boolean values. Expressions use standard arithmetic, comparison and logic binary operators, denoted respectively op a ::= {+, ×, -}, op b ::= {<=, =}, op l ::= {∨, ∧}. Since we use natural values, the subtraction is bounded by 0, as in Coq: if n ′ > n, the result of n -n ′ is considered to be 0. Expressions also include locations, possibly with a dereference or address operators. Figure 2 also presents the syntax of commands in L. Sequences, skip and conditions are standard. An assignment can be done to a location directly or after a dereference. Recall that a location x i contains as a value a natural number, say v, that can be seen in turn as the address of a location, namely x v , so the assignment * x i := a writes the value of expression a to the location x v , while the address operation &x i computes the address i of x i . An assertion command assert(P ) indicates that an assertion P should be valid at the point where the command occurs. The loop command while b inv P do {c 1 } is always annotated with an invariant P . As usual, this invariant should hold when we reach the command and be preserved by each loop step. Command call(y) is a procedure call. All annotations (assertions, loop invariants and procedure contracts) will be ignored during the program execution and will be relevant only for program verification in Section 5. Procedures do not have explicit parameters and return values (hence we use the term procedure call rather than function call ). Instead, as in assembly code [START_REF] Kip | Assembly Language for x86 Processors[END_REF], parameters and return value(s) are shared implicitly between the caller and the callee through memory locations: the caller must put/read the right values at the right locations before/after the call. Finally, to avoid ambiguity, we delimit sequences of commands with { }.

Example 2. Figure 3 shows an example of a command c rec and a procedure environment ψ where procedure y 1 points to a recursive command, called in c rec . With the semantics of Sec. 2.3, from any initial state, the command will return a state in which x 2 = x 3 × x 4 . Procedure y 1 returns a state where

crec ≜ x1 := x4; x2 := 0; call(y1) ψ =                    y1 → if x1 > 0 then { x2 := x2 + x3; x1 := x1 -1; call(y1) } else { skip } , . . .                    ϕ = y1 → λσ.σ(2) = σ(3) × (σ(4) -σ(1)) ∧ 0 ≤ σ(1) ∧ σ(1) ≤ σ(4), λσ.σ(2) = σ(3) × σ(4) , . . . .
ξa n σ ≜ n ξa xi σ ≜ σ(i) ξa * xi σ ≜ σ(σ(i)) ξa &xi σ ≜ i
x 2 = x 3 × x 4 if the initial state satisfies x 2 = x 3 × (x 4 -x 1 ) ∧ 0 ≤ x 1 ∧ x 1 ≤ x 4 .
This can be expressed by the contract environment ϕ given (in λ-notation) in Fig. 3. ⊓ ⊔

Operational Semantics

Evaluation of arithmetic and Boolean expressions in L is defined by functions ξ a and ξ b . Selected evaluation rules for arithmetic expressions are shown in Fig. 4. Operations * x i and &x i have a semantics similar to the C language, i.e. dereferencing and address-of. Semantics of Boolean expressions is standard [START_REF] Winskel | The formal semantics of programming languages -an introduction[END_REF].

Based on these evaluation functions, we can define the operational semantics of commands in a given procedure environment ψ. Selected evaluation rules8 are shown in Fig. 5. As said above, both assertions and loop invariants can be seen as program annotations that do not influence the execution of the program itself. Hence, command assert(P ) is equivalent to a skip. Likewise, loop invariant P has no influence on the semantics of while b inv P do {c}.

We write ⊩ ⟨c, σ⟩ ψ → σ ′ to denote that ⟨c, σ⟩ ψ → σ ′ can be derived from the rules of Fig. 5. Our Coq formalization, inspired by [START_REF] Pierce | Logical Foundations. Software Founda-tions series[END_REF], provides a deep embedding of L, with an associated parser, in files Aexp.v, Bexp.v and Com.v.

Functional Correctness

We define functional correctness in a similar way to the original Hoare triple definition [START_REF] Hoare | An axiomatic basis for computer programming[END_REF], except that we also need a procedure environment ψ, leading to a quadruple denoted ψ : {P }c{Q}. We will however still refer by the term "Hoare triple" to the corresponding program property, formally defined as follows. Definition 1 (Hoare triple). Let c be a command, ψ a procedure environment, and P and Q two assertions. We define a Hoare triple ψ : {P }c{Q} as follows:

⟨assert(P ), σ⟩ ψ → σ ξa a σ = n ⟨xi := a, σ⟩ ψ → σ[i/n] ξa a σ = n ⟨ * xi := a, σ⟩ ψ → σ[σ(i)/n] ⟨body ψ (y), σ1⟩ ψ → σ2 ⟨call(y), σ1⟩ ψ → σ2
ψ : {P }c{Q} ≜ ∀σ, σ ′ ∈ Σ. P (σ) ∧ (⊩ ⟨c, σ⟩ ψ → σ ′ ) ⇒ Q(σ ′ ).
Informally, our definition states that, for a given ψ, if a state σ satisfies P and the execution of c on σ terminates in a state σ ′ , then σ ′ satisfies Q.

Next, we introduce notation CV (ψ, ϕ) to denote the fact that, for the given ϕ and ψ, every procedure satisfies its contract.

Definition 2 (Contract Validity). Let ψ be a procedure environment and ϕ a contract environment. We define contract validity CV (ψ, ϕ) as follows:

CV (ψ, ϕ) ≜ ∀y ∈ Y. ψ : {pre ϕ (y)}call(y){post ϕ (y)}).
The notion of contract validity is at the heart of modular verification, since it allows assuming that the contracts of the callees are satisfied during the verification of a Hoare triple. More precisely, to state the validity of procedure contracts without assuming anything about their bodies in our formalization, we will consider an arbitrary choice of implementations ψ ′ of procedures that satisfy the contracts, like in assumption (3) in Lemma 1. This technical lemma, taken from [1, Equation (4.6)], gives an alternative criterion for validity of procedure contracts: if, under the assumption that the contracts in ϕ hold, we can prove for each procedure y that its body satisfies its contract, then the contracts are valid.

Lemma 1 (Adequacy of contracts). Given a procedure environment ψ and a contract environment ϕ such that

∀ψ ′ ∈ Ψ. CV (ψ ′ , ϕ) ⇒ ∀y ∈ Y, ψ ′ : {pre ϕ (y)}body ψ (y){post ϕ (y)}, (3)
we have CV (ψ, ϕ).

Proof. Any given terminating execution traverses a finite number of procedure calls (over all procedures) that can be replaced by inlining the bodies a sufficient number of times. We first formalize a theory of k-inliners (that inline procedure bodies a finite number of times k ≥ 0 and replace deeper calls by nonterminating loops) and prove their properties. Relying on this elegant theory, the proof of the lemma proceeds by induction on the number of procedure inlinings.

⊓ ⊔

From that, we can establish the main result of this section. Theorem 1, taken from [START_REF] Apt | Verification of Sequential and Concurrent Programs[END_REF]Th. 4.2] states that ψ : {P }c{Q} holds if assumption (3) holds and if the validity of contracts of ϕ for ψ implies the Hoare triple itself. This theorem is the basis for modular verification of Hoare Triples, as done for instance in Hoare Logic [START_REF] Hoare | An axiomatic basis for computer programming[END_REF][START_REF] Winskel | The formal semantics of programming languages -an introduction[END_REF] or verification condition generation.

Theorem 1 (Recursion). Given a procedure environment ψ and a contract environment ϕ such that ∀ψ ′ ∈ Ψ. CV (ψ ′ , ϕ) ⇒ ∀y ∈ Y, ψ ′ : {pre ϕ (y)}body ψ (y){post ϕ (y)}, and

CV (ψ, ϕ) ⇒ ψ : {P }c{Q},
we have ψ : {P }c{Q}.

Proof. By Lemma 1.

⊓ ⊔

We refer the reader to the Coq development, more precisely the results recursive_proc and recursive_hoare_triple in file Hoare_Triple.v for complete proofs of Lemma 1 and Theorem 1 for L. To the best of our knowledge, this is the first mechanized proof of these classical results.

An interesting corollary can be deduced from Theorem 1.

Corollary 1 (Procedure Recursion) Given a procedure environment ψ and a contract environment ϕ such that

∀ψ ′ ∈ Ψ. CV (ψ ′ , ϕ) ⇒ ∀y ∈ Y, ψ ′ : {pre ϕ (y)}body ψ (y){post ϕ (y)},
we have ∀y ∈ Y. ψ : {pre ϕ (y)}body ψ (y){post ϕ (y)}.

Relational Properties

Relational properties can be seen as an extension of Hoare triples. But, instead of linking one program with two properties, the pre-and postconditions, relational properties link n programs to two properties, called relational assertions.

We define a relational assertion as a predicate taking a sequence of memory states and returning a first-order logic formula. We use metavariables P , Q, ... to range over the set of relational assertions, denoted A. As a simple example of a relational assertion, we might say that two states bind location x 3 to the same value. This would be stated as follows:

λ(σ 1 , σ 2 ).σ 1 (3) = σ 2 (3).
A relational property is a property about n programs c 1 , ..., c n , stating that if each program c i starts in a state σ i and ends in a state σ ′ i such that P (σ 1 , ..., σ n ) holds, then Q(σ ′ 1 , ..., σ ′ n ) holds, where P and Q are relational assertions over n memory states.

We formally define relational correctness similarly to functional correctness (cf. Def. 1), except that we now use sequences of memory states and commands of equal length. We denote by (u k ) n a sequence of elements (u k ) n k=1 = (u 1 , . . . , u n ), where k ranges from 1 to n. If n ≤ 0, (u k ) n is the empty sequence denoted [ ].

ψ : { P } c sw1 ∼ c sw2 { Q}, P ≜ λσ 1 σ 2 . σ 1 (σ 1 (1)) = σ 2 (σ 2 (1)) ∧ σ 1 (σ 1 (2)) = σ 2 (σ 2 (2))∧ σ 1 (1) ̸ = σ 1 (2) ∧ σ 2 (1) ̸ = σ 2 (2) ∧ σ 1 (1) > 3 ∧ σ 1 (2) > 3 ∧ σ 2 (1) > 2 ∧ σ 2 (2) > 2, Q ≜ λσ ′ 1 σ ′ 2 . σ ′ 1 (σ ′ 1 (1)) = σ ′ 2 (σ ′ 2 (1)) ∧ σ ′ 1 (σ ′ 1 (2)) = σ ′ 2 (σ ′ 2 (2)
). Figure 6: A relational property for L programs c sw1 and c sw2 of Fig. 1.

Definition 3 (Relational Correctness). Let ψ be a procedure environment, (c k ) n a sequence of n commands (n ∈ N * ), and P and Q two relational assertions over n states. The relational correctness of (c k ) n with respect to P and Q, denoted ψ : { P }(c k ) n { Q}, is defined as follows:

ψ : { P }(c k ) n { Q} ≜ ∀(σ k ) n , (σ ′ k ) n . P ((σ k ) n ) ∧ ( n i=1 ⊩ ⟨c i , σ i ⟩ ψ → σ ′ i ) ⇒ Q((σ ′ k ) n ).
This notation generalizes the one proposed by Benton [START_REF] Benton | Simple relational correctness proofs for static analyses and program transformations[END_REF] for relational properties linking two commands: ψ : { P }c 1 ∼ c 2 { Q}. As Benton's work mostly focused on comparing equivalent programs, using symbol ∼ was quite natural. In particular, Benton's work would not be practical for verification of relational properties with several calls such as transitivity mentioned in Sec. 1.

Example 3 (Relational property). Figure 6 formalizes the relational property R sw for L programs c sw1 and c sw2 discussed in Ex. 1. Recall that R sw (written in Fig. 6 in Benton's notation) states that both programs executed from two states named σ 1 and σ 2 having the same values in * x 1 and * x 2 will end up in two states σ ′ 1 and σ ′ 2 also having the same values in these locations. Notice that the initial state of each program needs separation hypotheses (cf. the second line of the definition of P ). Namely, x 1 and x 2 must point to different locations and must not point to x 1 , x 2 or, for c sw1 , to x 3 for the property to hold. This relational property is formalized in the Coq development in file Examples.v.

⊓ ⊔

Verification Condition Generation for Hoare Triples

A standard way [START_REF] Floyd | Assigning meanings to programs[END_REF] for verifying that a Hoare triple holds is to use a verification condition generator (VCGen). In this section, we formalize a VCGen for Hoare triples and show that it is correct, in the sense that if all verification conditions that it generates are valid, then the Hoare triple is valid according to Def. 1.

Verification Condition Generator

We have chosen to split the VCGen in three steps, as it is commonly done [START_REF] Kirchner | Frama-C: A software analysis perspective[END_REF]:

function T c generates the main verification condition, expressing that the postcondition holds in the final state, assuming auxiliary annotations hold; function T a generates auxiliary verification conditions stemming from assertions, loop invariants, and preconditions of called procedures; finally, function T f generates verification conditions for the auxiliary procedures that are called by the main program, to ensure that their bodies respect their contracts.

Tc skip (σ, ϕ, f ) ≜ ∀σ ′ . σ ′ = σ ⇒ f (σ ′ ) Tc xi := a (σ, ϕ, f ) ≜ ∀σ ′ . σ ′ = set(σ, i, ξa a σ) ⇒ f (σ ′ ) Tc * xi := a (σ, ϕ, f ) ≜ ∀σ ′ . σ ′ = set(σ, σ(i), ξa a σ) ⇒ f (σ ′ ) Tc assert(P ) (σ, ϕ, f ) ≜ ∀σ ′ . σ ′ = σ ∧ P (σ) ⇒ f (σ ′ ) Tc c0; c1 (σ, ϕ, f ) ≜ Tc c0 (σ, ϕ, λσ ′ . Tc c1 (σ ′ , ϕ, f )) Tc if b then {c0} else {c1} (σ, ϕ, f ) ≜ (ξ b b σ ⇒ Tc c0 (σ, ϕ, f ))∧ (¬ξ b b σ ⇒ Tc c1 (σ, ϕ, f )) Tc call(y) (σ, ϕ, f ) ≜ pre ϕ (y)(σ) ⇒ (∀σ ′ . post ϕ (y)(σ ′ ) ⇒ f (σ ′ )) Tc while b inv inv do {c} (σ, ϕ, f ) ≜ inv(σ) ⇒ (∀σ ′ . inv(σ ′ ) ∧ ¬(ξ b b σ ′ ) ⇒ f (σ ′ ))

Definition 4 (Function T c generating the main verification condition).

Given a command c, a memory state σ representing the state before the command, a contract environment ϕ, and an assertion f , function T c returns a formula defined by case analysis on c as shown in Fig. 7.

Assertion f represents the postcondition we want to verify after the command executed from state σ. For each command, except sequence and branch, a fresh memory state σ ′ is introduced and related to the current memory state σ. The new memory state is given as parameter to f . For skip, which does nothing, both states are identical. For assignments, σ ′ is simply the update of σ. An assertion introduces a hypothesis over σ but leaves it unchanged. For a sequence, we simply compose the conditions, that is, we check that the final state of c 0 is such that f will be verified after executing c 1 . For a conditional, we check that if the condition evaluates to true, the then branch will ensure the postcondition, and that otherwise the else branch will ensure the postcondition. The rule for calls simply assumes that σ ′ verifies post ϕ (y). Finally, T c assumes that, after a loop, σ ′ is a state where the loop condition is false and the loop invariant holds. As for an assertion, the callee's precondition and the loop invariant are just assumed to be true; function T a , defined below, generates the corresponding proof obligations.

Example 4. For c ≜ skip; x 1 := 2, and f ≜ λσ. σ(1) = 2, we have:

T c c (σ, ϕ, f ) ≡ ∀σ ′ 1 .σ = σ ′ 1 ⇒ (∀σ ′ 2 .σ ′ 2 = set(σ ′ 1 , 1, 2) ⇒ σ ′ 2 (1) = 2). ⊓ ⊔ Ta skip (σ, ϕ) ≜ T rue Ta xi := a (σ, ϕ) ≜ T rue Ta * xi := a (σ, ϕ) ≜ T rue
Ta assert(P ) (σ, ϕ) ≜ P (σ)

Ta c0; c1 (σ, ϕ) ≜ Ta c0 (σ, ϕ)∧ Tc c0 (σ, ϕ, λσ ′ .(Ta c1 (σ ′ , ϕ))) Ta if b then {c0} else {c1} (σ, ϕ) ≜ ξ b b σ ⇒ Ta c0 (σ, ϕ)∧ ¬(ξ b b σ) ⇒ Ta c1 (σ, ϕ) Ta call(y) (σ, ϕ) ≜ pre ϕ (y)(σ) Ta while b inv inv do {c} (σ, ϕ) ≜ inv(σ)∧ (∀σ ′ , inv(σ ′ ) ∧ ξ b b σ ′ ⇒ Ta c (σ ′ , ϕ))∧ (∀σ ′ , inv(σ ′ ) ∧ ξ b b σ ′ ⇒ Tc c (σ ′ , ϕ, inv))
Figure 8: Definition of function T a generating auxiliary verification conditions.

Definition 5 (Function T a generating the auxiliary verification conditions). Given a command c, a memory state σ representing the state before the command, and a contract environment ϕ, function T a returns a formula defined by case analysis on c as shown in Fig. 8.

Basically, T a collects all assertions, preconditions of called procedures, as well as invariant establishment and preservation, and lifts the corresponding formulas to constraints on the initial state σ through the use of T c .

Finally, we define the function for generating the conditions for verifying that the body of each procedure defined in ψ respects its contract defined in ϕ.

Definition 6 (Function T f generating the procedure verification condition). Given two environments ψ and ϕ, T f returns the following formula:

T f (ϕ, ψ) ≜ ∀y, σ. pre ϕ (y)(σ) ⇒ T a body ψ (y) (σ, ϕ) ∧ T c body ψ (y) (σ, ϕ, post ϕ (y)).
The VCGen is defined in file Vcg.v of the Coq development. Interested readers will also find a proof (in file Vcg Opt.v) of a VCGen optimization (not detailed here), which prevents the size of the generated formulas from becoming exponential in the number of conditions in the program [START_REF] Flanagan | Avoiding exponential explosion: generating compact verification conditions[END_REF], which is a classical problem for "naive" VCGens.

Hoare Triple Verification

We can now state the theorems establishing correctness of the VCGen. Their proof can be found in file Correct.v of the Coq development.

First, Lemma 2 shows that, under the assumption of the procedure contracts, a Hoare triple is valid if for all memory states satisfying the precondition, the main verification condition and the auxiliary verification conditions hold. Lemma 2. Assume the following two properties hold:

∀σ ∈ Σ, P (σ) ⇒ T a c (σ, ϕ), ∀σ ∈ Σ, P (σ) ⇒ T c c (σ, ϕ, Q).
Then we have CV (ψ, ϕ) ⇒ ψ : {P }c{Q}.

Proof. By structural induction over c.

⊓ ⊔

Next, we prove in Lemma 3 that if T f (ϕ, ψ) holds, then for an arbitrary choice of implementations ψ ′ of procedures respecting the procedure contracts, the body of each procedure y respects its contract.

Lemma 3. Assume that the formula T f (ϕ, ψ) is satisfied. Then we have

∀ψ ′ ∈ Ψ. CV (ψ ′ , ϕ) ⇒ ∀y ∈ Y, ψ ′ : {pre ϕ (y)}body ψ (y){post ϕ (y)}.
Proof. By Lemma 2.

⊓ ⊔

Finally, we can establish the main theorem of this section, stating that the VCGen is correct with respect to our definition of Hoare triples.

Theorem 2 (Soundness of VCGen). Assume that we have T f (ϕ, ψ) and

∀σ ∈ Σ, P (σ) ⇒ T a c (σ, ϕ), ∀σ ∈ Σ, P (σ) ⇒ T c c (σ, ϕ, Q).
Then we have ψ : {P }c{Q}.

Proof. By Theorem 1 and Lemmas 2 and 3.

⊓ ⊔ Example 5. Consider again the command c rec , procedure environment ψ, and contract environment ϕ of Ex. 2 (presented in Fig. 3). We can apply Theorem 2 to prove its functional correctness expressed by the following Hoare triple:

ψ : {λσ.T rue} c rec {λσ.σ(2) = σ(4) × σ(3)} (see command com_rec in file Examples.v). ⊓ ⊔

Verification of Relational Properties

In this section, we propose a verification method for relational properties (defined in Section 4) using the VCGen defined in Section 5 (or, more generally, any VCGen respecting Theorem 2). First, we define the notation T cr for the recursive call of function T c on a sequence of commands and memory states:

Definition 7 (Function T cr ). Given a sequence of commands (c k ) n and a sequence of memory states (σ k ) n , a contract environment ϕ and a predicate Q over n states, function T cr is defined by induction on n as follows.

-Basis: n = 0.

T cr ([ ], [ ], ϕ, Q) ≜ Q([ ]).
-Inductive: n ∈ N * .

T cr ((c k ) n , (σ k ) n , ϕ, Q) ≜ T c c n (σ n , ϕ, λσ ′ n .T cr ((c k ) n-1 , (σ k ) n-1 , ϕ, λ(σ ′ k ) n-1 . Q((σ ′ k ) n ))).
Intuitively, for n = 2, T cr gives the weakest relational condition that σ 1 and σ 2 must fulfill in order for Q to hold after executing c 1 from σ 1 and c 2 from σ 2 :

T cr ((c 1 , c 2 ), (σ 1 , σ 2 ), ϕ, Q) ≡ T c c 2 (σ 2 , ϕ, λσ ′ 2 .T c c 1 (σ 1 , ϕ, λσ ′ 1 . Q(σ ′ 1 , σ ′ 2 ))).
Remark 1. Assume we have n > 0, a command c n , a sequence of commands (c k ) n-1 , and a sequence of memory states (σ k ) n-1 . From Def. 1, it follows that

∀σ n , σ ′ n . P ((σ k ) n ) ∧ (⊩ ⟨c n , σ n ⟩ ψ → σ ′ n ) ⇒ T cr ((c k ) n-1 , (σ k ) n-1 , ϕ, λ(σ ′ k ) n-1 . Q((σ ′ k ) n ))
is equivalent to

ψ : {λσ n . P ((σ k ) n )}c n {λσ ′ n .T cr ((c k ) n-1 , (σ k ) n-1 , ϕ, λ(σ ′ k ) n-1 . Q((σ ′ k ) n ))}.
Example 6 (Relational verification condition). In order to make things more concrete, we can go back to the relational property R sw between two implementations c sw1 and c sw2 of swap defined in Ex. [START_REF] Apt | Verification of Sequential and Concurrent Programs[END_REF] and examine what would be the main verification condition generated by T cr . Let P and Q be defined as in Ex. 3. In this particular case, we have n = 2, and ϕ is empty (since we do not have any function call), thus Def. 7 becomes:

T cr ((c sw1 , c sw2 ), (σ 1 , σ 2 ), ∅, Q) = T c c sw2 (σ 2 , ∅, λσ ′ 2 .T c c sw1 (σ 1 , ∅, λσ ′ 1 . Q(σ ′ 1 , σ ′ 2 ))).
We thus start by applying T c over c sw1 , to obtain, using the rules of Def. 4 for sequence and assignment, the following intermediate formula:

T cr ((c sw1 , c sw2 ), (σ 1 , σ 2 ), ∅, Q) = T c (c sw2 , σ 2 , ∅, λσ ′ 2 .∀σ 3 , σ 5 , σ 7 . σ 3 = σ 1 [3/σ 1 (σ 1 (1))] ⇒ σ 5 = σ 3 [σ 3 (1)/σ 3 (σ 3 (2))] ⇒ σ 7 = σ 5 [σ 5 (2)/σ 5 (3)] ⇒ Q(σ 7 , σ ′ 2 ).
13

We can then do the same with c sw2 to obtain the final formula:

T cr ((c sw1 , c sw2 ), (σ 1 , σ 2 ), ∅, Q) = ∀(σ k ) 8 . σ 4 = σ 2 [σ 2 (1)/σ 2 (σ 2 (1)) + σ 2 (σ 2 (2))] ⇒ σ 6 = σ 4 [σ 4 (2)/σ 4 (σ 4 (1)) -σ 4 (σ 4 (2))] ⇒ σ 8 = σ 6 [σ 6 (1)/σ 6 (σ 6 (1)) -σ 6 (σ 6 (2))] ⇒ σ 3 = σ 1 [3/σ 1 (σ 1 (1))] ⇒ σ 5 = σ 3 [σ 3 (1)/σ 3 (σ 3 (2))] ⇒ σ 7 = σ 5 [σ 5 (2)/σ 5 (3)] ⇒ Q(σ 7 , σ 8 ).
Here, σ k with odd (resp., even) indices result from T c for c sw1 (resp., c sw2 ). ⊓ ⊔

We similarly define a notation for the auxiliary verification conditions for a sequence of n commands.

Definition 8 (Function T ar ). Given a sequence of commands (c k ) n and a sequence of memory states (σ k ) n , we define function T ar as follows:

T ar ((c k ) n , (σ k ) n , ϕ) ≜ n i=1 T a c i (σ i , ϕ).
Remark 2. For n > 0, it trivially follows from Def. 8 that:

T ar ((c k ) n , (σ k ) n , ϕ) ≡ T a c n (σ n , ϕ) ∧ T ar ((c k ) n-1 , (σ k ) n-1 , ϕ).
Using functions T cr and T ar , we can now give the main result of this paper: it states that the verification of relational properties using the VCGen is correct.

Theorem 3 (Soundness of relational VCGen). For any sequence of commands (c k ) n , contract environment ϕ, procedure environment ψ, and relational assertions over n states P and Q, if the following three properties hold:

T f (ϕ, ψ), (4)
∀(σ k ) n , P ((σ k ) n ) ⇒ T ar ((c k ) n , (σ k ) n , ϕ), (5)
∀(σ k ) n , P ((σ k ) n ) ⇒ T cr ((c k ) n , (σ k ) n , ϕ, Q), (6)
then we have ψ :

{ P }(c k ) n { Q}.
In other words, a relational property is valid if all procedure contracts are valid, and, assuming the relational precondition holds, both the auxiliary verification conditions and the main relational verification condition hold. We give the main steps of the proof below. The corresponding Coq formalization is available in file Rela.v, and the Coq proof of Theorem 3 is in file Correct Rela.v.

Proof. By induction on the length n of the sequence of commands (c k ) n .

-Induction basis: n = 0. By Def. 3, our goal becomes:

ψ : { P }(c k ) 0 { Q} ≡ P ([ ]) ⇒ Q([ ]).
Indeed, by definition of T cr and Hypothesis [START_REF] Benton | Simple relational correctness proofs for static analyses and program transformations[END_REF]

, P ([ ]) ⇒ Q([ ]) holds.
-Induction step: assuming the result for n, we prove it for n + 1. So, assume we have a sequence of commands (c k ) n+1 , relational assertions and environments respecting (4), ( 5), ( 6) (stated for sequences of n + 1 elements). We have to prove ψ : { P }(c k ) n+1 { Q}, which, by Def. 3, is equivalent to:

∀(σ k ) n+1 , (σ ′ k ) n+1 . P ((σ k ) n+1 )∧( n+1 i=1 ⊩ ⟨c i , σ i ⟩ ψ → σ ′ i ) ⇒ Q((σ ′ k ) n+1 ). (7)
First, we can deduce from Hypothesis (5) and Remark 2:

∀(σ k ) n+1 , P ((σ k ) n+1 ) ⇒ T a c n+1 (σ n+1 , ϕ), (8)
∀(σ k ) n+1 , P ((σ k ) n+1 ) ⇒ T ar ((c k ) n , (σ k ) n , ϕ). (9)
By Hypothesis [START_REF] Benton | Simple relational correctness proofs for static analyses and program transformations[END_REF] and Def. 7, we have

∀(σ k ) n+1 , P ((σ k ) n+1 ) ⇒ T c c n+1 (σ n+1 , ϕ, λσ ′ n+1 .T cr ((c k ) n , (σ k ) n , ϕ, λ(σ ′ k ) n . Q((σ k ) n+1 ))). (10)
Using ( 4), ( 8) and [START_REF] Blatter | Static and dynamic verification of relational properties on self-composed C code[END_REF], we can now apply Theorem 2 (for an arbitrary subsequence (σ k ) n , that we can thus put in an external universal quantifier) to obtain:

∀(σ k ) n . ψ : {λσ n+1 . P ((σ k ) n+1 )}c n+1 {λσ ′ n+1 . T cr ((c k ) n , (σ k ) n , ϕ, λ(σ ′ k ) n . Q((σ ′ k ) n+1 ))}. (11)
Using Remark 1 and by rearranging the quantifiers and implications, we can rewrite [START_REF] Blazy | Verified validation of program slicing[END_REF] into:

∀σ n+1 , σ ′ n+1 . ⊩ ⟨c n+1 , σ n+1 ⟩ ψ → σ ′ n+1 ⇒ ∀(σ k ) n . P ((σ k ) n+1 ) ⇒ T cr ((c k ) n , (σ k ) n , ϕ, λ(σ ′ k ) n . Q((σ ′ k ) n+1 )). ( 12
)
For arbitrary states σ n+1 and σ ′ n+1 such that ⊩ ⟨c n+1 , σ n+1 ⟩ ψ → σ ′ n+1 , using (4), ( 9) and ( 12), we can apply the induction hypothesis, and obtain:

∀σ n+1 , σ ′ n+1 . ⊩ ⟨c n+1 , σ n+1 ⟩ ψ → σ ′ n+1 ⇒ ψ : {λ(σ k ) n . P ((σ k ) n+1 )}(c k ) n {λ(σ ′ k ) n . Q((σ ′ k ) n+1 )}.
Finally, by Def. 3 and by rearranging the quantifiers, we deduce [START_REF] Beringer | Abstraction and subsumption in modular verification of C programs[END_REF]. ⊓ ⊔ Example 7. The relational property of Ex. 3 is proven valid using the proposed technique based on Theorem 3 in file Examples.v of the Coq development. For instance, (6) becomes ∀σ 1 , σ 2 . P (σ 1 , σ 2 ) ⇒ T cr ((c sw1 , c sw2 ), (σ 1 , σ 2 ), ∅, Q), where the last expression was computed in Ex. 6. Such formulas-long for a manual proof-are well-treated by automatic solvers. Notice that in this example we do not need any code transformations or extra separation hypotheses in addition to those anyway needed for the swap functions while both programs manipulate the same locations x 1 , x 2 , and-even worsethe unknown locations pointed by them can be any locations x i , i > 3.

⊓ ⊔

Related Work

Relational Property Verification. Significant work has been done on relational program verification (see [START_REF] Naumann | Thirty-seven years of relational Hoare logic: Remarks on its principles and history[END_REF][START_REF] Maillard | The next 700 relational program logics[END_REF] for a detailed state of the art). We discuss below some of the efforts the most closely related to our work. Various relational logics have been designed as extensions to Hoare Logic, such as Relational Hoare Logic [START_REF] Benton | Simple relational correctness proofs for static analyses and program transformations[END_REF] and Cartesian Hoare Logic [START_REF] Sousa | Cartesian Hoare Logic for Verifying k-safety Properties[END_REF]. As our approach, those logics consider for each command a set of associated memory states in the very rules of the system, thus avoiding additional separation assumptions. Limitations of these logics are often the absence of support for aliasing or a limited form of relational properties. For instance, Relational Hoare Logic supports only relational properties with two commands and Cartesian Hoare Logic supports only k-safety properties (relational properties on the same command). Our method has an advanced support of aliasing and supports a very general definition of relational properties, possibly between several dissimilar commands.

Self-compositon [START_REF] Barthe | Secure information flow by self-composition[END_REF][START_REF] Scheben | Efficient self-composition for weakest precondition calculi[END_REF][START_REF] Blatter | RPP: automatic proof of relational properties by self-composition[END_REF] and its derivations [START_REF] Barthe | Relational verification using product programs[END_REF][START_REF] Shemer | Property directed self composition[END_REF][START_REF] Eilers | Modular product programs[END_REF] are well-known approaches to deal with relational properties. This is in particular due to their flexibility: self-composition methods can be applied as a preprocessing step to different verification approaches. For example, self-composition is used in combination with symbolic execution and model checking for verification of voting functions [START_REF] Beckert | Automated verification for functional and relational properties of voting rules[END_REF]. Other examples are the use of self-composition in combination with verification condition generation in the context of the Java language [START_REF] Dufay | Privacy-sensitive information flow with JML[END_REF] or the C language [START_REF] Blatter | RPP: automatic proof of relational properties by self-composition[END_REF][START_REF] Blatter | Static and dynamic verification of relational properties on self-composed C code[END_REF]. In general, the support of aliasing of C programs in these last efforts is very limited due the problems mentioned earlier. Compared to these techniques, where self-composition is applied before the generation of verification conditions (and therefore requires taking care about separation of memory states of the considered programs), our method can be seen as relating the considered programs' semantics directly at the level of the verification conditions, where separation of their memory states is already ensured, thus avoiding the need to take care of this separation explicitly.

Finally, another advanced approach for relational verification is the translation of the relational problem into Horn clauses and their proof using constraint solving [START_REF] Kiefer | Relational program reasoning using compiler IR -combining static verification and dynamic analysis[END_REF][START_REF] Unno | Constraint-based relational verification[END_REF]. The benefit of constraint solving lies in the ability to automatically find relational invariants and complex self-composition derivations. Moreover, the translation of programs into Horn clauses, done by tools like Reve9 , results in formulas similar to those generated by our VCGen. Therefore, like our approach, relational verification with constraint solving requires no additional separation hypothesis in presence of aliasing.

Certified Verification Condition Generation. In a broad sense, this work continues previous efforts in formalization and mechanized proof of program language semantics, analyzers and compilers, such as [START_REF] Pierce | Logical Foundations. Software Founda-tions series[END_REF][START_REF] Leroy | Formal verification of a C-like memory model and its uses for verifying program transformations[END_REF][START_REF] Herms | Certification of a Tool Chain for Deductive Program Verification[END_REF][START_REF] Beringer | Abstraction and subsumption in modular verification of C programs[END_REF][START_REF] Jourdan | A formally-verified C static analyzer[END_REF][START_REF] Jung | Iris from the ground up: A modular foundation for higher-order concurrent separation logic[END_REF][START_REF] Wils | Certifying C program correctness with respect to compcert with verifast[END_REF][START_REF] Krebbers | Formal C semantics: CompCert and the C standard[END_REF][START_REF] Blazy | Verified validation of program slicing[END_REF][START_REF] Parthasarathy | Formally validating a practical verification condition generator[END_REF]. Generation of certificates (in Isabelle) for the Boogie verifier is presented in [START_REF] Parthasarathy | Formally validating a practical verification condition generator[END_REF]. The certified deductive verification tool WhyCert [START_REF] Herms | Certification of a Tool Chain for Deductive Program Verification[END_REF] comes with a similar soundness result for its verification condition generator. Its formalization follows an alternative proof approach, based on co-induction, while our proof relies on induction. WhyCert is syntactically closer to the C language and the ACSL specification language [START_REF] Baudin | ACSL: ANSI/ISO C Specification Language[END_REF], while our proof uses a simplified language, but with a richer aliasing model. Furthermore, we provide a formalization and a soundness proof for relational verification, which was not considered in WhyCert or in [START_REF] Parthasarathy | Formally validating a practical verification condition generator[END_REF].

To the best of our knowledge, the present work is the first proposal of relational property verification based on verification condition generation realized for a representative language with procedure calls and aliases with a full mechanized formalization and proof of soundness in Coq.

Conclusion

We have presented in this paper a method for verifying relational properties using a verification condition generator, without relying on code transformations (such as self-composition) or making additional separation hypotheses in case of aliasing. This method has been fully formalized in Coq, and the soundness of recursive Hoare triple verification using a verification condition generator (itself formally proved correct) for a simple language with procedure calls and aliasing has been formally established. Our formalization is well-adapted for proving possible optimizations of a VCGen and for using optimized VCGen versions for relational property verification.

This work sets up a basis for the formalization of modular verification of relational properties using verification condition generation. We plan to extend it with more features such as the possibility to refer to the values of variables before a function call in the postcondition (in order to relate them to the values after the call) and the capacity to rely on relational properties during the proof of other properties. Future work also includes an implementation of this technique inside a tool like RPP [START_REF] Blatter | RPP: automatic proof of relational properties by self-composition[END_REF] in order to integrate it with SMT solvers and to evaluate it on benchmarks. The final objective would be to obtain a system similar to the verification of Hoare triples, namely, having relational procedure contracts, relational assertions, and relational invariants. Currently, for relational properties, product programs [START_REF] Barthe | Relational verification using product programs[END_REF] or other self-composition optimizations [START_REF] Shemer | Property directed self composition[END_REF] are the standard approach to deal with complex loop constructions. We expect that user-provided coupling invariants and loop properties can avoid having to rely on code transformation methods. Moreover, we expect termination and cotermination [START_REF] Hawblitzel | Towards modularly comparing programs using automated theorem provers[END_REF], [START_REF] Unno | Constraint-based relational verification[END_REF] to be used to extend the modularity of relational contracts. refer to x1, x2 and, for sw1, x3 themselves. Indeed, these separation hypotheses 11 are already ensured by the fact that x1, x2 and, for sw1, x3 are allocated during the call to the C function (and the pointers x1 and x2 are valid before the call).

The aforementioned parts of P and Q naturally come from the relational property R sw and the preconditions of the considered functions: in this sense, they are expected. However, they are not sufficient: in a real-life language with possible aliasing like C, to model the behavior of both programs correctly within the composed program and to prove the expected relational property, additional separation hypotheses between the variables coming from both programs C sw1 and C sw2 are required. They are expressed by lines 20-23 in the definition of P in Fig. 9.

Such additional separation hypotheses become even more complex for reallife programs, in particular in C, with a greater number of pointers and/or in the presence of multiple pointers (such as double pointers, for instance, int **p). Indeed, the required separation hypotheses for the composed program rapidly become extremely hard to specify (or to generate) in order to ensure a sound proof of relational properties on the composed program.

With this definition of precondition P and postcondition Q, the code of C sw3 can be proved to satisfy its contract by the deductive verification plugin Wp of Frama-C [START_REF] Kirchner | Frama-C: A software analysis perspective[END_REF]. 11 In L, for simplicity, we consider only global variables, therefore, in the counterparts csw1 and csw2 in language L, these additional separation hypotheses must be explicit (as we show in Ex. 3 and Fig. 6). This slight difference of modeling is intentional in order to show the most natural version of these functions in C with function parameters and local variables rather than with global variables only. We provide a complete list of rules for evaluation of arithmetic and Boolean expressions in L in Fig. 10. Evaluation of arithmetic and Boolean expressions in L is defined by functions ξ a and ξ b . As mentioned above, the subtraction is lower-bounded by 0. Operations * x i and &x i have a semantics similar to the C language, i.e. dereferencing and address-of. Semantics of Boolean expressions is standard [START_REF] Winskel | The formal semantics of programming languages -an introduction[END_REF].

B.2 Operational Semantics of Commands in L in L

We provide a complete operational semantics of commands in L in Fig. 11.

Figure 1 :

 1 Figure 1: Two C programs C sw1 and C sw2 swapping *x1 and *x2, their composition C sw3 , and their counterparts c sw1 and c sw2 in language L (defined below).

|Figure 2 :

 2 Figure 2: Syntax of arithmetic and Boolean expressions and commands in L.

Figure 3 :

 3 Figure 3: Example of an L program c rec with its environments.

Figure 4 :

 4 Figure 4: Evaluation of expressions in L (selected rules).

Figure 5 :

 5 Figure 5: Operational semantics of commands in L (selected rules).

Figure 7 :

 7 Figure 7: Definition of function T c generating the main verification condition.

/

  /C program Csw1 : void sw1 ( int * x1 , int * x2 ) { int x3 ; x3 = * x1 ; * x1 = * x2 ; * x2 = x3 ; } //C program Csw2 : void sw2 ( int * x1 , int * x2 ) { * x1 = * x1 + * x2 ; * x2 = * x1 -* x2 ; * x1 = * x1 -* x2 ; } {P } //Composed C program Csw3 : void sw3 ( int * x1_1 , int * x2_1 int * x1_2 , int * x2_2 ) { //Code simulating Csw1 : int x3_1 ; x3_1 = * x1_1 ; * x1_1 = * x2_1 ; * x2_1 = x3_1 ; //Code simulating Csw2 : * x1_2 = * x1_2 + * x2_2 ; * x2_2 = * x1_2 -* x2_2 ; * x1_2 = * x1_2 -* x2_2 ; } {Q} 1 //P is defined as follows:

2 3 /

 3 /Relation between initial 4 //values of Csw1 and Csw2 : 5 * x1_1 == * x1_2 && 6 * x2_1 == * x2_2 && 7 8 //Preconditions for Csw1 : 9 \valid ( x1_1 ) && 10 \valid ( x2_1 ) && 11 \separated ( x1_1 , x2_1 ) &&

2 3 /Figure 9 :

 39 Figure 9: Two C programs C sw1 and C sw2 swapping *x1 and *x2 and the Hoare triple {P } C sw3 {Q} to prove a relational property between them using their composition in C program C sw3 , as well as definitions of precondition P and postcondition Q of C sw3 .

Figure 10 :Figure 11 :

 1011 Figure 10: Evaluation of arithmetic and Boolean expressions in L.

For convenience of the reader, P and Q are defined in detail in Appendix A.

The Coq development is at https://github.com/lyonel2017/Relational-Spec, where the version corresponding to this paper is tagged iFM2022.

For convenience of the reader, full versions of Fig.4, 5 are given in Appendix B.

https://formal.kastel.kit.edu/projects/improve/reve/

Notice that this separation property is stronger in C than the non-equality constraint x1_1 != x2_1, which does not exclude that both locations have some bytes in common (if the pointers are not aligned). For simplicity, byte-related data representation and alignment constraints are not modeled in L, where the separation can be simply represented by non-equality constraints. This does not restrict the representativity of L for the purpose of our study.

⋆ Part of this work was funded by the AESC project supported by the Ministry of Science, Research and Arts Baden-Württemberg (Ref: 33-7533.-9-10/20/1). 5 Termination can be assumed (partial correctness) or proved separately (full correctness) in a well-known way [15]; for the purpose of this paper we can assume it. //C program Csw1 : x3 = * x1 ; * x1 = * x2 ; * x2 = x3 ; //C program Csw2 : * x1 = * x1 + * x2 ; * x2 = * x1 -* x2 ; * x1 = * x1 -* x2 ; //Composed C program Csw3 : x3_1 = * x1_1 ; * x1_1 = * x2_1 ; * x2_1 = x3_1 ; * x1_2 = * x1_2 + * x2_2 ; * x2_2 = * x1_2 -* x2_2 ; * x1_2 = * x1_2 -* x2_2 ; c sw1 ≜ x 3 := * x 1 ;

Appendix A Detailed Motivating Example

Recall that we consider a relational property R sw :

R sw : both programs, executed from two states in which *x1 has the same value for both programs and *x2 has the same value for both programs, will end up in two states in which each of these locations also has the same value.

To prove the target relational property, a new composed C program C sw3 with a C function sw3 is created (see Fig. 9) by composing the code of both functions. To distinguish variables of different programs, variables coming from C sw1 and C sw1 are marked, resp., with a suffix "_1" or "_2".

In the self-composition based approach, the target relational property for the composed program C sw3 is proved by the Hoare triple {P } C sw3 {Q}, where precondition P and postcondition Q are defined in Fig. 9. The definitions are expressed in the ACSL specification language [START_REF] Baudin | ACSL: ANSI/ISO C Specification Language[END_REF]. Lines 5-6 in the definition of P state that each of *x1 and *x2 has the same value in the states before the execution of sw1 and sw2. Similarly, lines 5-6 in the definition of Q state the same properties after the execution of sw1 and sw2. However, the precondition must also include additional constraints. Lines 9-11 in the definition of P provide usual preconditions for the swap function sw1 to be executed correctly: the input pointers must be valid and separated. For instance, validity of pointer x1_1 means that *x1_1 can be safely read and written. The separation property \separated(x1_1,x2_1) means that the locations *x1_1 and *x2_1 are disjoint, that is, do not share any byte 10 . Lines 14-16 in the definition of P provide similar preconditions for the swap function sw2. For simplicity, we ignore arithmetic overflows in sw2: the specification and verification of properties about the absence of arithmetic overflows are straightforward and orthogonal to the purpose of this paper.

Notice that thanks to the choice of having pointers x1 and x2 as function parameters and variable x3 in C sw1 as a local variable, for this version we do not need to state explicitly other separation hypotheses stating that x1 and x2 do not


Thibault Martin
email: thibault.martin@cea.fr

Nikolai Kosmatov
email: nikolaikosmatov@gmail.com

Virgile Prevosto
email: virgile.prevosto@cea.fr

Verifying Redundant-Check Based Countermeasures: A Case Study

Keywords: Security and privacy → Logic and verification, • Software and its engineering → Formal software verification, Fault injection attacks, software countermeasures, deductive verification, Frama-C verification platform

To thwart fault injection based attacks on critical embedded systems, designers of sensitive software use redundancy based countermeasure schemes. In some of these schemes, critical checks (i.e. conditionals) in the code are duplicated to ensure that an attacker cannot bypass such a check by flipping its result in order to get to a protected point (corresponding e.g. to a successful authentication or code integrity verification). This short paper presents a source-codelevel verification technique of the correct implementation of such countermeasures. It is based on code instrumentation and deductive verification. The proposed technique was implemented in a tool prototype and evaluated on a real-life case study: the bootloader module of a secure USB storage device called WooKey, supposed to be resistant to fault injection attacks. We were able to prove the correctness of almost all redundant-check countermeasures in the module except two, and found an error in one of the unproven ones.

INTRODUCTION

Context. Physical attacks of critical embedded systems (via light pulses, laser shots, clock, voltage or electromagnetic glitches, etc.) consist in causing a fault that alters correct execution of software [START_REF] Barenghi | Fault Injection Attacks on Cryptographic Devices: Theory, Practice, and Countermeasures[END_REF][START_REF] Bhasin | Malicious wave: A survey on actively tampering using electromagnetic glitch[END_REF]. A frequent goal of such attacks is to bypass some critical checks in the code (such as user authentication, software integrity or software authentication checks) in order to get to a protected point that gives access to sensitive information or physical resources.

To counter such attacks, designers of embedded software use in particular redundancy based countermeasure schemes [START_REF] Barenghi | Fault Injection Attacks on Cryptographic Devices: Theory, Practice, and Countermeasures[END_REF][START_REF] Barenghi | Countermeasures against fault attacks on software implemented AES: effectiveness and cost[END_REF]. In some of these schemes, critical checks (i.e. conditional statements, or tests) in the code are duplicated. In this way, if attackers manage to bypass one check by injecting a fault and flipping the result of the check, the redundant check still prevents from reaching the protected point. This countermeasure assumes that it is unlikely to inject two faults by physical attacks during the same execution in a coordinated way. It can be generalized to any number 𝑘 ≥ 1 of coordinated faults: if an attacker is assumed to be able to introduce 𝑘 coordinated faults, each critical check should be repeated 𝑘 + 1 times. For simplicity, in the examples of the paper we use 𝑘 = 1.

Note that, from a strict C standard point of view, these countermeasures are dead code. Hence, as stated for instance in the description of the Common Software Weakness CWE-733 1 and in the last release of the C coding rules [START_REF] Anssi | Règles de programmation pour le développement sécurisé de logiciels en langage C[END_REF] by the National Cybersecurity Agency of France (ANSSI), developers should ensure that optimisations enabled in the compilation toolchain do not eliminate such manually added software countermeasures. This point is beyond the scope of this paper.

Examples. A simple C code with a redundant-check countermeasure is illustrated by Fig. 1. Assuming password is a user-submitted password and secret is the correct password, the duplicated conditional ensures that a bad password will be detected even if one of the conditions is inverted by an attack. Figure 2 shows a more interesting example, with redundant code integrity checks. Such a check is performed by function check_code_integrity. As a protection to bit flipping, this function returns a value of the secbool type, whose values sectrue and secfalse have a maximal bit-distance. The second condition is written in a different way, and is erroneous here: the developer should have used a bitwise negation ~chck2 instead of a logical negation !chck2. If chck2 is secfalse, its logical negation is in fact 0 so that the test on line 8 is always false. Hence, if an attacker manages to flip the result of only the test on line 6, they will execute the protected line 9 even if code integrity check fails. This example illustrates an incorrect countermeasure, due to a misuse of secbool values. Other cases of wrong countermeasures are described below.

Motivation. Due to their redundant behavior, a correct implementation of countermeasures is difficult to verify, yet crucial to ensure resistance to the considered faults. Various approaches are used to assess the efficiency of countermeasures on a given system. Fault injection based techniques-reproducing potential physical attacks on the target device-allow validation engineers to detect (confirmed) vulnerabilities or get confidence that the system is sufficiently resistant to attacks. Such techniques have the advantage to consider the real-life target system, but remain costly and time-consuming, and cannot guarantee that the system will resist to similar attacks in a slightly different setting (e.g. different signal force, frequency, duration or number of attempts). Another approach consists in searching potential attacks at software level, by simulating a chosen set of possible faults in the code and trying to identify potential attacks using test generation [START_REF] Potet | Lazart: A Symbolic Approach for Evaluation the Robustness of Secured Codes against Control Flow Injections[END_REF] or its combination with static analysis [START_REF] Lacombe | Combining Static Analysis and Dynamic Symbolic Execution in a Toolchain to detect Fault Injection Vulnerabilities[END_REF], or to prove their absence using formal verification [START_REF] Christofi | Formal verification of a CRT-RSA implementation against fault attacks[END_REF][START_REF] Heydemann | Formally verified software countermeasures for control-flow integrity of smart card C code[END_REF]. Even if their results are subject to assumptions (about the considered fault model, fault simulation approach, compiler, etc.), software-level approaches provide a useful complement to physical evaluation: they are cheaper, can be fully automatic and can rigorously consider all potential faults with respect to the chosen fault simulation. Such techniques help to find hybrid software/hardware attacks [START_REF] Anssi | Inter-CESTI: Methodological and Technical Feedbacks on Hardware Devices Evaluations[END_REF].

This study continues previous efforts [START_REF] Christofi | Formal verification of a CRT-RSA implementation against fault attacks[END_REF][START_REF] Heydemann | Formally verified software countermeasures for control-flow integrity of smart card C code[END_REF][START_REF] Lacombe | Combining Static Analysis and Dynamic Symbolic Execution in a Toolchain to detect Fault Injection Vulnerabilities[END_REF][START_REF] Potet | Lazart: A Symbolic Approach for Evaluation the Robustness of Secured Codes against Control Flow Injections[END_REF] in this direction. We consider a simple fault model that allows the attacker to invert any subset of at most 𝑘 checks in the code. "Test inversion" is seen as a very useful mode of fault simulation in a recent joint report by the French certification and evaluation authorities [START_REF] Anssi | Inter-CESTI: Methodological and Technical Feedbacks on Hardware Devices Evaluations[END_REF]Sec. 16.4].

Contributions. This short paper presents a source-code-level formal verification technique of correct implementation of redundantcheck based countermeasures. Its purpose is to prove that provoking up to 𝑘 test inversions in the code should not allow an attacker to reach the protected code. It includes two steps: a dedicated code instrumentation simulating possible faults in critical checks ("test inversions") by mutations; and deductive verification of the resulting code trying to formally prove that the countermeasures effectively prevent attacks. The proposed technique was implemented inside LTest 2 [START_REF] Bardin | An All-in-One Toolkit for Automated White-Box Testing[END_REF], an open-source testing toolset, and relies on the Frama-C 3 verification platform [START_REF] Kirchner | Frama-C: A software analysis perspective[END_REF]. We evaluated this technique on a real-life case study: the bootloader module of a secure USB storage device called WooKey 4 , implemented by the ANSSI and 2 https://github.com/ltest-dev/LTest 3 https://frama-c.com 4 https://wookey-project.github.io/target.html supposed to be resistant to fault injection attacks. We were able to formally prove the correctness of all redundant-check countermeasures in the module except two, and found an error in one of the remaining ones. This error remained undetected despite the fact that this module was rigorously analyzed by 10 evaluation centers 5as part of a recent evaluation challenge [START_REF] Anssi | Inter-CESTI: Methodological and Technical Feedbacks on Hardware Devices Evaluations[END_REF]. It confirms the interest of the proposed dedicated approach.

VERIFICATION APPROACH

Overview. Our verification approach proceeds as follows. The user indicates the beginning and the end of the critical sections of the code, inside which all tests should resist to fault injection attacks. This is done to focus only on the critical steps (containing authentication, integrity checks, version control, etc.) since other parts of the code (e.g. following the authentication) are typically less critical and do not integrate countermeasures. The end of the indicated code segment corresponds to the protected point that gives access e.g. to sensitive resources or information. In a critical code segment, all checks are instrumented to simulate faults introduced by an attacker according to the considered fault model: an attacker can invert up to 𝑘 tests. The target property is expressed as an annotation in the Acsl6 specification language and states that no attack can reach the protected point. Then, a deductive verification tool is run on the instrumented code to try to formally verify this annotation. Figure 3b presents the instrumentation scheme for a critical part of code, given in Fig. 3a, with 𝑁 tests. We will now detail its main components.

Fault Simulation. To simulate a possible fault injection, we introduce a specific function, called mutated, for which we provide only an Acsl specification, as shown in Fig. 4. The implementation of this function is not required for our technique based on deductive verification. We can simulate at most 𝑘 faults (for any given 𝑘 ≥ 1) by changing the MAX_MUTATION macro definition to 𝑘 (here, we set 𝑘 = 1). The specification on lines 3-13 guarantees that mutated will return true (i.e. nonzero) at most MAX_MUTATION times during an execution. The order in which the true and false values are returned is left unspecified: it can be arbitrary. To count how many times the function has returned true so far, we introduce a new variable cpt_mut. Line 4 specifies that mutated only modifies cpt_mut, so it does not interfere with the application code. Then, two cases are considered (lines 5 and 9). If the maximal number of mutations has been hit (line 6), the function returns false, i.e. does not trigger a mutation, and the counter is unchanged (lines 7-8). If the maximal number of mutations is not reached (line 10), then the function either returns true and increments the counter (i.e. triggers a mutation), or returns false and leaves the counter unchanged (lines [START_REF] Laurent | Analyzing Software Security Against Complex Fault Models with Frama-C Value Analysis[END_REF][START_REF] Potet | Lazart: A Symbolic Approach for Evaluation the Robustness of Secured Codes against Control Flow Injections[END_REF].

As shown in Fig. 3b (e.g. line 1), for each test of a condition 𝐶 𝑖 , a call to mutated is added and its result is stored in a variable mut_i, that we call a mutation trigger. The role of mutation trigger mut_i is to indicate if a test inversion should be performed on the condition 𝐶 𝑖 .

Then the value of 𝐶 𝑖 is combined with the mutation trigger in order to trigger a test inversion, i.e. to take the opposite branch, if mutated returned true (e.g. line 2). Such instrumentation can be compared, albeit at a slightly higher level of abstraction, to the one done by Lazart [START_REF] Potet | Lazart: A Symbolic Approach for Evaluation the Robustness of Secured Codes against Control Flow Injections[END_REF] over LLVM bitcode or by [START_REF] Laurent | Analyzing Software Security Against Complex Fault Models with Frama-C Value Analysis[END_REF] over a translation of assembly code at C level.

Verified Properties. At the end of the critical code segment (line 8 in Fig. 3b), we insert check annotation, which states that all mutation triggers are false at the protected point. If this check is proved, we can conclude that the protected code section can never be reached through up to 𝑘 test inversions, or in other words, that redundantcheck countermeasures are correctly implemented. Indeed, if there is an attack path with a nonzero number of faults, i.e. on which some mutation triggers are true, this annotation cannot be proved in general. To try to prove this annotation, we rely on the Wp plugin of Frama-C [START_REF] Kirchner | Frama-C: A software analysis perspective[END_REF], that is based on deductive verification.

One Difficulty: Function Calls and Loops. In the presence of function calls and loops, deductive verification tools like Wp usually rely on manually written specifications. In our approach, having to provide them would come against our goal to make the verification process as automated as possible. For instance, to deal with the example of Fig. 2, the user would need to provide a complete specification of function check_code_integrity. To avoid these pitfalls, we propose to inline the called functions and unroll the loops so that the deductive verification tool can reason about the code without additional annotations. This solution has limitations: it will not work, for example, if the maximal number of loop iterations is very large or cannot be bounded. In practice, in critical code segments, loops with unbounded number of iterations are not so common, and it is often possible to determine the maximal number of loop iterations (a password is read at most three times, the secret code to check or the payload to copy is of a fixed ou bounded finite length, etc.). In our case study, this solution indeed allowed avoiding additional specifications, except in one case (see below).

EXPERIMENTS

The approach described above has been implemented in LTest [START_REF] Bardin | An All-in-One Toolkit for Automated White-Box Testing[END_REF], a set of tools for coverage-oriented testing, mostly written in OCaml as plugins of Frama-C [START_REF] Kirchner | Frama-C: A software analysis perspective[END_REF], a program analysis platform for C code. One of the plugins, LAnnotate, creates test objectives for given criteria. We implemented our technique as a new criterion, Redundant Check Countermeasures (RCC), which instruments countermeasures using annotations provided by the user. The instrumented code can then be given to another plugin, LUncov, which tries to prove, using Wp, that the target point cannot be reached by 𝑁 test inversions. We evaluated our tool on the 11 critical sections with redundantcheck based countermeasures in the bootloader of WooKey7 . Parts of code that are not protected by countermeasures were not considered. The table in Fig. 5 gives an overview of our experiments on all redundant check countermeasures in WooKey. For each critical section protected by redundant-check based countermeasures, the first columns provide the location of the section, whether it contains loops or function calls, the number of resulting objectives (that is, assertions to prove). When different, we also give the number of objectives after loop unfolding and function inlining. This number increases for the first section since the assertion is located inside the body of the unrolled loop. (In other cases, the number of assertions does not change despite using loop unrolling or function inlining.) The last two columns show the result of the proof (on the initial code) and our manual analysis of this result.

We were able to prove the efficiency of 9 of them, in around 2 minutes. One unproven section is correct but too hard to prove using Wp without adding function contracts and loop invariants: it has three function calls involving loops and bitwise operations, so that complete unrolling and inlining generates complex verification

1 if 3 /Figure 1 : 6 if 9 // Protected : Successful code integrity check 10 }Figure 2 :

 13169102 Figure 1: Password check with a countermeasure.

2 if 3 { 6 if 7 { codeN ;} 8 /Figure 3 : 1 # 2 unsigned 7 ensures ! \result ; 8 ensures

 2367831278 Figure 3: (a) A code example, and (b) its automatic annotation by mutations for fault simulation.

Figure 4 :

 4 Figure 4: Uninterpreted function mutated and its contract.

https://cwe.mitre.org/data/definitions/733.html

ITSEFs (Information Technology Security Evaluation Facility), or CESTIs in French

https://github.com/acsl-language/acsl/releases/latest

The tools were applied on the version of commit 00fd1c6 available on https://github. com/wookey-project/bootloader/.

Acknowledgements. This work was partially supported by ANR project SATOCROSS (grant ANR-18-CE25-0015-01). The authors thank the anonymous reviewers for their valuable comments. The authors are grateful to ANSSI researchers for presenting WooKey and useful discussions.

The second unproven section is shown in Fig. 6. The code sets the bootloader state to LOADER_ERROR and exits if the value of new_state is erroneous. The countermeasure is created by taking the conjunction of the original condition and its equivalent reformulation (see line 2). Using our method, we were not able to prove this countermeasure to be effective. In this case, it is indeed erroneous: the doubled condition on line 2 does the opposite of its purpose. Instead of protecting the critical code section, it allows a single mutation to bypass the check. Figure 7 gives correct patterns for doubled conditions (where the occurrences of condition 𝐶 1 can be equivalent but not necessarily the same, notably to avoid side-channel indications of redundant-check locations). The error here comes from the use of the logical operator AND (&&) instead of OR (||), unlike in Fig. 7b. This type of countermeasure, using a logical connector instead of successive if statements, occurs a few times in the WooKey bootloader, but this is the only case where the protected code is outside the condition block. In all other cases, the error is caught after, like in Fig. 7a.

This example shows that it is very easy to make an error in countermeasures that is not easy to find, as the code still works. It confirms the need for dedicated tools for verifying the countermeasures. After correcting the detected error, we proved a correct implementation of this redundant-check based countermeasure as well. Thus, our tool was able to automatically prove ∼90% of critical sections in the target module without adding contracts.

CONCLUSION

We have proposed in this paper a method for formally verifying at source-code level that countermeasures against test inversion attacks are correctly implemented and shown that it can be successfully used on real C code thanks to Frama-C/LTest. We believe that providing a suitable implementation for the mutated function will make our instrumentation suitable also for finding faults using a test generation based approach (like Lazart [START_REF] Potet | Lazart: A Symbolic Approach for Evaluation the Robustness of Secured Codes against Control Flow Injections[END_REF]). If so, it will allow the engineer to use the same instrumentation both to formally prove the correct implementation of countermeasures and to generate test cases illustrating attacks. This extension is part of future work. Future work also includes considering other fault models, notably allowing the attacker to flip the value of any variable (up to 𝑘 times) during the execution, automating the approach of [START_REF] Christofi | Formal verification of a CRT-RSA implementation against fault attacks[END_REF] thanks to the use of LAnnotate.


Said Choukri
email: said.choukri@univ-eiffel.fr

Hakim Takhedmit

Otman El Mrabet

Mariem Aznabet

Laurent Cirio

Wide Angle, Polarization Independent Metamaterial Absorber Unit-Cell for RCS Reduction and Energy Harvesting Applications

Keywords: Metamaterials, Metamaterials Perfect Absorbers, Energy Harvesting, Monostatic RCS, Polarizations

In this paper, a new design of Metamaterial Absorber unit-cell is presented with a high absorption coefficient of 99.78% at 10 GHz. The numerical results show that the proposed unit-cell has constant performances regardless the polarization state of the incoming waves, a wide angle of absorption up to 70 • for TE polarized waves, and 80 • for TM, RHCP, LHCP polarized waves is achieved. Analytical circuit model has been developed to describe the matching process between the unit-cell and free space impedances. The monostatic RCS capability of 12 × 12 metasurface array has been proved numerically by full wave simulation showing more than 10 dB RCS reduction at normal and oblique incidences. Finally a metasurface array was fabricated and tested experimentally, the simulated and measured results are in good agreement in terms of absorption rate and bandwidth, expect a frequency shift in terms of resonance frequency.

Introduction

Electromagnetic absorbing materials, or Radar Absorbing Materials (RAM), were created both in the USA and in Germany during the Second World War [START_REF] Saville | Review of Radar Absorbing Materials[END_REF]. An ideal absorber looks like an effective paint or coating for all polarizations over a wide frequency band and a wide range of incidences. Such material does not exist in reality and it seems difficult to have a prototype that perfectly meets this definition. The applications of absorbers mainly come from the field of Electromagnetic Compatibility (EMC) and Radar discretization [START_REF] Zhukov | The application of radar absorbing materials to reduce interference emissions from instruments and devices of spacecraft electrical systems[END_REF].

In 2002, N. Engheta showed in a theoretical article [START_REF] Engheta | Thin absorbing screens using metamaterial surfaces[END_REF] that if a surface with metamaterials is placed near a perfectly conductive foil, in a certain frequency band, this structure can behaves like a flat plate with a high impedance on its upper part. Thus, if a resistive sheet is placed on this plate of high impedance, it is possible to obtain a thin structure equivalent to an electromagnetic wave absorber which has reduced dimensions. Several types of electromagnetic wave absorbers have been proposed in the literature, in particular: Dielectric absorbers [START_REF] Capaccioli | Dielectric response analysis of a conducting polymer dominated by the hopping charge transport[END_REF], Structural absorbers with impedance matching [START_REF] Fallahi | Modeling Pyramidal Absorbers Using the Fourier Modal Method and the Mode Matching Technique[END_REF], Resonant absorbers [START_REF] Naishadham | Measurement of the microwave conductivity of a polymeric material with potential applications in absorbers and shielding[END_REF], Magnetic absorbers [START_REF] Sugimoto | M-type ferrite composite as a microwave absorber with wide bandwidth in the GHz range[END_REF] and Metamaterial absorbers [START_REF] Landy | Perfect metamaterial absorber[END_REF]. In [START_REF] Landy | Perfect metamaterial absorber[END_REF], the first Printed Circuit Board (PCB) topology of a Metamaterial Perfect Absorber (MPA) unit-cell at microwave frequencies has been introduced. This thin structure, with the thickness of λ 0 /35, has been optimized to achieve an intrinsic impedance close to free space characteristic impedance, hence a near unity absorption rate. This kind of MPA are being utilized for several applications ranging from microwaves to optics and photonics, such as RCS reduction [START_REF] El | Broadband RCS Reduction by a Quaternionic Metasurface[END_REF], energy harvesting [START_REF] Dinh | Dual-Polarized Wide-Angle Energy Harvester for Self-Powered IoT Devices[END_REF]- [START_REF] Choukri | Energy Harvesting using loaded Metamaterial Absorber Unit-Cell with polarization independent Capability[END_REF], Radio Frequency Identification (RFID) systems [START_REF] Okano | Development of Optically Transparent Ultrathin Microwave Absorber for Ultrahigh-Frequency RF Identification System[END_REF], sensing [START_REF] Hakim | Polarization insensitive symmetrical structured double negative (DNG) metamaterial absorber for Ku-band sensing applications[END_REF], mutual coupling reduction in antenna arrays [START_REF] Zhang | Mutual Coupling Reduction of a Circularly Polarized Four-Element Antenna Array Using Metamaterial Absorber for Unmanned Vehicles[END_REF] and so on. Although the functionality of MPA for various applications, harvesting electromagnetic energy and RCS reduction are the best suitable applications with MPA's operating principle, since they capture efficiently the up-coming electromagnetic waves on their front side, then the energy transported may either dissipated or collected depending on the desired application. For RCS reduction by using MPA, the incoming energy will be dissipated inside the unit-cell, since there will be no reflection neither transmission occurs due to the matching process between the unit-cell and the free space impedance, hence the backscattered energy is weaker and the target will be undetectable for certain angle of incidence and certain frequencies. So, in this case a substrate with high loss tangent is highly recommended in the design of the unit-cell. On the other hand, if we aim to use the MPA for energy harvesting purposes, we will have to use a substrate material with low loss tangent and high permittivity in the design of the MPA unit-cell, this will allow us to maximize absorption rate of incident waves and reduce energy dissipation in the cell. Using metamaterial absorbers for energy harvesting and RCS reduction has been explored much during last decade with much appreciable performances notably in terms of high absorption coefficient, wide range of incidence angle, polarization diversity and bandwidth. In [START_REF] Dinh | Dual-Polarized Wide-Angle Energy Harvester for Self-Powered IoT Devices[END_REF] M. Dinh proposed a dual-polarized metamaterial absorber cell with double integrated rectifying circuits, the cell operates at 3.75 GHz and shows a high RF-AC efficiency of 94% that preserved under a wide incident angle Figure 1: Unit-cell geometry 3D-Design up to 65 • in TE mode and 75 • in TM mode. In [START_REF] Li | Compact Dual-Band, Wide-Angle, Polarization-Angle -Independent Rectifying Metasurface for Ambient Energy Harvesting and Wireless Power Transfer[END_REF] Long Li el al. present a Dual-Band rectifying metasurface with wide range of incidence up to 60 • and with considerable conversion efficiency at the operating frequencies. In this paper, a new design of metamaterial absorber unitcell is proposed, the unit-cell performs as a perfect absorber with near unity absorption within the frequency bandwidth, which could be a good condidate to harvest surronding electromagnetic waves with different polarizations.

The proposed MPA Unit-cell Design

Figure 1 illustrates the proposed design of the metamaterial perfect absorcber structure. The proposed unit-cell consists of two simple concentric metallic rings etched in the center of a square shaped FR-4 substrate with a dielectric constante (ε r ) 4.3 and loss tangent (tan δ) 0.025 . Four gaps have been incorporated with the two concentric rings to improve the absorption bandwidth, four strips have also been merged with the two rings in order to make the cell rotationally symmetrical around its z axis, due to this symmetry purpose the cell will be able to capture efficientlly diffrent polarized up-coming waves either circularly or linearly polarized ones. The structure is backed by a full coppered reflective ground plane with the thichness of 35 µm. The geometrical parameters of the unit-cell are listed in table 1. Also shown in figure 1, the external excitation consiste of two incident plane waves propagating from top to bottom with electric feld polarized linearly in the y and x directions respectively for TE and TM modes. P 1 and P 2 are the propagation vectors for TE and TM polarized waves respectively.

Numerical Studies

Unit-Cell electromagnetic simulation

The unit-cell was simulated using commercial Computer Simulation Technology (CST) MWS software. The structure was placed in the center of a rectangular square aper-

S 21 (ω) = S xx 21 (ω) + S xy 21 (ω) (1)
In equations ( 1) and ( 2), the co-and cross-polarized components are denoted by "xx" and "xy", respectively. This configuration holds for an incident electric field polarized in the x direction (TM mode), for the second configuration where the incident electric field vector is polarized in the y direction (TE mode) the co-and cross-polarized components are denoted by "yy" and "yx", respectively. Since the unit-cell presents a low cross-polarization (S xy 11 ≈ 0) and (S xy 21 ≈ 0), the absorption coefficient can be formulated as follows :

A(ω, θ, ϕ) = 1 -|S 11 (ω, θ, ϕ)| 2 -|S 21 (ω, θ, ϕ)| 2 (3)
Since the unit-cell is backed by a full reflective metallic sheet which has the copper thickness of 35 µm, this value remains greater than the skin depth of copper over all the Frequency (GHz) [START_REF] Landy | Perfect metamaterial absorber[END_REF] 8 frequency range, so this metallic plane will efficiently prevent incident wave propagation in the other side, resulting zero transmission S 21 = 0 and equation ( 3) can be reduced to the following form :

A(ω, θ, ϕ) = 1 -|S 11 (ω, θ, ϕ)| 2 (4)
From euqation (4), it is clearly shown that the absorption coefficient depends on the incidence angle (θ) which also known as Elevation and on the Azimuthal angle ϕ. Figure 2 sketches the variation of the absorption coefficient computed by using equation ( 4) under normal incidence (θ = 0 • and ϕ = 0 • ). The unit-cell has been excited with differents polarization states of the incident electric field including linear polarizations TE and TM, as well as circular polarizations RH and LH. We can observe from figure 2 that the response of the unit-cell is very less sensitive to the polarization of the incident waves which proves that the unit-cell can capture and absorbe efficiently all incident waves. Moreover, this feature has an advantage for applications that aim to harvest surronding electromagnetic energy or Radar applications in which the target must not to be detectable by Radar screens. In addition, an absorption bandwidth of 530 MHz is achieved with an absorption rate above 70%. Figure 3 shows the unit-cell constitutive parameters in real and imaginary parts as a function of frequency in the X-band. The relative permittivity, relative permeability and refractive index are computed using NRW modified reflection only algorithm (RO) and the three parameters are given by following equations :

ε r (ω) = 1 + χ e (ω) = 1 + 2j k 0 (ω)h 1 -S 11 (ω) 1 + S 11 (ω) (5)
µ r (ω) = 1 + χ m (ω) = 1 + 2j k 0 (ω)h 1 + S 11 (ω) 1 -S 11 (ω) (6)
n(ω) = ε r (ω)µ r (ω) (7)
Where χ e and χ m are respectively the complex electric and magnetic susceptibilities, ω is the angular frequency, k 0 is the free-space wavenumber and h is thickness of the substrate. To achieve the minimum reflection from the absorber unit-cell, the normalized effective impedance (with respect to the free space impedance Z 0 = 377 Ω) z ef f = µ r (ω)/ε r (ω) needs to be matched with the free space impedance, so that z ef f ≈ 1 at the resonance frequency. From figures 3(a) and 3(b) at 10.04 GHz, z ef f ≈ 0.96 -j0.1 which still acceptable for ensuring good matching. The refcative index can be also formulated by n(ω) = n + jn , n is the refractive index whereas n is the extinction index, this later compute the losses in the medium. Moreover from figure 3(c), we can see that within the operating frequency band the real part of n is near to zero while the imaginary part has higher values due to the use of FR4 substrte having high loss tangent.

Equivalent Circuit Model Approach

In order to give a comprehensive understanding of the impedance matching process between the MPA unit-cell and the free space, we propose an analytical circuit model which is based on circuit theory and transmission line theory. The unit-cell with its three parts (Reflective metallic sheet, Substrate and the resonator) is described by the equivalent circuit shown in figure 4, whose parameters have been rigorously calculated and optimized. Moreover, the metal plane which plays the role of a reflector is modeled by its complex impedance based on the approximation of good conductor, this impedance is given by [START_REF] David | Microwave Engineering[END_REF]: Where ω is the angular frequency, µ is the permeability, σ is the copper conductivity and δ m is the skin depth of the metal. Then, based on tansmission lines theory, the substrate is modeled by a transmission line of length h terminated by a short circuit to take into account the ground connection. The input impedance seen looking into the line is deduced by an equivalence between fields theory and circuit theory and it is given by the following equation :

Z m = (1 + j) ωµ 2σ = (1 + j) 1 σδ m (ω) (9)
Z in (ω) = A 1 (ω) 1 -ω 2 LC -A 2 (ω)Cω + j 1 -LCω 2 + A 1 (ω)Cω A 3 (ω) (1 -LCω 2 -RCω) + A 1 (ω) -RCωA 2 (ω) + j [2A 2 (ω) -LCA 2 (ω)ω 2 ] (8) A 1 (ω) = - Z c σδ m (ω) tan (β s (ω)h) A 2 (ω) = Z c tan (β s (ω)h) A 3 (ω) = 1 δ m (ω)
Z s (ω) = j µ rs µ 0 ε rs ε 0 tan (β s h) = jZ c tan (β s (ω)h) (10)
Where β s = β 0 / √ ε r µ r is propagation constant in the substrate, ε rs and µ rs are the constitutive parameters of the substrate material while Z c its characteristic impedance. The etched metallic resonator on the top side of the substrate, which is the fundamental element that controls the cell's resonance, is modeled by a series RLC resonant tank which has the following impedance :

Z r (ω) = R + jLω + 1 jCω (11)
Since, the equivalent impedance seen looking into the input port of the circuit is calculated by equation [START_REF] Landy | Perfect metamaterial absorber[END_REF]. the three unknowns circuit parameters R, L and C are calculated by solving the following equation :

Z in (ω)| ω=ωr = Z 0 ( 12
)
Where ω r = 2πf r is the resonance frequency. After solving equation [START_REF] Okano | Development of Optically Transparent Ultrathin Microwave Absorber for Ultrahigh-Frequency RF Identification System[END_REF], the values of R, L and C are found to be respectively R = 601.62 mΩ, L = 2.54 pH and C = 1.06 pF . Figure 5 shows the frequency response of the circuit model compared to electromagnetic simulation In this section, we study numerically the effects of changing the incident and azimuthal angles of the incident electromagnetic waves on the unit-cell performances. MPA structures normally exhibit high absorption rate in normal incidence, but when increasing the incident angle θ the absorption values decrease automatically due to the nonlinearity between the reflection coefficient and the incident angle, which is given by equations ( 13) and ( 14) for TE and TM modes, respectively :

Γ T E (θ) = cos (θ) -n 2 -sin 2 (θ) cos (θ) + n 2 -sin 2 (θ) (13)
Γ T M (θ) = -n 2 cos (θ) -n 2 -sin 2 (θ) n 2 cos (θ) + n 2 -sin 2 (θ) ( 14
)
Where n is the refractive index of the MPA structure and θ is the incident angle. Since the challenge in designing MPA structures is to achieve a high absorption coefficient for large incident angles. Figure 6 depicts the absorption spectra of the unit-cell in which the variation of absorption coefficient is reported as a function of the incident and azimuthal angles. Note that when sweeping theta or phi angle the other angle is fixed at 0 • . From figure 6(a) for TE mode, we note that the unit-cell shows a less sensitive response to the variation of the angle θ, and the performance is still surprisingly quasi-uniform up-to 70 • , which we denote by θ max . As the angle is varied away from this So, all the electromagnetic waves arriving with an angle of incidence whose value is included within the aperture angle θ max of the absorber cone will be captured efficiently by the unit-cell with the minimum reflection as explained in figure 7. This structure has been designed to be rotationally symetrical around its z axis, this fact is clearly observed in figures 6(e), 6(f), 6(g) and 6(h) where the response is insensitive to the variation of ϕ, respectively for TE,TM, RHCP and LHCP polarizations and the unit-cell exhibits a constant absorption coefficient.

Metasurface RCS Reduction Capability

In this section, a demonstration of the metasurface RCS reduction capability is given with respect to the incidence angle at the maximum absorbance frequency point. The metasurface is built by arranging 12 × 12 unit-cell in two dimensions. At normal incidence, the RCS reduction by a metasurface consisting with M × N unit-cells is expressed as [START_REF] El | Broadband RCS Reduction by a Quaternionic Metasurface[END_REF] :

RCSR normal = 20 log M m=1 N n=1 E mn e ik0βmn (15)
Where E mn and β mn are respectively the amplitude and phase of the reflected electric field of the cell in row m and colum n of the metasurface, and k is the wavenumber of the incident wave in free-space. By using equation 8, we can easily obtain the RCS reduction trough substituting

RCSR oblique = 20 log E (θ, ϕ) E i (16)
Where E i is the magnitude of the incident electric field vector, and E (θ, ϕ) is the reflected back electric field by the whole metasurface array cells which can be expressed by :

E (θ, ϕ) = M m=1 N n=1
E mn e ik0[(m-1)dx cos ϕ+(n-1)dy sin ϕ] sin θ (17) The monostatic RCS of the metasurface has been computed numericaly using HFSS, where excitation with plane waves in spherical coordinates was used to illuminate the metasurface array at the frequency of interest (10 GHz). In order to test the RCS reduction for different values of the incidence angle, we sweeped the angle θ from -180 • to +180 • while the angle ϕ was fxed at 0 • . Then the same simulation setup has been performed to compute the monostatic RCS of equal-sized PEC sheet to the metasurface and results are shown in figure 8. We can see clearly that the metasurface contributes to reduce the monostatic RCS in

Experimental results

In order to evaluate the performances of the metamaterial absorber unit-cell and verify its performances, we fabricated a square prototype of 144 unit-cells. Figure 9 shows the fabricated sample on FR4 epoxy substrate with total dimensions of 15.3 × 15.3 × 0.08 cm 3 . Figure 10 describes the measurement setup used to evaluate the absorption coefficient in the free-space. Accordingly, two X-Band horn antennas were used to transmit electromagnetic waves and receive the reflected signal from the metasurface, an Agilent Power Network Analyser (PNA) is used to excite the transmitter and measure the S-parameters of the sample. The far-fleld distance was fixed at 0.92 m. The measurement setting can be summarized as follow : first the reflection coefficient from a conductive plat, which has the same dimensions of the sample, was extracted through the measured scattering parameter (S 21 ), then the metalic plat was replaced by the metasurface absorber which its reflection coefficient was extracted also through measured transmission coefficient (S 21 ). The final reflection coefficient of the metasurface was calculated through the substraction of the two measured reflection coefficients. Finally, The ab- The measured results are in good agreement with numerical results in terms of the absorption rate and the absorption bandwidth, except that a frequency shift was observed between the two results. This discrepancy is probably the manufacturing and the measurement setup imperfections.

conclusion

In this work, a metamaterial absorber unit-cell has been designed and simulated numericaly and the obtained results showed that the absorption is above 70% within the frequency bandwidth of 560 MHz, the unit-cell has the capability to absorb elecctromagnetic waves with different polarizations. A circuit model has been developed providing physical insights into the matching process with the freespace characteristic impedance to achieve full absorption. The monostatic RCS reduction of the metasurface array has been proved with 10 dB and more reduction at normal and oblique incidences. The absorption coefficient of a (12×12) metasurface array was calculated experimentally under normal incidence which has a near unit absorption rate at 10.45 GHz.

FrequencyFigure 2 :

 2 Figure 2: Absorption coefficient versus the frequency for different polarizations of the incident waves : TE, TM, RHCP and LHCP

Figure 3 :

 3 Figure 3: Metamaterial unit-cell constitutive parameters.

Figure 4 :

 4 Figure 4: Equivalent circuit model of the unit-cell

FrequencyFigure 5 :

 5 Figure 5: Unit-Cell reflection coefficient : EM Simulation versus circuit model responses

  (a) TE(θ, ϕ = 0 • ). (b) TM(θ, ϕ = 0 • ). (c) RHCP(θ, ϕ = 0 • ). (d) LHCP(θ, ϕ = 0 • ). (e) TE(θ = 0 • , ϕ). (f) TM(θ = 0 • , ϕ).

  (g) RHCP(θ = 0 • , ϕ).(h) LHCP(θ = 0 • , ϕ).

Figure 6 :

 6 Figure 6: Absorption Spectra of the unit-cell for different polarizations : Elevation angle θ test : (a)-Mode TE,(b)-Mode TM,(c)-RHCP and (d)-LHCP. Azhimutal angle ϕ test (e)-Mode TE, (f)-Mode TM, (g)-RHCP and (h)-LHCP.

Figure 7 :Figure 8 :

 78 Figure 7: Unit-cell maximum width angle

Figure 9 :

 9 Figure 9: Fabricated metasurface array (12 × 12) cells

Figure 11 :

 11 Figure 11: Simulated and measured absorption coefficient at normal incidence

Table 1 :

 1 Summary of Unit-Cell geometry.

		Parameter size [mm]
		R	6
		c	0.6
		d	0.4
		m	4.4
		y	2
		g	1.4
		h	0.8
		L	13
	8.4	9	9.6 10.2 10.8 11.4 12

Acknowledgement

This work was carried out within the framework of TOUBKAL PROJECT : TBK/20/100 Campus N • 43761TJ under the Franco-Moroccan cooperation between CNRST and Campus France. Authors would like to thank Stephane PROTAT for his technical support in the prototypes fabrication and measurements.