Amel Mammar
email: amel.mammar@it-sudparis.eu

Liu Penfei
email: pengfei.liu@inria.fr

A Proof-Based Approach to Detect Vulnerabilities in C programs

Keywords: Security, Vulnerability detection, Mapping rules, B formal method, Proofs, Model Checking

This paper presents a formal approach to detect vulnerabilities in a C program using the B formal method. Vulnerabilities denote faults that may be introduced unintentionally into programs making them behave incorrectly. Such faults (or programing errors) may lead to unpredictable behavior and even worse well-motivated attackers may exploit them later to cause real damage. Basically, the proposed approach consists in translating the vulnerable aspects of a C program into a B specification. On this B specification proof and model checking activities are performed in order to detect the presence or absence of vulnerabilities. Compared to the existing vulnerability detection techniques, a proof-based approach permits to eliminate false alarms and denial of service attacks.

Introduction

Software vulnerabilities are programming mistakes or bugs that compilers fail to detect. Buffer and arithmetic overflows are well-known examples of vulnerabilities. With the fast proliferation of complex, open and distributed systems, such software vulnerabilities become a real issue that needs to be fixed since these systems are often used in critical domains like transportation, finance, politics, etc; which makes attackers more and more motivated to cause important damage by exploiting these security breaches [6]. Above all, software defects are expensive, according to a 2002 National Institute of Standards and Technology study, software errors cost the U.S. economy an estimated 59.5 USD billion annually [START_REF]The Economic Impacts of Inadequate Infrastructure for Software Testing[END_REF].

To detect software vulnerabilities, several techniques have been developed [START_REF] Kuang | Analysis of Software Vulnerability, the 5 th WSEAS International Conference on Information Security and Privacy(ISP)[END_REF], [START_REF] Jimenez | Software Vulnerabilities, Prevention and Detection Methods: A Review, the 1 f irst International Workshop on Security in Model Driven Architecture(SEC-MDA)[END_REF]. Roughly speaking, these techniques can be classified into two classes: static and dynamic analysis. Each one has its own particular strengths, however one technique is not sufficient to deal with all the possible errors. In general, several techniques must be applied to detect a larger range of vulnerabilities. The main drawback of static techniques is the high number of false positives they can produce, whereas dynamic techniques suffer from denial of service since the detection is performed at program run-time. A more detailed description of these existing techniques is given in Section 7.

In this paper, we propose a formal approach, based on the B method, to detect vulnerabilities in a C program. Our approach consists in converting the C program into a B specification on which it is possible to perform correctness proof and model checking activities to detect programming bugs or errors. By converting a C program into a B specification, we generate the necessary and sufficient information about the C vulnerable statements. To deal with a buffer overflow for instance, we generate information about the size of the buffer and also the size of the data it holds at any time.

The rest of the paper is structured as follows. The vulnerabilities we consider in this paper are presented in Section 2. The B method is introduced in Section 3. Then, Section 4 gives an overview of the proposal which is described in detail in Section 5. The actual detection of vulnerabilities using proof and model checking activities is described in Section 6. Section 7 presents the related work and a comparison with our approach. Finally, we conclude and present some potential future work.

Software vulnerabilities

In [START_REF]Detecting C Program Vulnerabilities Master Thesis[END_REF], several types of vulnerabilities are described together with their countermeasures and how we deal with them using the B method. These vulnerabilities include buffer overflows and different arithmetic overflows and underflows but also format string vulnerabilities. For the sake of space, this paper only presents buffer overflows and arithmetic vulnerabilities.

Buffer overflows. To store the content of variables and buffers, a program reserves a specific amount of memory space. A buffer overflow occurs when a program attempts to put more data in a buffer than it can hold. A buffer is a sequential section of memory allocated to contain anything from a character string to an array of integers. Writing outside the bounds of a block of allocated memory can corrupt data, crash the program, or cause the execution of malicious code. Buffer overflows are the favorite exploit for hackers.

Arithmetic vulnerabilities. These vulnerabilities occur when a calculation produces a value that is greater in magnitude than a given register or storage location can store or represent. Each integer type in C has a fixed minimum and maximum values that depend on the type's machine representation, whether the type is signed or unsigned, and the type's width (e.g., 16-bits vs. 32-bits). At a high level, integer vulnerabilities arise because the programmer does not take into account the maximum and minimum values. Over one hundred C integer vulnerabilities have been publicly identified to date, some of which have resulted in serious disasters such as rocket malfunction.

Overview of the B method

