Dillon Pariente
email: dillon.pariente@dassault-aviation.com

Julien Signoles
email: julien.signoles@cea.fr

Static Analysis and Runtime-Assertion Checking: Contribution to Security Counter-Measures

This paper 3 presents a methodology which combines static analysis and runtime assertion checking in order to automatically generate counter-measures, and execute them whenever a flaw in the code which may compromise the security of an application is detected during execution. Static analysis pinpoints alarms that must be converted into runtime checks. Therefore the verifier is able to only monitor the security critical points of the application. This method allows to strengthen a security-critical source code in a cost-effective manner. We implemented it in the Frama-C framework and experimented it on a real use case based on Apache web server. The paper ends with preliminary considerations on potential perspectives for security evaluation and certification.

Introduction and context

Formal methods have been proved particularly powerful for runtime error search in safety context [START_REF] Bishop | Combining testing and proof to gain high assurance in software: A case study[END_REF][START_REF] Cuoq | Formal verification of software important to safety using the Frama-C tool suite[END_REF][START_REF] Souyris | Formal verification of avionics software products[END_REF], and also -more recently -for security verification and validation purpose, as demonstrated by recent success stories and compliance with international security standards [START_REF]PolarSSL 1.1.8 verification kit[END_REF]. Applying static analysis tools on real use cases, however, may represent an unaffordable cost with respect to non-vital programs whose allocated budget for verification activities is usually small compared to highly critical applications. Actually this is one of the most recurrent criticisms regarding widely spreading static analysis over source code validation and verification industrial practices: proving security properties or ensuring the absence of safety alarms may need extra-efforts like complex interactive proofs, heavy code annotation activities or lots of tool parameterizations for which an important amount of time and expertise is often required.

Therefore, this paper presents a method -named CURSOR -applicable to non-critical source code. First it is well known that most attacks exploit at least one vulnerability (sometimes referenced as a CVE: Common Vulnerability and Exposure4 ), which itself may be caused by one or several Common Weakness Enumeration (CWE) entries 5 6 . Based on this observation, CURSOR proposes to monitor some safety and security alarms raised by sound static analyzers (a relevant subset of the alarms detectable on C source code) in order to trigger predefined error-free counter-measures (CM) whenever alarms are really encountered at runtime. We have implemented this method within Frama-C [START_REF] Kirchner | Frama-C: A Software Analysis Perspective[END_REF], a framework for analysis of C source code which provides several sound static and dynamic analyzers, and experimented it on a real security-relevant use case: an Apache library. Indeed, Apache is one of the components used in an Aircraft e-Maintenance application (an ongoing development at Dassault Aviation) for which security analyses are required. The results demonstrate the usefulness of our approach, as well as its cost-efficiency.

Our contributions are therefore:

-a new cost-effective method, CURSOR, to trigger security counter-measures, which is based on static detection and runtime assertion checking of CWEs and requires no particular expertise in formal methods in order to be applied; -an implementation of this method within the Frama-C framework; -and its experimentation on a security-critical Apache library used in an Aircraft e-Maintenance application.

The paper is organized as follows. Section 2 presents Frama-C and its analyzers of interest for our study, namely its plug-ins Value and E-ACSL. Then Section 3 details the CURSOR method applied to an Apache library. Finally Section 4 briefly introduces practical considerations about security evaluation and certification concerns.

Tools: Static Analysis Contribution to Runtime-Assertion Checking

The CURSOR method, explained in Section 3, has been implemented within the Frama-C framework which we sum up here. More details can be found in Frama-C-specific papers [START_REF] Kirchner | Frama-C: A Software Analysis Perspective[END_REF][START_REF] Kosmatov | Frama-C, a Collaborative Framework for C Code Verification[END_REF]. Section 2.1 is a general overview of the framework while Section 2.2 and Section 2.3 describe the two most important plug-ins in our context, namely Value and E-ACSL, which respectively provide static analysis by abstract interpretation and runtime assertion checking.

Frama-C Overview

Frama-C is an open source platform7 which aims at analyzing source code written in ISO C99. This code may be annotated in ACSL formal specification language [START_REF] Baudin | ACSL: ANSI/ISO C Specification Language[END_REF] (briefly introduced later on in this section).

Recently Frama-Clang has been released as a prototype Frama-C extension to handle C++ code. The platform gathers together code analyzers. It is written in OCaml [START_REF] Cuoq | Experience report: Ocaml for an industrialstrength static analysis framework[END_REF] and based on a plug-in architecture [START_REF] Signoles | Software Architecture of Code Analysis Frameworks Matters: The Frama-C Example[END_REF]: each analyzer is a plug-in which is linked against the Frama-C kernel. This architecture allows users (including external ones) to easily extend the framework with extra features through new plug-ins [START_REF] Signoles | Frama-C Plug-in Development Guide[END_REF]. This proved useful for the CURSOR method whose implementation partly relies on a dedicated plug-in, namely Gena-CWE which is introduced in Section 3.

The Frama-C kernel provides a normalized representation of C programs and ACSL specifications. In addition, it yields several general services for supporting plug-in development and providing convenient features to Frama-C's end-users. The kernel also allows plug-ins to collaborate together either sequentially or in parallel. Sequential collaboration consists in a chain of analyses that perform operations one after another, while parallel collaboration combines partial analysis results from several analyzers to complete a full program verification. The CURSOR method described in Section 3 exemplifies sequential collaboration (it is however worth mentioning that in Frama-C, parallel collaboration relies on kernel consolidation of analysis results detailed in [START_REF] Correnson | Combining Analyses for C Program Verification[END_REF]).

The ACSL specification language is a tool of choice when combining Frama-C analyzers. Indeed it is shared by the whole framework: any analyzer may both verify and generate ACSL annotations, which can in turn be verified by other analyzers. Generally, ACSL allows its users to specify functional properties of C programs similarly to Eiffel [START_REF] Meyer | Object-Oriented Software Construction[END_REF] and JML [START_REF] Gary | How the design of JML accomodates both runtime assertion checking and formal verification[END_REF]. It is based on the notion of function contract which specifies the preconditions that are supposed to be true before a call of f (i.e. ensured by the caller), and the postconditions that should be satisfied after the call of f (and should be thus established during the verification of f ). Numerous examples may be found in the reference tutorial [START_REF] Burghardt | ACSL by Example[END_REF]. The most important feature of ACSL for this paper is assertions: predicates which must hold at a particular program point. It is worth noting that ACSL is powerful enough to be able to express most C99 undefined behaviors with such predicates as illustrated later on this paper. A Frama-C plug-in named RTE may even be used to generate ACSL assertions for every potential errors corresponding to certain families of runtime errors.

Value

The Value Analysis plug-in of Frama-C (Value for short) [START_REF] Cuoq | Frama-C's value analysis plug-in[END_REF] may still be proven by another plug-in, possibly a dedicated one. This Frama-C ecosystem leads to another Value functionality: the possibility to reuse its results. Indeed what Value has computed is (partly) available in the Frama-C GUI and helps the user better understand Value's results. An illustrative example for PolarSSL 1.1.710 is presented in Figure 1. It also allows derived analyses like slicing to be sound. In particular it helps these analyses to safely interpret function pointers and find out potential aliasing. In this way, several plug-ins have been developed by academic and industrial users for proving specific goals in a safe way without spending too much time with pointer intricacies [START_REF] Berthomé | Attack model for verification of interval security properties for smart card C codes[END_REF][START_REF] Cuoq | Fan-C, a Frama-C plug-in for data flow verification[END_REF][START_REF] Demay | SIDAN: a tool dedicated to software instrumentation for detecting attacks on non-control-data[END_REF]. The CURSOR method introduced in this paper also collaborates with Value by inspecting its results in order to discover complementary CWE alarms (see Section 3).

E-ACSL

Frama-C was originally oriented towards static verification. Consequently ACSL has the same bias. In particular, it contains several constructs (e.g. unbounded quantifications and axioms) with a well-defined mathematical meaning but no computational semantics because they cannot be executed. To circumvent this issue, an "executable" subset of ACSL has been identified in which all constructs are computationnally well-defined. This specification language is called E-ACSL ("E" stands for "executable") [START_REF] Delahaye | Common specification language for static and dynamic analysis of C programs[END_REF]. All annotations in this paper are actually both ACSL and E-ACSL annotations. In particular, all assertions corresponding to detectable CWEs and automatically generated by RTE and Value fall into this category.

A Frama-C plug-in also called E-ACSL is in charge of transforming E-ACSL annotations into executable code. More precisely, E-ACSL is a program transformation tool: it takes as input a C program p annotated with E-ACSL specifications and generates another C program which observationally behaves like p if each annotation is satisfied, or stops on the first failing annotation otherwise. In other words, E-ACSL generates an inline monitor [START_REF] Falcone | A tutorial on runtime verification[END_REF] for a C program based on its formal specification. The translation scheme is described in Figure 2. It highlights the fact that E-ACSL benefits from Frama-C and uses static analyses to optimize the generated code. For instance, before generating the code, it implements a backward sound over-approximating analysis [START_REF] Jakobsson | Fast as a Shadow, Expressive as a Tree: Optimized Memory Monitoring for C[END_REF] in order to reduce the instrumentation of memory: if there is no annotation depending on some memory location l (e.g. corresponding to some program variable x), there is no need to track its allocation, initialization and de-allocation. During code generation, it also uses a dedicated type system to optimize operations over integer (which are mathematical integers in E-ACSL) [START_REF] Jakobsson | Rester statique pour devenir plus rapide, plus précis et plus mince[END_REF]. It also takes care of not generating C99 undefined behaviors when translating annotations. The E-ACSL plug-in does require E-ACSL-annotated code as input. However there is no need to write these annotations manually. Therefore E-ACSL may really be used as a fully automatic tool. For instance, if interested in certain classes of runtime errors, the user may first use the RTE plug-in to generate E-ACSL annotations and then use E-ACSL to monitor them at runtime. Used this way, E-ACSL is similar to memory debuggers like ASan and MemCheck (built on top of Valgrind). Recent experiments on programs from SPEC CPU benchmark 11 show that runtime overheads of E-ACSL are on average 19 times the normal execution [START_REF] Vorobyov | Shadow State Encoding for Efficient Monitoring of Block-level Properties[END_REF]. That is comparable to MemCheck, while the average overhead of ASan is about 2. It is worth noting that E-ACSL checks more properties than these memory debuggers. The implementation of the CURSOR method uses E-ACSL in this spirit but in a more cost-efficient way (see Section 3). E-ACSL also allows to modify its default behavior which is to stop the program execution whenever an annotation is violated. Once again, the implementation of the CURSOR method relies on this feature.

