Sandrine Blazy

Vincent Laporte

David Pichardie

Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code *

Static analysis of binary code is challenging for several reasons. In particular, standard static analysis techniques operate over control flow graphs, which are not available when dealing with self-modifying programs which can modify their own code at runtime. We formalize in the Coq proof assistant some key abstract interpretation techniques that automatically extract memory safety properties from binary code. Our analyzer is formally proved correct and has been run on several self-modifying challenges, provided by Cai et al. in their PLDI 2007 paper.

Introduction

Abstract interpretation [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] provides advanced static analysis techniques with strong semantic foundations. It has been applied on a large variety of programming languages. Still, specific care is required when adapting these techniques to lowlevel code, specially when the program to be analyzed comes in the form of a sequence of bits and must first be disassembled. Disassembling is the process of translating a program from a machine friendly binary format to a textual representation of its instructions. It requires to decode the instructions (i.e., understand which instruction is represented by each particular bit pattern) but also to precisely locate the instructions in memory. Indeed instructions may be interleaved with data or arbitrary padding. Moreover once encoded, instructions may have various byte sizes and may not be well aligned in memory, so that a single byte may belong to several instructions.

To thwart the problem of locating the instructions in a program, one must follow its control flow. However, this task is not easy because of the indirect jumps, whose targets are unknown until runtime. A static analysis needs to know precisely enough the values that the expression denoting the jump target may evaluate to. In addition, instructions may be produced at runtime, as a result of the very execution of the program. Such programs are called self-modifying programs; they are commonly used in security as an obfuscation technique, as well as in just-in-time compilation. Analyzing a binary code is mandatory when this code is the only available part of a software. Most of standard reverse engineering tools (e.g., IDA Pro) cannot disassemble and analyze self-modifying programs.

In order to disassemble and analyze such programs, one must very precisely understand which instructions are written and where. And for all programs, one must check every single memory write to decide whether it modifies the program code.

Self-modifying programs are also beyond the scope of the vast majority of formal semantics of programming languages. Indeed a prerequisite in such semantics is the isolation and the non-modification of code in memory. Turning to verified static analyses, they operate over toy languages [START_REF] Cachera | A Certified Denotational Abstract Interpreter[END_REF][START_REF] Nipkow | Abstract Interpretation of Annotated Commands[END_REF] or more recently over realistic C-like languages [START_REF] Stewart | Verified heap theorem prover by paramodulation[END_REF][START_REF] Blazy | Formal Verification of a C Value Analysis Based on Abstract Interpretation[END_REF], but they assume that the control-flow graph is extracted by a preliminary step, and thus they do not encompass techniques devoted to self-modifying code.

In this paper, we formalize with the Coq proof assistant, key static analysis techniques to predict the possible targets of the computed jumps and make precise which instructions alter the code and how, while ensuring that the other instructions do not modify the program. Our static analysis techniques rely on two main components classically used in abstract interpretation, abstract domains and fixpoint iterators, that we detail in this paper. The complete Coq development is available online [START_REF]Companion website[END_REF].

Our formalization effort is divided in three parts. Firstly, we formalize a small binary language in which code is handled as regular mutable data. Secondly, we formalize and prove correct an abstract interpreter that takes as input an initial memory state, computes an over-approximation of the reachable states that may be generated during the program execution, and then checks that all reachable states maintain memory safety. Finally, we extract from our formalization an executable OCaml tool that we run on several self-modifying challenges, provided by Cai et al. [START_REF] Cai | Certified Self-Modifying Code[END_REF].

The paper makes the following contributions. -We push further the limit in terms of verified static analysis by tackling the specific challenge of binary self-modifying programs, such as fixpoint iteration without control-flow graph and simple trace partitioning [START_REF] Kinder | Towards static analysis of virtualization-obfuscated binaries[END_REF]. -We provide a complementary approach to [START_REF] Cai | Certified Self-Modifying Code[END_REF] by automatically inferring the required state invariants that enforce memory safety. Indeed, the axiomatic semantics of [START_REF] Cai | Certified Self-Modifying Code[END_REF] requires programs to be manually annotated with invariants written in a specific program logic. The remainder of this paper is organized as follows. First, Section 2 briefly introduces the static analysis techniques we formalized. Then, Section 3 details our formalization: it defines the semantics of our low-level language and details our abstract interpreter. Section 4 describes some improvements that we made to the abstract interpreter, as well as the experimental evaluation of our implementation. Related work is discussed in Section 5, followed by concluding remarks.

Disassembling by Abstract Interpretation

We now present the main principles of our analysis on the program shown in Figure 1. It is printed as a sequence of bytes (on the extreme left) as well as under a disassembled form (on the extreme right) for readability purposes. This program, as we will see, is self-modifying, so these bytes correspond to the initial content of the memory from addresses 0 to 11. The remaining of the memory (addresses in r´2 32 ; ´1s Y r12; 2 32 ´1s), as well as the content of the registers, is unknown and can be regarded as the program input.

All our example programs target a machine operating over a low-level memory made of 2 32 cells, eight registers (R0, . . . R7), and flags -boolean registers that are set by comparison instructions. Each memory cell or register stores a 32 bits integer value, that may be used as an address in the memory. Programs are stored as regular data in the memory; their execution starts from address zero. Nevertheless, throughout this paper we write the programs using the following custom syntax. The instruction cst v Ñ r loads register r with the given value v; cmp r, r' denotes the comparison of the contents of registers r and r'; gotoLE d is a conditional jump to d, it is taken if in the previous comparison the content of r' was less than or equal to the one of r; goto d is an unconditional jump to d. The instruction load *r Ñ r' and store r' Ñ *r denote accesses to memory at the address given in register r; and halt r halts the machine with as final value the content of register r.

The programming language we consider is inspired from x86 assembly; notably instructions have variable size (one or two bytes, e.g., the length of the instruction stored at line 1 is two bytes) and conditional jumps rely on flags. In this setting, a program is no more than an initial memory state, and a program point is simply the address of the next instruction to execute. In order to understand the behavior of this program, one can follow its code as it is executed starting from the entry point (byte 0). The first instruction compares the (statically unknown) content of two registers. This comparison modifies only the states of the flags. Then, depending on the outcome of this comparison, the execution proceeds either on the following instruction (stored at byte 3), or from byte 5. Executing the block from byte 5 will modify the byte 2 belonging to the gotoLE instruction (highlighted in Figure 1); more precisely it will change the jump destination from 5 to 4: the store R0 Ñ *R2 instruction writes the content of register R0 (namely 4) in memory at the address given in register R2 (namely 2). Notice that a program may directly read from or write to any memory cell: we assume that there is no protection mechanism as provided by usual operating systems. After the modification is performed, the execution jumps back to the modified instruction, jumps to byte 4 then halts, with final value the content of register R1.

This example highlights that the code of a program (or its control-flow graph) is not necessarily a static property of this program: it may vary as the program runs. To correctly analyze such a program, one must discover, during the fixpoint iteration, the two possible states of the instruction at locations 1 and 2 and its two possible targets. More specially, we need at least to know, for each program point (i.e., memory location), which instructions may be decoded from there when the execution reaches this point. This in turn requires to know what are the values that the program operates on. We therefore devise a value analysis that computes, for each reachable program point (i.e., in a flow sensitive way) an over-approximation of the content of the memory and the registers, and the state of the flags when the execution reaches that point.

The analysis relies on a numeric abstract domain N 7 that provides a representation for sets of machine integers (γ N P N 7 Ñ Ppintq) and abstract arithmetic operations. Relying on such a numeric domain, one can build abstract transformers that model the execution of each instruction over an abstract memory that maps locations (i.e., memory addresses3 and registers) to abstract numeric values. An abstract state is then a mapping that attaches such an abstract memory to each program point of the program, and thus belongs to addr Ñ `paddr `regq Ñ N 7 ˘.

To perform one abstract execution step, from a program point pp and an abstract memory state m 7 that is attached to pp, we first enumerate all instructions that may be decoded from the set γ N pm 7 pppqq. Then for each of such instructions, we apply the matching abstract transformer. This yields a new set of successor states whose program points are dynamically discovered during the fixpoint iteration.