Introduced by J. R. Abrial [START_REF] Abrial | The B-Book: Assigning Programs to Meanings[END_REF], B is a formal method for safe project development. B specifications are organized into abstract machines. Each machine encapsulates state variables on which operations are expressed. The set of the possible states of the system are described using an invariant. The invariant is a predicate in a simplified version of the ZFset theory, enriched with many relational operators. Operations are specified in the Generalized Substitution Language (GSL) which is similar to the DijkstraŠs guarded command notation. A substitution is like an assignment statement. It allows us to identify which variables are modified by the operation, while avoiding mentioning which ones are not. The generalization allows the definition of non-deterministic and preconditioned substitutions. Refinement is the process of transforming a specification into a less abstract one. A refinement can operate on an abstract machine or another refinement component. In B, we distinguish behavioral and data refinement. In this paper, we only use behavioral refinement that aims at eliminating non-determinism and coming close to the control structures used in the chosen target programming language. Behavioral refinement includes, for example, weakening of preconditions, the replacement of parallel substitution with a sequence one, etc. To ensure the correctness of a B specification, a set of proof obligations is generated for each B component. At the abstract level, these proofs aim at verifying that the invariant of the system is satisfied after the execution of each operation. Of course, such an invariant is assumed to be satisfied before an operation is executed. For each a given invariant Inv and an operation op whose precondition and substitution are P and S respectively, the following proof obligation is raised: (Inv ∧ P ) ⇒ [S]Inv. Notation "[S]Inv" denotes the predicate obtained by applying the substitution S to the variables of Inv. Refinement proofs permit us to check the correctness of each concrete operation with respect to its abstraction. We assume that readers are familiar with B method and more details can be found in [START_REF] Abrial | The B-Book: Assigning Programs to Meanings[END_REF].

Overview of the approach to detect vulnerabilities

Our method to deal with vulnerabilities using the B method includes four phases (See Figure 1):

• In a first step, the C code is transformed into an abstract form. To this end, we have defined a sub-set of the C language that include the declarations of buffers and arithmetic data. More details can be found in [START_REF]Detecting C Program Vulnerabilities Master Thesis[END_REF].

• From the abstract representation of the C code, a B formal specification is automatically generated. The B specification contains information about the vulnerable elements of the code. In case of a buffer for instance, we consider its size and also the size of the data it holds at any time.

• To detect the presence/absence of vulnerabilities, proof obligations are generated using the proof obligations generator (POG) of AtelierB. The prover of AtelierB is then used to discharge them. The failure of the prover to automatically demonstrate a goal (the proof) can be due to two different reasons: either it lacks tactics and needs human help and intervention or the goal is false.

• To be sure that an unproved goal corresponds to a vulnerability, we use the model-checker PROB [START_REF] Prob | [END_REF] in order to exhibit a state that satisfies the opposite (complement) of this goal. This means that the goal is really false. The following section describes the generation of a B specification from a C program in order to detect vulnerabilities.

Generation of a B model from a C program

In this section, we describe how it is possible to use the B method to detect vulnerabilities in a C program. Our method is based on extracting information about the vulnerable functions or data that are used in the program.

The subset of ANSI C

Our approach considers a subset of the ANSI C language satisfying the following assumptions:

-the ANSI-C program has been already preprocessed, e.g., all the #def ine directives are expanded (inline expansion).

-the supported C types are primitive integer and array.

-function calls are expanded (inline expansion), the return statement is replaced by an assignment (if the function returns a value).