CURSOR: principles and results

The method presented in the following is straightforward for some categories of applications and security flaws. The process is intended to be as simple as possible. For a few families of CWEs, it is almost fully automated for cost-efficiency, and provides a sensitive improvement regarding security flaw robustness.

At first, this process consists of identifying source code libraries of functionalities worth analyzing in order to be strengthened. For instance in the context of web applications and servers, it may consist of sets of functions dealing with low-level file management, sanitizing functions on strings or URLs, etc. These functions may implement SFR (Security Functional Requirements) as defined in Common Criteria 12 . These SFR are intended to meet the security objectives, which means to counter threats in the assumed operating environment of the ToE.

Then, a static formal analysis is performed by applying Frama-C's Value plug-in: at this point, several categories of CWE may be found in the C source code. TrustInSoft Analyzer 13 , which is based on the Frama-C platform and Value, was able for instance to identify automatically several CWEs (119 to 127: buffer-related weaknesses, 369: divide-by-zero, 415: double-free, 416: use-after-free, 457: use of uninitialized variable, 476: null pointer dereference, 562: return of stack variable address, 690: unchecked return value to null pointer dereference) on some commercial-of-the-shelf software [START_REF]PolarSSL 1.1.8 verification kit[END_REF]. When analyzing a source code with Value, the CWEs are expressed as ACSL annotations attached to the related statement. For instance, consider the following code snippet: // ...

j = i + 1; x = * ( p + j ) ; // ...
Value may raise some alarms as ACSL assertions: for instance an integer overflow 14 on the first statement, and an invalid dereferencing in the second one, as follows. These alarms could be spurious as the runtime context might never lead to an error or actual exploitable security flaw. The false positive alarms may be due to static over-approximations inherent to sound analyses by abstract interpretation, or a too imprecise initial state (i.e. domains of value for each location in memory) at the entry point of the analysis.

Once Value analysis has been performed, categories of CWEs are identified in the source code under study (in our sample code: CWE-190 "Integer Overflow or Wraparound", and CWE-125 "Out-of-bounds Read"). At this point, the CURSOR method benefits from the possibility to write its own Frama-C plug-ins [START_REF] Signoles | Frama-C Plug-in Development Guide[END_REF]: CURSOR is enriched by some scripts gathered in a plug-in named Gena-CWE. This plug-in detects complementary categories of CWEs which are not directly displayed by Value but are however computed and can be obtained by adequately querying its abstract states. For instance, among others, it can detect and locate CWE-174 "Double Release of Resource", CWE-457 "Uninitialized Variables", CWE-570 "Always False conditions", CWE-571 "Always True conditions". If not relevant with regards to risk analysis, the search for some families of CWE can also be deactivated.

In the case of a library, Value is applied function-by-function: the C functions under analysis can potentially be called at runtime from any control point of the application. Thus, it is necessary to analyze these functions with the largest possible input domain for each of their arguments, independently from the calling context. As Value is a context-sensitive analysis, the functions are analyzed and thus annotated separately.

The code, once automatically annotated with ACSL alarms corresponding to potential CWEs, can now be analyzed by the E-ACSL plug-in in order to translate all these annotations into executable statements. The previous code snippet is then transformed as the following instrumented code: e _ a c s l _ a s s e r t ( _ _ e _ a c s l _ v a l i d _ r e a So far, some code is added by E-ACSL which will be executed at runtime. It mainly contains memory management statements specific to E-ACSL, and condition evaluations corresponding to each alarm 15 . In case the conditions are met during execution (i.e., in the example code above, if the first argument of function e_acsl_assert is true), some extra-code will be triggered. Indeed, this extra-code constitutes the implementation of the related counter-measures (CM) in case the ACSL alarms are activated, making the application potentially more robust to attacks based on the targeted weaknesses in the source code. At the origin, e_acsl_assert was intended to stop the code execution -thus at runtime -whenever a violation was detected. But in CURSOR this mechanism is extended in such a way that the execution continues, activating some pre-defined counter-measure behaviors. All the arguments of e_acsl_assert can be used by the CM functions: of course the boolean condition, but also the kind of emitted alarm ("Assertion" in the example), the function in which this alarm is raised, the alarm expression itself, and finally the location (line number) in the source file.

In practice, these CM may range from logging the information (storing what happened, where and why, for any further processing as in case of forensics for instance), to halting the service or the system (or even any other defensive or "retaliating" measures!). The choice of the adequate CM is left to the user, with regards to the corresponding security risk analysis -only the latter is able to help identifying efficiently the relevant parts of the software to be CURSOR-ed. It is worth noting that these CM functions can be either specific to the alarm location and its context, or definitely generic. This is possible thanks to the information passed as argument at the calling context generated for each alarm: annotation kind, file location, rationale, etc., on which any on-the-fly filtering will allow to trigger the most suitable counter-measure.

Of course, these CM functions must themselves be free of dreaded weaknesses. The last step of the process will therefore consist in formally verifying the absence of flaws in the implementation of these CM functions according to security functional requirements (which includes avoiding any disclosure of sensitive data related to the triggered weaknesses). This is done by means of the Frama-C platform, its static analyzers, and possibly a set of security functional ACSL properties annotated in the source code. The plug-ins mostly involved in these verifications are Value and Wp 16 . When required, they are also combined with dynamic analyses. Indeed, dynamic analyses may help static ones decide the validity of some complex alarms: for instance, dynamic approaches combining fuzzy testing and static techniques [START_REF] Kiss | Dynamic analyses for vulnerability detection: Illustration on heartbleed[END_REF] can automatically generate executable scenarios that will compromise a given sought security property, and thus confirm the presence of a related vulnerability. Otherwise, the very same property could have required important efforts and expertise to be discharged when only using formal methods. Indeed, static and dynamic techniques are commonly seen as able to palliate their mutual limitations in numerous situations, and their coupling constitutes a promising field of investigation extending results presented in [START_REF] Kiss | Dynamic analyses for vulnerability detection: Illustration on heartbleed[END_REF].

A more sophisticated -thus less push-button -version of the CUR-SOR method is currently defined in this regard, yielding some hints on static/dynamic possible combinations, but this approach still needs more experiments and consolidations at this stage.

Finally, the whole annotated code enriched with automatic CM calling contexts and CM implementations can be pentested for further detection of vulnerabilities not caught by static analysis (therefore by dynamic analysis means, like automatic security-oriented fuzzers -as AFL 17 -, applied on the instrumented program) and/or embedded into the system for operations. Figure 3 presents the whole process. In this figure, squares represent either existing tools or complements implemented for the sake of the method. It is worth noting that generating, even automatically, as many CM calling contexts as alarms (spurious or not) may result in a lot of extra-code, and in some cases with potential impacts on the execution time and memory consumption at runtime. This point is addressed by several means. First, the method is not applied to the whole application, but only on security sensitive parts (typically some wellchosen libraries). Second, some strategies relying on security risk analysis might allow to get rid of some categories of alarms (or CWEs) emitted by Frama-C plug-ins: from a functional viewpoint, for a given function, the same alarm kind occurring on the same variable but in different control points should be kept only once in the source code, namely the first time it appears in the control flow. This heuristic has been implemented by a new Frama-C script, with no particular difficulty from a technical point of view. However, it may also break the soundness of the formal analyses, and thus should be used with care and duly justified.

Application to Apache libraries. The simplified process presented above was applied to several Apache libraries. As an illustration, it was used to strengthen the httpd/server/util.c source code, a representative library containing some file management and sanitizing functions, relevant for security analysis purpose. The snapshot of this (100+ functions) library callgraph is given in Figure 4. This code is originally 7,958 loc (before pre-processing by Frama-C, 14.8 kloc afterward in particular because of macro expansions and inclusion of external libraries). On this library, 340 ACSL annotations are generated by Value and Gena-CWE. E-ACSL plug-in is then applied, expanding instrumented source code to 9,759 loc (excluding counter-measures to be implemented on the user side). This instrumentation represents an increase of about 22% of the original source code size. This code can then be compiled and executed: any violation of a CWE alarm will thus trigger one of the implemented counter-measures, with negligible impact on memory consumption and execution time from a functional standpoint (for more issues about performance, see [START_REF] Vorobyov | Shadow State Encoding for Efficient Monitoring of Block-level Properties[END_REF]).

Security Evaluation and Certification Considerations

(This section briefly presents some insights into CURSOR and Common Criteria certification process. For convenience, it can be skipped for the reader not concerned with certification issues.)

The CURSOR method has a clear impact on the attack surface and application behavior, which is definitely modified by inserting the CM calling contexts into the source code. These CM intend to drastically change the behavior of the application under analysis. In this respect, the pentester (and possibly the hacker) will face different reactions for theapparently -same software according to whether CURSOR was applied or not. Namely, whenever a pentester might expect triggering an error from a given vulnerability in the code (for instance detected after a "fruitful" white-box manual review of the source code), the CURSOR-ed version of the application will bifurcate at runtime to the corresponding CM which may be as stealthy as possible (at least, the CM should hide clues to the pentester about the original flaw in the code), and thus diverting from the expected original behavior.

Besides, in a Common Criteria (CC) certification context, the method presented in this paper comes with some clear benefits (in the following ATE_* and FAU_* identify some CC security requirements):

-Completing in some extent the security functional requirements (SFR) through automatic generation of potential alarms and their executable translation, -Replacing some documentation effort by generating evidence: providing automated coverage testing (ATE_COV) marks for the new functional requirements, -Security audit data generation (FAU_GEN): the executable code generated by the CURSOR method allows to log causes of crashes or attack "witnesses", then contributing to the FAU_GEN requirement, -To some extent, security audit automatic response (FAU_ARP), analysis (FAU_SAA), and review (FAU_SAR) can also be addressed by CURSOR.

These considerations are not exhaustive, and still preliminary at this stage. Further analyses are necessary to assess the perimeter of use and the benefits which can be expected when applying the CURSOR method in a certification process. However, the approach seems already quite promising, and cost-efficient from security and affordability standpoints.

Conclusion and Perspectives

The CURSOR method presented in this paper permits to automatically counter some families of attacks based on CWEs. It first consists in generating as many ACSL alarms in the source code as the Frama-C sound formal static analyzers will find, and then translating them -even the spurious ones -as executable code for further pentesting/dynamic analyses and eventually operational use. Most of the process is fully automated, and scalable as the static formal analyses can be done functionby-function. It is also cost-efficient as no particular expertise is needed in formal methods, at least in the simplified version of the method: ACSL annotations corresponding to security alarms are not expected to be discharged during the process.

CURSOR remains a straightforward exploitation of Frama-C plug-ins, with some further developments depending on the complementary and relevant CWEs refined from application-dependant security risk analyses. Moreover, future developments will consist in developing a Frama-C plug-in to automatically classify Frama-C alarms with respect to their corresponding CWEs, while extending the scope of detectable CWEs. First experiments with CURSOR method, performed in an R&T context at this stage, are quite conclusive, even for open source applications for which design and development documentations are either unavailable, or only exploitable with a certain amount of investment not always affordable for applications with a low level of criticality. It is worth noting that this paper includes the very first publicly available R&T evaluation of E-ACSL. Yet the exact impact of the deployment of counter-measures in terms of time efficiency and memory consumption is still to be done, even if recent intensive benchmarking on an evolved version of E-ACSL [START_REF] Vorobyov | Shadow State Encoding for Efficient Monitoring of Block-level Properties[END_REF] might suggest it is clearly acceptable. Also E-ACSL is still a young tool and lots of improvements are already planned to enhance memory footprint and computing time consumption of the generated monitors, as well as the scope of sought security alarms. Some insights were also presented in this paper with regards to security evaluation and CC certification processes, which might be argued and deepened in order to obtain concrete recognition of CURSOR's benefits among security communities and certification bodies.

Fig. 1 .

 1 Fig. 1. Frama-C GUI with Value's results on PolarSSL's function net_recv. It displays the possible values of the function's parameter buf per callstack.

Fig. 2 .

 2 Fig. 2. E-ACSL Translation Scheme.

/

  / ... /* @ assert Value : s i g n e d _ o v e r f l o w : i +1 <= 2 1 4 7 4 8 3 6 4 7 ; */ j = i + 1; /* @ assert Value : m e m _ a c c e s s : \ v a l i d _ r e a d ( p + j ) ; */ x = * ( p + j ) ; // ...

/

  / ... /* @ assert Value : s i g n e d _ o v e r f l o w : i +1 <= 2 1 4 7 4 8 3 6 4 7 ; */ _ _ s t o r e _ b l o c k (( void *) (& p ) ,4 U ) ; e _ a c s l _ a s s e r t ( i + 1 <= 2147483647 , ( char *) " Assertion " ,( char *) " f_ABSCAL " , ( char *) " Value : s ig ne d _o ve rf l ow : i +1 <= 2147483647 " , 3056) ; j = i + 1; /* @ assert Value : m e m _ a c c e s s : \ v a l i d _ r e a d ( p + j ) ; */ { int _ _ e _ a c s l _ v a l i d _ r e a d ; _ _ e _ a c s l _ v a l i d _ r e a d = _ _ v a l i d _ r e a d (( void *) ( p + j ) , sizeof ( char ) ) ;

  d ,( char *) " Assertion " ,( char *) " f_ABSCAL " , ( char *) " Value : mem_access : \\ valid_read ( p + j ) " ,3058) ; } x = ( char *) *( p + j ) ; _ _ d e l e t e _ b l o c k (( void *) (& p ) ) ; _ _ e _ a c s l _ m e m o r y _ c l e a n () ; // ...

