Arnaud De Grandmaison

Karine Heydemann

Quentin L Meunier

ARMISTICE: Micro-Architectural Leakage Modelling for Masked Software Formal Verification

Keywords: Side Channel Attacks, Masking, Verification, Micro-architectural Leakage Key[12] ^ Key[15] (ex0) Key[12] ^ Key[14] (ex1) Key[14] ^ Key[15] (ex2) SBox[Key[12]] (ex3) SBox[Key[14]] (ex4) SBox[Key[15]] (ex5) SBox[Key[12]] ^ SBox[Key[15]] (ex6) SBox[Key[14]] ^ SBox[Key[15]]

Side channel attacks are powerful attacks for retrieving secret data by exploiting physical measurements such as power consumption or electromagnetic emissions. Masking is a popular countermeasure as it can be proven secure against an attacker model. In practice, software masked implementations suffer from a security reduction due to a mismatch between the considered leakage sources in the security proof and the real ones, which depend on the micro-architecture. We propose ARMISTICE, a framework for formally verifying the absence of leakage in first-order masked implementations taking into account modelled micro-architectural sources of leakage. As a proof of concept, we present the modelling of an Arm Cortex-M3 core from its RTL description and leakage test vectors, as well as the modelling of the memory of a STM32F1 board, exclusively using leakage test vectors. We show that, with these models, ARMISTICE pinpoints vulnerable instructions in real world masked implementations and helps the design of masked software implementations which are practically secure.

I. INTRODUCTION

Side Channel Attacks (SCA) exploit physical measurements, like power consumption or electromagnetic (EM) emissions, during the execution of an application to recover secret data. They constitute a powerful class of attacks, allowing to break software and hardware implementations of cryptographic algorithms otherwise proven secure at the algorithmic level.

Introduced in the early 2000s [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF], masking countermeasures at order d aim at encoding a secret data into d + 1 parts called shares, such that any combination of less than d + 1 shares is statistically independent from the secret. This theoretically prevents SCA, as the power consumption and EM emissions are directly linked to the values manipulated by the program. A masking countermeasure can be proven secure against an attacker model, e.g. an attacker able to probe t measurements per execution, which leads to the notion of t-probing security (or probing security at order t) [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF], [START_REF] Barthe | maskverif: Automated verification of higher-order masking in presence of physical defaults[END_REF]. Proofs are conducted at a given abstraction level, most often at algorithmic or source code level, and are based on a given leakage model. The latter is typically either the value-based leakage model, in which the leakages are the values of intermediate computations; or the transition-based leakage model, in which the leakages are combinations between two consecutive values in some A. de Grandmaison was with ARM, Paris, France (email: arnaud.degrandmaison@arm.com) K. Heydemann and Quentin L. Meunier were with Sorbonne University, CNRS, LIP6, FR-75005 France (emails: karine.heydemann@lip6.fr, quentin.meunier@lip6.fr) elements, such as variables at algorithmic level or registers at assembly level.

Implementing a masking scheme at software level without unmasking secrets and detecting such unmasking by hand are far from trivial tasks. Consequently, some verification techniques and tools have been recently proposed to help designers detect flaws in their implementations [START_REF] Barthe | maskverif: Automated verification of higher-order masking in presence of physical defaults[END_REF]- [START_REF] Pengfei | Formal verification of masking countermeasures for arithmetic programs[END_REF]. We argue that verification should be carried out on the compiled code for two main reasons. To start with, compilers perform code transformations, from simplifications of the expressions to the reordering or removal of some instructions, possibly harming or deconstructing the carefully added masking scheme along the way. Then, proofs require the knowledge of the sources of leakage, and are then limited to what is visible at the chosen abstraction level. The lowering of the source code into assembly code introduces data transfers between memory and CPU registers manipulated by instructions, and the leakage relative to successive writes into the same architectural register and consecutive memory accesses are most often not related to the same source-level variable. Some recent work propose some compilation approaches for removing such issues [START_REF] Wang | Mitigating power side channels during compilation[END_REF], [START_REF] Seuschek | Side-channel leakage aware instruction scheduling[END_REF]. There also exist some tools for verifying masked assembly code [START_REF] El Ouahma | Sidechannel robustness analysis of masked assembly codes using a symbolic approach[END_REF], [START_REF] Meunier | SELA: a Symbolic Expression Leakage Analyzer[END_REF]. However, analysis at the ISA level is still not sufficient: masked software implementations suffer from a security reduction due to the mismatch between the considered sources of leakage and the real ones, which depend on the target micro-architecture and may not be visible at the ISA level [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF], [START_REF] Papagiannopoulos | Mind the gap: Towards secure 1st-order masking in software[END_REF]. For example, some remnant effects may appear, or some internal resources, like pipeline registers or buses, can lead to unmasking.

Yet higher-order masking is supposed to be effective against more powerful attackers, with a major impact on performances and code size. However, using it in an attempt to shield from the architecture implementation details is not a solution [START_REF] Moos | On the easiness of turning higher-order leakages into first-order[END_REF]. A promising approach is to take into account leakage at processor design time [START_REF] Slpsk | Karna: A gatesizing based security aware eda flow for improved power side-channel attack protection[END_REF], [START_REF] Balasch | Towards efficient and automated side-channel evaluations at design time[END_REF], but no such leakage-free architecture is available yet. Accurate modelling of leakage sources for an actionable verification of masked software running on generic off-the-shelf processors is still an open research question.

An actionable verification needs to be conducted with much more details in the processor micro-architecture, in order to accurately detect all possible data combinations in a processor implementation and pinpoint to the precise location and root cause of a leakage. Existing approaches [START_REF] Le Corre | Micro-architectural power simulator for leakage assessment of cryptographic software on arm cortex-m3 processors[END_REF]- [START_REF] Barthe | Masking in fine-grained leakage models: Construction, implementation and verification[END_REF] all have limitations regarding the considered sources of leakage. In this article, we propose the ARMISTICE framework to fill the gap between formal verification approaches and real sources of leakage. From an application running on a processor model, ARMISTICE extracts all intermediate values computations as symbolic masked expressions and formally verifies the absence of leakage in them. As proof of concept, we build a model of the Cortex-M3, by studying the RTL available through the Arm Academic Access1 (AAA) program. The white-box modelling enabled by analysing the micro-architecture RTL description is experimentally verified with specifically designed leakage test vectors, to both confirm the model correctness and rank the leakage sources according to their impacts. Some areas of the model, related to the memory subsystem, require a blackbox approach only based on dedicated leakage test vectors. We show that ARMISTICE is able to recover where and what leaks on two different masked AES implementations as well as on 5 other benchmarks. We also show experimentally on two of these masked implementations the accuracy of the found leakages on a real hardware target and how ARMISTICE can help designers remove them.

This paper makes the following contributions: • ARMISTICE, a framework for formally verifying first-order masked implementations at binary level, and precisely pinpointing where and why secret data leak; this makes ARMISTICE an invaluable and actionable tool for designers to verify masked implementations and fix them if need be. • A model of the Cortex-M3 with meaningful and additional details to some recent papers (e.g. [START_REF] Marshall | Miracle: Micro-architectural leakage evaluation[END_REF], [START_REF] Gao | Reverse engineering the microarchitectural leakage features of a commercial processor[END_REF]) that studied the same processor. • A qualitative and quantitative analysis conducted with dedicated leakage test vectors of the Cortex-M3 leakage sources, including an in-depth study of the memory subsystem. The paper is organized as follows: Sec. II gives some background and experimentally motivates this paper; the modelling of the Arm Cortex-M3 processor core and memory subsystem is detailed in Sec. III; Sec. IV and Sec. V present respectively the ARMISTICE framework and experimental results before discussing the closest related work in Sec. VI and concluding in Sec. VII.

II. BACKGROUND AND MOTIVATING EXAMPLE

While real attacks can be attempted on a device, this is not so practical when assessing the device's immunity to side channel leakages. Practitioners have thus proposed several leakage assessment methods: some based on formal methods, some based on statistical analysis. Formal verification approaches of either a masked algorithm or a masked software or hardware implementation are all based on a symbolic representation of the variables or input data, which are tagged either secret, public or mask [START_REF] Barthe | maskverif: Automated verification of higher-order masking in presence of physical defaults[END_REF], [START_REF] Barthe | Verified proofs of higher-order masking[END_REF], [START_REF] El Ouahma | Sidechannel robustness analysis of masked assembly codes using a symbolic approach[END_REF], [START_REF] Meunier | LeakageVerif: Scalable and Efficient Leakage Verification in Symbolic Expressions[END_REF]. The verification consists in checking that a set of symbolic expressions, built upon these symbolic variables and representing internal values in the program or circuit, has a distribution which is independent from all the secret variables. Such a check can be performed using either a type inference [START_REF] El Ouahma | Sidechannel robustness analysis of masked assembly codes using a symbolic approach[END_REF], or an iterative substitution process trying to soundly remove secrets from the expressions [START_REF] Barthe | Verified proofs of higher-order masking[END_REF], [START_REF] Meunier | LeakageVerif: Scalable and Efficient Leakage Verification in Symbolic Expressions[END_REF]. Regarding statistical approaches, Test Value Leakage Assessment [START_REF] Goodwill | A Testing Methodology for Side-Channel Resistance Validation[END_REF] (TVLA) is probably the most popular one. It has two variants: specific and non-specific. For both variants, two sets of traces are compared. In the non-specific case, one set is generated with a fixed (secret) data, and the other with random (secret) data. A t-test analysis on these sets allows to detect any possible leakage without any assumption on the leakage model, i.e. which part of the computation is leaking in which part of the implementation. The non-specific t-test requires using a specific randomlyinterleaved procedure in order to avoid false-positive results [START_REF] Schneider | Leakage assessment methodology -a clear roadmap for side-channel evaluations[END_REF]. In the specific t-test, the traces are split into two sets according to the leakage model (e.g. hamming weight) of a known intermediate value. Other statistical tools are available to practitioners, like the Pearson correlation [START_REF] Hastie | The Elements of Statistical Learning[END_REF] which is often used in place of the specific t-test.