The abstract interpretation of a whole program iteratively builds an approximation executing all reachable instructions until nothing new is learned. This iterative process may not terminate, since there might be infinite increasing chains in the abstract search space. As usual in abstract interpretation, we accelerate the iteration using widening operations [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. Once a stable approximation is finally reached, an approximation of the program listing or control-flow graph can be produced.

To illustrate this process, Figure 2 shows how the analysis of the program from Figure 1 proceeds. We do not expose a whole abstract memory but only the underlying control-flow graph it represents. On this specific example, three Initially, at iteration 0, only program point 0 is known to be reachable and the memory is known to exactly contain the program, denoted by the first control-flow graph. The only successor of point 0 is point 1 and it is updated at the next iteration. After a few iterations, point 9 is reached and the abstract control-flow graph a is updated into a control-flow graph b that is propagated to point 10. After a few more iterations, the process converges.

In addition to a control-flow graph or an assembly listing, more properties can be deduced from the analysis result. We can prove safety properties about the analyzed program, like the fact that its execution is never stuck. Since the semantics only defines the good behaviors of programs, unsafe programs reach states that are not final and from which no further execution step is possible (e.g., the byte sequence at current program point is not the valid encoding of an instruction).

The analysis produces an over-approximation of the set of reachable states. In particular, a superset of the reachable program points is computed, and for each of these program points, an over-approximation of the memory state when the execution reaches this program point is available. Thus we can check that for every program point that may be reached, the next execution step from this point cannot be stuck. This verification procedure is formally verified, as described in the following section.

The static analyzer is specified, programmed and proved correct using the Coq proof assistant. This involves several steps that are described in this section: first, define the semantics of a binary language, then design abstract domains and abstract transformers, as well as write a fixpoint iterator, and lastly state and prove soundness properties about the results of the static analysis.

Concrete Syntax and Semantics

The programming language in which are written the programs to analyze is formalized using the syntax shown on Figure 3. So as to model a binary language, we introduce a decoding function dec (mem: (addr Ñ int)) (pp: int) : option (instruction * nat) that given a memory mem (i.e., a function from addresses to values) and an address pp yields the instruction stored from this address along with its byte size. Since not all integer sequences are valid encodings, this decoding may fail (hence the option type4 ). In order to be able to conveniently write programs, there is also a matching encoding function. However the development does not depend on it at all. The language semantics is given as a small-step transition relation between machine states. A machine state may be xpp, f, r, my where pp is the current program point (address of the next instruction to be executed), f is the current flag state, r is the current register state, and m is the current memory. Such a tuple is called a machine configuration (type machine_config). Otherwise, a machine state is rvs, meaning that the program stopped returning the value v.

The semantics is defined as a set of rules of the following shape:

dec m pp = tpi, zqu xpp, f, r, my ù xpp', f', r', m'y .
The premise states that decoding the bytes in memory m from address pp yields the instruction i whose size in memory is z. Then each rule describes how to execute a particular instruction at program point pp in memory m with flag state f and register state r. In each case, most of the state is kept unchanged. Instructions that are not branching proceed their execution at program point pp+z (since z is the size of this instruction once encoded). The whole set of rules can be found in the Coq development [START_REF]Companion website[END_REF]. We describe only some of them. Finally, we define the semantics vPw of a program P as the set of states that are reachable from an initial state, with current program point zero and memory P (where ù ‹ denotes the reflexive-transitive closure of the small-step relation).

vPw " ts | Df r, x0, f, r, Py ù ‹ su

Abstract Interpreter

In order to analyze programs, we build an abstract interpreter, i.e., an executable semantics that operates over abstract elements, each of them representing many concrete machine configurations. Such an abstract domain provides operators that model basic concrete operations: read a value from a register, store some value at some address in memory, and so on. The static analyzer then computes a fixpoint within the abstract domain, that over-approximates all reachable states of the analyzed program.

We first describe our abstract domain before we head to the abstract semantics and fixpoint computation. An abstract memory domain is a carrier type along with some primitive operators whose signatures are given in Figure 4. The ab_num type refers to a numeric abstract domain, as described in [START_REF] Blazy | Formal Verification of a C Value Analysis Based on Abstract Interpretation[END_REF]: we only require that this type is equipped with a concretization to sets of machine integers and abstract transformers corresponding to arithmetic operations.

The carrier type ab_mc is equipped with a lattice structure. An object of this type represents a set of concrete machine states, as described by the primitive gamma. It can be queried for the values stored in some register (var) or at some known memory address (load_single); these operators return an abstract numeric value. Other operators enable us to alter an abstract state, like assign that sets the contents of a register to a given abstract numeric value, and store_single that similarly updates the memory at a given address.

All these operators obey some specifications. As an example, the load_sound property states that given a concrete state m in the concretization of an abstract state ab, the concrete value stored at any address a in m is over-approximated by the abstract value returned by the matching abstract load. The γ symbol is overloaded through the use of type classes: its first occurrence refers to the concretization from the abstract memory domain (the gamma field of record mem_dom) and its second occurrence is the concretization from the numeric domain ab_num.

Record mem_dom (ab_num ab_mc: Type) := { as_wl: weak_lattice ab_mc ; var: ab_mc Ñ reg Ñ ab_num ; load_single: ab_mc Ñ addr Ñ ab_num ; store_single: ab_mc Ñ addr Ñ ab_num Ñ ab_mc ; assign: ab_mc Ñ reg Ñ ab_num Ñ ab_mc (* more abstract operators omitted *) ; gamma: gamma_op ab_mc machine_config ; as_adom : adom ab_mc machine_config as_wl gamma ; load_sound: @ ab:ab_mc, @ m: machine_config, m P γ(ab) Ñ @ a:addr, m(a) P γ(load_single ab a) (* more properties omitted *) }. To prevent the domain of the ab_mem map from infinitely growing, we bound it by a finite set computed before the analysis: the analysis will try to compute some information only for the memory addresses found in this set [START_REF] Balakrishnan | WYSINWYX: What you see is not what you eXecute[END_REF]. The content of this set does not alter its soundness: the values stored at addresses not in it are unknown and the analyzer makes no assumptions about them. On the other hand, the success of the analysis and its precision depend on it. In particular, the analyzed set must cover the whole code segment.

As a second layer, we build abstract transformers over any such abstract domain. Consider for instance the abstract load presented in Figure 5; it is used to analyze any ILoad instruction (T denotes a record of type mem_dom ab_num ab_mc). The source address may not be exactly known, but only represented by an abstract numeric value a. Since any address in γ(a) may be read, we have to query all of them and take the least upper bound of all values that may be stored at any of these addresses:

Ů tT.(load_single) m x | x P γpaqu. However the set of concrete addresses may be huge and care must be taken: if the size of this set exceeds some threshold, the analysis gives up on this load and yields top, representing all possible values.

We build enough such abstract transformers to be able to analyze any instruction (function ab_post_single, shown in Figure 6). This function returns a list of possible next states, each of which being either Hlt v (the program halts returning a value approximated by v) or Run pp m (the execution proceeds at program point pp in a configuration approximated by m) or GiveUp (the analysis is too imprecise to compute anything meaningful). The computed jump (IGotoInd) also has a dedicated abstract transformer (inlined in Figure 6): in order to know from where to continue the analysis, we have to enumerate all possible targets. Then, function ab_post_many performs one execution step in the abstract. To do so, we first need to identify what is the next instruction, i.e., to decode in the abstract memory from the current program point. This may require to enumerate all concrete values that may be stored at this address. Therefore this abstract decoding either returns a set of possible next instructions or gives up. In such a case, the whole analysis will abort since the analyzed program is unknown.

Finally, the abstract semantics is iteratively applied until a fixpoint is reached following a worklist algorithm as the one found in [1, § 3.4]. However there may be infinite ascending chains, so to ensure termination we need to apply widening operators instead of regular joins frequently enough during the search.

In our setting, with no control-flow graph available, the widening is applied on every back edge, but the implementation makes it easy to try different widening strategies. So as to convince Coq that the analysis indeed terminates, we rely on a counter (known as fuel) that obviously decreases at each iteration; when it reaches zero, the analyzer must give up.

To enhance the precision, we have introduced three more techniques: a dedicated domain to abstract the flag state, a partitioning of the state space, and a use of abstract instructions. They will be described in the next section.

Soundness the Abstract Interpreter

We now describe the formal verification of our analyzer. The soundness property we ensure is that the result of the analysis of a program P over-approximates its semantics vPw. This involves on one hand a proof that the analysis result is indeed a fixpoint of the abstract semantics and on the other hand a proof that the abstract semantics is correct with respect to the concrete one.

The soundness of the abstract semantics is expressed by the following lemma, which reads: given an abstract state ab and a concrete one m in the concretization of ab, for each concrete small-step m ù m', there exists a result ab' in the list ab_post_single m.(pc) ab that over-approximates m'. Our use of Coq type classes enables us to extensively overload the γ notation and write this statement in a concise way as follows. The proof of this lemma follows from the soundness of the various abstract domains (as load_sound in Figure 4), transformers and decoder. The proof that the analyzer produces a fixpoint is not done directly. Instead, we rely on a posteriori verification: we do not trust the fixpoint computation and instead program and prove a checker called validate_fixpoint. Its specification, proved thanks to the previous lemma, reads as follows.

Lemma validate_correct : @ (P: memory) (dom: list addr) (E: AbEnv), validate_fixpoint P dom E = true Ñ vPw Ď γ(E).

Going through this additional programming effort has various benefits: a direct proof of the fixpoint iterator would be very hard; we can adapt the iteration strategy, optimize the algorithm and so on with no additional proof effort.

This validation checks two properties of the result E: that it over-approximates the initial state; and that it is a post-fixpoint of the abstract semantics, i.e., for each abstract state in the result, performing one abstract step leads to abstract states that are already included in the result. These properties, combined to the soundness of the abstract semantics, ensure the conclusion of this lemma.

Finally we pack together the iterator and the checker with another operation performed on sound results that checks for its safety. The resulting analysis enjoys the following property: if, given a program P, it outputs some result, then that program is safe.

Theorem analysis_sound : @ (P: memory) (dom: list addr) (fuel: nat) (ab_num: num_dom_index), analysis ab_num P dom fuel ‰ None Ñ safe P.

The arguments of the analysis program are the program to analyze, the list of addresses in memory to track, the counter that enforces termination and the name of the numeric domain to use. We provide two numeric domains: intervals with congruence information and finite sets.

Case Studies and Analysis Extensions

The extraction mechanism of Coq enables us to generate an OCaml program from our development and to link it with a front-end. Hence we can automatically analyze programs and prove them safe. This section shows the behavior of our analyzer on chosen examples, most of them taken from [START_REF] Cai | Certified Self-Modifying Code[END_REF] (they have been rewritten to fit our custom syntax). All examples are written in an assembly-like syntax with some syntactic sugar: labels refer to byte offsets in the encoded program, the enc(I) notation denotes the encoding of the instruction I. The study of some examples highlights the limits of the basic technique presented before and suggests to refine the analyzer as we describe below. The source code of all the examples that are mentioned thereafter is available on the companion web site [START_REF]Companion website[END_REF].

Basic Example

The multilevel runtime code generation program of Figure 7 is a program that, when executed, writes some code to line gen on and runs it; this generated program, in turn, writes some more code at line ggen and runs it. Finally execution starts again from the beginning. Moreover, at each iteration, register R6 is incremented.

The analysis of such a program follows its concrete execution and exactly computes the content of each register at each program point. It thus correctly tracks what values are written and where, so as to be able to analyze the program as it is generated.

However, when the execution reaches program point loop again, both states that may lead to that program point are merged. And the analysis of the loop body starts again. After the first iteration, the program text is exactly known, but each iteration yields more information about the dynamic content of register R6. Therefore we apply widening steps to ensure the termination of the analysis. Finally, the set of reachable program points is exactly computed and for each of them, we know what instruction will be executed from there.

Many self-modifying programs are successfully analyzed in a similar way: opcode modification, code obfuscation, and code checking [START_REF]Companion website[END_REF].

cst 0 Ñ R6 cst 1 Ñ R5 loop: add R5 Ñ R6 cst gen Ñ R0 cst enc(store R1 Ñ *R2) Ñ R1 store R1 Ñ *R0 cst enc(goto R2) Ñ R1 cst gen + 1 Ñ R0 store R1 Ñ *R0 cst ggen Ñ R2 cst loop Ñ R0 cst

A First Extension: Dealing with Flags

The example program in Figure 8 illustrates the abstract domain for the flags. This program stores the content of R0 in an array (stored in memory from address ´128 to address ´96) at the offset given in register R1. Before that store, checks are performed to ensure that the provided offset lies inside the bounds of the array. The destination address is compared against the lowest and highest addresses of the array; if any of the comparisons fails, then the store is bypassed.

To properly analyze this program, we need to understand that the store does not alter the code. When analyzing a conditional branch instruction, the abstract state is refined differently at its two targets. However, the only information we have is about one flag, whereas the comparison that sets this flag operated on the content of registers. We therefore need to keep the link between the flags and the registers.

To this end, we extend our ab_machine_config record with a field containing an optional pair of registers ab_reg: option (reg * reg). It enables the analyzer to remember which registers were involved in the last comparison (the None value is used when this information is unknown). With such information available, even though the conditional jump is not directly linked to the comparison operation, we can gain some precision in the various branches.

Indeed, when we assume that the first conditional branch is not taken, the flag state is abstracted by the pair t(R6,R1)u, so we refine our knowledge about register R1: its content is not less than the ´128. Similarly, when we assume that the second conditional branch is not taken, the abstract flag state is t(R1,R7)u, so we can finally infer that the content of register R1 is in the bounds.

This extension of the abstract domain increases a lot the precision of the analyzer on some programs, yet has little impact on the formalization: we need to explain its lattice structure (top element, order and least upper bound) and define its concretization. Then it enables us to program more precise primitives (namely compare and assume) that we must prove correct. No other part of the development is modified.

A Second Extension: Trace Partitioning

Some self-modifying programs store in the same memory space various pieces of their code. Successfully analyzing such programs requires not to merge these different code fragments, i.e., we need to distinguish in the execution which code is being run: flow sensitivity is not enough. To this end we use a specific form of trace partitioning [START_REF] Kinder | Towards static analysis of virtualization-obfuscated binaries[END_REF] that makes an analysis sensitive to the value of a particular memory location.

Consider as an example the polymorphic program [START_REF]Companion website[END_REF] that we briefly describe below. Polymorphism here refers to a technique used by for instance viruses that change their code while preserving their behavior, so as to hide their presence. The main loop of this program repeatedly adds forty-two to register R3. However, it is obfuscated in two ways. First, the source code initially contains a jump to some random address. But this instruction will be overwritten before it is executed. Second, this bad instruction is written back, but at a different address. So when the execution reaches the beginning of the loop, the program stored in memory is one of two different versions, both featuring the unsafe jump.

When analyzing this program, the abstract state computed at the beginning of the loop must over-approximate the two program versions. Unfortunately it is not possible to analyze the mere superposition of both versions, in which the unsafe jump may occur. The two versions can be distinguished through, for instance, the value at address 12. We therefore prevent the merging of any two states that disagree on the value stored at this address. Two different abstract states are then computed at each program point in the loop, as if the loop were unrolled once.

More generally, the analysis is parametrized by a partitioning criterion δ: ab_mcÑint that maps abstract states to values (the criterion used in this example maps an abstract state m to the value stored at address 12 in all concrete states represented by m; or to an arbitrary constant if there may be many values at this address). No abstract states that differ according to this criterion are merged. Taking a constant criterion amounts to disabling this partitioning. The abstract interpreter now computes for each program point, a map from criterion values to abstract states (rather than only one abstract state). Given such an environment E, a program point pp, and a value v, if there is an abstract state m such that Epppqpvq " tmu, then δpmq " v. Such an environment E represents the following set of machine configurations: γpEq " tc P machine_config | Dv, c P γ pEpc.pcqpvqqu

To implement this technique, we do not need to modify the abstract domain, but only the iterator and fixpoint checker. The worklist holds pairs (program point, criterion value) rather than simple program points, and the iterator and fixpoint checker (along with its proof) straightforwardly adapted. The safety checker does not need to be updated since we can forget the partitioning before applying the original safety check.

Thanks to this technique, we can selectively enhance the precision of the analysis and correctly handle challenging self-modifying programs: control-flow modification, mutual modification, and code encryption [START_REF]Companion website[END_REF]. However, the analyst must manually pick a suitable criterion for each program to analyze.

A Third Extension: Abstract Decoding

The program in Figure 9 computes the n th Fibonacci number in register R2, where n is an input value read from address ´1 and held in register R0. There is a for-loop in which register R1 goes from 1 to n and some constant value is added to register R2. The trick is that the actual constant (which is encoded as part of an instruction and is stored at the address held in R6) is overwritten at each iteration by the previous value of R2.

When analyzing this program, we cannot infer much information about the content of the patched cell. Therefore, we cannot enumerate all instructions that may be stored at the patched point. So we introduce abstract instructions: instructions that are not exactly known, but of which some part is abstracted by a suitable abstract domain. Here we only need to abstract values using a numeric domain. With such a tool, we can decode in the abstract: the analyzer does not recover the exact instructions of the program, but only the information that some (unknown) value is loaded into register R4, which is harmless (no stores and no jumps depend on it).

This self-modifying code pattern, in which only part of an instruction is overwritten occurs also in the vector dot product example [START_REF]Companion website[END_REF] where specialized multiplication instructions are emitted depending on an input vector.

The techniques presented here enable us to automatically prove the safety of various self-modifying programs including almost all the examples of [START_REF] Cai | Certified Self-Modifying Code[END_REF]. Out of twelve, only two cannot be dealt with. The self-replicating example is a program that fills the memory with copies of itself: the code, being infinite, cannot be represented with our abstract domain. The bootloader example does not fit in the considered machine model, as it calls BIOS interrupts and reads files. Our Coq development [START_REF]Companion website[END_REF] features all the extensions along with their correctness proofs. Most of the previous works on mechanized verification of static analyzes focused on standard data-flow frameworks [START_REF] Klein | A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler[END_REF] or abstract interpretation for small imperative structured languages [START_REF] Cachera | A Certified Denotational Abstract Interpreter[END_REF][START_REF] Nipkow | Abstract Interpretation of Annotated Commands[END_REF]. In a previous work [START_REF] Blazy | Formal Verification of a C Value Analysis Based on Abstract Interpretation[END_REF], we formally verified a value analysis for an intermediate language of the Compcert C compiler toolchain. The current work shares the same notion of abstract numerical domain but develops its own notion of memory abstraction, dynamic control-flow graph reconstruction and trace partitioning.

The current work formalizes more advanced abstract interpretation techniques, targeting self-modifying low-level code, and is based on several recent non-verified static analyses. A large amount of work was done by Balakrishnan et al. in this area [START_REF] Balakrishnan | WYSINWYX: What you see is not what you eXecute[END_REF]. Control-flow graph reconstruction was specially studied by Kinder et al. [START_REF] Kinder | Towards static analysis of virtualization-obfuscated binaries[END_REF] and Bardin et al. [START_REF] Bardin | Refinement-Based CFG Reconstruction from Unstructured Programs[END_REF]. Still, these works are unsound with respect to selfmodifying code. Bonfante et al. provide a paper-and-pencil operational semantics for self-modifying programs [START_REF] Bonfante | A Computability Perspective on Self-Modifying Programs[END_REF].

Our current work tackles a core subset of a self-modifying low-level programming language. More realistic formalizations of x86 semantics were proposed [START_REF] Myreen | Verified just-in-time compiler on x86[END_REF][START_REF] Morrisett | RockSalt: better, faster, stronger SFI for the x86[END_REF][START_REF] Kennedy | Coq: The world's best macro assembler?[END_REF] but none of them handles the problem of disassembling self-modifying programs. Our work complements other verification efforts of low-level programs [START_REF] Chlipala | Mostly-automated verification of low-level programs in computational separation logic[END_REF][START_REF] Cai | Certified Self-Modifying Code[END_REF][START_REF] Jensen | High-Level Separation Logic for Low-Level Code[END_REF] based on program logics. While we provide automatic inference of loop invariants, they are able to handle more expressive correctness properties.

Conclusion and Perspectives

This work provides the first verified static analyis for self-modifying programs. In order to tackle this challenge, we formalized original techniques such as controlflow graph reconstruction and partitioning. We formalized these techniques on a small core language but we managed to verify ten out of twelve of the challenges proposed in [START_REF] Cai | Certified Self-Modifying Code[END_REF].

An important further work is to scale these technique on more realistic Coq language models [START_REF] Morrisett | RockSalt: better, faster, stronger SFI for the x86[END_REF][START_REF] Kennedy | Coq: The world's best macro assembler?[END_REF]. Developing directly an analyzer on these representations may be a huge development task because of the number of instructions to handle. One strategy could be to relate on a good intermediate representation such as the one proposed by Rocksalt [START_REF] Morrisett | RockSalt: better, faster, stronger SFI for the x86[END_REF]. Our current work does not consider the specific challenge of call stack reconstruction [START_REF] Balakrishnan | WYSINWYX: What you see is not what you eXecute[END_REF] that may require some form of verified alias analysis [START_REF] Robert | A Formally-Verified Alias Analysis[END_REF]. This is an important place for further work.

Figure 2 .

 2 Figure 2. Iterative fixpoint computation

  Inductive reg := R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7. Inductive flag := FLE | FLT | FEQ. Inductive instruction := (* arithmetic *) | ICst (v:int) (dst:reg) | ICmp (src dst: reg) | IBinop (op: int_binary_operation) (src dst: reg) (* memory *) | ILoad (src dst: reg) | IStore (src dst: reg) (* control *) | IGoto (tgt: addr) | IGotoInd (r: reg) | IGotoCond (f: flag) (tgt: addr) | ISkip | IHalt (r: reg).

Figure 3 .

 3 Figure 3. Language syntax

Figure 4 .

 4 Figure 4. Signature of abstract memory domains (excerpt)

Inductive

  botlift (A:Type) : Type := Bot | NotBot (x:A). Definition load_many (m: ab_mc) (a: ab_num) : botlift ab_num := match concretize_with_care a with | Just addr_set ñ IntSet.fold (λ acc addr, acc \ NotBot (T.(load_single) m addr)) addr_set Bot | All ñ NotBot top end.

Figure 5 .

 5 Figure 5. Example of abstract transformer

Figure 6 .

 6 Figure 6. Abstract small-step semantics (excerpt)

  Lemma ab_post_many_correct :@ (m:machine_config) (m':machine_state) (ab:ab_mc), m P γ(ab) Ñ m ù m' Ñ m' P γ(ab_post_single m.(pc) ab).

Lemma

  abstract_decode_at_sound : @ (m:machine_config)(ab:ab_mc)(pp:addr), m P γ(ab) Ñ dec m.(mc_mem) pp P γ(abstract_decode_at pp ab).

Figure 9 .

 9 Figure 9. Fibonacci

  Instruction ICmp rs rd updates the flag state according to the comparison of the values held by the two involved registers. Conditional jump instruction IGotoCond c v jumps to address v or falls through to pp+z depending on the current state of flag c. Indirect jump instruction IGotoInd rd proceeds at the program point found in register rd.

Type addr is a synonym of int, the type of machine integers.

Values of type option A are either None or tau with a a value of type A.

* This work was supported by Agence Nationale de la Recherche, grant number ANR-11-INSE-003 Verasco.


Alain Gadalia
email: a.gadalia@brgm.fr

Jean-Michel Baltassat
email: jm.baltassat@brgm.fr

Vincent Bouchot
email: v.bouchot@brgm.fr

Séverine Caritg-Monnot

Frederick Gal
email: f.gal@brgm.fr

Jean-François Girard
email: jf.girard@brgm.fr

Alexis Gutierrez
email: a.gutierrez@brgm.fr

Thomas Jacob
email: t.jacob@brgm.fr

Guillaume Martelet
email: g.martelet@brgm.fr

Nicolas Coppo
email: n.coppo@brgm.fr

Setareh Rad
email: s.rad@brgm.fr

Anne-Lise Tailame
email: a.tailame@brgm.f

Hervé Traineau
email: h.traineau@cfg-brgm.fr

Benoit Vittecoq
email: b.vittecoq@brgm.fr

Pierre Wawrzyniak
email: p.wawrzyniak@brgm.fr

The Petite Anse-Diamant Geothermal System (Martinique Island, Lesser Antilles): Results of the 2012-2013 Exploration

Keywords: Flank collapse, intrusive complex, paleo-geothermal system, water-rock interaction, geothermometers, magmatic degassing, caprock doming, MT resistive body

A 2012-2013 additional and combinedgeological, hydrogeological, geochemical, geophysical -surface exploration results in a new insight of the Martinique geothermal systems, including Petite Anse -Diamant area.

The Petite Anse -Diamanthot spring is located at the foot of a small volcano -Morne Jacquelinepart of a NW-SE volcanotectonic corridor. The Southern flank of this volcano collapsed leading to the outcrop: 1) A previous neutral, high temperature hydrothermal activity corresponding to a MT conductive layer interpreted as a clay cap of the present geothermal system. The bottom of the conductive layer displays also a doming shape, characterizing the top of geothermal system; 2) A dyke of diorite coinciding with the top of a huge MT resistive body, following the volcanic corridor, and interpreted as a magma intrusion; it generates several on and off-shore spots of magmatic degassing; this intrusive gas -rock may act as a heat source and interact with the geothermal fluid. The Petite Anse spring water is of Na-Cl type due to a seawater contribution. The associated geothermal reservoir temperature is estimated at 190-210°C.