Fig. 3 .

 3 Fig. 3. CURSOR method process.

Fig. 4 .

 4 Fig. 4. An Apache library's callgraph.

  Value

	automatically computes sets of possible values 8 for the variables of an analyzed program at each program point, by means of abstract interpretation [7]. It also warns about potential runtime errors through the generation of ACSL annotations similar to those of the RTE plug-in. Value aims at being directly usable on any C code in any applicative domain, from low-level system libraries to safety-critical applications. Indeed Value relies on a general-purpose efficient domain (a.k.a. lattice) in order to represent the possible values of memory locations at each program point. However this domain can be less precise than a custom domain designed for a particular code pattern. In order to circumvent this issue,

has recently been improved by Eva (Evolved Value Analysis)

[START_REF] Blazy | Structuring abstract interpreters through state and value abstractions[END_REF]

which aims at reconciling the efficiency of the Value's domain with the flexibility of collaborative custom domains. Another way to circumvent possible precision issues is provided by Frama-C itself: what cannot be proven by Value (or Eva)

9

This work is done in the context of project VESSEDIA, which has received funding from the European Union's Horizon 2020 Research and Innovation Program under grant agreement No 731453.

http://cve.mitre.org

http://cwe.mitre.org

See for instance https://www.cvedetails.com/vulnerability-list/cweid-200/ vulnerabilities.html

http://frama-c.com

These sets are named domains, and can be represented in their simplest form as intervals of values.

Value and Eva share the same user interface. The rest of this paper applies in the same way to both plug-ins. We will continue to use Value for the sake of consistency.

See https://tls.mbed.org/.

https://www.spec.org/cpu/

A standardized framework for the definition and validation of the security provided by a given product (a.k.a. Target of Evaluation, or ToE). http://www. commoncriteriaportal.org

[START_REF] Demay | SIDAN: a tool dedicated to software instrumentation for detecting attacks on non-control-data[END_REF] https://trust-in-soft.com

The interested reader may refer to the E-ACSL documentation[START_REF] Signoles | E-ACSL User Manual[END_REF] and related publications[START_REF] Jakobsson | Fast as a Shadow, Expressive as a Tree: Optimized Memory Monitoring for C[END_REF][START_REF] Kosmatov | An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs[END_REF][START_REF] Vorobyov | Shadow State Encoding for Efficient Monitoring of Block-level Properties[END_REF] for further details, in particular on how pointer validity is efficiently managed at runtime through the tracking of allocated memory blocks.

American Fuzzy Lop: http://lcamtuf.coredump.cx/afl

Acknowledgements:

The authors would like to thank Marion Daubignard, Raphaël Rigo and the anonymous reviewers for their helpful and constructive comments that contributed to improving the final version of the paper.


Juan J Garcia Pabon

Leandro C Pereira

Gleberson Humia

Ali Khosravi

Rémi Revellin

Jocelyn Bonjour

Luiz Machado

Experimental study on the void fraction during two-phase flow of R1234yf in smooth horizontal tubes

Keywords: Void fraction, quick-closing valve(s) method, R1234yf, R134a, Two-phase flow, Smooth horizontal tubes

Void fraction is an important parameter to design and simulate thermal systems involving two-phase flows. In this research, an experimental investigation of the void fraction in adiabatic two-phase flow of R1234yf in horizontal and smooth tubes with an internal diameter of 4.8 mm was carried out. For the experimental tests, the vapor quality ranges from 0.1 to 1 while two saturation temperatures (15 and 25°C) and two mass flow rates (180 and 280 kg.m -2 s -1 ) are investigated. The quick-closing valve(s) method is used to measure the volumetric void fraction. Tests are also undertaken with R134a used as a reference in this study. The results highlight that the void fraction of R1234yf is 5% lower than that for R134a. In addition, the experimental data of R1234yf were compared against seven correlations from the literature: the Baroczy and the Hughmark correlations were shown to provide the best prediction, with a mean absolute error of 2% and 3.2%, respectively.

INTRODUCTION

In recent years, many researches in the field of engineering were motivated by the global environmental concerns. They were aiming at developing and optimizing the conventional engineering systems, or at introducing new materials and configurations for industrial equipment [START_REF] Khosravi | Numerical analysis of magnetic field effects on the heat transfer enhancement in ferrofluids for a parabolic trough solar collector[END_REF]. R134a is an extremely common refrigerant used in a wide range of refrigeration systems and air conditioning (both domestic and commercial) including small and medium capacity and medium and high temperature refrigeration [START_REF] Khosravi | Thermo-economic analysis and sizing of the components of an ejector expansion refrigeration system[END_REF]. However, this fluid has a high Global Warming Potential (GWP=1340 t CO 2 eq), and it is responsible for 2% of the greenhouse gases present in the atmosphere [START_REF] Thompson | Advancing ozone and climate protection Technologies: next steps[END_REF]. International regulations (e.g.

the directive 517/2014 of Europe Union) impose that R134a should phase out and be replaced [START_REF] Sánchez | Energy performance evaluation of R1234yf, R1234ze(E), R600a, R290 and R152a as low-GWP R134a alternatives[END_REF].

Among several candidates to substitute this fluid, R1234yf (GWP<1 t CO 2 eq) is a great option [START_REF] Garcia | Comparison of transient response of an evaporator model for water refrigeration system working with R1234yf as a drop-in replacement for R134a[END_REF]. The thermophysical properties of R1234yf are similar to R134a [START_REF] Cho | Experimental investigation of performance and exergy analysis of automotive air conditioning systems using refrigerant R1234yf at various compressor speeds[END_REF]. Several investigations evaluated and compared the performance of R134a and R1234yf as working fluid in refrigeration and air conditioning systems [START_REF] Garcia | Comparison of transient response of an evaporator model for water refrigeration system working with R1234yf as a drop-in replacement for R134a[END_REF]. Initially, the efficiency of R1234yf refrigerant has been studied in automotive systems [START_REF] Lee | A brief performance comparison of R1234yf and R134a in a bench tester for automobile applications[END_REF][START_REF] Qi | Performance improvement potentials of R1234yf mobile air conditioning system[END_REF][START_REF] Qi | Experimental study on evaporator performance in mobile air conditioning system using HFO-1234yf as working fluid[END_REF]. Nowadays, researches continue to study the efficiency of R1234yf in other refrigeration equipment. For example, [START_REF] Belman-Flores | Experimental study of R1234yf as a drop-in replacement for R134a in a domestic refrigerator[END_REF] studied the efficiency of R1234yf in domestic refrigerator; [START_REF] Nawaz | R1234yf and R1234ze(E) as low-GWP refrigerants for residential heat pump water heaters[END_REF] and [START_REF] Botticella | Multi-criteria (thermodynamic, economic and environmental) analysis of possible design options for residential heating split systems working with low GWP refrigerants[END_REF] applied R1234yf in residential heat pumps. These investigations showed that R1234yf can be considered as an alternative for R134a with the same efficiency and without large changes on the equipment.