Let us now consider the proven first-order probing secure masking scheme from Ishai, Sahai and Wagner (ISW) [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF] and apply it to a software boolean AND computation. isw_and, shown in C language in Lst. 1, takes as inputs two secret values a and b, each split across two shares a0 and a1 (resp. b0 and b1). It produces as a result a secret value c, which corresponds to a & b, split across 2 shares c0 and c1, without ever exposing any secret value. As pointed out in the introduction, compilation can harm the carefully designed masking scheme. In this case, GCC does simplify the expressions, breaking the ISW scheme altogether. Some intermediate computations are thus protected with the enforce macro which forces GCC to materialize the intermediate value in a register rather than leaving the expression open to optimisations. # define enforce ( r ) __asm__ __volatile__ \

6

( " @enforce \ n \ t " : " + r " ( r ) ::) Lst. 1 is compiled, with size optimisations for example, for the Arm Cortex-M3 processor, a common processor in embedded devices. As our implementation is masked using the ISW scheme, and protected from compiler optimisations, one can check for himself that the secret values a, b and c do not appear in Lst. 2. Moreover, formal verification with our own ARMISTICE framework confirms the absence of leakage at the ISA level, in the value-and transition-based models.

With power traces captured on a STM32F1 target board 1, that all secret values are leaked during the execution of the isw_and function. Some of the peaks can be explained, e.g. the two consecutive str instructions (lines 10-11) are likely to leak the transition of the data written to memory [START_REF] Marshall | Miracle: Micro-architectural leakage evaluation[END_REF], [START_REF] Shelton | Rosita: Towards automatic elimination of power-analysis leakage in ciphers[END_REF], explaining partly the peak on the blue curve at samples 120 -128 in Fig. 1. One can note that leakages are increasing again after sample 132, although the ISW AND sequence is over: this illustrates the fact that despite being no longer explicitly used by the source code, the secrets a, b and c continue to leak due to some remnant effect. The Pearson correlation metric is used in this example because it makes the leakage on c more visible than with a t-test, which is affected by the low probability of having more than 16 bits set in c due to the underlying boolean AND operation. Despite the apparent simplicity of Lst. 1, most other peaks do not have a clear explanation from the literature, motivating the work described in this article: understanding the Cortex-M3 micro-architecture in enough details so that it can be modelled and used with a formal analysis tool to provide clear explanations for these leakages.

III. CORTEX-M3 MODELLING

In this section, we present the modelling of the Arm Cortex-M3 data path. We also discuss the leakage profile from off-core components, i.e. memory related components.

A. Abstract Model

As we have access to the Cortex-M3 RTL description through AAA, we go for a white-box approach to model the processor micro-architecture, which involves Verilog source files eye-ball analysis and Verilog simulations.

1) Under the Processor's Hood: The Cortex-M3 implements the ARMv7-M ISA composed of 32-bit and 16-bit instructions. It is a 3-stage pipeline processor comprising a Fetch, a Decode and one or two Execute stages depending on the instruction. As the Fetch stage does not manipulate data, we do not consider it further in the context of this paper.

The main components found in the Cortex-M3 core, depicted in Fig. 2, are: • A register file (RegFile), containing the general purpose registers (GPR), that has two read ports, named port A and port B, and one write port, named port D. • An arithmetic logic unit (ALU), to perform actual computations on data stored in micro-architectural registers RegA, RegB and RegImm. As most ALU instructions allow shifting the second operand, a barrel shifter (BS) can optionally be used on RegB's output to the ALU. • An address generation unit (AGU), with a dedicated adder (named Addr Adder in Fig. 2), to compute the address used for accessing memory, from two micro-architectural registers RegAddr1 and RegAddr2, containing the base address and the offset respectively. • A load / store unit (LSU), to deal with data sent to or received from memory, like extracting the relevant part of the received data. The memory is accessed over the AHB-Lite bus, which is pipelined with an address-phase followed by a data-phase one cycle later.

2) How Instructions Use the Micro-architecture: We only consider in this description simple instructions typically used in cryptographic implementations: simple ALU instructions and memory accesses. We also assume that there is a single execution path regardless of the secret input values. This requirement is usually met to avoid timing side channel attacks and is recommended by all secure coding rules. As a consequence, no jump nor branch can depend on secret data.

After being fetched, an instruction goes through the decode stage, which prepares the data subsequently processed by the execute stage. It retrieves operands in the register file or the instruction itself and updates RegA, RegB, RegImm, RegAddr1 and RegAddr2. Depending on RTL-implementation choices, read ports and internal registers that are not used by the current instruction can either keep their previous values, be reset to some default value, or get a value related to a bit field of the instruction which is not semantically relevant. For example, the decoding of the instruction mov.w Rd,#imm, which has only an immediate as source operand, selects PC on port A and R imm[3:0] on port B. RegA is written, while RegB is not. The choice of updating or not an unused register or read port, and in which way, takes into account 1) the requirement of maintaining an understandable code by the RTL developers and 2) some performance, cost or area trade-offs. In the next section, we illustrate the consequences of these choices regarding potential leakage.

Simple ALU instructions (e.g. add, eor, mov, sign extension or bit selection) are executed in one cycle during the execute stage. For most ALU operations, port A and RegA receive the first register operand, and port B and RegB the second one. This is not the case for pure shift operations for which port B/RegB receives the operand to shift (first operand) while port A/RegA receives the shift amount (second operand) -a necessary twist because the BS is located on RegB's output to support the optional shift of the second operand on ALU instructions. At the end of the execution cycle, the destination register is written into the RegFile through port D.

A single load or store instruction requires two execution cycles: during the first cycle (EXE1) the address is computed, while in the second cycle (EXE2), the data to write (resp. read) is sent to (resp. received from) memory. Two addressing modes are available for memory accesses: an immediate-offset addressing mode and a register-based one. In both cases, the offset is added to a base register (a GPR). The base register is read through port A and written both in RegA and RegAddr1. In case of a register offset, it is read through port B and written both in RegB and RegAddr2. Depending on the addressing mode for write memory accesses, the data sent to memory either goes to RegB and DataReg (immediate offset) or only goes to RegA (register offset). Moreover, a store with a register offset prevents any following instruction from passing the decode stage.

In case of data dependencies, forwarding mechanisms exist in order to avoid pipeline stalls. The ALU result or the data read from memory can be forwarded to RegA, RegB, RegAddr1 and RegAddr2 registers. In case of a data dependency between a load and a pipelined store with immediate offset (for instance ldr Rx, [Ry, Rz], str Rx, [Ry', #imm]), the read value is forwarded to DataReg.

B. Sources of Leakage

In this section, we present the leakage test vectors, or test vectors for short, designed in order to 1) confirm or disprove with experimental measurements our findings from the RTL analysis regarding the data path components involved in the execution of an instruction 2) quantitatively evaluate the leakage due to the different components and 3) analyse and model the memory subsystem using a black-box approach.

1) Experimental Setup: All measurements are performed on NewAE's ChipWhisperer Pro (CW1200) with a STM32F1 target board [START_REF] Oflynn | Chipwhisperer: An open-source platform for hardware embedded security research[END_REF] embedding a Cortex-M3 configured to run at 7.37MHz. The CW1200 acquires four samples per CPU cycle. Depending on the test vector, we acquire from 10,000 up to 500,000 power consumption traces, each with different random inputs generated with a Mersenne Twister RNG.

2) Anatomy of a Test Vector: A test vector has several random inputs, named Opi and starts (resp. ends) with a preamble (resp. postamble). The actual payload of a test

Op0 ^ Op1 ^ Op2 ^ Op3 Op0 ^ Op1 Op0 ^ Op2 Op0 ^ Op3 Op1 ^ Op2 Op1 ^ Op3 Op2 ^ Op3
Fig. 3. Specific t-test results using the test vector of Lst. 3 using 20,000 traces.

vector consists in a small assembly instruction sequence that manipulates some random input values. The preamble achieves three goals: the loading of random input values into GPRs, their optional preparation (e.g. extracting a specific byte or masking some parts), and the reset to a specific state, zero or random, of all elements along a data path. The postamble's role is to ensure some form of quietness for a few cycles, in order to ease the experimental measurements and their subsequent analysis.

For each test vector, several specific t-tests are performed using the Hamming Weight of expressions composed of logical or arithmetic operations on the test vector's random input values (32-bit or less). A concluding specific t-test (i.e. with a tvalue higher than 4.5) on the exclusive-or between expressions (e.g., input values) shows that there is a transition leakage induced by a micro-architectural component between these expressions.

An example is given in Lst. 3: it is composed of two exclusive-OR instructions (eor), each with different source GPR operands holding different random input values. The destination GPR operands are also distinct. We perform a specific t-test on the traces resulting from the execution of the code given in Lst. 3 to measure the interaction between the consecutive values of the first (resp. second) operand of both instructions using the expression HW(Op0^Op2) (resp. HW(Op1^Op3)), where HW denotes the Hamming Weight of an expression. The value of this expression is directly linked to the power consumption of the port A and RegA (resp. port B and RegB). Thus, a high t-test value for this specific expression indicates a leakage in at least one of these two components. Similarly, we also measured the interaction between two consecutive values at the ALU output (or BusD) using the expression HW((Op0^Op1)^(Op2^Op3)).