The recharge of the system is likely to be low, because of both a bad permeability resulting from the extensive acidic alteration related to previous fumarolic expression, and limited rainfalls.

An exploration drilling area is proposed at the North of the Petite Anse village.

INTRODUCTION

The project of "Additional geothermal exploration of Martinique Island (Lesser Antilles)" lies within the framework of the revival and development of renewable energy in French overseas territories (50% share of these energies in these territories by 2020). On volcanic islands such as Martinique, geothermal energy is a priori the most promising renewable energy. This project joined the will of the French Government and the Region Martinique to go toward the energy independence of the island in 2030.

The project was co-financed by the ERDF (European Regional Development Fund), ADEME (French Agency for Environment and Energy Management), the Regional Council of Martinique, the Joint Union of Electricity in Martinique (MEMS) and BRGM (French Geological Survey).

Geothermalexploration of theMartiniqueisland

Geothermalexploration,inMartinique,begantheremore than 40 years ago. It can bedivided into threesteps: (1) late 60s, focused mainlyon the plain ofLamentin(e.g. Cormyet al, 1970.), (2) late 70s-early 80s, incorporatingplainofLamentinandMorne RougeareabetweenMount PeléeandPitonsdu Carbet(e.g.Westercamp1978; [START_REF] Iundt | Ré-évaluation géochimique du potentiel géothermique de l'île de la Martinique[END_REF] and (3)the early 2000swhen it wastargeted to thesouth and SW flanks of Mount Pelée,thePetite Ansesector (e.g. Sanjuanet al., 2003a) and, moreover, the NW of plainLamentin. The 2003 campaign (Sanjuan et al., 2003a) led toidentifythe vicinity of thePetite Anse hot springasone of the twoareasof "priority1" because of the combination ofgeophysicalanomalies,geochemicalandgeologic indices.

2012-2013 Exploration campaign

Scientifically geophysical methods have had a major contribution in this campaign [START_REF] Coppo | -3-D Magnetotelluric Investigations in Martinique (Lesser Antilles). Characteistic Deep Resistivity Structures and Shallow Resistivity Distribution Matching Heliborne TEM results[END_REF]. The magnetotelluric (MT) data acquisition, their processing and inversion / modeling used the latest methods and software. Overflying the island of Martinique by helicopter electromagnetic method (MarTEM project) yielded, on the most superficial levels (<200 m), results of an exceptional resolution, and made possible a calibration of the two methods (MT and TEM) for the resistivity distribution of the investigated areas. New means of data processing and modeling also allowed to update the processing of the old data (acquired in 2003 and in the 80s) in MT, gravimetry and magnetism. Coupled modeling MT-gravimetry and integration of reinterpreted old data helped to highlight coincidence of anomalies, including Petite Anse. Concerning the geochemistry, the use of some isotopic analyses (Li, C , O, H , He) has completed our information on magmatic signatures or on their absence. The mineralogical characterization of hydrothermal alteration, in geology, led to identify stages of old hydrothermal activity as possible indicators of the surveyed current systems.

Beyond the innovative techniques and methods, this project sought to develop,at each stage, asynergybetween the different methodsby comparing the resultsobtained bygeology, hydrogeology, water andgas geochemistry and geophysics.Eventually,thismultidisciplinaryexchangehelped to build conceptualmodels that canbe usefulin later stagesof investigation such as exploration bydeep drilling. Among the four areas that were surveyed two are proposed for further exploration drilling including the Petite Anse area. Concerning the nomenclature: "Les Anses d'Arlet" represent the larger surveyed area while "Petite Anse" (or Petite Anse -Diamant) is restricted to the area of interest for further investigations and "Les Eaux Ferrées" is the local name for the studied hot spring.

The work presented hereby theBRGMhascompletedsurface explorationwiththree main objectives:

-Secure theimplementation and executionoffutureexploration drilling(mitigation of thegeological risk) -Better assess thegeothermal resourcesof the island, -Opendrilling opportunitiesin an environment wherethere are many constraints.

GEOLOGICAL SURVEY

New observations and analyzes (Traineauet al., 2013) have clarified the geological context of the Petite Anse / Diamant prospect. As follows:

-Extending the investigation area to the whole volcano-tectonic NW-SE axis, between Pointe Burgos and Diamant Rock , a consistent framework was given to magmatic and hydrothermal activity of the SW Trois -Ilets peninsula ; -Highlighting a spatio-temporal continuum of hydrothermal activity between -1.5 My and today from a detailed mapping of fossil alteration zones related to their tectonic controls, the targeted geothermal reservoir was better constrained at this stage of its evolution [START_REF] Bouchot | Toward a Continuum Geothermal Model to Explain Coexistence of Medium to High (100 to 250°C) Temperature Geothermal Systems in Martinique and Guadeloupe[END_REF] -Clarifying the close relations between the volcano-magmatic activity and the hydrothermal activity, particularly at the Morne Jacqueline, the context of the identified geothermal reservoir was defined.

A three stages evolution is proposed in line with the work of [START_REF] Germa | The K-Ar Cassignol-Gillot technique applied to western Martinique lavas: A record of Lesser Antilles arc activity from 2 Ma to Mount Pelée volcanism[END_REF] and [START_REF] Westercamp | Carte géologique de la France (1/50 000), feuille Martinique[END_REF].

Initial stage

2.1.1 Volcanism Between 1.5 and 0.35 My, a "hydrothermal magmatic system" is developing more or less related to the multi-staged activity of Roches Genty eruptive center (undated). Many volcanoes were then built, from North to South (Figure 1):

-the Pointe Burgos Strombolian cone and its quartz basalt flow (dated at 1.72 ± 0.2 My), which can be related to the Morne La Plaine thick basaltic andesites flows (1.175 ± 0.020 My) ; -the Morne Champagne lava dome of the (0.617 ± 0.052 My); -the Roches Genty eruptive center (undated); -the Morne Clochette andesitic dome (1.33 ± 0.03 My); -the mainly dacitic Morne Jacqueline volcano (undated) followed by a pipe explosion at its Western flank; -the Morne Larcher strato-volcano (0.346 ± 0.027 My); -the Sec and Diamant Rock domes / intrusions and (1.097 ± 0.018 My).

Volcanism, often explosive and marked by interaction with water (hydro-magmatic), was expressed by persistent coexistence (or even the mixture) of deep-originated basaltic lavas and shallower quartz dacitic ones [START_REF] Gourgaud | Le système volcanique Diamant-Burgos (Sud-Ouest Martiniquais) : mélange de magmas en volcanisme différencié linéaire et origine des basaltes à quartz[END_REF][START_REF] Gourgaud | Mise en évidence de réalimentations magmatiques dans le système volcanique linéaire Burgos-Diamant (Martinique)[END_REF]. This feature reflected the existence of magma chamber (s) where the magma can differentiate at shallow depth (6 km according the mineralogy).

This volcanism has a consistency in several ways:

-spatial and temporal restricted distribution; -associated tectonic system, characterized by two groups of sub-perpendicular faults (the regional one corresponding to the volcano-tectonic axis and the one forming a NE-SW "en échelon" network); -similar petrographic properties subject to the same bimodal magmatic mixture with a similar mineralogy [START_REF] Gourgaud | Le système volcanique Diamant-Burgos (Sud-Ouest Martiniquais) : mélange de magmas en volcanisme différencié linéaire et origine des basaltes à quartz[END_REF][START_REF] Gourgaud | Mise en évidence de réalimentations magmatiques dans le système volcanique linéaire Burgos-Diamant (Martinique)[END_REF] Thereis, however, no evidencethat a singlemagma chamberis at the originof all this volcanism; several may have coexisted. Recurrentascents ofdeepbasalticmagma [START_REF] Gourgaud | Mise en évidence de réalimentations magmatiques dans le système volcanique linéaire Burgos-Diamant (Martinique)[END_REF],thanks tothe crossing oftectonicdirectionsNE-SWandNW-SE, may have helped to maintain thevolcanic systemofthe SWpeninsulaTroisIlets,active for atleast 1.1My. Thesemagma chambersand associated subsurface intrusionswould, then, formed theheat source(s) of ahydrothermalsystem.

2.1.2. Earlyhydrothermal system Among the water-magma interactions that characterize this volcanic area, some geological formations (La Charmeuse) contain elements of an ancient underground hydrothermal alteration (undated but clearly preceding the Morne Larcher terminal activity), probably associated with the activity of the Roches Genty eruptive center. Altered blocks (with jasper and natro-alunite, ...) have been raised due to a hydro-magmatic eruption and may indicate an acidic alteration forming the swept part of a magmatic hydrothermal system.

. Intermediate stage 2.2.1 . Fossil hydrothermal

It is represented by the decline of magmatic component and the evolution of " hydrothermal -magmatic " acid system ( described above ) toward a wide High Temperature geothermal system dominantly neutral. It develops a clayey cap (caprock ) and a surface fumarolic activity along a strip linking Anse d' Arlet and Petite Anse , demonstrating the existence of a fossil high temperature geothermal reservoir ( Figure 1). This corridor parallel to the volcanic axis NW-SE is crossed by faults and fractures which have oblique or perpendicular directions (NNW -SSE to WSW -ENE) regarding it. Examination of these faults and joints shows that they frequently worked in tension, creating favorable conditions for the opening and fluid flowing. Locally, the circulation of hydrothermal fluids could coincide with the operation of a N150 °E fracture, as at Anse Chaudière. Thishydrothermalismcanbe summarized into threetypes ofalteration,spatially distinct:

•kaolinite-alunite alteration : itis observedin several placesfrom the Morne La Capote pass to lesAnses d'Arlet village andis symptomatic of afumarolicactivity(boiling fluidwithinshallowaquifersor an oldgeothermal reservoir) and therefore temperature conditionsabove 100°C;

•silica deposits(sinter): observed on theuphill Petite Anse village, they are formedfrom neutral(sodium chloride) andsilica-richfluids and coming fromhigh temperature geothermalreservoirs;

•clay mineralsilliteand interstratifiedillite/smectite:in the area ofLes Eaux Ferrées, they reflectcirculationofhydrothermal fluidsat temperaturesof about150-180° Candcharacterize a fossilcaprock area.

Flankcollapseofthe MorneJacquelinevolcano

Duringthe activity of thegeothermal systemorlater on, theclayey cap that could havebeen used as slipsole as in othercases (e.g. Belousovet al., 1999. Boudonet al., 2007.), the Southern flankofMorneJacquelinewas destabilized. This flank collapseled to outcropping at least partof the cap of the geothermal reservoiras well as intrusions(igneous dykecrossed byvolcanic micro-dykesof the same composition).Theseintrusions reveal agreater proximity toa magmaticstock and areNW-SEoriented, along theregional direction.Morphologicalfreshness of MorneJacqueline volcano suggeststhat this collapsemust have happenedthereonlya few hundred thousandyears ago.

Currentgeothermal activity

It is primarilyrepresented by thethermo-mineral spring ofLes Eaux Ferrées. This spring andthe small water and gas emergences together with it200m along beachfront, display degassingandtravertine deposits. Several featureslead to assumeareduction in the extentand intensityofsurface manifestations:

-the lowflow rate (0.03 l /s) of the springswith respect totheextensionof the area impactedbyhydrothermal alterations;

-the fossilfumarolic and hightemperaturesystem of alunite-kaolinite acidalterationis taken overtodaybylow temperature springlets,confined to thevicinity of the main spring of Les Eaux Ferrées but always fromthe same fractures and therefore circulation system.

This may suggest a contraction or possibly a migration of high-temperature geothermal system southward. The current reservoir is assumed to be located under the alteration zone of Petite Anse. There is a network of faults likely to display conditions of hydrothermal circulation between the Petite Anse area and les Eaux Ferrées hot spring.

Finally, the investigated area was expanded and new springs were studied. The synthesis of these geological data allowed integrating the Petite Anse geothermal system in a larger magmatic and hydrothermal frame (within the axis Pointe-Burgos -Diamant Rock) and in the evolution of this set over 1.5 Ma. The present hydrothermal activity seems more limited in space and its intensity lower than in the past.

HYDROGEOLOGICAL SURVEY

Hydrogeological investigations in the area of Petite Anse focused on:

-seeking areas likely to feed seaside springs and possible associated geothermal system;

-locating any outfalls, thermal anomalies or degassing sites in the Bay of Petite Anse through underwater investigations;

Only degassing zones (of mainly CO 2 ) could be identified without being associated with water ingress nor thermal anomalies [START_REF] Vittecoq | avec la collaboration de G. Braibant : Compléments d'exploration géothermique de la Martinique -Volet « hydrogéologie[END_REF].

The low infiltration rate estimated on the Morne Jacqueline is compatible with the low flow rate of the springs (<1 l / s). The precise location of the deep water ascent may lie a few tens or hundreds of meters upstream the springs.

The area of la Charmeuse and the western flank of Morne Larcher are formed with permeable breccias and pyroclastic flows that may (i) constitute a prime infiltration zone and (ii) contribute to the recharge of the geothermal system.

However, two factors can strongly limit the infiltration at depth:

-the low rainfall and the high evapotranspiration lead to assess the infiltration values between 50 and 75 mm / year, or 20 to 30 times less than on the Mount Pelée; what to add, however, a likely contribution, roughly equivalent seawater;

-a uniform conductive level from 200 m depth, highlighted by the MT survey [START_REF] Coppo | Exploration géophysique (magnétotellurique et gravimétrie) du potentiel géothermique de la Martinique (Montagne Pelée, Anses d'Arlet, Pitons du Carbet et Lamentin)[END_REF] and probably corresponding to a clay cap (cap rock), therefore, slightly permeable.

It is therefore very likely that the natural recharge of the geothermal system is limited. Without more precise evaluation, we think it is limited by a precipitation regime at least 4 times "drier" than on Mount Pelée (less than 80 km northward) and a priori less permeable [START_REF] Vittecoq | avec la collaboration de G. Braibant : Compléments d'exploration géothermique de la Martinique -Volet « hydrogéologie[END_REF].

Conversely, for the same reason highlighted by the MT survey, the presence of a clay cap may explain the rarity of leaks of the geothermal system.4. HYDROGEOCHEMICAL SURVEY

History of works and geological context of the Petite Anse / Diamant spring

Geothermal significance of this spring began to be reported during the exploration of the 1980s [START_REF] Iundt | Ré-évaluation géochimique du potentiel géothermique de l'île de la Martinique[END_REF]) on hydrogeochemical criteria. Exceptional chemical and isotopic properties of this source, in the Caribbean context, and its close association with gas ascents of clearly magmatic origin were then highlighted [START_REF] Pedroni | Ar, and isotope systematics of geothermal emanations in the lesser Antilles Islands Arc[END_REF]. The pursuit of geothermal exploration, then confirmed the interest of the "Diamant spring" area [START_REF] Sanjuan | Réévaluation du potentiel géothermique dans les régions de Morne Rouge-Montagne Pelée et du Diamant (Martinique) : étude géochimique[END_REF] while a geochronological study (e.g. [START_REF] Germa | The K-Ar Cassignol-Gillot technique applied to western Martinique lavas: A record of Lesser Antilles arc activity from 2 Ma to Mount Pelée volcanism[END_REF] rejuvenated from 1 My to a little more than 300 000 years the surrounding volcanism.

The close association with the activity of the Morne Jacqueline volcano is underlined by the geological survey (see § 1):

Other springs located near the axis of past hydrothermal activity were studied. From North to South, it is Colette, Sucrerie, Colibri and Larcher springs. Their possible link to "les Eaux Ferrées" spring is discussed.

Characteristics and origins of water

4.2.1. "Les Eaux Ferrées" spring (Petite Anse) Thephysico-chemical (including temperature), chemical as well asisotopic characteristics and the sourceofwaterRailwayshave notsignificantly changed since the first availableanalyses: a relatively highmineralization (between 19 and20 g/ l) of dominantlysodium chloride type, a temperaturebetween34and35°CandapHbetween5.99and6.3(the higheruncertainty is due toCO 2 degassing).

Among the trace elements,characteristicofwater-rock interactionat high temperature,the concentrations ofAs,Cs,Rbvary little. The increaseinboronis consistent withother indicators ofinteractionas 18 O(which alsoincreases).On the other hand, the decrease oflithium concentration(about 20% compared to the expectedtrend)cannot be explained.

"Les Eaux Ferrées" springislocatedin the area ofthe"mature"waters of the Cl-SO 4 -HCO 3 Giggenbach's chart(1988) (Figure 3). Theirchlorinatedfeaturemay be due tomixing withtheseawater. However, such watersdiffer from themixing line between fresh waters andseawaterinaBr/Clchart. This difference mayrepresentan excess ofchlorideof 34%.Given the otherparameters andthe  D/ 18 O chart(Figure 5), it seems legitimateto attributethis chlorineexcess to a magmaticorigin. Gases isotopic ratios of ( see § 5 ) clearly indicate a magmatic contribution to both the helium and CO 2 carbon and both on land and at sea The high value of "Les Eaux Ferrées" spring water  13 C (4.7 ‰ vs PDB) is most likely due to a magmatic origin rather than a marine one ; there would be a fractionation by CO 2 degassing together with a precipitation of carbonate (Rive , 2013 , pers. comm.). Travertine can be seen, indeed, around the spring. [START_REF] Ruzié | Carbon and Helium isotopes in thermal springs of La Soufrière volcano (Guadeloupe, Lesser Antilles): Implications for volcanological monitoring[END_REF] and similar (7.9 Ra) than those found by [START_REF] Pedroni | Ar, and isotope systematics of geothermal emanations in the lesser Antilles Islands Arc[END_REF], at the same "Les Eaux Ferrées" spring. This may confirm the permanence of a mantle feeding and thus of a magmatic activity at this level.

The high concentrations of certain trace elements (As, B, Cs, Li, Rb, ... ) and  18 O (Figure 3),  7 Li (6.3 to 7.1 ‰) isotopic ratios are compatible with water-rock interaction -at high temperature. The isotopic ratio of hydrogen (D) does not display any anomaly relative to the local groundwater. A simple mixture between a seawater and a magmatic pole as proposed in other island arc settings [START_REF] Dotsika | Natural tracers for identifying the origin of the thermal fluids emerging along the Aegean Volcanic arc (Greece) : Evidence of Arc-Type Magmatic Water (ATMW) participation[END_REF][START_REF] Giggenbach | Isotopic shifts in waters from geothermal and volcanic systems along convergent plate boundaries and their origin[END_REF] seems hardly feasible in view , inter alia, the diagram D /  18 O. Chlorine mineralization is still not compatible with such a mixing of sea water / magmatic water. Magmatic signature of CO 2 and He, Cl excess and a trend towards a deuterium deficit suggest, however, that this magmatic contribution does exist. The parent geothermal fluid of "Les Eaux Ferrées" spring could then be the result of a mixing of seawater, meteoric water that interacted strongly with the rock at 200 ° C and a magmatic component. Comparison of chemical and isotopic compositions of different thermal springs and fumaroles from the Aegean volcanic arc suggests that the presence of such a magmatic component characterizes geothermal fields in more active context [START_REF] Dotsika | Natural tracers for identifying the origin of the thermal fluids emerging along the Aegean Volcanic arc (Greece) : Evidence of Arc-Type Magmatic Water (ATMW) participation[END_REF]. Such a component would be present in Montserrat [START_REF] Chiodini | Fluid geochemistry at Montserrat island, West Indies -Bull[END_REF] and in Wotten Waven, Dominica (Traineau, pers. comm., 2014), two volcanically active sites of the Caribbean arc. The confirmation of such a component on Petite Anse would result in, at least, maintaining some magmatic activity without prejudice to the status of the geothermal system itself [START_REF] Gadalia | Taïlamé -Compléments d'exploration géothermique : volet hydrogéochimie[END_REF]) The estimate of the temperature by water-rock interaction geothermometry is illustrated by the Na-K-Mg Giggenbach's chart (Figure 4). Several geothermometers converge to a temperature range of 190 to 210°C [START_REF] Sanjuan | Réévaluation du potentiel géothermique dans les régions de Morne Rouge-Montagne Pelée et du Diamant (Martinique) : étude géochimique[END_REF]. Gadalia et al, 2014.).

The silica geothermometers significantly underestimate the temperatures due to:

-either the likely dilution of this species with surface waters;

-or precipitation of silica during an ascent where cooling (most likely) occurs.

The absence of tritium in water in 2003 [START_REF] Sanjuan | Réévaluation du potentiel géothermique dans les régions de Morne Rouge-Montagne Pelée et du Diamant (Martinique) : étude géochimique[END_REF] indicates a circulation / transit time exceeding 50 years. It is possible to interpret the trace elements and isotopes anomalies with a low water-rock ratio and a significant interaction time. This would be consistent with geological findings suggesting a contraction of the system.

.

Other sources sector Anses d'Arlet (Colette, Sucrerie, Ravine Chaudière and Larcher)

Observations and physico-chemical measurements were made on ten water points, including 3 wells beachfront. The 7 sources , not studied before, have in common a low flow rate (<2 l / min), a temperature close to the average local air (24-26 ° C , depending on altitude), significantly lower mineralization than "Les Eaux Ferrées" spring , the absence of degassing and a sodium chloride dominant mineralization [START_REF] Traineau | Compléments d'exploration géothermique en Martinique : volet géologie[END_REF][START_REF] Taïlame | Compléments d'exploration géothermiques en Martinique. Volet géochimie des fluides[END_REF].

Colibri and Sucrerie springs display travertine deposits and are located either in the environment or at the intersection of listed faults. The Larcher spring has no deposit and, as the Colibri spring, has a very light thermal character, given its altitude of emergence. Other springs ( Bellevue, Colette , Charmeuse, Colibri) have relatively high conductivity for surface waters (300 to 2300 S / cm), probably reflecting leaching of fossil hydrothermal alteration.

Their composition bears the trace or a water-rock interaction at high temperature, or a magmatic contribution. The Giggenbach's chart (1988) ( Figure 4) is symptomatic : these waters are near the "superficial" magnesium end member and are distinguished , in fact, from "Les Eaux Ferrées" spring [START_REF] Gadalia | Taïlamé -Compléments d'exploration géothermique : volet hydrogéochimie[END_REF]. Conversely, among the emergences of "Les Eaux Ferrées" some of them may have mixed with local groundwater as the mixing line N° 2 of Figure 3 can display it.

These sources have four  13 C values of a typical biogenic origin and very low levels of high temperature water-rock interaction indicators. Relatively negative deuterium values can be compared to those found in some local rain water (e.g. [START_REF] Arnaud | Étude du transfert de la chlordécone vers les eaux souterraines en Martinique[END_REF], or other groundwaters (such as Habitation Dizac at Diamant village, in [START_REF] Brenot | Système d'information sur les eaux souterraines de Martinique : caractérisation physico-chimique naturelle des eaux souterraines[END_REF].

The absence of links between these sources and "Les Eaux Ferrées" spring goes in the direction of a limited and / or deep hydrothermal system, centered on Petite Anse.

The hydrogeochemical study leads to the following conclusions:

-the"Les Eaux Ferrées" spring displays, in its chemical and isotopic composition, a signature of an interaction with magmatic rocks at high temperature;

-the temperature of the interaction, estimated by geothermometry, rises to 190-210°C;

-we can assume that the interaction is made with a very low water-rock ratio and / or on a long-term;

-the geothermal fluid likely results from a mixing between a meteoric water, a seawater and a magmatic components;

-some new analyzed springs, although neighboring "Les Eaux Ferrées" spring and the former hydrothermal system do not reveal any mixing link with "Les Eaux Ferrées" spring. It seems that none of these waters has known or interaction at high temperature, or contribution of magmatic gases.

SOIL GASGEOCHEMICALMAPPING

The available datafor the areaof Les Anses d'Arlet are derived from previous [START_REF] Sanjuan | Réévaluation du potentiel géothermique dans les régions de Morne Rouge-Montagne Pelée et du Diamant (Martinique) : étude géochimique[END_REF] andrecent [START_REF] Gal | Compléments d'exploration géothermique de la Martinique: suivi géochimique des gaz du sol -Mesures de Février[END_REF] investigations.

In mostcases itis not possibleto demonstratedeepgas ascent (CO 2 and/orhelium). Some stations(as inAnseDufour, northern MorneReduit) may indicate abnormally highCO 2 without beingmarkedby a helium anomaly(content close to the atmosphere one), andwitha valueclearlybiogenicforthis CO 2 (-24.6 ‰vsPDB).

However, the area of Petite Anse, where flows carbonated mineral water of "Les Eaux Ferrées" springcanundoubtedlybe linkedto phenomenaofgas ascents from deep origin (mantle). Near thespring, many CO 2 vents are identifiable andallowhighlightingtheseascents of deep originatedgas:

-the presence of high concentrations of CO 2 (up to 100%);

-the presence of helium anomalies with a strong enrichment relative to the atmosphere (from 5.24 to 7.56 ppm);

-Isotopic signatures of -1.7 to -5.5 ‰ vs PDB for 13 C of CO 2 and 3 He/ 4 He ratios clearly of mantle origin (> 7Ra).

The combination of these three indicators used to characterize this Petite Anse area as an upflowing zone of deep fluids. It is possible to say that the surface anomaly has a relatively small geographic expression, indicating that the ascent of the fluids occur through drains having a reduced lateral extension and / or that the permeability is space-limited.

Groundwatersuse, in general, the same conduits (faults) as deep originated gases. Theyarealso sometimesvectors. However, measurements carried out close to somesprings in the vicinity of les Anses d'Arlet (Colibri,...)give nopositive anomalyneither in helium, nor in CO 2 . Thisis in line withthe conclusions of §5.3about thesesprings.

GEOPHYSICAL SURVEY

Thismajor part of the2012-2013explorationcampaign is more specificallydeveloped byCoppoet al. (2015).

The Figure 5 (from Coppoet al., 2013)summarizesmost of theobservations and measurements(MT, TEM, gravity andmagnetism)that guided theinterpretation of these datain terms ofgeothermalexploration.

The interpretation of these geophysical results leads to the following considerations:

the cap of a possible geothermal system would be provided by the conductive superficial layer (<10 Ωm ), a few hundred meters thick, present throughout the area. The thickest cap layer, located between the resistive "intrusion" at the NW and the Morne Larcher at the SE, indicates the most active geothermal system. The thinnest cap layer, North, could correspond to an older system and would be partially eroded. At the boundary between the two places, a weakness area of this cap allows the emergence of Petite Anse hot springs. It is also on the edge of the resistive intrusion and this border zone could be a priority way of channeling for the geothermal fluids;

-the resistivity area (10 to 50 ohm.m) developed under the thickest conductive cap layer and located between the resistive "intrusion" and the conductive magmatic conduit of Morne Larcher leads, constitutes a favorable area for the development of a geothermal system . This would be in agreement with the Raharjo' synthetic model ( 2012);

-the potential heat source of the geothermal system (not imaged by the geophysical survey) could be either a magma chamber located beneath the Morne Larcher (which is the newest volcanic edifice in the area with an activity dated at 0.346 ± 0.27 My) or more probably related to the resistive intrusion at the NW. -the existence of a high temperature geothermal system characterized by a strong water-rock and magmatic gases interaction ;

-a hydrothermal circulation system that would have been intensely developed in the past but is now smaller in space;

-the existence of a high temperature geothermal reservoir is initially suggested by the geochemical characteristics of "Les Eaux Ferrées" spring showing a water-rock interaction estimated by geothermometers at 190-200 ° C within a deep reservoir fed by seawater, meteoric fluids and a magmatic contribution;

-The geology highlighted fossil hydrothermal alterations suggesting that the geothermal reservoir has been active for a long time and was much more active in the past. This is why the conceptual model (Figure 6) considers a contraction of the reservoir and the development of a thick clay cap over the time;

-this reservoir would be located along the NW-SE oriented volcano-tectonic axis where focused the magmatic activity since 1.5 My. Specifically, the geophysical methods (MT and gravimetry) identified a dense resistive body, NNW-SSW oriented, underlying volcanic units from Morne Bigot to Morne Jacqueline (Figure 5). This shallow mass is interpreted as a magmatic intrusion according to the geological observations. The presence of dykes, adjacent to "Les Eaux Ferrées" spring could be its surface expression, as a result of a flank collapse that would have impacted the southern flank of Morne Jacqueline;

-this intrusion, as it is cooling, could play, at depth, the role of the heat source in the geothermal system and would go on emitting gases (CO 2 , He) with clear magmatic signature;

-the eastward resistive extension, developed under a doming of the conductive layer (caprock) is interpreted as the site of an existing geothermal reservoir; -this geothermal system would now lean on the SE flank of this intrusion that would have acted as a hydraulic barrier. To the East, the Morne Larcher volcanic system limits the development of this field.

the conductive level (<10 Ω.m) of variable thickness and outcropping in the area of "Les Eaux Ferrées" springmay be the clay cap (caprock) of the current geothermal reservoir while having previously been initiated in a context of higher temperature. Several questions remain about this reservoir including its recharging and therefore its capacity, volume and depth.

"Les Eaux Ferrées" springwould be a leak of this reservoir largely guided by a dyke crossing the Morne Jacqueline volcanic formations.

The other explored springs during this additional exploration are unrelated to this geothermal system, confirming its limits.

Figure 1 :

 1 Figure 1: Location ofsourcesand outcrops impacted by a fossilhydrothermal alteration, identifiedin the area of Les Anses d'Arlet.

Figure 2 :

 2 Figure 2:Giggenbach's chart(1991)displaying the distributionofmajor anions of the springsin the areaof les Anses d'Arlet.

Figure 3 :

 3 Figure 3: Water stableisotopesof lesAnses d'Arlet area. Legend: WML: WorldMeteoric Line, y = 8x+10);LML:LocalMeteoric Line(Guadeloupe), y = 8x+10;supposed mixing linesare listed(1) betweenseawaterand deepcenter for "Les Eaux Ferrées" spring, (2) between "Les Eaux Ferrées" spring andlocal groundwater

Figure 4 :

 4 Figure 4: Giggenbach's chart -geothermometer (1988) displaying the major cations distribution of the springs in the area of Les Anses d'Arlet.

Figure 5 :

 5 Figure 5: Representations in cross-section and in plan of the resistivity and density distributions on Les Anses d' Arlet area.

Figure 6 :

 6 Figure 6: Proposed Conceptual Model of the Petite Anse geothermal system. Depths are given for information only

  An additional clue to the rise of deep fluids in this area is provided by the few measurements on gas springs sampled underwater in the bay of Petite Anse , in the extension of the anomalous zone of "Les Eaux Ferrées" spring. It is essentially composed of CO 2 (> 60 %) but with locally abnormal concentrations of helium (2.2 to 15.8 ppm for 5.24 ppm in the atmosphere). The helium isotope ratios ( 3 He/ 4 He ) of the sample reaches 7.26 Ra . This is a high value, greater than (7.2 Ra) at the Rivière Chaude hot springs(Jean- Baptiste , 2013 , pers. comm.) under the Mount Pelee dome, close to the gases (8.2 Ra ) emitted by the Soufrière of Guadeloupe (

		Sea Water
	Sea Water	Ravine Chaudière Source Sucrerie
	LML	Source Colette Source Larcher
		Surficial waters
	WML	Eaux Ferrées
	1
	Water-Rock
	Interaction
	Arc Type Magmatic Water
	? Parent Hydrothermal Fluid