In addition, for this substitution, characterizing the behavior of R1234yf during two-phase flow is fundamental. Many studies focused on the evaluation of the heat transfer coefficient of R1234yf [START_REF] Anwar | Flow boiling heat transfer, pressure drop and dryout characteristics of R1234yf: Experimental results and predictions[END_REF][START_REF] Choi | Comparison of heat transfer coefficient during evaporation of natural refrigerants and R-1234yf in horizontal small tube[END_REF][START_REF] Del Col | Flow boiling of R1234yf in a 1 mm diameter channel[END_REF][START_REF] Del Col | Heat transfer and pressure drop during condensation of the low GWP refrigerant R1234yf[END_REF][START_REF] Illán-Gómez | Experimental twophase heat transfer coefficient and frictional pressure drop inside mini-channels during condensation with R1234yf and R134a[END_REF][START_REF] Li | Flow boiling heat transfer of HFO1234yf and R32 refrigerant mixtures in a smooth horizontal tube: Part I. Experimental investigation[END_REF][START_REF] Lu | Investigation of the two-phase convective boiling of HFO-1234yf in a 3.9 mm diameter tube[END_REF][START_REF] Mortada | Boiling heat transfer and pressure drop of R-134a and R-1234yf in minichannels for low mass fluxes[END_REF][START_REF] Saitoh | Boiling heat transfer of HFO-1234yf flowing in a smooth small-diameter horizontal tube[END_REF][START_REF] Sempértegui-Tapia | Flow boiling heat transfer of R134a and low GWP refrigerants in a horizontal micro-scale channel[END_REF][START_REF] Wang | Experimental study on condensation heat transfer and pressure drop of low GWP refrigerant HFO1234yf in a horizontal tube[END_REF]. [START_REF] Padilla | Flow regimes and twophase pressure gradient in horizontal straight tubes: Experimental results for HFO-1234yf, R-134a and R-410[END_REF] investigated the two-phase flow patterns of R1234yf. [START_REF] Mastrullo | Experimental CHF for low-GWP fluids and R134a. Effect of the Lh/D ratio at low and high mass velocities[END_REF][START_REF] Mastrullo | Critical heat flux: Performance of R1234yf, R1234ze and R134a in an aluminum multi-minichannel heat sink at high saturation temperatures[END_REF] studied the critical heat flux during flow boiling of R1234yf.

However, the void fraction for R1234yf was no studied.

The volumetric void fraction is defined as the ratio between the volume of vapor and the total volume of a two-phase liquid-vapor mixture. This parameter is crucial for the determination of the inventory, which is the quantity of mass fluid refrigerant in refrigeration systems. The void fraction

A C C E P T E D M A N U S C R I P T
is predicted with a variety of prediction tools (semi-empirical correlations or models) available in the literature.

There are several measurement methods to determine the void fraction, among which the capacitance, conductance, optical, ultrasonic, or radiative methods are renowned [START_REF] Tompkins | Wire-mesh sensors: A review of methods and uncertainty in multiphase flows relative to other measurement techniques[END_REF]. Radiative methods are non-intrusive techniques that employ radiations such as neutron, gamma, and X-rays. The radiative methods are expensive compared to other methods, and precautions must be taken for radiation source. The sonic methods (that use ultrasound or acoustic transmissions) are limited to the low vapor fractions. The processing of ultrasonic techniques requires significant computational effort and small changes in the setup geometry have a large impact on the accuracy of the results [START_REF] Schabowicz | Ultrasonic tomography -The latest nondestructive technique for testing concrete members -Description, test methodology, application example[END_REF]. The optical-based methods use the attenuation of light or laser. These methods also have the disadvantages of high cost and higher requirements of the measurement environment [START_REF] Li | A New Void Fraction Measurement Method for Gas-Liquid Two-Phase Flow in Small Channels[END_REF]. The visualization method includes high-speed cameras, digital cameras, and optical tomography, etc. The information extracted from these 2D images is limited [START_REF] Li | Void fraction measurement of bubble and slug flow in a small channel using the multivision technique[END_REF]. Electrical methods are based on the difference in the permittivity, conductivity or impedance between the fluid phases. Their accuracy depends significantly on the flow regime [START_REF] Paranjape | Electrical impedance-based void fraction measurement and flow regime identification in microchannel flows under adiabatic conditions[END_REF].

In addition to the methods mentioned above, the void fraction can be measured by quick-closing valves (QCV) method. Two valves are located upward and downward of the test section and actuated (closed) simultaneously causing an almost immediate two-phase flow interruption.

Following, the contained mass fluid is measured. The cross-section area and length of the tube are known, then the average void fraction can be deduced from the measurement of fluid mass. This method has an advantage that can be employed for any flow patterns with a low cost and low uncertainty. The QCV method was used to obtain the results published in the present research.

Experimental studies involving the QCV method were performed by [START_REF] Abdul-Majeed | Liquid holdup in horizontal two-phase gas-liquid flow[END_REF] for kerosene-air two-phase flow, and [START_REF] Sujummong | Heat transfer, pressure drop and void fraction in two-phase, two compo-nent flow in a vertical tube[END_REF] for water-glycerine two-phase flow. Rocha and Simões-Moreira (2008) used the QCV method and Multiple-Electrode Impedance Sensors to measure void fraction in air-water two-phase flow in a vertical tube. The QCV method was considered as calibration standard for void fractions ranging from 0.17 to 0.7 and had an overall void fraction measuring uncertainty of 0.05. [START_REF] Funahashi | Interfacial and wall friction factors of swirling annular flow in a vertical pipe[END_REF] measured the void fraction of air-water flow by the QCV method with an uncertainty of 0.15%. Recently, [START_REF] Qian | Void Fraction Measurement and Flow Regimes Visualization of R134a in Horizontal and Vertical ID 7 mm Circular Tubes[END_REF] measured the void fraction by the QCV in horizontal and vertical round smooth tubes (ID 7 mm) with R134a in the adiabatic conditions, saturation temperature at 33°C and low mass fluxes (40-150

A C C E P T E D M A N U S C R I P T 5
kg/m²s). They concluded that the void fraction of horizontal tubes is larger than that of vertical tubes, and higher mass flux also results in larger void fraction compared that of lower mass flux.

Based on the literature, many studies were conducted to investigate R1234yf from different aspects including the efficiency in refrigeration systems, size of the components, two-phase flow patterns, and critical heat flux. The present investigation focuses on of the void fraction of R1234yf.

For this target, several experimental tests using the quick-closing valves method are performed for R1234yf, as well as for R134a that is considered as a well-known reference. The void fractions for both fluids are compared and presented. The effect of saturation temperature, mass flux and vapor quality on void fraction is analyzed. In addition, a compare son between the experimental data and classical prediction tools is carried out.

EXPERIMENTAL SETUP

Figure 1 shows a schematic of the experimental setup used to measure the void fraction. The refrigerant loop is made of a copper tube with an internal diameter of 4.8 mm and consists of a selflubricating oil-free gear micropump (series GJ of MICROPUMP INC) which delivers subcooled refrigerant to the heater. The refrigerant is preheated and partially evaporated in the heater to the desired vapor quality. The fluid passes through the test section (2 m length and 4.8 mm inner diameter), and then, the fluid is condensed and subcooled in the condenser. Finally, the refrigerant returns to the micropump as a subcooled liquid. To reduce the heat exchange with the surroundings, the entire apparatus was insulated. The refrigerant flow rate can be controlled by adjusting the frequency of the magnetic gear pump. The vapor quality at the inlet of the test section can be adjusted by the heating power supplied to the refrigerant in the pre-heater. The pressure can be controlled in the condenser by means of water loop, whose temperature can be chosen by the operator owing to an auxiliary refrigeration system. A sub-tank with a water bath was used to control the amount of refrigerant in the circuit for each test.

Thermocouples and pressure transducers were installed in various position of refrigerant loop to determine the fluid conditions. The accuracy of the T-type thermocouples was within ±0.2°C.

The pressure was measured using calibrated manometers (Novus, model NP460) with an accuracy of ±0.02 bar. The facility also included a turbine-type flow meter (Kobold, model DPM-1130) with accuracy of ±3.0%. The electrical input power in the pre-heater was measured using a voltmeter and amperemeter with accuracy of ±1.6%. Once steady state was reached, the valves were closed. The accumulated fluid in the test section was conducted to a bottle (previously in vacuum) by opening the third valve which links the test section with the bottle. The test section is heated for a short period of time to fully evaporate the fluid in the tests section. When the thermal and mechanical equilibrium between the test section and the bottle was reached, the third valve is closed and the bottle is weighed by a precision scale (model AD2000 MARTE) with uncertainly of ±0.1g.

Data reduction

The mass flux is calculated as:

2 4m G D   (1) Water loop m MP 8 P5 A C C E P T E D M A N U S C R I P T 7
where ̇ is the measured mass flow rate and is the internal cross-sectional area of the tube.

The flashing effect was calculated based on equation developed by [START_REF] Revellin | A comprehensive non-equilibrium thermodynamic analysis applied to a vapor-liquid two-phase flow of a pure fluid[END_REF], and was found to be negligible. Thus, the vapor quality at the outlet of the preheater could be determined through a simple energy balance over the preheater.

 

, , , ,

1 ph ph out l ph ph in lv ph Q x i i im        (2)
where is the enthalpy of the liquid at the inlet of the preheater, is the enthalpy of the saturated liquid and is the latent heat of vaporization considering the saturation temperature at the outlet of the preheater (inlet of the test section). The ̇ is the heat rate in the preheater:

ph ph ph ph QI   (3)
where and are the voltage and current electrically applied in the preheater. is the efficiency between heat and electrical power in the preheater. It was identified owing to preliminary single-phase experimental calibration ( ).

Finally, the void fraction in the test section is calculated as:

  1 ts l l v ts M V            (4)
where and are the mass and volume of fluid contained in the test section, and are the liquid and vapor density, respectively, at the considered saturation temperature. was measured through the previous measurement regarding volume of water into the test section (prior to running the experiment).

The mass of fluid in the test section was calculated as the sum of mass of fluid contained in the bottle measured with the balance and the mass of the vapor constrained in the test section after the equilibrium with the bottle had been reached (the vapor density is a function of room temperature and pressure in the steady state of test section-bottle set). The preliminary single-phase experiments mentioned previously were mostly made to validate the QCV method. They essentially consisted in applying the methodology described previously to a single-phase flow, i.e. trap a certain amount of liquid in the test section, let the equilibrium establish with the bottle, weigh the bottle and apply

A C C E P T E D M A N U S C R I P T 8
Eq. ( 4). This was done for different mass fluxes and saturation temperatures. Obviously, a void fraction equal to zero was expected independently of the experimental conditions for such singlephase flow. The standard deviation 1 of the whole dataset of measurements for these single-phase flow tests was found to be 0.045, so that the QCV was validated.

Uncertainty analysis

The uncertainty analysis was carried out to assess the quality and the repeatability of the experimental data following the procedure exposed by [START_REF] Moffat | Describing the uncertainties in experimental results[END_REF]. The known accuracy of instruments (refrigerant and water mass flow meters, current sensor, voltage sensor, pressure sensors, and scale) coupled with calibrated accuracy of thermocouples was used to evaluate the uncertainty propagation of the calculated parameters as vapor quality, mass flux and void fraction.