The result of the specific t-test for the previous example is plotted in Fig. 3. In this figure, we clearly see the interaction between operands on the paths from the RegFile to RegA/RegB (curves named Op0^Op2 and Op1^Op3, samples 5-9) and once latched in RegA/RegB (curves named Op0^Op2 and Op1^Op3, samples 10-13). We can also see the interaction between the results of both instructions (curve named Op0^Op1^Op2^Op3, samples 10-13). As the preceding and following instructions manipulate constant values, the results of both instruction leak (curve Op0^Op1, samples 5-9 and curve named Op2^Op3 at samples 14-18).

Op0 ^ Op1 Op0 ^ Op2 Op0 ^ Op3 Op1 ^ Op2 Op1 ^ Op3 Op2 ^ Op3
3) Invisible Source of Leakage at ISA Level: One major outcome of the RTL analysis is the discovery of some potential sources of leakage without any explicit link with data manipulated by instructions. In this section, we give some examples of such invisible leakage at ISA level.

We first illustrate the consequence of the choices of the decoding stage regarding read ports. As previously mentioned, the decode stage of a mov.w Rd,#imm instruction selects R imm[3:0] on port B without writing it in RegB. Using a dedicated test vector and a specific t-test with 50,000 traces, an interaction between the data previously read on port B and the content of the register R imm[3:0] is visible (max t-value of 9.1). This behaviour can reveal secret data, e.g., when the register R imm[3:0] contains one share of a first-order masked data and the second share has been read on port B in the previous cycle.

The encoding used for an instruction is also of critical importance, as the RegA and RegB write enable signals may depend on the instruction encoding. For example, the decoding of the instruction ldr ROp2, [Raddr, #imm] writes ROp2 into RegB if and only if the instruction uses a 32-bit encoding. Fig. 4 shows specific t-test results when running a 16-bit or a 32-bit encoded load instruction. We can see that a 32-bit encoding leads to a write of the destination register content into RegB as there is an interaction between Op1 and Op2 visible at samples 13-18 and 25-31. Considering that RegB is always written with the destination register of a load instruction with immediate offset may lead to miss potential interactions between the values written into RegB before and after the load if the load is actually 16-bit encoded; alternatively, considering it is never written may lead to miss potential interactions between Op2 and the values written into RegB before and after the ldr when it is 32-bit encoded.

Another important knowledge gained from the RTL is related to the forwarding mechanisms and internal registers. As an example, DataReg contains the value to be sent to the memory in case of a store with an immediate offset. If there is a dependence on this value with the preceding load instruction, the loaded value is forwarded to the DataReg. The RegB register is however still written with the content of the register supposed to contain the value to be sent, but which is in this case the old value held in this register. This may be a source of leakage which can only be determined with the knowledge of both the issue time of instructions and the implemented forwarding mechanisms in the processor.

4) Leakage Test Vector Suite:

We have carefully designed 77 test vectors: 31 devoted to the analysis of the data path components involved in each class of instructions, 5 devoted to forwarding mechanisms, 7 devoted to writing back into the register file and 34 devoted to the analysis of the LSU and memory. Test vectors enable us to assess and confirm the potential leakage on the different buses and internal registers as well as leakage due to memory transfers in the Cortex-M3 core of our STM32F1 target. Contrary to the ARM processor core whose RTL must not be modified (apart from selecting some configurable options), the memory subsystem implementation varies between targets with an identical core [START_REF] Marshall | Miracle: Micro-architectural leakage evaluation[END_REF]: the (offcore) memory subsystem on our STM32F1 target is thus a black box. Test vectors dedicated to the memory and LSU enable us to model the memory subsystem.

Unsurprisingly, a small subset of our test vectors are similar to those from MIRACLE [START_REF] Marshall | Miracle: Micro-architectural leakage evaluation[END_REF]. The RTL availability allows us to have an exact knowledge of the data manipulated by instructions. As a consequence, we design more specific test vectors in order to profile the leakage induced by the microarchitectural components and to explain where in-core leakage stems from. We cannot describe all the test vectors here but they are available online with their results [START_REF]ARMISTICE: Micro-Architectural Leakage Modelling for Masked Software Formal Verification[END_REF]. We summarize the main results in the next section.

5) Leaking Components:

Our analysis reveals that the RTL version of the Cortex-M3 we have access to is more recent than the one used for the implementation of the Cortex-M3 core in the STM32F1. For example, shifted operands are sent to RegA and not RegB. Each time a 32-bit instruction does not have a source register operand, R0 is read in the register file on the corresponding read port (note that it is the default behaviour for the 16-bit instructions decoding). Moreover, some crossed leakages between RegA and RegB appear in case of consecutive ALU instructions with different operations. The abstract processor model used for the ARMISTICE tool, presented in the next section, reflects our findings.

Due to the CMOS technology, any component (bus, register, ...) is a source of transition leakage and can lead to the reveal of secret data. However the number of traces needed to see a transition leakage depends on the components. The more combinatorial logic the component is connected to, the less the number of traces. The table below gives the number of traces (starting with 10,000 traces) required to see, using a specific t-test, a transition leakage into a specific component. These values correspond to experiments with 32-bit manipulated data. More traces are needed when data have a smaller bitwidth: e.g. 500,000 traces are needed to see a transition leakage due to consecutive writes of 8-bit values in a given GPR. From the RTL of the Cortex-M3 core, we know that memory is byte-addressed and the width of the data bus is 32 bits. Also, an aligned word is always loaded from the memory: when reading a byte (resp. half-word), the containing 32-bit word is sent to the CPU and then the LSU extracts the requested byte (resp. half-word). Regarding data writes into memory, a data whose width is less than a word is duplicated to form a 32-bit value to be sent to the memory. Our test vectors devoted to the analysis of the LSU and the black-box memory subsystem reveal several interactions from which we build a model of the memory subsystem, as depicted in Fig. 5: • Read Side: There is a transition leakage between bytes at the same index in words loaded consecutively, be they separated or not by other non-memory instructions. Moreover, when bytes or half-words are requested, some leakage is visible between them with enough traces, even when they are not at the same word index. The data extraction in the LSU induces intra-word leakage when two load instructions are pipelined in the LSU: the data extraction is performed as soon as the extraction pattern is known, but the data arrival is at the end of the cycle. As a consequence, the extraction is performed during a small amount of time on the data read in the previous cycle. This provokes some intra-word leakage in the first loaded data. • Write Side: Due to the duplication of data in case of byte (resp. half-word) write in the memory, a stored byte can interact with all other bytes (resp. aligned half-word) of the data sent to the memory in the previous cycle. When two store instructions are not issued in consecutive cycles, the stored bytes only interact with the ones at the same index in the previously read or written data. On our STM32F1 target, the DataOut bus seems to be reset between writes and there is, seemingly in the off-core memory, a one-word buffer which contains the last piece of data read or written, as explained next. • Read Write Interaction: Consecutive memory instructions (load-store, store-load), even separated by non-memory instructions, do interact. As there are two data buses (DataIn and DataOut), the interaction takes place in the memory subsystem. Our test vectors enable us to confirm that there is a one-word buffer containing either the last read word or the result of the last written word. When storing a byte or half word, the targeted aligned word is retrieved in the memory and the word resulting from the write (i.e. with one or two changed bytes) is written in this buffer. This behaviour is consistent with all the interactions we described before between two consecutive load or store instructions separated by non-memory instructions. Fig. 5 illustrates the inferred memory model and the one-word buffer. This section has shown that each micro-architectural element can leak, some more obviously than others, i.e. requiring more or less traces. This is by no means specific to the Cortex-M3 though, and all processors are plagued with similar leakage sources. Despite the Cortex-M3 being a simple processor, manually checking all possibilities for securing a piece of code against side channels quickly becomes a daunting task for a developer, thus motivating the need for tooling to automate the task and manage the complexity.

IV. FORMAL VERIFICATION WITH A MICRO-ARCHITECTURAL MODEL

This section introduces ARMISTICE, a framework designed for formally proving the absence of leakage in a masked program when executing it on a specific processor core.

Overview: ARMISTICE implements different symbolic ARMv7-M instruction set simulators, denoted processor models in the remainder, targeting different abstraction levels such as ISA level or micro-architectural level. Such a symbolic simulator builds symbolic expressions representing the values passing through the hardware components of the processor when executing a masked program. The symbolic variables in expressions are typed as masks, secrets or public variables (e.g. plaintext). Other variables, whose values do not depend on the inputs (such as loop counters), have concrete values. These expressions provide an accurate model of the leakage due to the manipulated data, and proving that these expressions, or some combinations of expressions, are statistically independent from secret values gives a valuable guarantee regarding secret independence on a real execution. ARMISTICE leverages an external formal analysis tool to prove the absence of leakage in a given leakage model, and allows to avoid a statistical analysis or interpretation as would happen with a leakage trace simulator.

The verification process is depicted in Fig. 6. First, from a binary code, an entry point of the program to analyse and information on symbolic variables with their type, an execution trace is generated using an external symbolic execution engine. This step enables one to retrieve 1) the sequence of instructions executed by the program (we assume a single execution path i.e. no jump depends on a symbolic input) and 2) the symbolic content of relevant memory locations for the program just before its beginning. Then, the execution trace is simulated using the user-specified processor model which computes the symbolic expressions in hardware elements at each execution cycle and performs all formal checks according to the user-specified leakage model, either value-based or transitionbased. In the value-based model, the verified expression is the new content of each modelled hardware component. In the transition-based model, it is the exclusive-or between the old and new expressions of each modelled hardware component. ARMISTICE retrieves the verification results from the external verification tool and eventually outputs a synthesis of all the results. It can also give, for each detected leakage, the involved assembly instruction(s), the leaking expression as well as the leaking hardware element. The user can leverage these precise sources of leakage to remove them. For example, he can then reorder instructions or insert specific instructions, and check that the new code is leakage-free.