-all the arithmetic operations contain two operands, that is, they are of the form (z := x op y). Multioperand operations are transformed into binary operations by introducing temporary variables. For instance, operation (a = a 1 + a 2 + a 3 ) is replaced by the following two binary operations: a temp = a 1 + a 2 , a = a temp + a 2 . This transformation is necessary in order to detect any arithmetic overflow. Indeed, multi-operand operations may mask some overflows like in statement (x = maxint + 1 -1) where the sub-assignment (x = maxint + 1 produces an overflow while its equivalent (x = maxint) does not.

-the declaration of variables, buffers and files, -the predefined C functions like input/output functions (printf , scanf , etc.) and also the functions on buffers (strcpy, strncpy) and files (f scanf , f gets),

-the assignment, the sequence and the choice (IF) statements.

A complete grammar of the subset of ANSI C supported by the proposed approach to detect vulnerabilities is provided in [START_REF]Detecting C Program Vulnerabilities Master Thesis[END_REF]. Hereafter, we describe how we obtain the B model from a C program written according to this subset.

The B model architecture

Recall that our objective is not to build an equivalent B model for a C program. Indeed, our goal is to build an abstraction of a C program by extracting the useful information to detect vulnerabilities that may be present in a C program. Figure 2 depicts the architecture of the B model that we derive from a C program. The B model we derive from a C program is composed of two B components:

-At the abstract level, a B machine is defined. It contains the variables of the C program and an invariant to state the types of these variables but also to express that the C program we would like to build should not contain any vulnerability, that is, all the variables are in their respective ranges. An operation M ain is specified to model the behavior part of the C program. This operation consists of a non-deterministic substitution that states that some values are assigned to variables according to the invariant. In other words, the operation represents the behavior of a C program that assigns values to its variables without producing any vulnerability.

-At the refinement level, a B component that refines the first one is created. The refined operation M ain of this component contains the translation of the instructions of the

Buffer declaration size_buf f char buff[N ] N char buff[N ]="hello_world" N char buff[] 1 char buff[] = { a , b , c } 3 char *buff ="hello_world" 11 Table 1
DEFINITION OF THE SIZE OF A BUFFER C program we are dealing with. By this way, the refinement proofs will demonstrate that the refinement component is conform to its abstract specification, that is, it does not contain any vulnerability.

In the following sections, we present some translation rules to derive a B model from a C program.

Translation of buffers

To detect buffer overflows, we have to generate information about the maximum size of each declared buffer and also the amount of the data that it contains at any time. This information is stored in two integer B variables buffer_max and buffer_used defined as follows:

Constants buffer_max Properties buffer_max=size_buff Variables buffer_used Invariant buffer_used ∈ NAT ∧ buffer_used ≤ buffer_max
where size_buf f is the size of the declared buffer that is defined according to a set of rules described in [START_REF]Detecting C Program Vulnerabilities Master Thesis[END_REF].

Hereafter, Table 1 gives some examples on how size_buf f is obtained.

Variable buf f er_used, initialized to 0, is updated each time a new variable is assigned to the buffer. In [START_REF]Detecting C Program Vulnerabilities Master Thesis[END_REF], we have defined a set of rules that generate a B substitution for each C instruction that modifies the value of the buffer. Table 2 gives some examples.

Substitution (CHOICE buf f er_used := 1 OR buf f er_used := buf f er_max END) means that we have to deal with limit cases, that is, the buffer may contain data

(buf f ) f scanf (f ile_name, "%s",&buf f ) scanf ("%s",&buf f ) CHOICE buf f er_used := 1 OR buf f er_used := buf f er_max END f gets(buf f, size, f p) read(f d, buf f, size) buf f _used := size strcpy(dest_buf f, source_buf f ) dest_buf f _used := source_buf f _used strncpy(dest_buf f, src_buf f, size) dest_buf f _used := size

Translation of arithmetic data

To detect arithmetic vulnerabilities, we have to verify whether the value assigned to a given variable goes beyond the scope of its type. To do this, we have to memorize the minimum x max and maximum x min values that each variable x can represent. Table 3 gives some examples on how these variables are defined according to the different types of the C language: For each declared variable x, we generate the following invariant to state that its value must belong to the range of its type: (x ∈ x min .. x max ). To detect vulnerabilities, we have also to translate each C instruction that modifies variable x. To get a value from a user, function scanf ()

Translation of C control structures into B

So far, we have seen how to translate declarations (buffer and arithmetic data) and basic C instructions into B. However, a C code may include control structures like conditional (IF) and sequential structures. The C control structures we consider in this paper are described by the following BNF grammar:

Instruction ::= / * assignment * / | varID = expression / * Sequencing * / | Instruction1; Instruction2 / * choice * / | if (expression) { Instruction1 } else { Instruction2 }
Since the B method supports all the above C control structures with the same semantics, the choice, assignment and sequencing instructions are mapped straightforwardly into the IF, assignment and sequencing substitutions respectively of the B language.

Illustrative example

To illustrate our approach, let us apply the different translation rules we have defined on the following C program: #include <stdio.h> void main(){ FILE * fp; char tmp [40], buff [START_REF] Wahbe | Efficient Software-Based Fault Isolation[END_REF]; fp = fopen("example.txt", "r"); fgets(tmp,30,fp); strcpy(buff,tmp); puts(buff); short int x,y; scanf("%h",&x); y=x+2; y=x;} which is translated into:

MACHINE Example CONSTANTS tmpmax, buf fmax PROPERTIES tmpmax = 40 ∧ buf fmax = 20 VARIABLES tmp used , buf f used , x, y INVARIANT tmp used ∈ N AT ∧ tmp used ≤ tmpmax ∧ buf f used ∈ N AT ∧ buf f used ≤ bufmax ∧ x ∈ 0..32767 ∧ y ∈ 0..32767 INITIALISATION tmp used , buf f used , x, y := 0, 0, 0, 0 OPERATIONS Main = BEGIN tmp used , buf f used , x, y : (tmp used ∈ N AT ∧ tmp used ≤ tmpmax ∧ buf f used ∈ N AT ∧ buf f used ≤ bufmax ∧ x ∈ 0..

Vulnerability detection

In this section, we discuss how it is possible to detect vulnerabilities thanks to refinement proofs but also using the PROB tool. To demonstrate the absence of vulnerabilities, we have to discharge all the specification proofs of the abstract component but also those of the refinement component:

1. Specification proofs: these proofs aim at demonstrating that operation M ain, defined in the first abstract level, is correct. We have to prove that this operation re-establishes the invariant: Inv ⇒ [V 1 , . . . V n : (Inv)]Inv where V i and Inv denote respectively the variables and the invariant of the abstract component. This proof is obvious and automatically discharged.

2. Refinement proofs: these proofs aim at demonstrating that the refinement of operation M ain does not contradict or violate its abstraction. In other words, we have to prove that the refined operation also re-establishes the invariant: Inv ⇒ [S]Inv where S denotes the B translation of the instructions defined in the C program. When establishing these proofs, two cases are possible:

-the proof is discharged (automatically or interactively): this case means that the program is correct and does not contain any vulnerability.

-the prover of AtelierB fails to discharge the proof: this case means that the prover fails to prove a given goal (Predicate) G. Since the complexity of these proofs is very low, such a failure denotes an invariant violation in general, that is, the occurrence of a vulnerability in the corresponding C program. To be sure that this potential vulnerability is a real one, we use the model checking functionality of the PROB tool as a plugins in order to check that the invariant is really violated by finding, for instance, a state that does not satisfy predicate G or contradicts the global invariant.

Let us illustrate this approach on the previous example. For the abstract component Example, the POG of Ate-lierB generates 3 proof obligations that are all automatically discharged as expected. However for the refinement component Example_Ref , the POG also produces six proof obligations but it succeeds to perform only five of them. The remaining proof obligation is related to invariant (buf f _used ≤ buf f _max): (30 ≤ buf f _max) which is obviously false. Let us remark that the prover did not point out that invariant (yy ∈ 0..32767) is also violated. The reason is that the semantics of the ASSERT substitution considers its predicate as true to continuous the remaining substitutions. As predicate (30 ≤ buf f _max) is not fulfilled, any invariant becomes true (f alse ⇒ Inv is always true). This feature is very interesting in our case since it permits an incremental vulnerability detection. Now, let us replace substitution (tmp used := 30) by (tmp used := 10). The POG generates the following unproved proof related to invariant (yy ∈ 0..32767): (xx + 2 ∈ 0..32767). To be sure that this formula is not valid. We use PROB model checker in order to find a state that satisfies its complement (xx + 2 / ∈ 0..32767). Figure 3 depicts the answer of PROB model checker for the query of finding a state that satisfies the last predicate. Since, a state that violates our goal (xx + 2 ∈ 0..32767) is found, we can conclude that the instruction (y := x + 2) is vulnerable.

Related work

To deal with vulnerabilities, several techniques have been developed. We present hereafter those related to buffers and arithmetic data:

-Buffer overflows vulnerabilities: the techniques to detect buffer overflows can fall into two categories: static and dynamic. According to the dynamic technique, the buffer overflow is avoided by restricting the access to the memory of an application. This method primarily relies on a safe code being preloaded before an application is executed. This preloaded component can either provide safer versions of the standard unsafe functions, or it can ensure that the return addresses of the functions are not overwritten. StackGuard [START_REF] Calton | StackGuard: Automatic Adaptive Detection and Prevention of Buffer-Overflow Attacks[END_REF] is an example of the tools following such a method. It places a canary word next to the return address whenever a function is called. If the canary word has been altered when the function returns, we are sure some attempt has been made on the overflow buffers. In that case, it responds by emitting an alert message and halting the program. This technique is also used by StackShield1 , SFI [START_REF] Wahbe | Efficient Software-Based Fault Isolation[END_REF], libsafe2 and GCC. Another approach developed by Arash Baratloo et. al. [START_REF] Baratloo | Transparent Run-Time Defense Against Stack-Smashing Attacks Protecting Systems from Stack Smashing Attacks with StackGuard[END_REF] consists in replacing unsafe library functions with safe implementations. However, run-time solutions always incur some performance penalty(StackGuard reports performance overhead up to 40% [START_REF] Cowan | Protecting Systems from Stack Smashing Attacks with StackGuard[END_REF]). The other problem with run-time solutions is that while they may be able to detect or prevent a buffer overflow attack, they effectively turn it into a denialof-service attack.

Static techniques permit to overcome this problem by detecting likely vulnerabilities before deployment. RATS [START_REF]Fortify Software Inc Secure software solutions, rats, the rough auditing tool for security[END_REF] and ITS4 [START_REF] Viega | ITS4: A Static Vulnerability Scanner for C and C++ Code[END_REF] are examples of tools based on the static analysis technique. They use lexical analysis and compare the identified lexemes with a "suspects" database to identify vulnerabilities in C source files. The main drawback of such tools is that they may generate false warnings and sometimes miss real problems. Another tool, CodeAuditor [START_REF] Wang | Automated Detection of Code Vulnerabilities Based on Program Analysis and Model Checking[END_REF], uses Model checking to find the vulnerabilities. However as we know, if the code is very large, we can not finish the verification in an acceptable period of time. If we reduce the code source size, we may miss some vulnerabilities also.

-Integer vulnerabilities: one approach to fix integer vulnerabilities is to raise a compile-time warning for each potential vulnerability and let the programmer fix them. However, the number of actual vulnerabilities is an order of magnitude less than the number of warnings. Another approach consists in translating the C code into a typesafe code, e.g., Cyclone [START_REF] Jim | Cyclone: A Safe Dialect of C[END_REF] or CCured [START_REF] Necula | CCured: Type-Safe Retrofitting of Legacy Code[END_REF]. However, this option may not be practical in many settings, such as for performance-critical applications or when the user is not familiar with the type-safe code. PICK [START_REF] Brumley | Towards Automatically Eliminating Integer-Based Vulnerabilities[END_REF] is a tool that uses sub-typing rules to detect unsafe integer operations and inserts the necessary dynamic checks to prevent exploits. But it only deals with the casting vulnerabilities. RICH [START_REF] Brumley | Automatically Protecting Against Integer-Based Vulnerabilities[END_REF] uses a similar approach to PICK and also suffers of denial of service attacks.

In this paper, we define a formal approach to detect buffer and arithmetic vulnerabilities using the B method. Our approach consists of a static analysis of the code in order to extract the sufficient and the necessary information about the different elements that may produce vulnerabilities. This information is then modeled in B in order to prove the presence/absence of vulnerabilities. Based on a static technique and a formal method, our approach has the advantage of avoiding denial of service attacks and false alarms at the same time.

Conclusion and future work

Software security has always been a concern in the software industry. The C language is one of the most used program language in the world, also its vulnerabilities are well-known. In this paper, we have defined a formal method based on the B method in order to detect vulnerabilities with the ultimate goal of correcting them. Basically, our proposal consists in defining variables to store the size of buffers, and also to store the values each integer variable can represent. These different informations together with the C program are then translated into a B specification on which we perform proof and model checking activities to detect the presence of vulnerabilities. We have applied this approach on several applications (larger and more complex than the example given in this paper) that gave very promising results. Compared to other approaches, our approach can detect buffer overflow and Integer vulnerabilities at the same time without generating false alarms. In addition, our proposal can be applied on any other programming language, like JAVA for instance, by defining new translation rules to deal with its vulnerable functions. Finally to make our approach workable, we have developed a tool that permits us to point out the vulnerable statements in a C program. This tool is implemented in JAVA and described elsewhere in [START_REF]Detecting C Program Vulnerabilities Master Thesis[END_REF]. Currently, we are working on extending the proposed approach to support loops and recursive functions. Future work include also the development of a process that would permit to correct automatically the C code by exploring the B proof and model-checking result activities. Basically, we have to define the condition to add within the M ain operation in order to establish the invariant and correct the corresponding C program. To do that, we can reuse our previous work presented in [START_REF]A Systematic Approach to Generate B Preconditions: Application to the Database Domain[END_REF] that defines a formal process to calculate the weakest precondition of a B operation to reestablish an invariant.

  Fig. 1 DETECTING C VULNERABILITIES USING THE B METHOD

Fig. 3 DETECTION

 3 Fig. 3 DETECTION OF VULNERABILITIES USING PROB MODEL CHECKER

Table 2 B

 2 TRANSLATION OF C INSTRUCTIONS ON BUFFERS

of minimum or maximum size, this size may be especially equal buf f er_max to simulate a potential attacker. To detect a potential vulnerability at each point of the program, we have to add the following B substitution after each assignment on variable buf f er_used

ASSERT (buf f er_used ≤ buf f er_max) THEN skip END

Table 3 MINIMUM

 3

	AND MAXIMUM VALUES OF SOME C ARITHMETIC TYPES
	is the most common one. Since we have to consider the
	worst case, each C instruction scanf ("f ormat", &x) is
	translated into the following B substitutions: CHOICE x :=
	x

min OR x := x max END. Other arithmetic operations, like additions, subtractions, multiplications and assignments are straightforwardly translated into B since they are all supported by similar operators with equivalent semantics. As for buffers, after each assignment of variable x, we have to add the following B substitution in order to detect any vulnerability: ASSERT (x ∈ x min .. x max ) THEN skip END.

http://www.angelfire.com/sk/stackshield

http://www.research.avayalabs.com/project/libsafe


Nicolas Massacret

Joseph Moysan
email: joseph.moysan@univ-amu.fr

Marie-Aude Ploix

Jean-Philippe Jeannot

Naïm Chaouch

STUDY OF ULTRASONIC PROPAGATION THROUGH VORTICES FOR ACOUSTIC MONITORING OF HIGH-TEMPERATURE AND TURBULENT FLUID

Ultrasonic monitoring in high temperature fluids with turbulences requires the knowledge of wave propagation in such media and the development of simulation tools. Applications could be the monitoring of sodium-cooled fast reactors. The objectives are mainly acoustic telemetry and thermometry, which involve the propagation of ultrasounds in turbulent and heated sodium flows.

We developed a ray-tracing model to simulate the wave propagation and to determine wave deviations and delays due to an inhomogeneous medium. In previous work we demonstrated the sensitivity of ultrasounds to temperature gradients in liquid sodium. To complete that study, we need to investigate the sensitivity of ultrasounds to vortices created in a moving fluid. We designed a specific experimental setup called IKHAR (Instabilities of Kelvin-Helmholtz for Acoustic Research) in order to assess the validity of the ray-tracing model and the potential of ultrasounds for monitoring such fluid.

In this experiment, Von Karman instabilities were created in a flow of water. Fluid temperature was homogeneous in our experimental setup. Through a careful choice of the parameters, periodic vortices were generated. The experiment was also simulated using Comsol ® to allow discussion about repeatability. The throughtransmission method was used to measure wave delays due to the vortices. Arrays of transducers were used to measure time of flight variations of several nanoseconds with a high spatial resolution.

Results were similar to simulation results. They demonstrate that beam delays due to vortices can be measured and confirm the potential of ultrasounds in monitoring very inhomogeneous fluid media such as liquid sodium used as coolant fluid in nuclear fast reactors.

Introduction

The Sodium-Cooled Fast Reactor (SFR) has been chosen by France as the reference option in the framework of the Generation IV International Forum [START_REF] Gauche | Generation IV approach -The development of sodium fast reactors[END_REF]. For this kind of reactor, it is necessary to develop a specific instrumentation, compatible with liquid sodium used as coolant, and to meet the Generation IV requirements, particularly in terms of reliability.

In the area of the reactor between the outlet of the fuel assemblies and the upper core structure, there is a need for some thermometry and telemetry instrumentation. Thermometry would be used to monitor the assembly sodium outlet temperature and telemetry would be used to detect the movements of these assemblies. Ultrasounds are suitable for these measurements because they propagate rapidly in liquid sodium, and are weakly attenuated. Furthermore, with this method, the transducer can be placed far from the measurement area in order to minimize its effect on the sodium flow (as pressure loss). However, in this area, the sodium flow is turbulent and presents significant temperature variations. Depending on the orientation of the acoustic beam, these inhomogeneities may result in deviations and changes in the ultrasonic time of flight, which could interfere with measurements.

Numerical codes, such as AcRaLiS (Acoustic Ray in Liquid Sodium) [START_REF] Massacret | Etude d'une méthode ultrasonore d'estimation des temperatures locales du sodium liquid en sortie coeur RNR-Na[END_REF] or CIVA [START_REF] Lu | Modélisation de la propagation et de l'interaction d'une onde acoustique pour la télémétrie de structures complexes[END_REF], have been developed to compute ultrasonic propagation in such environments. Some experiments in static thermal inhomogeneous medium have already been performed to verify a part of the model used in AcRaLiS simulation code [START_REF] Massacret | Modelling of ultrasonic propagation in turbulent liquid sodium with temperature gradient[END_REF]. However, in a turbulent medium, the chaotic nature of the flow makes the experimental verification of the model complex. To deal with this issue, an experimental bench named IKHAR (Instabilities of Kelvin-Helmholtz for Acoustic Research) has been set up. It produces a flow of water with specific and reproducible vortices which are crossed by ultrasonic beams.

After a short presentation of the numerical model used in AcRaLiS, we will describe the functioning of the IKHAR experiment bench and the way the acoustic measurements were realized. Then we will discuss the IKHAR experimental results and their comparison with numerical results obtained with Comsol ® and AcRaLiS. We will describe the way Comsol is used to realize simulations of the fluid dynamics in IKHAR, and how the numerical thermo-hydraulic data obtained are used with AcRaLiS.

The acoustic ray model of AcRaLiS

The simulation of an acoustic wave propagation in a fluid medium may be realized with numerical models based on different kinds of theory or method, such as:

-the ray theory, which consists in discretizing the wave front of an ultrasonic wave, and following the path independently of each point on this front. The path followed by these points will appear as a ray whose behavior may be quite close to that of a light beam [START_REF] Pierce | Acoustics: An Introduction to Its Physical Principles and Applications[END_REF].

the finite elements method consists in discretizing the medium in small volumes or surfaces, where partial differential equations are solved. Application of this method requires the solution of equations in the entire medium.

the spectral finite elements method is a method similar to the finite elements method, but in the frequency domain. Moreover, its particular implementation allows it to be more accurate and faster than a conventional finite elements method when the wavelength of the wave to propagate is very small in comparison with the propagation medium [START_REF] Komatitsch | The spectral-element method: an efficient tool to simulate the seismic response of 2D and 3D geological structures[END_REF].

The finite elements and spectral finite elements method can accurately simulate wave propagation in a complex fluid medium (inhomogeneous temperature and turbulent flow) if the system of partial differential equations is well adapted to the medium. This accuracy, however, is related to the size of the mesh: the smaller the wavelength is, the smaller the size of the elements has to be. As here the frequency of the propagating wave is of the order of a few megahertz (wavelength approximately equal to 2.3 mm in 500°C liquid sodium) and as the propagation length is over several tens of centimeters, then the number of elements in which the partial differential equation will be resolved is very important. That implies significant costs calculations.

The ray method is much faster for high frequency applications because it only takes into account the parts of the medium in which the ultrasonic waves propagate. Moreover, this method is able to conveniently consider both the effects of temperature and turbulence in the medium. It is for these reasons that we have chosen to implement a code based on this method. This code is called AcRaLiS, for Acoustic Ray Theory in Liquid Sodium.

Following previous work, we coded AcRaLiS as an iterative code [START_REF] Iooss | Numerical simulation of transit-time ultrasonic flowmeters: uncertainties due to flow profile and fluid turbulence[END_REF]:

-At time , a point of the wavefront is situated at the coordinates of the point . At this point the wavefront has a propagation direction , and celerity .

-Taking into account these characteristics of the wavefront, and the local flow velocity and the temperature of the medium, the position of this point on the wavefront at the next time step is computed.

-The calculation is repeated by taking into account the new features of the wavefront and the thermo-hydraulic parameters of the medium at the new point.

The equations used for this calculation are the following:

= , + , , = , + , , = - -∧ ∧ -⋅
where is a point on the wavefront, the flow speed, the ray propagation direction, and the slowness vector, as = ⋅ , and = 1 -. . At the end of the calculations, it is easy to determine the shape of the wavefront at each time step.

The calculation of the energy is performed using the method of summation of Gaussian beams [START_REF] Cerveny | Computation of wave fields in inhomogeneous media -Gaussian beam approach[END_REF]. As the remainder of this document concerns the accuracy of the wavefront shape calculated by the code and not the amplitude of the signal, the Gaussian beams summation method will not be described here.

The part of this model that calculates interactions between ultrasounds and the medium temperature was already validated using an inhomogeneous temperature field in silicon oil [START_REF] Massacret | Modelling of ultrasonic propagation in turbulent liquid sodium with temperature gradient[END_REF]. In the work presented here, we designed a specific experiment to estimate the AcRaLis accuracy to calculate the interactions between ultrasounds and a turbulent flow. To this end, an experimental bench named IKHAR was set up.

The IKHAR experimental bench

The difficulty of producing a turbulent flow of water in which to propagate ultrasonic waves, is to control this flow, to repeat it if necessary, and especially to determine the flow velocity field. This last point is important because without the knowledge of the velocity field it is not possible to use AcRaLiS (or other code) to simulate the propagation of ultrasound and so to compare the numerical simulation results with the experimental ones.

Vortices generation

We present here the flow turbulences produced by generating Von Karman vortices. In previous work we produced Kelvin-Helmholtz instabilities [START_REF] Massacret | Etude d'une méthode ultrasonore d'estimation des temperatures locales du sodium liquid en sortie coeur RNR-Na[END_REF], and we want now to test our model with Von Karman instabilities which are simpler to simulate with Comsol ® (cf. next chapter).

Von Karman instabilities are vortices that occur downstream of a cylindrical obstacle placed in a steady-state water flow [START_REF] Cerveny | Computation of wave fields in inhomogeneous media -Gaussian beam approach[END_REF]. In our experiments, the water flow speed is about one meter per second.

These vortices have the advantage of being periodic. This period depends directly on the velocity of the flow upstream of the obstacle and the geometry of this obstacle. This relationship is expressed by the Strouhal number which is defined as follows [START_REF] Cerveny | Computation of wave fields in inhomogeneous media -Gaussian beam approach[END_REF]:

= ⋅
where is the frequency of vortex detachment, is the diameter of the obstacle, and is the velocity of the flow. is the Strouhal number, and has a constant value of 0.2 for a cylindrical obstacle as in our experiment.

Thus, once the speed of the water flow is adjusted, all the generated vortices have similar thermohydraulic characteristics. In addition, the geometry of the flow velocity field is simple and can be obtained through Computational Fluid Dynamics (CFD) simulations.

It is the experimental bench named IKHAR which generates these vortices. IKHAR is a hydraulic loop generating a water flow at a speed of 3 m.s -1 in a pipe of rectangular section (11cm x 4 cm) [START_REF] Massacret | Etude d'une méthode ultrasonore d'estimation des temperatures locales du sodium liquid en sortie coeur RNR-Na[END_REF]. This section is 3.1 m long. The mean flow velocity is measured by means of an electromagnetic flowmeter. The water flow reaches a steady-state in the first half of the section, and then meets the cylindrical obstacle. Von Karman vortices are generated in the second part of the section which is instrumented with ultrasonic transducers. A diagram of the test section of the IKHAR bench is shown in the figure below. The objective of this experiment being to measure the influence of a disturbed velocity field on the propagation of ultrasounds, two ultrasonic transducers are arranged face to face on each side of the produced vortices to accurately measure the wave distortion.

Acoustical measurement and signal processing

The transducers used to measure the influence of vortices on the propagation of ultrasound are two identical one dimension linear arrays. They each have 64 elements (each element being 0.5 mm wide and 10 mm high) with an inter-element space of 0.1 mm. Their central frequency is 5 MHz.

These two transducers are arranged face to face on each side of the test section and both work as emitter and receiver. They simultaneously emit an acoustic wave, then each transducer receives the propagating signal from the other transducer. When the wave reaches the transducer, the times of flight are recorded independently on each element of the phased array. The small size of the elements allows us to accurately determine which parts of the wave front have been delayed and which parts have been accelerated.

The Mach number, which is the ratio between flow velocity and acoustic wave velocity, is here very small, of the order of 0.06%, and the time of flight variations are only of a few nanoseconds. To measure these fine variations several operations must be performed on the acquired signal.

First we measure the time of flight of the acoustic signal received by each element. This measure is realized using an interpolation to enhance the time resolution. Then we eliminate some intrinsic time of flight variations that are independent of the vortex passage and constant during acquisition. These variations may result from the disposition of the two transducers (whose surfaces may not be perfectly parallel), the shape of the transmitted signal (the wave front may be slightly curved) or the intrinsic characteristics of the transducers.

These constant variations are independent of the flow and are a continuous component of all the acquired signal. On the contrary, the time of flight variations due to the vortices in the flow are time-dependent and are alternately positive and negative, depending on the part of the vortex on which the measurement is made. Also, by averaging the time of flight measured by each element on a large number of acquisitions (several thousand), variations due to flow instabilities tend to disappear, while the continuous component is enhanced. Then, by subtracting this average to the time of flight measurements, we get the variations which are only due to the passage of vortices. These variations appear on the following figure.

Experimental results

These measurements, realized simultaneously on the two transducers during several seconds and reported as a function of the acquisition duration, gave the following results: The simultaneous use of two transducers as emitter and receiver placed face to face ensures that these variations are due to the flow velocity field. Indeed, if an acoustic wave propagating in one direction is accelerated by the flow, the acoustic wave propagating in the opposite direction at the same time will be slowed. Thus, the influence of the flow on the celerity of the waves is vectorial, unlike the effect of temperature which is scalar. Figure 4 presenting the variations in time of flight of two waves propagating in opposite directions shows clearly these opposite variations. This confirms that these small changes are not due to possible temperature changes or evolution in the distance between the two transducers.

These time of flight variations are periodic, with a frequency around 17 Hz (as predicted with a Strouhal number equal to 0.2) and a regular amplitude in the order of 11 ns. These results confirm the periodic and stable generation of Von Karman vortices in the IKHAR bench.

Comparison with numerical data

For the comparison of experimental data with numerical results, the difficulty lies in obtaining a numerical mapping of the flow velocity field in vortices. This mapping of the flow is subsequently used for simulating the propagation of ultrasound with AcRaLiS. In this study we obtained this mapping of the water flow within the IKHAR testing section by running a Computational Fluid Simulation in Comsol ® . This solution is simple and provides a realistic mapping of the flow. To get a more accurate mapping, the solution could be to measure the velocity of flow in IKHAR with an optical technique like Particle Image Velocimetry. However, this solution is more complex to implement and was not used in these first comparisons.

Thermo-hydraulics simulations

These simulations were performed using Comsol Multiphysics software. They are two dimensional and use the physical module named "Laminar Flow". This module solves the Navier-Stokes equations without averaging the turbulences, like the models based on RANS (Reynolds Average Navier-Stokes) methods. The geometry of the simulation is presented in Figure 4 and Figure 5.

The water flow enters the section with a direction parallel to the positive axis X. To be more realistic, a velocity profile is given to the flow of water as it enters the simulated section, that is, on each side of the obstacle. This profile is shown in Figure 4. The average value of the velocity profile used is the average value measured by the electromagnetic flowmeter in the IKHAR loop. These figures show the vortices generated by the cylindrical obstacle, the so-called Von Karman vortices. For a better visualization of the eddies, the flow vorticity is also displayed (cf. Figure 5). Vorticity is calculated by applying the curl operator to the flow velocity field.

AcRaLiS simulations

The acoustic rays were emitted from a horizontal line at Y=-0.055 m and between X=0.075 m and X=0.113 m (see Figure 6). This 3.8 cm long emitter line was therefore representative of the transducer used. The result obtained -presented in Figure 8 -is consistent with the velocity field through which the waves are propagating: the generated vortices rotating in alternating directions create fluid streams oriented along the (positive or negative) Y axis. It is these currents that are responsible for the time of flight variations. Comparing the numerical results with experimental data collected on IKHAR gives very good results: variations appear in both cases as regular oscillations. These variation amplitudes are similar and the difference is only of 1.5 ns. Also, in this particular case the relative difference in oscillation frequency is of about 5 Hz.

Conclusion

These first comparison results are encouraging and suggest that a numerical tool based on the ray theory is efficient to calculate ultrasonic time of flight in a flowing medium whose velocity field is slightly disturbed.

It is likely that some of the differences observed when comparing the results come from the numerical mapping of the velocity field used for acoustic simulation. It is therefore possible to improve these results, either by improving the quality of the CFD simulation (by performing 3D computation) or by instrumenting the IKHAR bench test section to measure the actual velocity field (through an optical method like Particle Image Velocimetry).

From an experimental point of view, combining the generation of Von Karman vortices and the use of phased array transducers was a good choice. This allowed us to measure rapid, weak and localized variations in ultrasonic time of flight.

The next step will be to measure the deviation of the ultrasounds when passing through the vortices. Again, the use of phased array transducers whose elements have a width of 0.5 mm seems well suited to measure local and small variations in acoustic energy.

The methodology presented in this study was created to validate ultrasonic measurements, which are a good candidate for monitoring variations in inhomogeneous liquid sodium. This methodology is now confirmed with numerical and experimental results on separate phenomena. The final validation will require the development of a more complex experimental bench which could create known variations in both temperature and local velocity fields.

Figure 1 .

 1 Figure 1. Diagram of IKHAR test section.

Figure 2 .

 2 Figure 2. Influence of Von Karman vortex on time of flight variations.

Figure 3 .

 3 Figure 3. Time of flight measurement on the two transducers (A and B) at the same time.

Figure 4 .

 4 Figure 4. Mapping of velocity field amplitude in XY plan. CFD simulation of IKHAR test section.

Figure 5 .

 5 Figure 5. Mapping of vorticity field along Z axis. CFD simulation of IKHAR test section

  213 rays were emitted orthogonally to the line. The time of flight of each acoustic ray was recorded on a receiving line of identical size, located at Y = 0.055 m. The following figure describes this arrangement.

Figure 6 .

 6 Figure 6. Position of acoustic rays emission line.

Figure 7 .

 7 Figure 7. Comparison of numerical time of flight variations obtained with AcRaLiS and experimental data obtained with IKHAR.