The uncertainties are summarized in Table 1.

f V M     (5) 1 standard deviation √ ∑ A C C E P T E D M A N U S C R I P T 9
The uncertainty for the void fraction is calculated from the propagation of the uncertainty for these parameters, based on the method of [START_REF] Taylor | Guidelines for evaluating and expressing the uncertainty of NIST measurement results[END_REF].

2 2 2 2 2 VM l v ts ts l v ts ts u u u u u VM                                                                    (6) 22 2 2 1 2 2 2 2 lv TT sat sat l sat v sat ts ts L D M ts ts ts ts ts u u u TT VV u u u V L D M                                                                                     (7)
where in the relative uncertainty. When the saturation temperature and mass flux are fixed.

The last term of Eq. 7 varies with the vapor quality because the mass of fluid contained in the test section changes with vapor quality. Fig. 2 shows the uncertainty in the void fraction, as calculated by Eq. 7 with the data given in Table 1. The uncertainty in void fraction increases when the vapor quality decreases.

CORRELATIONS

Void fraction is a critical unknown parameter involved in the prediction of the pressure drop and heat transfer during two-phase flow, as well as of the charge of two-phase systems. The determination of void fraction from input conditions in a given tube (such as mass flux, vapor quality, tube diameter and saturation temperature) is complicated, due to the slip ratio, i.e. the ratio between the velocities of vapor and liquid phases. Because of the complexity and lack of understanding of the basic underlying physics of the problem, the majority of the analyses were more inclined towards semi-empirical correlations.

The void fraction correlations can be classified in four groups defined and named by [START_REF] Woldesemayat | Comparison of void fraction correlations for different flow patterns in horizontal and upward inclined pipes[END_REF]: -slip ratio correlations‖, -Kα H correlations‖, -drift flux correlations‖ and -general correlations‖.

Slip ratio correlations

The correlations of this group explicitly account for the effect of the slip ratio and can be written

Where and are the slip ratio, and vapor and liquid velocities, respectively. The correlations of [START_REF] Baroczy | Correlation of liquid fraction in two-phase flow with application to liquid metals[END_REF], [START_REF] Zivi | Estimation of Steady-State Steam Void-Fraction by Means of the Principle of Minimum Entropy Production[END_REF] and [START_REF] Butterworth | A comparison of some void-fraction relationships for co-current gas-liquid flow[END_REF] belong to this category.

The homogeneous model or non-slip void fraction considers both phases as the homogeneous mixture, i.e., the vapor and liquid phases flow with same velocity, .

1 1 1 v H l x x                ( 10
)
This model can be applied where the vapor and liquid velocities are close the one to the other (e.g. for bubbly flow or mist flow patterns), or for high mass flux [START_REF] El Hajal | Condensation in horizontal tubes, part 1: two-phase flow pattern map[END_REF].

Kα H correlations

The correlations belonging to this category involve a parameter that multiplies the void fraction calculated by the homogenous model. [START_REF] Bankoff | A Variable Density Single-Fluid Model for Two-Phase Flow With Particular Reference to Steam-Water Flow[END_REF] named that constant K. Hugmark (1961) proposed that the K constant should be based on the mass flow rate of two-phase mixture, and introduced the Froud number and the Reynolds number.

Drift flux correlations

These correlations take into consideration the non-uniformity in the flow captured by a distribution parameter ( ), and the drift velocity ( ), defined as the difference between the vapor phase velocity ( ) and the two-phase mixture velocity ( ). The superficial vapor velocity ( ) has an equally important part in the expression as is shown:

0 sv m vm U C U U    (11)
Note that if and , the equation resembles the homogeneous model.

A C C E P T E D M A N U S C R I P T

General correlations [START_REF] Woldesemayat | Comparison of void fraction correlations for different flow patterns in horizontal and upward inclined pipes[END_REF] classified as belonging to the category of general correlations all those that use other physical parameters, such as the Martinelli parameter (χ), the Froude number (Fr) or the Weber number (We), among others.

Selected correlations

Table 2 shows the chosen correlations, namely the correlations of [START_REF] Zivi | Estimation of Steady-State Steam Void-Fraction by Means of the Principle of Minimum Entropy Production[END_REF]), Hugmark (1961), [START_REF] Rouhani | Calculation of void volume fraction in the subcooled and quality boiling regions[END_REF], [START_REF] Domanski | Computer Modeling of the Vapor Compression Cycle With Constant Flow Area Expansion Device[END_REF], [START_REF] Baroczy | Correlation of liquid fraction in two-phase flow with application to liquid metals[END_REF] and [START_REF] Kanizawa | Void fraction predictive method based on the minimum kinetic energy[END_REF], for investigating the experimental data concerning the void fraction. The decision was made to choose at least one correlation of each group and also the correlations commonly used in the literature for horizontal and macro-channels. [START_REF] Wojtan | Measurement of dynamic void fractions in stratified types of flow[END_REF] used [START_REF] Zivi | Estimation of Steady-State Steam Void-Fraction by Means of the Principle of Minimum Entropy Production[END_REF] and [START_REF] Rouhani | Calculation of void volume fraction in the subcooled and quality boiling regions[END_REF] correlations to assess the experimental data. [START_REF] Woldesemayat | Comparison of void fraction correlations for different flow patterns in horizontal and upward inclined pipes[END_REF] recommended Hugmark (1961) correlation for horizontal flow. [START_REF] Kanizawa | Void fraction predictive method based on the minimum kinetic energy[END_REF] recently developed a novel method based on a huge database to analyze the void fraction parameter. Finally, [START_REF] Domanski | Computer Modeling of the Vapor Compression Cycle With Constant Flow Area Expansion Device[END_REF] and [START_REF] Baroczy | Correlation of liquid fraction in two-phase flow with application to liquid metals[END_REF] are classical methods that have been utilized in many studies [START_REF] El Hajal | Condensation in horizontal tubes, part 1: two-phase flow pattern map[END_REF].

) 1 1 3 1 1 v v l l x x                         Slip ratio
z z z K z z z                       8 8 for z for z       1 1 2 8 6 1 1 l v l v H H D G Gx z gD                                 
            1 0.25 0.5 1.18 1 1 1 0.12 1 lg v v l l xg x x x x G                                 
v l l v x x                             
                            Gener al - G<1515 kg.m -2 s - 1 ; α < 0.36
Based on the minimum kinetic energy

RESULTS

In this section, the results of experimental tests are presented: this investigation of the void fraction for R1234yf and R134a in adiabatic conditions inside a smooth horizontal tube was done for two mass fluxes (180 and 280 kg/m²s), two saturation temperatures (15°C and 25°C) and for a vapor quality ranging from 0.1 to 1. A total of 53 points were collected during the tests.

Effect of mass flux

The mass flux is an important parameter for evaluation of the two-phase flow. However, the mass flux does not significantly affect the void fraction. Fig. 3 demonstrates that by increasing the mass flux from 180 to 280 kg/m²s, only a slight increase of the void fraction is visible for some points, probably due to fact that the increase in the mass flux is limited, which results in a nonsignificant change in the void fraction. The increase of entrainment ratio with mass flux is negligible which leads to a very small effect of the mass flux at high vapor quality.

Comparison between R1234yf and R134a

Figure 5 shows the measured void fraction for R134a and R1234yf versus the vapor quality for a saturation temperature equal to 15°C and for both studied mass fluxes. Generally, at a given vapor quality, the void fraction for R134a is slightly higher than that for R1234yf, mainly in low mass flux. This is due to the fact that for a given temperature, R1234yf has a higher saturation pressure and thus a higher vapor density that causes the vapor to flow at a lower velocity.

Comparison of experimental results with existing correlations

In this section, the R1234yf experimental data are compared with the predictions obtained the various correlations of the literature mentioned in Table 2. The homogeneous model, and [START_REF] Zivi | Estimation of Steady-State Steam Void-Fraction by Means of the Principle of Minimum Entropy Production[END_REF]), Hugmark (1961), [START_REF] Rouhani | Calculation of void volume fraction in the subcooled and quality boiling regions[END_REF], [START_REF] Domanski | Computer Modeling of the Vapor Compression Cycle With Constant Flow Area Expansion Device[END_REF], [START_REF] Baroczy | Correlation of liquid fraction in two-phase flow with application to liquid metals[END_REF] and [START_REF] Kanizawa | Void fraction predictive method based on the minimum kinetic energy[END_REF] The [START_REF] Baroczy | Correlation of liquid fraction in two-phase flow with application to liquid metals[END_REF] and Hugmark (1961) correlations present the best prediction and trend, while all the other correlations tend to over predict the data on the whole range of values.

The performance of all correlations as the percentage of MRD (mean relative deviation) and MARD (mean absolute relative deviation) is presented in Table 3. It is observed that the [START_REF] Baroczy | Correlation of liquid fraction in two-phase flow with application to liquid metals[END_REF] correlation is the best, with a MARD equal to 2.0%. Some others correlations also show quite low errors: Hugmark (1961) (3.2%), [START_REF] Zivi | Estimation of Steady-State Steam Void-Fraction by Means of the Principle of Minimum Entropy Production[END_REF] (3.4%), [START_REF] Kanizawa | Void fraction predictive method based on the minimum kinetic energy[END_REF] (3.3%) and [START_REF] Domanski | Computer Modeling of the Vapor Compression Cycle With Constant Flow Area Expansion Device[END_REF] (4.2%). The correlation of [START_REF] Rouhani | Calculation of void volume fraction in the subcooled and quality boiling regions[END_REF] and the homogenous model shows the worst agreements, with a MARD of 4.9% and 11.0%, respectively.

A simple scatter plot of the calculated void fractions vs the measured experimental data is presented in Fig. 7 for the Hugmark (1961) and [START_REF] Baroczy | Correlation of liquid fraction in two-phase flow with application to liquid metals[END_REF] correlations. These graphs reveal that 100% of the datapoints are within a ±10% error band. observed that for a given vapor quality, the void fraction for R134a is higher than for R1234yf.

The experimental data were used to evaluate the performance of eight void fraction models of correlations for R1234yf. [START_REF] Baroczy | Correlation of liquid fraction in two-phase flow with application to liquid metals[END_REF] provides reasonable predictions of the experimental database, with a MARD less than 5% and almost all the data predicted within a ±10% error band.