Implementation: The different parts of ARMISTICE are implemented in Python. Currently, there are two processor models for the Armv7-m ISA: one at ISA level and one at micro-architecture level, denoted Arm ISA and Arm Cortex-M3 respectively. However, ARMISTICE offers an easy way to add new models by implementing a specified interface, comprising a few functions called by a common simulation engine core. In the Arm ISA model, each instruction executes in one cycle and only modifies the content of the destination registers or the memory according to its semantics. The Arm Cortex-M3 model implements a cycle-accurate description of the abstract model presented in Sec. III with a 3-stage pipeline (DEC, EXE1, EXE2). Modelled hardware components comprise GPR, internal CPU and memory registers, data memory as well as multiplexers and buses. At each simulation cycle, each modelled hardware component is updated according to the instruction processed in the corresponding pipeline stage. Note that the Arm ISA is a subset of the Arm Cortex-M3 one. Currently, the execution trace is generated using the symbolic engine angr [START_REF]angr: a platform-agnostic binary analysis framework[END_REF]. For the formal verification of symbolic expressions, we selected LeakageVerif which has been shown to be the most efficient, accurate and appropriate for verifying first-order probing security of expressions representing intermediate computations of masked software [START_REF] Meunier | LeakageVerif: Scalable and Efficient Leakage Verification in Symbolic Expressions[END_REF].

Example: The example in Fig. 6 illustrates how symbolic expressions are constructed in both models, focusing on Port A and Port B for the Arm Cortex-M3 model. We consider a sequence of two instructions, namely eor r6, r4, r5 and eor r8, r6, r7, performing a remasking of a secret k from the mask m0 to the mask m1. The 'initial' column in the ISA model ('cycle 0' column in the Arm Cortex-M3 model) gives the content of the relevant GPR just before the sequence: e.g. r4 contains the symbolic variable m1, r6 contains the concrete value 0. In the Arm ISA model, the registers are updated after the execution of each instruction: r6 contains the symbolic values m0 ⊕ m1 then r8 contains k ⊕ m1. In this model, ARMISTICE guarantees the absence of leakage both in value and transition. In the Arm Cortex-M3 model, in cycle 1, the instruction eor r6, r4, r5 is in the decode stage, and so Port A and Port B contain respectively the expressions m1 and m0. In cycle 2, this instruction advances in the execute stage and the instruction eor r8, r6, r7 goes into the decode stage, what updates Port A with value 0 (as r6 has not been updated yet) and Port B with value k ⊕ m0. Focusing on the components Port A and Port B, this creates the following two transitions: m1 → 0 and m0 → k ⊕ m0. The resulting expressions, respectively m1 and k, show that there is no secret leakage on Port A, but that a secret leakage in transition is present on Port B. The subsequent writes in r6 and r8 do not result in a secret leakage, as for the Arm ISA model. Back to the motivating example: Let us now consider again our software implementation of the ISW AND algorithm, with a C code implementation shown in Lst. 1, and its compiler-emitted assembly code from Lst. 2. The results of the ARMISTICE analysis on Cortex-M3 in the transition leakage model are reported in the tables from Fig. 7. The upper table displays, for each instruction, which micro-architectural elements are leaking, together with a link to the expression and the secret values (a, b, c) leaked by that expression in the lower table. The correlation plot is the one from Fig. 1, with annotations to explain the leakage origins using the expressions from the tables. It is worth reminding here that due to the nature of the operation performed by the ISW AND, a bitwise and, a leakage on a or b implies a leakage on c.

As made obvious in Fig. 7, no processor cycle is leakagefree and all secrets are leaking in the transition leakage model most of the time. The leakages found by ARMISTICE match perfectly those found experimentally on the STM32F1. Next section will dive deeper in the details of the ARMISTICE results with real benchmarks.

V. EXPERIMENTAL EVALUATION

We show that our framework ARMISTICE modelling the Cortex-M3 allows us to find theoretical secret leakages in the micro-architecture, even when the masking scheme has been shown to be secure in their considered leakage model. Finally, we show on examples that the secret leakages found are experimentally visible. Expressions Fig. 7. Detailed analysis of ISW AND in the transition leakage model. The tables display the ARMISTICE results. The Pearson correlation plot from Fig. 1 is annotated with vertical bars to show the processor cycles, the leaking expressions and the instructions that are in the different pipeline stages at each cycle.

• b1 ⊕ a1 a, c e1 a0 • b1 ⊕ b0 b, c e2 a0 ⊕ a1 a, c e3 a0 • b0 ⊕ a1 • b0 a, c e4 a0 • b0 ⊕ a1 • b1 a, b, c e5 a1 • b0 ⊕ b1 b, c e6 a0 • b0 ⊕ a0 • b1 ⊕ a1 • b0 a, b, c e7 a0 • b0 ⊕ a0 • b1 ⊕ a1 • b0 ⊕ a1 • b1 a, b, c 0

A. Benchmarks

In order to illustrate the relevance of ARMISTICE, we consider 4 C-source implementations masked in the first-order value-based probing security model: Secmult, the popular secure Galois field multiplication [START_REF] Rivain | Provably secure higher-order masking of AES[END_REF]; AES-Herbst and AES-KS a masked version of AES and its key schedule, following the masking scheme proposed by Herbst et al. [START_REF] Herbst | An AES smart card implementation resistant to power analysis attacks[END_REF]; AES-Yao another masked version of AES [START_REF] Yao | Faultassisted side-channel analysis of masked implementations[END_REF]. The main difference in AES-Yao, compared to AES-Herbst, is the multiplication by constants 2 and 3 in the MixColumns step that is performed via table lookups. As the key schedule in AES-Yao is not masked, it is not considered in the evaluation. C-source benchmarks were compiled using GCC 10.2, at optimisation level O2. These benchmarks are first-order value-based masked, hence they are not secure in the transition-based leakage model. ARMISTICE is likely to detect leakages at ISA and micro-architectural level.

We also select 4 Arm assembly-level masked implementations. Arm-Add and Arm-Add-opt are two masked implementations of an addition of two secrets split in two shares [START_REF] Jungk | Efficient side-channel protections of ARX ciphers[END_REF]. They are provided as Arm assembly code and are, to the best of our understanding, designed to be masked in the first-order transition-based probing security considering GPR. ARMISTICE should then not detect leakages due to writes in the RegFile. Dil-And is a 32-bit masked logical AND and Dil-A2B is a 32bit conversion from arithmetic to boolean masking. These two functions are provided as part of a masking scheme of the Dilithium algorithm for the Cortex-M3 [START_REF] Migliore | Masking dilithium[END_REF]. Both versions have been implemented using an enhanced version of the MAPS simulator. As they are supposed to take into account the Cortex-M3 micro-architecture, it is interesting to know if ARMISTICE can find remaining secret leakages or not at microarchitectural level.

B. Leakage Analysis

For each benchmark, a verification is performed on both the Arm ISA and Arm Cortex-M3 processor models.