The correlations developed by [START_REF] Kanizawa | Void fraction predictive method based on the minimum kinetic energy[END_REF], [START_REF] Domanski | Computer Modeling of the Vapor Compression Cycle With Constant Flow Area Expansion Device[END_REF]Didion (1983), Hugmark (1961) and [START_REF] Rouhani | Calculation of void volume fraction in the subcooled and quality boiling regions[END_REF], can provide acceptable predictions



  Experiments on void fraction of R1234yf in a horizontal smooth tube  Effects of experimental conditions on void fraction of R1234yf is analyzed  Experimental data of void fraction of R1234yf are compared with correlations  The quick close valve method was used to measure the local void fraction A C C E P T E D M A N U S C R I P T

Figure 1 .

 1 Figure 1. Test bench including: 1-magnetic micropump; 2-heater; 3-condenser; 4-bottle; 5-solenoid valve; 6-subtank; 7-test section; 8-Balance scale. Tubes of 0.5 m length and 4.8 mm inner diameter were located at upstream and downstream of the test section to achieve a fully-developed flow condition. To operate the measurement of the void fraction with QCV methods, two solenoid valves (Normally Closed) with same inner diameter of test section were controlled by computer. A third valve was located in the downstream of the test section to link the bottle. A hole with 0.5 mm diameter was made in the wall (up position) of the test section to connect the third valve. This configuration minimizes the influence of junction on flow.

Figure 2 .

 2 Figure 2. Uncertainty of void fraction in function of vapor quality.

Figure 3 :Figure 4 Figure 4 :

 344 Figure 3: Effect of mass flux on the void fraction at saturation temperature (a) T sat =15°C; (b) T sat =25°C 4.2 Effect of the saturation temperature Figure 4 represents the void fraction of R1234yf as a function of the vapor quality for a given mass flux and two saturation temperatures. The void fraction increases with the vapor quality, but not linearly. The uncertainty bars underline that, as explained previously, the uncertainties are larger at low than at high void fraction. Increasing the saturation temperature results in a decrease of the void fraction.This behavior can be explained by the reduction of the density ratio (ρ l/ ρ v ) when increasing the saturation temperature, as shown in Table3. As a result, the slip ratio increases and the void fraction decreases. This general trend is easily captured from Eq. 8 (homogeneous model) and it is respected by the subsequent correlations.

  Figure 5: experimental void fraction. a) G=180kg/s and b) G=280kg/s.

Figure 6 :

 6 Figure 6: comparison of void fraction for R1234yf of different with models of open literature

  Figure 7: experimental void fraction vs Hugmark and Baroczy correlations for R1234yf. 5 CONCLUSION An experimental investigation of the void fraction of R1234yf in two-phase flow in smooth and horizontal tubes was undertaken. The test conditions were: a tube internal diameter of 4.8 mm; a mass flux of 180 kg/m²s or 280 kg/m²s; a saturation temperature of 15°C or 25°C; adiabatic conditions; and vapor quality ranging from 0.1 to 1. During the experiments more than 50 points were measured and tests were also performed for R134a as a reference. The purpose of the tests was to study the effects of vapor quality, mass flux and saturation temperature on the void fraction of R1234yf and R134a. The void fraction increased when decreasing the saturation temperature, due to the decrease of the vapor density. Within the range of test conditions, the mass flux has almost no influence on the void fraction. Additionally, it was

Table 1

 1

					. Uncertainties
					Parameter Internal diameter Tube length Refrigerant mass flow rate Electric current Electric voltage Pressure Temperature Mass fluid Mass flux Vapor quality Void fraction *the maximum value at low vapor qualities Uncertainty ± 0.4% ± 0.1%  2.5% ± 1.5 % ± 1.8 % ± 0.2 bar ± 0.5 °C ± 0.5 g ± 3.4 % ± 3.8 %* ± 4.7 %*
	Especially, Eq. (4) shows that the experimental void fraction depends on four parameters:
		l	, , , g ts	ts	

Table 2 .

 2 Void fraction correlations.

	Author equation

Table 3 .

 3 Thermodynamic properties of R134a and R1234yf at similar operating conditions

	Fluid R134a R1234yf	T sat P sat °C bar 15 4.88 25 6.66 15 5.10 25 6.83	σ mN.m -1 9.36 8.03 7.44 6.19	ρ l 1243 kg.m -3 1207 1127 1093	ρ v 23.78 32.37 28.32 37.94	ρ l/ ρ v -52.29 37.27 0.1944 0.0119 µ l µ v mPa.s 0.22 0.0115 39.81 0.1722 0.0109 28.79 0.153 0.0114	µ l/ µ v -19.07 16.24 15.75 13.39

Table 3 .

 3 Deviation of correlations

	Correlation Homogenous Hugmark (1965) Zivi (1964) Rouhani and Axelsson (1970) Domanski and Didion (1983) Baroczy (1965) Kanizawa and Ribatski (2016)	MRD MARD 11,0 11,0 -3,2 3,2 2,2 3,4 4,9 4,9 4,2 4,2 -0,2 2,0 3,3 3,3

ACKNOWLEDGMENT

The authors appreciate the support of CAPES, CNPq, and FAPEMIG in Brazil. We would also like to express our heartfelt gratitude to Dr. Ricardo Koury (in memoriam), Professor at Federal University of Minas Gerais and dear friend.

). The use of the homogeneous model is not recommended in the range of studied operating conditions. As a final remark, the authors believe that a similar research would deserve to be conducted in the future for hydrocarbons (e.g. R600a, R290), as these fluids are also often viewed as a track to reduce the environmental effect of refrigeration systems.

A C C E P T E


Julien Signoles

Nikolai Kosmatov

Kostyantyn Vorobyov

E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs (tool paper)

Keywords: Runtime Verification Tool, Runtime Assertion Checking, Memory Debugger, Formal Specification Language

published or not. The documents may come

E-ACSL, a runtime verification tool for safety and security of C programs (tool paper)

1 Introduction E-ACSL is a runtime verification tool within Frama-C [START_REF] Kirchner | Frama-C: A software analysis perspective[END_REF], a framework dedicated to source code analysis of C programs1 . E-ACSL is capable of checking various safety and security properties at runtime including (but not limited to) complex functional specifications, well ordering of function calls, information flow leakage and a broad range of undefined behaviors, focusing on such issues as division by zero, integer overflows, validity of pointer dereferences and accesses to uninitialized memory. These properties are expressed as source code annotations written using a formal specification language also called E-ACSL.

The E-ACSL tool consumes a C program annotated with specifications written in the E-ACSL specification language and outputs a new C program that embeds an inline monitor generated from the formal E-ACSL specification. At runtime the monitored program behaves similarly to the original if the formal properties are satisfied, or aborts its execution if any property is violated. It is worth noting that since Frama-C provides several plug-ins to generate E-ACSL annotations from high-level or implicit specifications, most usages of E-ACSL do not require annotating programs manually. Verifying properties at runtime with E-ACSL is thus a mostly automatic process.

Even though several papers have already described such E-ACSL components as its specification language [START_REF] Delahaye | Common specification language for static and dynamic analysis of C programs[END_REF], memory model [START_REF] Vorobyov | Shadow state encoding for efficient monitoring of blocklevel properties[END_REF][START_REF] Vorobyov | Runtime detection of temporal memory errors[END_REF], static analyses to optimize code generation [START_REF] Jakobsson | Rester statique pour devenir plus rapide, plus précis et plus mince[END_REF][START_REF] Jakobsson | Fast as a Shadow, Expressive as a Tree: Optimized Memory Monitoring for C[END_REF], and possible usages in conjunction with other Frama-C plug-ins [START_REF] Kosmatov | A lesson on runtime assertion checking with Frama-C[END_REF][START_REF] Pariente | Static Analysis and Runtime Assertion Checking: Contribution to Security Counter-Measures[END_REF][START_REF] Barany | Hybrid Information Flow Analysis for Real-World C Code[END_REF], this paper aims at presenting a quick overview of the whole tool.

Outline Section 2 briefly describes the E-ACSL specification language. Section 3 gives a sketch of the tool's design. Section 4 points out several possible practical usages of E-ACSL and Section 5 summarizes results of experiments and case studies involving practical runtime verification of C programs with E-ACSL.