Tab. 8 presents a synthesis of the analysis results for the Cortex-M3 processor model per benchmark. Namely, it gives for each modelled component of the Cortex-M3 the number of secret data leakages in the value-based leakage model (#VL column) and in the transition-based one (#TL column). As expected, the results for the GPR (line "R0 to R14") are the same, and so stand for both this model and the Arm ISA processor model, in which only the GPR are considered as sources of leakage. This also comprises values read from and written to memory as they necessarily pass through a GPR.

At ISA level, for Secmult, AES-KS, AES-Herbst and AES-Yao, the analysis in the value-based leakage model confirms there is no leakage in the GPR, hence nor in memory, as claimed by their authors.

For the Arm Cortex-M3 processor model, for the same benchmarks, we can first notice that as expected there is no leakage in the value-based leakage model, except for the memory related components (DataOut, DataIn and ReadWriteBuffer). This is because when a masked byte of the AES state is read, the whole memory word is actually read in memory and transferred, containing four state bytes. As there is a single mask byte for masking each of these four bytes, this constitutes a leakage. We can also notice that there is an enormous amount of leakages in transition on microarchitectural components for these benchmarks. In fact, all of the components except MuxRegAddr2, RegAddr2, MuxBS, MuxDataAdder and 5 GPR have at least a transition revealing secret information. While a verification in the value-based leakage model at the ISA level is a required first step towards leakage-free implementations, it leaves many secret leakages on the table.

The Arm-Add and Arm-Add-Opt benchmarks both contain secret leakages in GPR in the value-based and transition-based leakage models. This suggests that there may be a flaw in the design of these programs contrary to the claim of the authors. Unsurprisingly, there are many other secret leakages in other hardware elements of the core, as those were not taken into consideration in the masking scheme design.

Finally, for the Dil-And and Dil-A2B benchmarks, almost all the secret leakages in value and transition have been eliminated. Yet, a few secret leakages in transition remain: they occur on the path from the ALU to the RegFile, in the DataReg, and in the ReadWriteBuffer. We first looked at leakages in the path from the ALU to the RegFile in Dil-A2B, as it should have been taken into consideration in the design of these programs. Unfortunately, the leaking expressions are too big for a manual analysis (more than 800 KB per leaking expression). Therefore, we rather performed a manual analysis of the leaking expressions reported for the Dil-And program. Both leakages on DataReg and ReadWriteBuffer happen when writing back in memory the two shares of the result. If the two stores have been separated by a logical instruction to clean the data path, this instruction does neither erase the content of the Data Reg, nor the one of the ReadWriteBuffer. Consequently, the two stores of the two shares reveal the secret results in these two hardware elements. We show in the next section that this secret leakage can be experimentally observed at the ARMISTICE's reported time in the power trace.

These results show that the ISA level or the value-based leakage model are not good abstractions of the real power consumption. Instead, there is a need to take into account a more detailed description of the device executing the program. The RTL level combined with the transition-based leakage model is a better abstraction for leakage analysis, as together they are much closer to the hardware transitions, responsible for most of the power consumption. Besides, the Dil-And and Dil-A2B results show that it is difficult to take into account micro-architectural details without a formal approach, as manual approaches will fail to take into account every aspect, even with detailed knowledge. These results thus show the relevance of the proposed approach, by being able to pinpoint the instructions, the moments and hardware elements in the core responsible for secret leakages, even for codes designed to be secure for the Cortex-M3 core.

C. Accuracy and Exploitability

In order to illustrate the accuracy of the approach, we run three experiments. First, in order to show that the leakages found on the Dil-And benchmark are real, we capture 500,000 traces with the setup described in Sec. III-B1. We run a specific t-test on the leaking expression and look at the t-test value for the samples corresponding to the cycles at which ARMISTICE detected the leakages: the results, shown in Fig. 10, demonstrate a perfect match.

In a second experiment, we repeat the same process for all of the simple secret leaking expressions in the first round of the Key Schedule in the transition leakage model. By simple, we mean expressions with at most one binary operator. There are height such expressions. In Fig. 9, we can see that all the secret leakages experimentally observed are detected by ARMISTICE at the expected location in the trace. However, four secret leakages detected by ARMISTICE do not translate into concluding t-tests, making them seemingly false positives. However, after further investigations:

• Two of these leakages result from writing a byte in R0 (ex6 and ex7). As shown in section III-B5, transitions in R0 on a single byte can hardly be observed with 500,000 traces.

Here, in both cases, as there is still a remnant effect from a big previous leakage, these leakages on R0 cannot be distinguished on the trace. • One of these leakages results from the transition between two register values put on the Bus B, but not written into Reg B (ex5). In fact, the two corresponding instructions do not read the registers, but the latter are selected because of the immediate values contained in the instructions. We designed a specific test vector for this case which confirmed that no leakage can be observed in this case, at least with our experimental setup. • The last leakage corresponds to an already observed leakage situation, since it occurs on ALU out (ex2). After investigation, it appears that in some cases, the processor stalls for one cycle, which is not taken into account in our model. While we have not yet found out the reason why such stall cycles occur, we suspect they come from the fetch of some instructions in the Flash memory. Adding an extra instruction to shift the two non leaking consecutive instructions makes the stall cycle disappear and the leakage found by ARMISTICE visible.

In order to deal with the non-visible leakages, one can decide to deactivate leakage analysis in some hardware elements for a given data size if the leakages in these elements are experimentally too small to be observable. Regarding the unexplained stall cycles, not modelling them only results in false positives as the stall resets some signal values. Yet, future work includes understanding why such stall cycles occur.

For the third experiment, we modify the assembly code of the previous experiment to remove all the possible secret leakages detected by ARMISTICE. Some of them, occurring in the memory, were not taken into consideration as they require modifying the memory data layout of the program. For each detected secret leakage, we add one or several instructions in order to clean the parts of the data path involved in the leaking transition. The added instructions can have three different kinds: for transitions happening in the arithmetic and logic data path, we use a orr lr, lr, lr instruction, not a nop neither a mov instruction, in order to be sure to clean regA and regB; for transitions happening in the AGU, LSU or memory, we use either a load or a store by making sure that the address is secret independent and that the value read or written is a constant; finally, for transitions happening in a GPR, we use a orr rX, lr, lr to erase the content of the register with a constant value before the new one. Once all instructions are added, the new code is run again on ARMISTICE to ensure that no more leakage is found. Fig. 11 shows the t-test values obtained for all the expressions after patching the code: all leakages have disappeared. This second experiment shows how ARMISTICE can help designers remove all the potential secret leakages in a code, by exhibiting the specific leakages, along with where and when they happen. This information allows ones to write the minimal code patch to remove such leaking transitions. The patched code can eventually be analysed by ARMISTICE in order to verify the absence of leakage.

To conclude, ARMISTICE is a valuable tool that detects secret leakages happening during the execution of a masked software on a processor. It can also help patch a code to suppress leakages, and verify a patched code. These results show that a RTL description is a relevant abstraction level to perform a formal leakage analysis. Although some modelled transitions may not translate into visible leakages, removing all RTL transitions leaking a secret provides a valuable security guarantee.

Currently, glitches are not taken into consideration in ARMISTICE. While nothing theoretically prevents considering them, we believe that considering them "as such" will result in a lot of detected leakages that are unlikely to be observed on a real target device. A more detailed analysis of the circuit is required in order to select existing glitches, which is left for future work.

VI. RELATED WORK

Power or electromagnetic trace simulators using a model inferred from experimental measurements intrinsically take into account micro-architectural leakage [START_REF] Mccann | Towards practical tools for side channel aware software engineering: 'grey box' modelling for instruction leakages[END_REF], [START_REF] Sehatbakhsh | EMSim: A Microarchitecture-Level Simulation Tool for Modeling Electromagnetic Side-Channel Signals[END_REF]. ELMO [START_REF] Mccann | Towards practical tools for side channel aware software engineering: 'grey box' modelling for instruction leakages[END_REF] pioneered such trace simulators with a power model of the Arm Cortex-M0 for a subset of the ISA composed of the most frequent instructions in cryptographic implementations. The accuracy of such simulators depends on the set of experiments used to learn the model. Recently, ELMO has been extended into ELMO* in order to better model register or memory reuse as well as interaction between non consecutive instructions [START_REF] Shelton | Rosita: Towards automatic elimination of power-analysis leakage in ciphers[END_REF]. As for MAPS [START_REF] Le Corre | Micro-architectural power simulator for leakage assessment of cryptographic software on arm cortex-m3 processors[END_REF], it has been built using the RTL description of the Arm Cortex-M3. It focuses on the potential leakage due to internal registers at the entrance of the ALU: our experiments show that ARMISTICE outperforms MAPS regarding the modelling of the processor core in addition to help remove the found leakage by pinpointing the leaking instructions and the leaking hardware elements.

MIRACLE [START_REF] Marshall | Miracle: Micro-architectural leakage evaluation[END_REF] is an infrastructure proposing several test vectors for highlighting micro-architectural leakages due to interactions between operands of instructions or memory accesses, or due to speculative execution. While this work shows that the leakage varies between architectures and even implementations of the same processor core, it does not explain how to use test vectors to understand or describe the micro-architecture to model the leakage sources. Gao et al. [START_REF] Gao | Reverse engineering the microarchitectural leakage features of a commercial processor[END_REF] go one step further by reverse-engineering some micro-architectural leakage features of an Arm Cortex-M3 processor running 16-bit instructions only. Using test vectors and their recently so-called collapsed models [START_REF] Gao | A novel completeness test and its application to side channel attacks and simulators[END_REF], they deduce a model of the different components of the Arm Cortex-M3. Barenghi et al. explore how to infer the structure of different Arm Cortex-A and Cortex-M pipelines, using a framework of microbenchmarks and the CPI metric (Clock cycles Per Instruction) [START_REF] Barenghi | Side-channel security of superscalar CPUs: Evaluating the Impact of Micro-Architectural Features[END_REF], [START_REF] Barenghi | Exploring cortexm microarchitectural side channel information leakage[END_REF]. They highlight the potential side channel leakages resulting from the pipeline structures and some architectural choices. As we have access to the RTL of the Cortex-M3 processor, we can use a white-box approach for the processor core; we go deeper in the modelling of the leakage sources, like considering both the 16-bit and 32-bit variants of the instruction set. We give clear explanations of the leakages found on the Cortex-M3 and reported by those related work. However, as previous work, we resort to a blackbox approach based on leakage test vectors for modelling the memory subsystem but we go one step further as this model is used by ARMISTICE for detecting leakages due to interaction in the memory subsystem.

In order to remove the micro-architectural leakage, the ROSITA tool [START_REF] Shelton | Rosita: Towards automatic elimination of power-analysis leakage in ciphers[END_REF] automates leaking pattern replacement detected by using ELMO* and non specific t-tests. The iterative process is able to remove most leakages from three implementations but fails for one implementation. The modelling may be incomplete, or, as ELMO* cannot help pinpointing the source of leakage, the replacement patterns may not be fully secure. In addition, these patterns may not be as small as they could be with a better leakage source understanding. Also, when the patching fails, developers are left clueless with the leakage, advocating for a solution able to explain it. On the hardware side, the usage of dedicated logic or design tools can help reduce the sources of potential leakage [START_REF] Slpsk | Karna: A gatesizing based security aware eda flow for improved power side-channel attack protection[END_REF], [START_REF] Balasch | Towards efficient and automated side-channel evaluations at design time[END_REF]. Such design-time solutions do not help for existing processors. FENL [START_REF] Gao | FENL: an ISE to mitigate analogue micro-architectural leakage[END_REF] extends the ISA with additional instructions for cleaning off in-core resources that may be the source of leakage. This is an appealing solution as it offers developers means to avoid in-core leakage at a lower cost than using tediously designed cleaning gadgets, but it still does not help for existing processors. Moreover, automated solutions such as ARMISTICE are required to help determine how and where to use such dedicated instructions.

Finally, two recent works target the verification of masked software on a low-level processor description.

Barthe et al. propose a Domain Specific Language for modelling assembly implementations and for specifying finegrained leakage models [START_REF] Barthe | Masking in fine-grained leakage models: Construction, implementation and verification[END_REF]. The semantics of assembly instructions can then be enriched with the leakage effects of the instruction. In particular, different leakage effects due to some internal registers or some buffers in memory can be made explicit. They propose the scVerif tool as a front end of MaskVerif [START_REF] Barthe | maskverif: Automated verification of higher-order masking in presence of physical defaults[END_REF], [START_REF] Barthe | Verified proofs of higher-order masking[END_REF] for formally verifying masked assembly gadgets and implementations. scVerif allows one to build micro-architectural leakage aware gadgets, be they masking gadgets or cleaning gadgets. Such gadgets can then be used in an automatic composition in order to reduce the time required to implement secure solutions [START_REF] Abromeit | Automated masking of software implementations on industrial microcontrollers[END_REF]. The proposed approach enables one to take into account the interactions inside the pipeline or due to memory access during the formal verification. However, it relies on the knowledge of the microarchitectural source of leakage and requires the explicit modelling of leaking components (e.g. internal registers or memory buffers). These papers do not explain how the modelling of the Arm Cortex-M0+ targeted in the experiments was carried out. As shown in our paper, the decoding stage of the Arm Cortex-M3 processor induces different leakage effects depending on the binary encoding of the instruction, thus requiring as many instruction specifications as the number of encodings per instruction. Moreover, the user would have to explicit the instruction encoding in his implementation expressed in the scVerif's input language. A verification using the binary code as we propose seems more appropriate for avoiding putting the burden on the user. Finally, as scVerif executes sequentially the instructions, it cannot model the effects of the forwarding mechanism.

Coco [START_REF] Gigerl | Coco: Co-Design and Co-Verification of Masked Software Implementations on CPUs[END_REF] is an approach for formally verifying if a masked software would securely be executed on a CPU. Leakages are searched for at gate-level, comprising glitches. Authors show several weaknesses in the RISC-V IBEX core related to the register file, ALU and LSU units that can be removed with small changes. Coco requires the analysed masked implementation to satisfy two constraints: 1) shares related to a same secret must not be processed by consecutive instructions 2) registers and memory locations which contain a share must not be overwritten with the second share. If these constraints may be sufficient for the IBEX core simple micro-architecture, they are not sufficient for the Cortex-M3 in which non consecutive instructions may write into a same micro-architectural register. The first constraint is not necessary either as consecutive instructions do not lead to a secret leakage when the explicitly or implicitly manipulated shares are not combined inside the processor. Moreover, meeting such constraints requires dedicated tools, such as formal verification tools at ISA level. ARMISTICE has no constraint on the analysed masked implementation, it is able to find leakage due to any modelled hardware element: GPR, internal register, bus, memory buffer or memory location. In addition, it helps designers to remove such interactions thanks to its outputs.

This comparison shows that ARMISTICE outperforms the existing approaches as it automates formal verification taking into account all the micro-architectural details of a processor, and makes a link between the secret leakages found, the hardware, and the executed software.

VII. CONCLUSION

We presented ARMISTICE, a framework for formally verifying the absence of leakage considering first-order value-based or transition-based probing security in masked software implementations. Using an accurate model of a target core and memory subsystem, ARMISTICE allows to take into account microarchitectural leakages in the verification process. We presented the modelling of an Arm Cortex-M3 based STM32F1 board based both on a white-box analysis of the core and on a blackbox analysis of the memory subsystem via leakage test vectors. We experimentally showed that our modelling is relevant for detecting micro-architectural leakages as well as for manually removing them thanks to the ARMISTICE's output, comprising leaking instructions and hardware components where leakages stem from. Future work will consider higher order leakage verification, the automation of model extraction from a RTL design and automatic code patching from an analysis result.

7 8 1 ;

 71 aux0 = m ^enforce ( a0 & b1 ); 9 aux1 = aux0 ^enforce ( a1 & b0 ); 10 c0 = ( a0 & b0 ) ^m ; 11 c1 = ( a1 & b1 ) ^aux1 ; Listing 2. ISW AND (GCC assembly output) r0 : a0 , r1 : b0 , r2 : a1 , r3 : b1 , r6 : c [] r7 : m

Fig. 1 .

 1 Fig. 1. Pearson correlation results for Lst. 1.

Fig. 2 .

 2 Fig. 2. Data path of the Cortex-M3 processor core

Fig. 4 .

 4 Fig. 4. Specific t-test results when placing a ldr ROp2, [Raddr, #imm] between two eor Rdst, ROp0, ROp1. On the left, ldr is 16-bit encoded; on the right it is 32-bit encoded. 200,000 traces were used.

Fig. 5 .

 5 Fig. 5. Model of the memory subsystem of our STM32F1 target #Traces Leaking Components 10,000+ RegA, RegB, RegAddr1, RegAddr2, AluOut, Addr Bus, Data Out, Data In 50,000+ Port A, Port B, DataReg 200,000+ Bus D, GPR

Fig. 6 .

 6 Fig. 6. ARMISTICE framework and example of symbolic expressions construction

Fig. 8 .

 8 Fig. 8. ARMISTICE analysis results for the 8 benchmarks. Columns #VL (resp. #TL) gives the number of value (resp. transition) leakages found.

Fig. 9 .

 9 Fig.9. Comparison between the secret leakages found by ARMISTICE in the first round of AES-KS, and the corresponding specific t-tests. The pink rectangles indicate the cycles at which a leakage was found in ARMISTICE for the corresponding expression.

Fig. 10 .

 10 Fig. 10. Comparison between the secret leakages found by ARMISTICE in the Dil-And benchmark, and the corresponding specific t-test. The pink rectangle indicates the cycles at which a leakage was found in ARMISTICE.

Fig. 11 .

 11 Fig. 11. t-test values of the eight originally leaking expressions (ex0 to ex7) in AES-KS, after patching the assembly code. No more expression is leaking.

The Arm Academic Access (AAA) is a free-of-charge program that provides access to an expanding range of Arm IP for academic purposes only: https://www.arm.com/academicaccess


Mathuran Kandeepan

Clara Ciocan

Maxime Millet

Manuel Bouyer

Adrien Cassagne

Lionel Lacassagne

Fast Meteor Detection Toolbox

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Fast Meteor Detection Toolbox

Overlapped duration of ground truth and automatic detection (overall tracking rate: T r = 80.4%).

SEQUENTIAL TIME DISTRIBUTION

2.4% 57.98%

29.07% 6.92%

3.63%

Odroid-XU4

EXPERIMENTATION RESULTS

• Video resolution: 1920x1200 (HD)

• GNU compiler: -O3 -march=native

• Odroid-XU4 -Feb. 2016 -28 nm proc.

-4 × LITTLE ARMv7 Cortex-A7 CPU @ 1.4 GHz -4 × Big ARMv7 Cortex-A15 CPU @ 1.

3 ]

 3 MATHURAN KANDEEPAN, CLARA CIOCAN, MAXIME MILLET, MANUEL BOUYER, ADRIEN CASSAGNE AND LIONEL LACASSAGNE Sorbonne Université, CNRS, LIP6, F-75005, Paris, France CONTEXT • Detection and characterization of meteoroids and space debris that enter into our atmosphere -From satellite (CubeSat) [1, 2] -From weather balloon -From aircraft observation campaign [Better observation conditions than from earth • Greyscale input videos, output tracks (= positions of meteors) • Real-time constraints & Challenges -Non-stabilized cameras, noisy video sequences -Limited computational power: 10 Watts -Embedded systems (RPi, Jetson, ...) & RISC architectures [4] • LIP6/ALSOC & IMCCE joint-team: https://www.imcce.fr/recherche/ campagnes-observations/meteors/2022the 2022 τ -HERCULIDS METEOR CLUSTER of the 34 τ -Herculids meteor cluster (duration: 7.5 s) from an airborne observation campaign [3]. Center: Ursa Minor constellation.

FMDT: COMPUTER-VISION DETECTION CHAIN

	image (t + 0) image (t + 1)		intensity hysteresis thresholding intensity hysteresis thresholding		connected-component (CC) labeling & analysis connected-component (CC) labeling & analysis	morphological thresholding thresholding morphological	k-nearest neighboor (k-NN) matching	global motion estimation	residual motion computation	motion thresholding	piece-wise tracking
																	open source initiative
	Parallel task		Input socket		FIFO buffer
	Sequential task		Output socket		Thread
	Auto. add task													pull n	t 2	t 3	t 4	n push
	t 1 Sequence 1 = Stage 1	t 2 t 2 t 2 t 2	t 3 t 3 t 3 t 3 Sequence 2 = Stage 2		t 4 t 4 t 4 t 4		t 5 Sequence 3 = Stage 3	t 6	t 1	push 1 Stage 1	pull n ′ pull n ′′	t ′ 2 t ′′ 2	t ′ 3 t ′′ 3	t ′ 4 t ′′ 4	push n ′ push n ′′	pull 1	t 5 Stage 3	t 6
				Pipeline user description 1) Describe the app in a tasks graph (dataflow model)			pull n ′′′	t ′′′ 2	t ′′′ 3	t ′′′ 4	push n ′′′
					2) Group tasks in pipeline stages 3) Select the number of threads per stage 4) [Pin threads to cores] [Choose pipeline sync. type]		1 to n adaptor	Stage 2 Pipeline automatic internal implementation n to 1 adaptor
												AFF3CT pipeline parallel construct.
	A 3-stage pipeline using the AFF3CT DSEL [5] has
	been implemented:
	1 Copy image I t (sequential stage)
	2 Costly processing tasks from hysteresis to morphological thresholding (parallel stage)	-Dependency: stage 3 tasks require memorized t -1 statistics
	3 Lightweight processing tasks from k-NN to tracking (sequential stage)	• Tracking is mainly a sequential task, history management of statistics
								METEORS AUTOMATIC DETECTION EFFICIENCY
		0.7 0.8															Ground truth (ref.)	Automatic detection
	Duration (s)	0.2 0.3 0.4 0.5 0.6
		0.1
		0	1	2	3	4	5	6	7	8	9	10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
															Meteor id

blob of pixels CCs = list of regions, surface S & centroid (x G , y G ) sub-list of CCs with S ∈ [S min , S max ] list of (t + 0,t + 1) matchings translation & rotation CCs speed (v x , v y ) & stats ēt , σ t initial list of meteors / stars final list of meteors Computer-vision detection detailed chain. • Source code available on GitHub: https://github.com/alsoc/fmdt R TASKS GRAPH AND MULTI-THREADING WITH AFF3CT • Design choice: most tasks of stage 3 are parallel but they are run on a single thread -Image processing results from I t are memorized for iteration t + 1