/* @ requires 2 <= n <= 10000; requires \forall integer j ; 0 <= j < n == > \valid ( t + j ); ensures \forall integer j ; 0 <= j < n == >

( t [ j ] != 0 <== > ( j >= 2 && ( \forall integer d ; 2 <= d < j == > j % d != 0) ) ); assigns t [0.. n -1]; */ void primes ( int *t , int n ) { int i , k ; t [0]= t [1]=0; /* @ loop invariant I1 : 2 <= i <= n ; loop invariant I2 : \forall integer j ; 0 <= j < i == > ( t [ j ] != 0 <== > ( j >= 2 && ( \forall integer d ; 2 <= d < j == > j % d != 0) ) ); loop assigns i , k , t [0.. n -1]; loop variant n -i ; */ for ( i =2; i < n ; i ++) { /* @ loop invariant I3 : 2 <= k <= i && t [ i ] == 1; loop invariant I4 : \forall integer j ; 0 <= j < i == > ( t [ j ] != 0 <== > ( j >= 2 && ( \forall integer d ; 2 <= d < j == > j % d != 0) ) ); loop invariant I5 : \forall integer d ; 2 <= d < k == > i % d != 0 ; loop assigns k , t [0.. i ]; loop variant i -k ; */ for ( k =2 , t [ i ]=1; k < i ; k ++) { if ( i % k == 0){ t [ i ]=0; break ; } } } } int main (){ int i , a [100];
primes (a , 200); // provokes illegal memory access /* @ assert \base_addr (& i ) != \base_addr ( a ); */ /* @ assert \forall integer j ; 0 <= j < 100 == > \initialized ( a + j ); */ }

E-ACSL Specification Language

The E-ACSL specification language is formally described in the reference manual [START_REF] Signoles | E-ACSL: Executable ANSI/ISO C Specification Language[END_REF], and its overview is presented in an earlier article [START_REF] Delahaye | Common specification language for static and dynamic analysis of C programs[END_REF]. This section gives a brief summary of its main features.

The E-ACSL specification language [START_REF] Signoles | E-ACSL: Executable ANSI/ISO C Specification Language[END_REF] is an executable subset of the ACSL specification language [START_REF] Baudin | ACSL: ANSI/ISO C Specification Language[END_REF]. This language is a contract-based behavioural specification language à la Eiffel [START_REF] Meyer | Applying "Design by Contract[END_REF] whose design was inspired by JML [START_REF] Leavens | JML: A Notation for Detailed Design[END_REF]. ACSL logic is a typed first-order logic whose terms are pure (i.e. side-effect free) C expressions extended with keywords and built-ins to handle C specificities.

Fig. 1 shows an example C program with ACSL annotations. Given an array t of n integers, the function primes writes a non-zero value to array element t[j] if j is a prime number, and 0 otherwise. The function main calls primes on the integer array a of 100 elements, but erroneously specifies its size as 200 instead of 100. The execution of main may thus provoke runtime errors.

The contract of the function primes is given via annotations at lines 1-6 of Fig. 1. The precondition clauses at lines 1-2 assume that the value of n is between 2 and 10000, and the array t has valid cells for all indices j between 0 and n-1. It is expressed as validity of the pointer t+j to the corresponding cell t[j] using the builtin predicate \valid. For a pointer p, \valid(p) states that memory location *p can be safely read and written. The postcondition of the function states that for every index j, t[j] is non-zero if and only if j is prime. The fact that j is prime is expressed as being greater or equal to 2, and having no divisor d such that 2<=d<j. The clause at line 6 states that the elements of array t are the only variables that can have a different value after the function call.

The annotations at lines 10-15 and 17-23 express loop contracts. Each contract contains loop invariants, a loop assigns clause and a loop variant. Loop invariants must be true before the loop and after each loop iteration. The clause loop assigns indicates variables whose values can change during the execution of the loop. A loop variant is an integer expression that must be non-negative whenever a loop iteration starts, and must strictly decrease at each iteration, thus allowing a deductive verification tool to deduce the termination of the loop after a finite number of steps.

Two other builtin predicates of ACSL are illustrated by assertions at lines 36-37. The first one specifies that the memory blocks containing variable i and array a do not have the same base address. In other words, they are two different blocks. The ACSL construct \base_addr(p) denotes the base (i.e. start) address of the memory block pointer p belongs to. The assertion at line 37 specifies that all array elements are initialized. The ACSL predicate \initialized(p) expresses that the memory location *p referred to by pointer p has been initialized.

Using the deductive verification plug-in Frama-C/Wp, one can easily prove that function primes respects its ACSL contract. As expected, the proof that the call to primes at line 35 respects its precondition will fail (for the precondition at line 2) because the validity for all required indices (up to 200 -1 = 199) is not ensured here. The assertion at line 36 is proved as well (while that at line 37 is left unknown since Wp does not support the \initialized predicate yet). While detailed function and loop contracts are mandatory to obtain a complete proof and/or meaningful proof failures using a deductive verification tool, runtime assertion checking can be applied without having to manually specify all of them.

Although inspired by JML, ACSL was designed for static analysis and notably program proof by means of Dijkstra's weakest precondition calculus (WP) [START_REF] Dijkstra | Guarded commands, nondeterminacy and formal derivation of programs[END_REF]. In particular, several constructs have no executable meaning, e.g. quantification over infinite sets. That is why E-ACSL was designed as a large subset of ACSL such that all its terms and predicates can be evaluated at runtime. For instance, each quantified integer variable in E-ACSL must be syntactically bounded in order to restrict quantification to finite integer intervals. Actually, the most practical ACSL constructs are still part of E-ACSL. For example, all ACSL annotations of the program of Fig. 1 also belong to E-ACSL. E-ACSL includes mathematical integers and built-in memory predicates and functions even if checking such constructs at runtime efficiently is challenging.

The executable nature of E-ACSL implies one fundamental semantic difference with ACSL: undefinedness. Indeed, ACSL is based on standard mathematical logic in which any well-typed construct is well-defined. In particular, any predicate is either true or false (even if possibly unprovable). It is not the case in E-ACSL because some constructs, e.g. the expression 1/0, cannot be evaluated at runtime without errors. Consequently, E-ACSL is based on 3-valued logic in which these constructs are undefined. For instance, the predicate 1/0 == 1/0 is valid in ACSL (by reflexivity of equality) but is undefined in E-ACSL. Both logic remain nevertheless consistent: for any E-ACSL predicate p, if p is valid (resp. invalid) in ACSL then p is either valid (resp. invalid) or undefined in E-ACSL. Conversely, if p is valid (resp. invalid) in E-ACSL then p is also valid (resp. invalid) in ACSL. This fundamental property ensures tool compatibility between ACSL and E-ACSL.

Monitor Generation Scheme

The E-ACSL runtime verification tool is implemented as a plug-in of Frama-C [START_REF] Kirchner | Frama-C: A software analysis perspective[END_REF], a framework dedicated to source code analysis of C programs. Frama-C is in charge of preprocessing, parsing, typing and providing an abstract syntax tree (AST) representing the input C code annotated with ACSL annotations. E-ACSL in turn generates a new AST that represents the output C program that embeds monitors generated from E-ACSL annotations. Fig. 2 shows a translation scheme of the E-ACSL plug-in. Two static analyses are executed prior to code generation. One analysis identifies the goto-like statements which go outside blocks in order to soundly insert necessary code when exiting a block, while the other one finds out an over-approximation of the statements which are necessary to monitor in order to verify memory properties (if any) [START_REF] Jakobsson | Fast as a Shadow, Expressive as a Tree: Optimized Memory Monitoring for C[END_REF]. For instance, considering a pointer p of type int* and a program containing a single annotation \valid(p), it is only necessary to monitor statements which assign p and its potential aliases.

Two other analyses are performed on the fly during a code generation phase. First, the type system [START_REF] Jakobsson | Rester statique pour devenir plus rapide, plus précis et plus mince[END_REF] deals with E-ACSL mathematical integers: for any E-ACSL term it computes the smallest C type that can safely encode it. If the term cannot be safely represented by a C type, the generated code uses the Gmp multiple precision arithmetic library2 to encode it. For instance, assuming a typical 64-bit architecture, if the type of both x and y is int, this type system infers that the result of x+1 fits in a long.

Finally, the RTE plug-in of Frama-C is used to prevent undefined behaviors in the generated code. For instance, for the following E-ACSL annotation /*@ assert x / y == 0; */, RTE automatically generates an additional assertion y != 0 to prevent potential division by zero at runtime.

Possible Usages

E-ACSL comes with a companion script called e-acsl-gcc.sh that simplifies the process of invoking Frama-C and E-ACSL to generate an inline monitor m from an input C program p, and further compile and link it against the E-ACSL runtime library using a C compiler (gcc by default).

From a user's viewpoint, the main issue is thus writing formal annotations. This process, however, can often be automated. The most important usages of E-ACSL are the following. Notable only the fifth one requires manual annotations. Here is a few details about these activities. First, checking the absence of a broad class of undefined behaviors is possible due to the Frama-C plug-in RTE [START_REF] Herrmann | Annotation generation: Frama-C's RTE plug-in[END_REF] that automatically generates E-ACSL assertions to prevent such undefined behaviors as arithmetic overflows, undefined downcasts, array out-of-bound accesses and invalid pointer dereferences. Once generated by RTE, these annotations are translated into runtime checks by E-ACSL. It is worth noting that, when focusing on detection of invalid memory accesses E-ACSL operates similar to a memory debugger such as Address Sanitizer [START_REF] Serebryany | AddressSanitizer: A fast address sanity checker[END_REF] or Valgrind [START_REF] Nethercote | Valgrind: A framework for heavyweight dynamic binary instrumentation[END_REF]'s MemCheck [START_REF] Seward | Using Valgrind to detect undefined value errors with bit-precision[END_REF].

Consider an example program in Fig. 1. Even if no E-ACSL annotations are provided by the user, RTE can be used to add assertions verifying the validity of memory accesses. Thanks to these checks out-of-bounds memory accesses in function primes at line 35 can be detected by E-ACSL without manual annotation effort.

Second, in checking high-level properties E-ACSL also relies on other Frama-C plug-ins to generate annotations. For instance, the Aoraï [START_REF] Stouls | Aoraï plug-in tutorial[END_REF] plug-in can generate annotations from a Büchi automaton (or, equivalently, an LTL formula) that models function call ordering, e.g. "function f must always be called twice before function g". This has been proven useful in practice when modeling function relationship of library APIs. Another example is the SecureFlow plug-in. SecureFlow is a source-to-source transformation that encodes information flows of an input program into itself [START_REF] Assaf | Program transformation for non-interference verification on programs with pointers[END_REF][START_REF] Barany | Hybrid Information Flow Analysis for Real-World C Code[END_REF]. It is then possible to verify with E-ACSL that the generated code does not contain information flow leakage, e.g. that no confidential data leaks onto a public channel.

Third, all the properties that E-ACSL validates at runtime may theoretically be verified by means of static techniques including abstract interpretation, model checking or WP. However, practical tool limitations may prevent some verifications. In any case, it is often costly to verify properties statically: verifying a subset of properties statically and delegating verification of the remaining properties to E-ACSL may be a good compromise between exhaustiveness of static verification and the cost of the verification process.

Consider an example program in Fig. 1. Suppose line 35 is replaced by primes(a, 100). In this case, even if the loop contracts are not provided by the user, E-ACSL can check that the call to primes verifies its precondition before the call, and its postcondition after the call. In contrast, the deductive verification plug-in Wp is not able to check the postcondition without the loop contract. For the original version presented in Fig. 1,E-ACSL detects that the call primes(a, 200) on line 35 does not respect its precondition before the call. E-ACSL is also capable of checking the assertions on lines 36 and 37 (even if no other annotations are provided).

Fourth, improving detection capabilities of testing mainly rely on the first two items. For instance, many undefined behaviors remain undetected by testing because they do not lead to program crash or incorrect results on the tested inputs and user system. Coupling E-ACSL to a test case generation tool like PathCrawler [START_REF] Botella | Automating structural testing of C programs: Experience with PathCrawler[END_REF] or a fuzzing tool such as American Fuzzy Lop3 may significantly improve their detection rate of errors.

Fifth, before proving complex functional specifications by means of WP, it may be reasonable to test them. Indeed, in case of proof failure, a user must investigate the cause of the bug which requires time and expertise [START_REF] Petiot | Your proof fails? testing helps to find the reason[END_REF]. It is particularly difficult for non-experts [START_REF] Kosmatov | A lesson on proof of programs with Frama-C[END_REF]. Among others, one possible cause is that the code does not match the specification because one of them is wrong: in that case, testing their compliance in a preliminary step (by means of the fourth E-ACSL usage) improves confidence that the proof failure comes from another cause.

Practical Runtime Verification with E-ACSL

One of the strengths of E-ACSL is its practical application to runtime verification of C code. Over the past several years E-ACSL has been experimentally evaluated and used in a number of case studies involving runtime verification of benchmarked and industrial-strength code [START_REF] Kosmatov | An optimized memory monitoring for runtime assertion checking of C programs[END_REF][START_REF] Jakobsson | Fast as a Shadow, Expressive as a Tree: Optimized Memory Monitoring for C[END_REF][START_REF] Bartocci | First International Competition on Runtime Verification. Rules, Benchmarks, Tools and Final Results of CRV[END_REF][START_REF] Barany | Hybrid Information Flow Analysis for Real-World C Code[END_REF][START_REF] Pariente | Static Analysis and Runtime Assertion Checking: Contribution to Security Counter-Measures[END_REF][START_REF] Vorobyov | Shadow state encoding for efficient monitoring of blocklevel properties[END_REF][START_REF] Vorobyov | Runtime detection of temporal memory errors[END_REF]. This section now briefly summarizes the results of these experiments.

Competitions on Runtime Verification

One key evaluation of E-ACSL has been performed by an independent committee during Competitions on Runtime Verification (CRV) organized in 2014 [START_REF] Bartocci | First international competition on software for runtime verification[END_REF] and in 2015 [START_REF] Falcone | Second international competition on runtime verification CRV[END_REF] as part of the International Conference on Runtime Verification. E-ACSL participated in the C program monitoring track both in 2014 and in 2015. The 2016 edition of the C track did not take place due to a lack of participants.

Each competition was split into three phases. During the first phase the participants were invited to submit their benchmarks to a public repository. In the second, monitor collection phase, the participants were invited to submit their monitors generated from the shared code. During the final evaluation phase the qualified tools were evaluated by running the generated monitors and ranked using different criteria such as memory or CPU utilization overhead and correctness of the runtime analysis.

In the 2014 installment of CRV four runtime verification tools (E-ACSL, RiTHM-1, RTC and ARTiMon) had registered for competing in the track on online monitoring of C programs but only E-ACSL, RiTHM-1 and RTC submitted their solutions for evaluation. In 2014 E-ACSL had won the second place, falling behind the RTC tool 4 . In 2015, where overall six tools registered for the track (E-ACSL, MarQ, RiTHM-v2.0, RTC, RV-monitor and TimeSquareTrace) and only two tools (E-ACSL and RV-monitor) submitted their solutions, E-ACSL arrived at the first place5 .

Runtime Detection of Memory Errors

One of the benefits of E-ACSL is its ability to detect memory errors such as buffer overflows, illegal dereferences, double free and similar vulnerabilities.

At a specification level, memory error detection via E-ACSL uses built-in annotations including such key predicates as \valid(p), \initialized(p), \base_addr(p), \offset(p) and \block_length(p). For a given pointer p, these predicates respectively denote the validity of p (i.e., whether p is safe to dereference), if the value pointed to by p has been initialized by previously writing to it, the base (start) address of the memory block p belongs to, the byte-length of that block and the byte offset of p relative to the base address.

Memory-related annotations of E-ACSL allow to reason about memory allocated by the program at a block-level, resulting in a much more powerful analysis when compared to state-ofthe-art memory debuggers [START_REF] Vorobyov | Shadow state encoding for efficient monitoring of blocklevel properties[END_REF]. For instance, for a dereference *(p+i) the E-ACSL expression \base_addr(p) == \base_addr(p+i) specifies that p+i belongs to the same memory block that p points to. This detects an out-of-bounds access if both p and p+i point to two different allocated areas. The E-ACSL specification language can express a large variety of contract properties [START_REF] Delahaye | Common specification language for static and dynamic analysis of C programs[END_REF] that go far beyond out-of-bounds checks, where block-level properties can be also very useful.

To support E-ACSL memory predicates, code generated by E-ACSL relies on a C memory monitoring library. This is such that memory modifications made by the program at runtime are stored in the library by the monitor and checking annotations corresponds to querying it. Before program instrumentation, static analysis is performed to safely remove unnecessary memory instrumentation to improve efficiency of the monitor [START_REF] Jakobsson | Fast as a Shadow, Expressive as a Tree: Optimized Memory Monitoring for C[END_REF]. Memory monitoring in E-ACSL has initially been implemented using a compact prefix tree called patricia trie [START_REF] Kosmatov | An optimized memory monitoring for runtime assertion checking of C programs[END_REF]. The trie stores per-block metadata in its leaves and uses base addresses of memory blocks as keys associated with trie nodes. Routing from the root to a leaf is ensured by internal nodes of the trie.

Initial experiments that involved checking memory-related annotations in a number of small programs (see [START_REF] Kosmatov | An optimized memory monitoring for runtime assertion checking of C programs[END_REF]) indicated that results produced by E-ACSL are precise. Yet, due to complexity of trie lookups, even in small code samples such an approach is prone to producing high runtime overheads of over 100 times compared to performance of unmonitored programs [START_REF] Jakobsson | Fast as a Shadow, Expressive as a Tree: Optimized Memory Monitoring for C[END_REF]. Further experiments with computationally intensive benchmarks from SPEC CPU datasets [26] revealed that overheads of memory analysis using a patricia trie can exceed 600 times when compared to unobserved executions [START_REF] Vorobyov | Shadow state encoding for efficient monitoring of blocklevel properties[END_REF].

To aid high overheads incurred by the monitoring library built upon a patricia trie, it has been replaced by a novel shadow memory monitoring scheme [START_REF] Vorobyov | Shadow state encoding for efficient monitoring of blocklevel properties[END_REF] allowing to capture bounds of memory blocks and benefit from constant-time lookups.

Empirical evaluation of the E-ACSL implementation using shadow memory has been conducted for a problem of checking validity of pointer and array accesses over SPEC CPU programs (see [START_REF] Vorobyov | Shadow state encoding for efficient monitoring of blocklevel properties[END_REF]). This evaluation compared performance overheads of E-ACSL to the overheads incurred by state-of-the-art memory debuggers and an implementation of E-ACSL using a patricia trie. This experimentation has shown that for the purpose of verifying validity of memory accesses runtime overheads of E-ACSL (avg. ×19) are significantly better than the overheads of a patricia trie approach (avg. ×77.5) and comparable to the runtime overheads of such state-of-the-art memory debuggers as MemCheck (avg. ×15.5) or Dr. Memory (avg. ×18). Furthermore, memory overheads of E-ACSL shadow memory monitoring (avg. ×2.9) were on average the lowest of all tools including E-ACSL patricia trie implementation. It is worth noting that E-ACSL as it stands now has undergone several optimization passes that reduced the average runtime overhead over SPEC CPU programs to only 13 times when compared to runs of original programs.

Case Studies Using E-ACSL

CURSOR E-ACSL has also been used to analyze industrial-strength code using third-party tools. For instance, a technique called CURSOR [START_REF] Pariente | Static Analysis and Runtime Assertion Checking: Contribution to Security Counter-Measures[END_REF] uses the Frama-C Value plugin to generate assertions for dynamically verifying a number of Common Weakness Enumeration (CWE) [START_REF]Common Weakness Enumeration: A community developed dictionary of software weakness types[END_REF] vulnerabilities and further dynamically verify them using E-ACSL.

To support their approach, Pariente and Signoles applied CURSOR to several Apache libraries (of approximately 8,000 LOC) containing file management and sanitizing functions relevant to security analysis. As a result of its static analysis, CURSOR generated 340 assertions that were further converted to executable code using E-ACSL, leading to a 22% increase of the source code base and an average runtime overhead of less than 3 times.

Secure Flow

In another instance E-ACSL has been used alongside a hybrid flow-sensitive information flow analysis of C programs called Secure Flow [START_REF] Barany | Hybrid Information Flow Analysis for Real-World C Code[END_REF] to dynamically enforce an information flow policy protecting against timing attacks on a cryptographic library. E-ACSL has been applied to protect against memory errors and ensure correctness of the information flow analysis via Secure Flow.

During the experimentation (reported in [START_REF] Barany | Hybrid Information Flow Analysis for Real-World C Code[END_REF]) Secure Flow and E-ACSL analyzed 14 cryptographic algorithms belonging to LibTomCrypt library 6 . In this study E-ACSL has shown slowdowns of approximately 15 times compared to unobserved executions. This result is consistent with experimentation using SPEC CPU benchmarks [START_REF] Vorobyov | Shadow state encoding for efficient monitoring of blocklevel properties[END_REF].

Conclusion

In this tool paper we have given a broad overview of E-ACSLan online verification tool for C programs. E-ACSL is built atop Frama-C, an industrial-strength framework for source code analysis of C programs. At its core E-ACSL transforms an input program P annotated with formal specifications written in the E-ACSL specification language into a program instrumented with a monitor automatically generated from the specification. A run of the monitored program is aborted is any of the properties given by the specification is violated, otherwise, the behaviour of the monitored program is functionally equivalent to the input program.

The E-ACSL specification language allows for specification of a wide range of properties including such issues as well-ordering of function calls, information flow leakage, integer overflows and memory errors. Most of these properties can be generated automatically using Frama-C, for instance via the RTE plug-in capable of generating annotations verifying the absence of undefined behaviors at runtime. E-ACSL is a runtime verification tool that has a variety of practical applications. Over the past several years E-ACSL has been applied to a number of problems in runtime analysis of benchmarked and industrial strength code including detection of spatial and temporal memory errors, enforcing information flow security properties and CWE vulnerabilities.

Future Work

At the present stage of its implementation E-ACSL supports generating C monitors from most common constructs provided by its specification language. However, more work is required to support the E-ACSL specification language in full. The second direction of future work relates to application of static analyses during the monitor generation phase. Even though E-ACSL already uses sound static techniques to reduce the amount of instrumentations (and consequently reduce runtime overheads), better static analyses are likely to improve the overheads results. Also these analyses and the E-ACSL code generator are quite complex pieces of code: future work includes their formalization and proof of correctness. Finally, E-ACSL lacks support for detecting concurrency issues such as deadlocks or data races. We are looking to address such concurrency problems in the future.

Figure 1 :

 1 Figure 1: Example of an annotated C program primes computing prime numbers

Figure 2 :

 2 Figure 2: E-ACSL Translation Scheme.

1 .

 1 Checking the absence of a wide class of undefined behaviors; 2. Checking high-level properties; 3. Improving detection capabilities of testing; 4. Complement static analyzers; 5. Debugging specifications.

Frama-C, including E-ACSL, is freely available from http://frama-c.com

http://gmplib.org

http://lcamtuf.coredump.cx/afl/

https://www.rv-competition.org/2014-2

https://www.rv-competition.org/2015-2

http://www.libtom.net/LibTomCrypt/

Acknowledgment

The authors would like to the anonymous reviewers from their helpful feedback. This work has received funding for the S3P project from French DGE and BPIFrance.