domain: sdv sde

text:
Laure Mamy

Pauline Vrignaud

Nathalie Cheviron

Francois Perreau

Mehdi Belkacem

Agathe Brault

Sébastien Breuil

Ghislaine Delarue

Jean Pierre Petraud

Isabelle Touton

François Perreau

Jean-Pierre Pétraud

Christian Mougin

Chaplain  Véronique

No evidence for effect of soil compaction on the degradation and impact of isoproturon

Keywords:

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers,

Introduction

Soil is a non-renewable resource which performs many functions and delivers services vital to human activities and ecosystems survival. However, the capacity of soil to keep on fully performing its broad variety of crucial functions is damaged by several threats, and among them chemical contamination by pesticides and compaction (Directive 2006/0086/EC). Compaction due to agricultural practices (farm traffic, soil tillage, short rotations…) leads to modifications in soil physical properties such as a decrease in porosity, air content or water infiltration that can modify the biological functioning of soil with, for example, creation of anaerobic media [START_REF] Dick | Soil enzyme activities as integrative indicators of soil health[END_REF][START_REF] Hamza | Soil compaction in cropping systems. A review of the nature, causes and possible solutions[END_REF]. As a consequence, these modifications might change the fate and impact of pesticides in soils. But, to the best of our knowledge, no results have been yet published in the literature.

Isoproturon (N,N-dimethyl-N'-[4-(1-methylethyl)phenyl]-urea) is a selective herbicide used against annual grasses and broad-leaved weeds. It is one of the most used herbicide in European cereals production [START_REF] Sørensen | Microbial degradation of isoproturon and related phenylurea herbicides in and below agricultural fields[END_REF]). In the soil, the degradation of isoproturon is well known: it is mainly biological [START_REF] Sørensen | Microbial degradation of isoproturon and related phenylurea herbicides in and below agricultural fields[END_REF] with laboratory half-life ranging from 6 to 223 days [START_REF] Walker | Spatial variability in the degradation rates of isoproturon and chlorotoluron in a clay soil[END_REF][START_REF] Alletto | Effects of temperature and water content on degradation of isoproturon in three soil profiles[END_REF]. The main degradation pathway leads to the formation of three metabolites: monodesmethyl-isoproturon, didesmethyl-isoproturon and 4-isopropylaniline [START_REF] Sørensen | Microbial degradation of isoproturon and related phenylurea herbicides in and below agricultural fields[END_REF][START_REF] Alletto | Effects of temperature and water content on degradation of isoproturon in three soil profiles[END_REF]). On the contrary, the effects of isoproturon on the biological functioning of soil and on soil organisms were less studied. Some results showed a low ecotoxicity of isoproturon (Agritox 2009).

Enzyme activities are relevant indicators of soil health that have been successfully used to discriminate a wide range of soil management practices including amendments, xenobiotics spreading, and landscapes disturbance [START_REF] Dick | Soil enzyme activities as integrative indicators of soil health[END_REF]). Among these enzymes, β-glucosidase has a critical role in releasing low molecular weight sugars that are important sources of energy for micro-organisms, and catalyzes the hydrolysis of cellobiose thus playing a major role in the initial phases of the decomposition of organic C compounds [START_REF] Eivazi | Glucosidases and galactosidases in soils[END_REF][START_REF] Dick | Soil enzyme activities as integrative indicators of soil health[END_REF].

Therefore, the aim of this work was to study the effect of soil compaction on (1) the degradation of isoproturon, (2) the impact of this herbicide assessed through the β-glucosidase activity.

Experimental

Soil samples

Undisturbed soil samples were taken, using plastic rings (5 cm diameter, 2 cm height), in the 2-4 cm layer of a plot located in a French experimental site (La Cage, INRA, Versailles, France). The samples were randomly collected in the totality of the plot in April 2008. The soil is a loam with 17.3% clay, 61.1% loam, 21.6% sand, 1.69% of organic matter and pH in water of 7.3. The field was cropped with oilseed rape under intensive agriculture practices and was previously treated with isoproturon in 2002, 2004 and 2006. The soil samples were prepared at three realistic levels of compaction (no, moderate and high) so that the increase in bulk density was 0.3 g cm -3 between no and high compaction, as observed following wheeling [START_REF] Défossez | Modeling change in soil compaction due to agricultural traffic as a function of soil water content[END_REF]) (Table 1). Moderate and high compaction resulted in a reduction in soil volume of 10% and 20%, respectively. Compaction was applied uniformly on the soil surface with a cylinder having a diameter equal to the inner diameter of the cylinders.

For each level of compaction, the physical properties of the soil samples were characterized (Table 1): the bulk densities (ρ) of three randomly selected samples were measured, then the porosity (P), the pore volume (Vp), the water (Vw) and air (Va) contents, and the degree of saturation (s) were calculated as follows:

P = 1 -(ρ / 2.65)
where 2.65 is the particle density of soil solids;

Vp (cm 3 ) = Volume of soil sample -(Mass of dry soil / 2.65);

Vw (cm 3 ) = Initial soil water content + Volume of isoproturon added;

Va (cm 3 ) = Vp -Vw; s (%) = (Vw / Vp)  100.
The average dry weight of twelve soil samples was measured and was equal to 51.3 ± 4.8 g.

Chemicals

Isoproturon and two of its metabolites in soil (monodesmethyl-isoproturon, didesmethylisoproturon) were purchased from Dr Ehrenstorfer GmbH (Augsburg, Germany) with 99.0%, 99.5% and 99.0% purity for isoproturon, monodesmethyl-isoproturon and didesmethyl-isoproturon, respectively. A 20 mg L -1 aqueous solution of isoproturon was prepared in water and methanol (99.7/0.3; v/v). In addition, standard solutions of isoproturon and metabolites were prepared in acetonitrile at concentrations ranging from 5 to 50 mg L -1 .

Incubation procedure

The samples were placed in 500 mL hermetically stoppered jars. Two millilitres of isoproturon solution were added on the surface of soil to reach a final concentration of herbicide of 0.75 mg kg -1 dry soil, corresponding approximately to application rates of 1 kg ha -1 . Isoproturon-free not compacted soil samples were also incubated as control to study the effect of the herbicide on glucosidase activity (see below).

Each jar contained a vial with 10 mL of water to keep the relative humidity constant. Soil samples were incubated at 18  1°C in the dark, for 63 days. Jars were opened weekly to maintained aerobic conditions, and soil water content was periodically adjusted by weighing each sample and adding the required amount of water. At 0, 2, 7, 14, 28, 63 days after the beginning of the incubation, soil samples were analysed for isoproturon and its metabolites, and enzyme activity (see below). Six replicates were done for each compaction, and sampling dates (three replicates for chemical analyses and three replicates for enzyme activity analyses).

Chemical analysis

Soil samples were sequentially extracted three times (for 24, 5 and 24 hours) with 150 mL of methanol. They were mechanically shaken at 20  2°C in the dark and then centrifuged for 20 minutes at 1800  g. Average recovery of isoproturon was 93.3  6.0%.

The three successive methanol extracts of each soil sample were pooled. They were concentrated using a rotary evaporator (Büchi, Flawil, Switzerland) under vacuum, and filtered through a syringe-PTFE filter (0.45 µm, Millipore, Molsheim, France). HPLC-UV analyses were performed with a Dionex (Voisins le Bretonneux, France) system, including an ASI100 autosampler, a P580 Pump, a STH585 column oven and a UVD340S UVdiode-array detector. Separation of isoproturon was conducted on an Nucleodur C8 column (250  4.6 mm i.d., 5 m granulometry; Macherey-Nagel, Hoerdt, France), with a gradient of water/acetonitrile as mobile phase at 1 mL min -1 . Samples were kept at 4°C in the autosampler before being injected (30 L). Quantification was done at 250 nm.

β-glucosidase activity

The activity of β-glucosidase (EC 3.2.1.21) was measured according to the method of [START_REF] Eivazi | Glucosidases and galactosidases in soils[END_REF] at the soil pH. Each soil sample was homogenized, then 1 g of soil was dissolved in 4 mL water (MilliQ, Millipore) followed by the addition of 1 mL of 0.05 M p-nitrophenyl-β-Dglucopyranoside. Samples were vortexed and incubated for 2 hours at 25°C. One millilitre of 0.5 M CaCl2 and 4 mL of 0.5 M NaOH were then added and the mixture was agitated. Finally, 1 mL of the suspension was centrifuged 2 min at 12000  g and the absorbance of the supernatant was determined by UV spectrophotometer at 410 nm. Three replicates were done for each soil sample.

Data analysis

Herbicide degradation was described using single first-order kinetics:

C(t) = Co exp(-kt)
where C(t) is amount of remaining extractable herbicide (% of initial applied dose) at time t, Co is initial extractable percentage of herbicide, and k the first-order rate constant of degradation (day -1 ).

The values of k were determined by non-linear regression (Marquardt-Levenberg algorithm, SigmaPlot, SPSS Inc., Chicago, IL, USA) and were used to calculate the herbicide degradation halflives (T1/2) with the following equation:

T1/2 (days) = ln(2) / k.
Statistical analyses were done with XLstat (AddinSoft, Brooklyn, NY, USA). The impact of isoproturon on β-glucosidase activity was tested by the Mann-Whitney test, and the effects of soil compaction on isoproturon degradation and -glucosidase activity were tested by the Kruskal-Wallis test. In addition, the Dunn test was done with the correction of Bonferroni for pairwise comparison between compaction conditions. The effects were considered significant when P < 0.05.

Results and discussion

Effect of soil compaction on the degradation of isoproturon

In any case, the degradation of isoproturon fitted well a first-order kinetic (r 2 > 0.89) (Table 2, Fig. 1a). However, the model deviated slightly from observed values at the end of incubation, probably because of lowest availability of isoproturon with time due to long-term sorption phenomenon, including non-extractable residues formation [START_REF] Alletto | Effects of temperature and water content on degradation of isoproturon in three soil profiles[END_REF]. Several other models (like biexponential) were tested to fit the data but they did not allow a better description of the observations (data not shown).

Degradation did not evidence a lag phase indicating that no adaptation of microorganisms was necessary, and that isoproturon was co-metabolized. The half-lives of isoproturon, according to the adjustment with the first-order kinetic model, were 11.9, 17.3 and 10.5 days in the not, moderately and highly compacted soils, respectively (Table 2). They are in agreement with the lowest values found in the literature probably because of accelerated degradation due to several previous applications of isoproturon in the field in combination with a soil pH higher than 7 [START_REF] Cox | Evidence for the accelerated degradation of isoproturon in soils[END_REF][START_REF] Walker | Spatial variability in the degradation rates of isoproturon and chlorotoluron in a clay soil[END_REF].

No significant modification in the degradation of isoproturon with compaction was observed (Fig 1a), except a difference between the moderately and not compacted soils after 63 days. Though compaction can facilitate the contact between isoproturon and soil constituents therefore decrease its bioavailability for microorganisms (by adsorption phenomena) [START_REF] Sørensen | Microbial degradation of isoproturon and related phenylurea herbicides in and below agricultural fields[END_REF], there was no increase in the persistence of isoproturon. On the contrary, the degradation of isoproturon proceeded slightly faster in the highly compacted soil (Table 2), probably because the water content (or degree of saturation) was higher than in the moderately and not compacted soils (Table 1) [START_REF] Alletto | Effects of temperature and water content on degradation of isoproturon in three soil profiles[END_REF].

The lack of significant modification in isoproturon degradation with soil compaction can be related to the results of [START_REF] Shestak | Compaction alters physical but not biological indices of soil health[END_REF] and [START_REF] Gregory | Physical resilience of soil to field compaction and the interactions with plant growth and microbial community structure[END_REF] showing that compaction generally did not affect microbial communities and processes (in laboratory compacted soils and in durably compacted soils in the field) because of reduction in porosity favouring smaller, habitable pore volume accessible primarily to bacteria and fungi. Soil respiration is also known to be unaffected if more than 10% of the pore volume is air-filled (Table 1) [START_REF] Shestak | Compaction alters physical but not biological indices of soil health[END_REF].

As the degradation of isoproturon is mainly biological [START_REF] Sørensen | Microbial degradation of isoproturon and related phenylurea herbicides in and below agricultural fields[END_REF], it is not modified by soil compaction. In addition, because applied on soil surface (as often in crop treatment), the herbicide might have been not uniformly distributed in the soil samples and mainly been located on the surface. Its fate would have been therefore less influenced by compaction. However, this is representative of field conditions, particularly if no rainfall occurs to facilitate the infiltration of pesticides after their application. Independently of compaction, the formation of the monodesmethyl-isoproturon metabolite was observed (Fig. 1b) but not that of didesmethyl-isoproturon. This is in agreement with other results concerning the degradation of isoproturon in the soil [START_REF] Sørensen | Microbial degradation of isoproturon and related phenylurea herbicides in and below agricultural fields[END_REF][START_REF] Alletto | Effects of temperature and water content on degradation of isoproturon in three soil profiles[END_REF]. The maximum amounts of monodesmethyl-isoproturon were 5.1 ± 0.8% in the not compacted soil after 7 days, 5.0 ± 0.3% in the moderately compacted soil at the end of incubation and 3.8 ± 0.6% in the highly compacted soil 14 days after treatment. In addition, two unidentified polar metabolites were detected (maximum amounts of 6.2  0.4% after 14 days and 10.5  4.1% after 28 days) that can be 4-isopropylaniline and/or hydroxylated metabolites [START_REF] Sørensen | Microbial degradation of isoproturon and related phenylurea herbicides in and below agricultural fields[END_REF][START_REF] Alletto | Effects of temperature and water content on degradation of isoproturon in three soil profiles[END_REF]. The formation kinetics of these three metabolites were not significantly different among the three levels of compaction with the exception of the amounts of monodesmethyl-isoproturon in the moderately compacted soil that are different from those of the not and highly compacted soils after 63 days. This can be related to the different behaviour of isoproturon in this soil 63 days after treatment (see above).

In the conditions of this experiment, our results showed that soil compaction did not modify the degradation of isoproturon, neither the formation rates nor the nature of its metabolites.

Therefore, the persistence of pesticides in the field is not expected to increase under zones that are compacted because of traffic, tillage or short rotations.

Effect of soil compaction on β-glucosidase activity

The kinetics of β-glucosidase activity showed the same trends in all experiments (Fig. 2a,b). There was an increase in the activity till 28 days followed by a decrease till the end of incubation. Similar trends were observed in soils treated with fungicides like mefenoxam [START_REF] Demanou | Structural and functional diversity of soil microbial communities as a result of combined applications of copper and mefonoxam[END_REF] but not with the herbicide 2,4-D [START_REF] Bécaert | Effect of 2,4-D contamination on soil functional stability evaluated using the relative soil stability index (RSSI)[END_REF], however, the applied dose was considerably higher than in our study. The increase may reflect the degradation of dead cell walls after isoproturon application as β-glucosidase is involved in the degradation steps of complex sugars which are important constituents of plant and fungal cell walls [START_REF] Demanou | Structural and functional diversity of soil microbial communities as a result of combined applications of copper and mefonoxam[END_REF]). The following decrease may result from a decrease in microbial biomass [START_REF] Waldrop | Linking microbial community composition to function in a tropical soil[END_REF] rather than exhaustion of Csubstrates and nutrients [START_REF] Monkiedje | Soil quality changes resulting from the application of the fungicides mefenoxam and metalaxyl to a sandy loam soil[END_REF] or air-drying of soil [START_REF] Bandick | Field management effects on soil enzyme activities[END_REF] as the soil moisture was constant all along the experiment.

No significant impact of isoproturon on the β-glucosidase activity was observed compared to the control (Fig. 2a). Unlike what was evidenced for other pesticides (Monkiedje et al. Bécaert al. 2006), there was no decrease in β-glucosidase activity after application of isoproturon.

The lack of effect of isoproturon on the activity can be due to the adaptation of microorganisms following the previous applications of the herbicide in the field [START_REF] Cox | Evidence for the accelerated degradation of isoproturon in soils[END_REF].

In general, compaction did not modify significantly the impact of isoproturon on βglucosidase (Fig. 2b). However, the activity in the moderately compacted soil was different from those of the not and highly compacted soils at the beginning of incubation (day 0), and after 14 and 63 days. The initial difference in the activity might explain the differences in isoproturon degradation and monodesmethyl-isoproturon formation in this soil compared to the other soils (see above), as soil enzymes are the mediators of detoxification of xenobiotics [START_REF] Dick | Soil enzyme activities as integrative indicators of soil health[END_REF]).

Nevertheless, the general trend showed no modification in the β-glucosidase activity following compaction. This result is in agreement with previous studies showing that compaction was without effect on enzyme activities (dehydrogenase, protease, phosphatase), and is of little consequence on the microbial communities [START_REF] Shestak | Compaction alters physical but not biological indices of soil health[END_REF][START_REF] Gregory | Physical resilience of soil to field compaction and the interactions with plant growth and microbial community structure[END_REF][START_REF] Tan | Soil compaction and forest floor removal reduced microbial biomass and enzyme activities in a boreal aspen forest soil[END_REF].

As a result, the impact of isoproturon on β-glucosidase activity was not affected by soil compaction, suggesting that in the field, the biological functioning of soil might not be different under the compacted zones and the less compacted ones.

Conclusion

The effects of soil compaction on the degradation and impact of isoproturon were studied in laboratory. Our experimental conditions were closed to the field ones: undisturbed soil samples, application of pesticide on soil surface, same water contents in all samples. To our knowledge, these are the first results concerning the interactions between soil compaction and the degradation and impact of a pesticide. In the conditions of this experiment, compaction did not modify the degradation of isoproturon, neither the formation rates nor the nature of its metabolites. In addition, compaction did not modify the impact of isoproturon on β-glucosidase activity. Therefore, our results suggest that under soils compacted zones (due to traffic, tillage or short rotations), the persistence of pesticides should not increase and their impact should not be modified. However, further studies measuring additional biological indicators (phospholipids fatty acids, microbial biomass…), studying the relationship between compaction and the degree of soil saturation, and studying the overall balance of the fate of pesticides (mineralization, extractability, formation of non-extractable residues) should be performed.

Fig. 1

 1 Fig. 1 Degradation kinetics of isoproturon (a) and formation kinetics of monodesmethylisoproturon (b) in () not compacted, (------) moderately compacted and (  ) highly compacted soil. For isoproturon, lines are adjustment with first-order kinetics. The degradation of isoproturon and the formation rates of its metabolite were not significantly modified by compaction.

Fig. 2

 2 Fig. 2 β-glucosidase activity in (a) not compacted soil treated () or not () with isoproturon; and (b) () not compacted, (------) moderately compacted, (  ) highly compacted soil treated with isoproturon. The β-glucosidase activity was not significantly affected by isoproturon and by compaction.

Table 1 .

 1 Soil physical properties as a function of compaction

Table 2 .

 2 Isoproturon degradation rates, initial concentrations, halflives and correlation coefficients estimated according to single firstorder kinetic

Acknowledgement The authors are grateful to Dr Jérémie D. Lebrun for constructive comments and to Dr Florent Allais, Rachid Benabdallah and Cédric Repinçay of INRA for complementary chemical analyses.