Philippe Ayrault

Matthieu Carlier

David Delahaye

Catherine Dubois

Damien Doligez

Lionel Habib

Thérèse Hardin

Mathieu Jaume

Charles Morisset

François Pessaux

Renaud Rioboo

Pierre Weis

la diffusion de documents scientifiques de niveau

recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Since at least forty years, an important area of software engineering is concerned with safety of industrial systems as those critical systems use more and more software components. Since twenty years, security problems of information systems spread from military domain to all society activities. Some fifteen years ago, safety and security of systems were usually considered of separated concern. Now, although their concerns are different, it is recognized that, in most cases, these two families of requirements must be considered together to receive satisfactory solutions (see the new rules for SCADA systems for example). Moreover, some methods to deal with safety requirements can be adapted to security requirements and conversely. Whatever is the domain, their methods are evolving, ad-hoc and empirical approaches being replaced by more formal methods. For example, for high levels of safety, formal models of the requirement/specification phase are more and more considered as they allow mechanized proofs, test or static analysis of the required properties. In the same way, high level assurance in system security asks for the use of true formal methods along the process of software development and is often required for the specification level.

To ease developing high integrity systems with numerous software components, an Integrated Development Environment (IDE) must provide tools to formally express specifications, to describe design and coding and to ensure that specification requirements are met by the corresponding code. This is not enough. First, standards of critical systems ask for pertinent documentation which has to be maintained along all the revisions during the system life cycle. Second, the evaluation conformance process of software is by nature a sceptical analysis. Thus, any proof of code correctness must be easily redone at request and traceability must be eased. Third, design and coding are difficult tasks. Research in software engineering has demonstrated the help provided by some object-oriented features as inheritance, late binding and early research works on programming languages have pointed out the importance of abstraction mechanism such as modularity to help invariant maintaining. There are a lot of other points which should also be considered when designing an IDE for safe and/or secure systems to ensure conformance with high Evaluation Assurance or Safety Integrity Levels (EAL-5,7 or SIL 3,4) and to ease the evaluation process according to various standards (e.g. IEC61508, CC, ...): handling of non-functional contents of specification, handling of dysfunctional behaviors and vulnerabilities from the true beginning of development and fault avoidance, fault detection by validation testing, vulnerability and safety analysis.

The main aim of this paper is to present an IDE, called Focal [START_REF] Prevosto | Algorithms and proof inheritance in the Foc language[END_REF][START_REF] Dubois | Building certified components within focal[END_REF] (freely distributed at http://focal.inria.fr), dedicated to the complete development of high integrity software, which attempts to give a positive solution to the three requirements identified above, the other items being currently under consideration. It provides means for the developers to formally express their specifications and to go step by step (in an incremental approach) to design and implementation while proving that such an implementation meets its specification or design requirements. It also provides some automation of documentation production and management.

Focal has already been used to develop huge examples. First, a computer algebra library was developed by Rioboo [START_REF] Rioboo | Programmer le Calcul Formel, des Algorithmes à la Sémantique[END_REF], it offers full specification and implementation of usual algebraic structures up to multivariate polynomial rings with complex algorithms. The point was to measure how Focal can help to render mathematical specifications and also to measure efficiency of the produced code, which is comparable (even little better) to the best general computer algebra systems in existence. Such a library is very useful when formalising the algebra of access control models, using implementations of orderings, lattices and boolean algebras (presented below). Focal was also very successfully used to formalise airport security regulations [START_REF] Delahaye | Formal Modeling of Airport Security Regulations using the Focal Environment[END_REF].

Focal semantics was initially specified in Coq, which brings a satisfactory confidence in the language's correctness. On the other side, the correction of the compiler against Focal's semantics is proved (by hand) [START_REF] Prevosto | Conception et Implantation du langage FoC pour le développement de logiciels certifiés[END_REF].

In a second part, we will expose the usability of Focal through the formalization and development of access control policies. We present how formal methods can be used in practice to obtain trusted implementations of an access control policy. The library of access control policies offers a generic specification of the model and several developments based on it, giving implementations of classic access control policies.

The Focal Philosophy

Since our aim is to have a unique framework from specification to implementation, from code to proofs of requirements, Focal provides a unique and manifold language to express all theses aspects of software development.

Before really entering inside Focal, we briefly remind a few well-known concepts in term of software engineering. Specifications of a system describe its functionalities, without referring to any particular practical solution. On the other side, the implementation gives an explicit, algorithmic, solution making the system running.

The Statement of Work of critical systems require the holding of certain properties (often called "requirements") to ensure that the system will be indeed operational. All along the development cycle, such requirements must be expressed and verified. Moreover, each development stage may introduce its own requirements. For instance, at specification-time, a railway system may require that doors of a train can't be opened while running. At implementation-time, this requirement must still hold, but some extra ones, due to implementation constraints may arise. For instance, the fact that a square root function is only called on positive numbers in the speed computation. This requirement was previously hidden since the speed comparison was not expressed finely enough to make the square root function appearing.

Considering these concepts, Focal allows management of declarations (specification), algorithms (implementation), properties (requirements) and proofs (demonstrations that requirements hold).

The Basic Brick

The primitive entity of a Focal development is the species. It can be viewed as a record grouping "things" related to a same concept. Like in most modular design systems (i.e. objected oriented, algebraic abstract types) the idea is to group a data structure with the operations to process it. Since in Focal we don't only address data type and operations, among these "things" we also find the specification of these operations, the representation of requirements (properties) and their proofs.

We now describe each of these "things", called methods.

-The method introduced by the keyword rep gives the data representation (carrier) that the species embeds. It is a type called the carrier type and defined by a type expression. The carrier may be not-yet-defined in a species, meaning that the real structure of the datatype the species embeds does not need to be known at this point. In this case, it is represented by a type variable. However, to obtain an implementation, the carrier has to be defined later either by setting rep = exp where exp is a type expression or by inheritance (see below). Type expressions in Focal are roughly MLlike types (variables, basic types, inductive types, record types) plus species carrier types, denoted by keyword Self inside the species and by the name of their species outside of them.

Each species has a unique method rep and thus, a unique carrier. This is not a restriction compared to other object-oriented languages where an object can own several private variables representing the internal state, hence the data structure of the object. In such a case, the carrier type can simply be the tuple grouping all these variables that were disseminated all along the object. -Declarations (signature) introducing a name and a type allows to announce a method to be defined later, i.e. to only specify its type, without implementation yet. Such methods are especially dedicated for specification or design purposes since it allows to use the name of the introduced method to define others methods while delaying the choice of its implementation. The type provided by the signature allows Focal to ensure via type-checking that the method is used in contexts compatibles with this type. The late-binding and the collection mechanisms, further introduced, ensure that the definition of the method will be effectively known when needed. -Definitions (let) made of a name, a type and an expression introduce functions, i.e. computational operations. The core language used to implement them is roughly ML-like expressions (let-binding, pattern matching, conditional, higher order functions, . . . ) with the addition of a construction to call a method from a given species. Mutually recursive definitions are introduced by let rec. -Statements (property) introduce a name and a first-order formula. A property may serve to express requirements (i.e. facts that the system must hold to conform to the Statement of Work delivered by the customer) and then can be viewed as a specification purpose method, like signatures were for let-methods. It will lead to a proof obligation later in the development.

A property may also be used to express some "quality" information of the system (soundness, correctness, ..) also submitted to a proof obligation. Formulae are written with usual logical connectors, universal and existential quantifications over a Focal type, and names of methods known within the species's context. For instance, a property telling that if a speed is non-null, then doors can't be opened could look like:

all v in Speed, v <> Speed!zero -> ∼ doors open
In the same way as signatures, even if no proof is yet given, the name of the property can be used to express other ones and its statement can be used as an hypothesis in proofs. Focal late binding and collection mechanisms ensure that the proof of a property will be ultimately done. -Theorems (theorem) made of a name, a statement and a proof are properties together with the formal proof that their statement holds in the context of the species. The proof accompanying the statement will be processed by Focal and ultimately checked with the theorem prover Coq.

Like in any formal development, one severe difficulty before proving is obviously to enounce a true interesting and meaningful statement. For instance, claiming that a piece of software is "formally proved" as respecting the safety requirements system ok "since its property is demonstrated" is a lie if this property was, for instance, 1 = 1 -> system ok. This is obviously a nonsense since the text of the property is trivial and does not link system ok with the rest of the software (see [START_REF] Jaeger | A few remarks about developing secure systems in b[END_REF] for less trivial examples).

We now make concrete these notions on an example we will incrementally extend. We want to model some simple algebraic structures. Let's start with the description of a "setoid" representing the data structure of "things" belonging to a set, which can be submitted to an equality test and exhibited (i.e. one can get a witness of existence of one of these "things"). species Setoid = s i g n a t u r e ( = ) : Self -> Self -> bool ; s i g n a t u r e element : Self ;

property refl : all x in Self , x = x ; property symm : all x y in Self , x = y -> y = x ; property trans : all x y z in Self , x = y and y = z -> x = z ; let d i f f e r e n t (x , y ) = basics # not_b ( x = y ) ; end ;;

In this species, the carrier is not explicitely given (no rep) , since we don't need to set it to be able to express functions and properties our "setoid" requires. However, we can refer to it via Self and it is in fact a type variable. In the same way, we specify a signature for the equality (operator =). We introduce the three properties that an equality (equivalence relation) must conform to.

We complete the example by the definition of the function different which use the name = (here basics#not b stands for the function not b, the boolean and coming from the Focal source file basics.foc). It is possible right now to prove that different is irreflexive, under the hypothesis that = is an equivalence relation (i.e. that each implementation of = given further will satisfy these properties).

It is possible to use methods only declared before they get a real definition thanks to the late-binding feature provided by Focal. In the same idea, redefining a method is allowed in Focal and, it is always the last version which is kept as the effective definition inside the species.

Type of Species, Interfaces and Collections

The type of a species is obtained by removing definitions and proofs. If rep is still a type variable say α, then the species type is prefixed with an existential binder ∃α. This binder will be eliminated as soon as the rep will be instantiated (defined) and must be eliminated to obtain runnable code. The species types remain implicit in the concrete syntax.

The interface of a species is obtained by abstracting the rep type in all the method types of the species type and this abstraction is permanent (see the paragraph Collections). No special construction is given to denote interfaces in the concrete syntax, they are simply denoted by the name of the species underlying them. Interfaces can be ordered by inclusion, a point providing a very simple notion of subtyping.

A species is said to be complete if all declarations have received definitions and all properties have received proofs.

When complete, a species can be submitted to an abstraction process of its carrier to create a collection. Thus the interface of the collection is built out of the type of its underlying species. A collection can hence be seen as an abstract data type, only usable through the methods of its interface, but having the guarantee that all methods/theorems are defined/proved.

Combining Bricks by Inheritance

A Focal development is organised as a hierarchy which may have several roots. The upper levels of the hierarchy are built during the specification stage while the lower ones correspond to implementations. Each node of the hierarchy, i.e. each species, is a progress to a complete implementation. On the previous example, forgetting different, we typically presented a kind of species for "specification" since it expressed only signatures of functions to be later implemented and properties to which, later, give proofs.

We can now create a new species, may be more complex, by inheritance of a previously defined. We say here "may be more complex" because it can add new operations and properties, but it can also only bring real definitions to signatures and proofs to properties, adding no new method.

Hence, in Focal inheritance serves two kinds of evolutions. In the first case the evolution aims making a species with more operations but keeping those of its parents (or redefining some of them). In the second case, the species only tends to be closer to a "run-able" implementation, providing explicit definitions to methods that were previously only declared. A strong constraint in inheritance is that the type of inherited, and/or redefined methods must not change. This is required to ensure consistence of the Focal model, hence of the developed software.

Continuing our example, we want to extend our model to represent "things" with a multiplication and a neutral element for this operation.

species Monoid inherits Setoid = s i g n a t u r e ( * ) : Self -> Self -> Self ;

s i g n a t u r e one : Self ; let element = one * one ; end ;;

We see here that we added new methods but also gave a definition to element, saying it is the application of the method * to one twice, both of them being only declared. Here, we used the inheritance in both the presented ways: making a more complex entity by adding methods and getting closer to the implementation by explicitly defining element.

Multiple inheritance is available in Focal. For sake of simplicity, the above example uses simple inheritance. In case of inheriting a method from several parents, the order of parents in the inherits clause serves to determine the chosen method.

The type of a species built using inheritance is defined like for other species, the methods types retained inside it being those of the methods present in the species after inheritance is resolved.

Combining Bricks by Parameterisation

Until now we are only able to enrich species (may be "refine", even if we do not address the notion of "refinement" of the Atelier B [START_REF] Weis | The B Book, Assigning Programs to Meanings[END_REF]). However, we sometimes need to use a species, not to take over its methods, but rather to use it as an "ingredient" to build a new structure. For instance, a pair of setoids is a new structure, using the previous species as the "ingredient" to create the structure of the pair. Indeed, the structure of a pair is independent of the structure of each component it is made of. A pair can be seen as parameterised by its two components. Following this idea, Focal allows two flavors of parameterisation.

Parameterisation by Collection Parameters

We first introduce the collection parameters. They are collections that the hosting species may use through their methods to define its own ones.

A collection parameter is given a name C and an interface I. The name C serves to call the methods of C which figure in I. C can be instantiated by an effective parameter CE of interface IE. CE is a collection and its interface IE must contain I. Moreover, the collection and late-binding mechanisms ensure that all methods appearing in I are indeed implemented (defined for functions, proved for properties) in CC. Thus, no runtime error, due to linkage of libraries, can occur and any property stated in I can be safely used as an hypothesis.

Calling a species's method is done via the "bang" notation: !meth or Self!meth for a method of the current species (and in this case, even simpler: meth, since the Focal compiler will resolve scoping issues). To call collection parameters's method, the same notation is used: A!element stands for the method element of the collection parameter A.

To go on with our example, a pair of setoids has two components, hence a species for pairs of setoids will have two collection parameters. It is itself a setoid, a fact which is simply recorded via the inheritance mechanism: inherits Setoid gives to Setoid product all the methods of Setoid. We express the carrier of the product of two setoids as the Cartesian product of the carriers of the two parameters. In A * B, * is the Focal type constructor of pairs, A denotes indeed the carrier type of the first collection parameter, and B the one of of the second collection parameter.

Next, we add a definition for = of Setoid product, relying on the methods = of A (A!( = )) and B (which are not yet defined). Similarly, we introduce a definition for element by building a pair, using the function create (which calls the predefined function basics#crp) and the methods element of respectively A and B. And we can prove that = of Setoid product is indeed reflexive, upon the hypothesis made on A!( = ) and B!( = ). The part of Focal used to write proofs will be shortly presented later, in section 2.6.

This way, the species Setoid product builds its methods relying on those of its collection parameters. Note the two different uses of Setoid in our species Setoid product, which inherits of Setoid and is parameterised by Setoid.

Why such collection parameters and not simply species parameters? There are two reasons. First, effective parameters must provide definitions/proofs for all the methods of the required interface: this is the contract. Thus, effective parameters must be complete species. Then, we do not want the parameterisation to introduce dependencies on the parameters' carrier definitions. For example, it is impossible to express " if A!rep is int and B!rep is bool then A*B is a list of boolean values". This would dramatically restrict possibilities to instantiate parameters since assumptions on the carrier's structure, possibly used in the parameterised species to write its own methods, could prevent collections having the right set of methods but a different internal representation of the carrier to be used as effective parameters. Such a behaviour would make parameterisation too weak to be usable. We choose to always hide the carrier of a collection parameter to the parameterised hosting species. Hence the introduction of the notion of collection, obtained by abstracting the carrier from a complete species.

Parameterisation by Entity Parameters

Let us imagine we want to make a species working on natural numbers modulo a certain value. In 5 modulo 2 is 1, both 5 and 2 are natural numbers. To be sure that the species will consistently work with the same modulo, this last one must be embedded in the species. However, the species itself doesn't rely on a particular value of the modulo. Hence this value is clearly a parameter of the species, but a parameter in which we are interested by its value, not only by its carrier and the methods acting on it. We call such parameters entity parameters, their introduction rests upon the introduction of a collection parameter and they denote a value having the type of the carrier of this collection parameter.

Let us first have a species representing natural numbers:

species IntModel = s i g n a t u r e one : Self ; s i g n a t u r e modulo : Self -> Self -> Self ; end ;; Note that IntModel can be later implemented in various ways, using Peano's integers, machine integers, arbitrary-precision arithmetic . . . We now build our species "working modulo . . . ", embedding the value of this modulo like: Using the entity parameter n, we ensure that the species Modulo work will work for any value of the modulo, but will always use the same value n of the modulo everywhere inside the species.

species M o d u l o _ w o r k ( Naturals is IntModel , n in Naturals ) = let job1 ( x in

The Final Brick

As briefly introduced in 2.2, a species needs to be fully defined to lead to executable code for its functions and checkable proofs for its theorems. When a species is fully defined, it can be turned into a collection, that can roughly be seen as an instance of the species. Hence, a collection represents the final stage of the inheritance tree of a species and leads to an effective structure of the carrier with executable functions processing it.

For instance, providing that the previous species IntModel turned into a fullydefined species MachineNativeInt through inheritances steps, with a method from string allowing to create the natural representation of a string, we could get a related collection by: c o l l e c t i o n M a c h i n e N a t i v e I n t C o l l i m p l e m e n t s M a c h i n e N a t i v e I n t ;;

Next, to get a collection implementing arithmetic modulo 8, we could extract from the species Modulo work the following collection: As seen by this example, a species can be applied to effective parameters by giving their values with the usual syntax of parameter passing.

As said before, to ensure modularity and abstraction, the carrier of a collection turns hidden. This means that any software component dealing with a collection will only be able to manipulate it through the operations (methods) it provides. This point is especially important since it prevents other software components from possibly breaking invariants required by the internals of the collection.

Properties, Theorems and Proofs

Focal aims not only to write programs, it intends to encompass both the executable model (i.e. program) and properties this model must satisfy. For this reason, "special" methods deal with logic instead of purely behavioral aspects of the system: theorems, properties and proofs.

Stating a property expects that a proof that it holds will finally be given. For theorems, the proof is directly embedded in the theorem. Such proofs must be done by the developer and will finally be sent to the formal proof assistant Coq who will automatically check that the demonstration of the property is consistent. Writing a proof can be done in several ways.

It can be written in "Focal's proof language", a hierarchical proof language that allows to give hints and directions for a proof. This language will be sent to an external theorem prover, Zenon [START_REF] Bonichon | Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs[END_REF][START_REF] Doligez | version 0.4.1[END_REF] developed by D. Doligez. This prover is a first order theorem prover based on the tableau method incorporating implementation novelties such as sharing. Zenon will attempt, from these hints to automatically generate the proof and exhibit a Coq term suitable for verification by Coq. Basic hints given by the developer to Zenon are: "prove by definition of a method" (i.e. looking inside its body) and "prove by property" (i.e. using the logical body of a theorem or property". Surrounding this hints mechanism, the language allows to build the proof by stating assumptions (that must obviously be demonstrated next) that can be used to prove lemmas or parts for the whole property.

The detailed presentation of Zenon, its internals and its language (the one we called "Focal's proof language") is outside the scope of this presentation. We however show below an example of such demonstration. <1 >1 assume x in Self , assume y in Self , assume i in Self , assume H1 : ! o r d e r _ i n f(i , x ) , assume H2 : ! o r d e r _ i n f(i , y ) , prove ! o r d e r _ i n f(i , ! inf (x , y ) ) <2 >1 prove ! equal (i , ! inf (! inf (i , x ) , y ) ) by h y p o t h e s i s H1 , H2 property i n f _ l e f t _ s u b s t i t u ti o n_ ru l e , equal_symmetric , e q u a l _ t r a n s i t i v e d e f i n i t i o n of o r d e r _ i n f <2 >9 qed by step <2 >1 property i n f _ i s _ a s s o ci at iv e , e q u a l _ t r a n s i t i v e d e f i n i t i o n of o r d e r _ i n f <1 >2 qed . ;

The important point is that Zenon works for the developer: it searches the proof itself, the developer does not have to elaborate it formally "from scratch".

Like any automatic theorem prover, Zenon may fail finding a demonstration. In this case, Focal allows to write verbatim Coq proofs. In this case, the proof is not anymore automated, but this leaves the full power of expression of Coq to the developer.

Finally, the assumed keyword is the ultimate proof backdoor, telling that the proof is not given but that the property must be admitted. Obviously, a really safe development should not make usage of such "proofs" since they bypass the formal verification of software's model. However, such a functionality remains needed since some of "well-known" properties can never be proved for a computer. For instance, ∀x ∈ IN, x + 1 > n does not hold in a computer with native integers: in this case arithmetic works modulo the number of bits of the machine word ! However, in a mathematical framework, this property holds and is needed to carry out other proofs ! On another side, a development may be linked with external code, trusted or not, but for which properties can't be proved inside the Focal part since it does not belong to it. Expressing properties of the Focal part may need to express properties on the imported code, that cannot be formally proved, then must be "assumed".

Around the Language

In the previous sections, we presented Focal through its programming model and shortly its syntax. We especially investigated the various entities making a Focal program. We now address what becomes a Focal program once compiled. We recall that Focal supports the redefinition of functions, which permits for example to specialize code to a specific representation of the carrier (for example, there exists a generic implementation of integer addition modulo n but it can be redefined in arithmetics modulo 2 if boolean values are used to represent the two values). It is also a very convenient tool to maintain software.

Consistency of the Software All along the development cycle of a Focal program, the compiler keeps trace of dependencies between species, their methods, the proofs, . . . to ensure that modifications of an entity will be detected on any of those depending of the former.

Focal considers two types of dependencies:

-The decl-dependency: a method A decl-depends on a method B, if the declaration of B is required to write A. -The def-dependency: a method (and more especially, a theorem) A defdepends on a method B, if the definition of B is required to write A (and more especially, to prove the property stated by the theorem A).

The redefinition of a function may invalidate the proofs that use properties of the body of the redefined function. All the proofs which truly depend of the definition are then erased by the compiler and must be done again in the context updated with the new definition. Thus the main difficulty is to choose the best level in the hierarchy to do a proof. In [START_REF] Prevosto | Making proofs in a hierarchy of mathematical structures[END_REF], Prevosto and Jaume propose a coding style to minimize the number of proofs to be redone in the case of a redefinition, by a certain kind of modularisation of the proofs.

Code Generation Focal currently compiles programs toward two languages, OCaml to get an executable piece of software, and Coq to have a formal model of the program, with theorems and proofs.

In OCaml code generation, all the logical aspects are discarded since they do not lead to executable code.

Conversely, in Coq, all the methods are compiled, i.e. "computational" methods and logical methods with their proofs. This allows Coq to check the entire consistence of the system developed in Focal.

Since Focal's compilation model is based on record types (i.e. struct à la C) code generation toward most of the current programming languages can be imagined. A C backend is currently under study, which should allow to manage once for all the compilation of high-level constructs found in ML-like languages and reused in Focal (pattern-matching, higher-order functions, variant types . . . ).

Tests Focal incorporates a tool named FocalTest [START_REF] Carlier | Functional testing in the focal environment[END_REF] for Integration/Validation testing. It allows to confront automatically a property of the specification with an implementation. It generates automatically test cases, executes them and produces a test report as an XML document. The property under test is used to generate the test cases, it also serves as an oracle. When a test case fails, it means a counterexample of the property has been found: the implantation does not match the property; it can also indicate an error in the specification.

The tool FocalTest automatically produces the test environment and the drivers to conduct the tests. We benefit from the inheritance mechanism to isolate the testing harness from the components written by the programmer.

The testable properties are required to be broken down into a precondition and a conclusion, both executable. FocalTest proposes a pure random test cases generation: it generates test cases until the precondition is satisfied, the verdict of the test case is given by executing the postcondition. It can be an expensive process for some kind of preconditions. To overcome this drawback, a constraint based generation is under development: it allows to produce directly test cases for which the precondition is satisfied.

Documentation

The tool called focdoc [START_REF] Maarek | Focdoc: The documentation system of foc[END_REF] automatically generates documentation, thus the documentation of a component is always coherent with respect to its implementation.

This tool uses its own XML format that contains information coming not only from structured comments (that are parsed and kept in the program's abstract syntax tree) and Focal concrete syntax but also from type inference and dependence analysis. From this XML representation and thanks to some XSLT stylesheets, it is possible to generate HTML files or L A T E X files. Although this documentation is not the complete safety case, it can helpfully contribute to its elaboration. In the same way, it is possible to produce UML models [START_REF] Delahaye | A Formal and Sound Transformation from Focal to UML: An Application to Airport Security Regulations[END_REF] as means to provide a graphical documentation for Focal specifications. The use of graphical notations appears quite useful when interacting with end-users, as these tend to be more intuitive and are easier to grasp than their formal (or textual) counterparts. This transformation is based on a formal schema and captures every aspect of the Focal language, so that it has been possible to prove the soundness of this transformation (semantic preservation).

Focal's architecture is designed to easily plug third-parties analyses that can use the internal structures elaborated by the compiler from the source code. This allows, for example, to make dedicated documentation tools for custom purposes, just exploiting information stored in the Focal program's abstract syntax tree, or extra information possibly added by extra processes, analyses.

Access control : a Case Study within Focal

Access control is any mechanism by which a system grants or revokes the rights for active entities, the subjects, to access some passive entities, the objects, or perform some action. In this section we present a brief survey of the library of access control models developed within Focal.

Several approaches have been followed in order to build a formal library of access control models. First, in [START_REF] Gureghian | A full formalisation of the Bell and Lapadula security model[END_REF], we have formalised within Coq [START_REF] Project | The Coq Proof Assistant Reference Manual[END_REF] the Bell & LaPadula (BLP) model by following the original paper [START_REF] Lapadula | Secure Computer Systems: A Mathematical Model[END_REF] : definition of the policy, of the transition function between states of the system and formal proof of the "Basic Security Theorem" [START_REF] Lapadula | Secure Computer Systems: A Mathematical Model[END_REF] stating that the transition function preserves the policy. Then, by using the program extraction (from a proof) mechanism of Coq, we have obtained a certified implementation of this access control policy. Such development formally ensures that the program we have obtained satisfies the desired security properties, thus providing a greater level of confidence. However, it is rather technical and time-consuming and requires some backgrounds within Coq. Furthermore, this formalisation cannot be easily reused if we want to implement another policy. Indeed many policies share some definitions and properties and, as it is widely recognised, it seems desirable to deal with an abstract generic framework in order to ease and speed implementations by reusing. Indeed, having an abstract formalism would allow to obtain an implementation which is well-suited for a given context just by instantiating parameters. Hence, in a second time, we have used Focal to implement the algebra of security model introduced by J.McLean in [START_REF] Mclean | The algebra of security[END_REF]. Such algebra provides a generic framework to specify policies. From this implementation, we have instantiated the framework in order to obtain a formal development of the BLP model [START_REF] Jaume | Formalisation and implementation of access control models[END_REF][START_REF] Jaume | A formal approach to implement access control[END_REF]. In order to illustrate the practical applicability of the previous development, we have refined this system to manage accesses into a relational database. To achieve this goal, we do not want to define the complete database in Focal, but rather to define a reference monitor and to plug it into an existing database, such as MySQL. So we have to catch every SQL query sent to the server and translate it in terms of access, thus providing requests for the access control system. Then these requests are executed by our Focal program, which returns an answer. If this answer is yes, then the SQL query is executed by the SQL server, else an error message is returned to the user (see figure 1). Of course, more sophisticated security models exist for databases, but our aim was to show that our "formal program" can be used in concrete contexts. All this work is described in [START_REF] Blond | Formalisation et implantation d'une politique de sécurité d'une base de données[END_REF][START_REF] Blond | Un moniteur de référence sûr d'une base de données[END_REF].

Unfortunately, the framework of the "algebra of security" is not enough expressive for some access control models and we have defined and implemented within Focal a specification of access control policies at a deeper level. Hence, we have addressed the question of "what is an access control model ?" regardless of any specific context, by defining a general semantical framework allowing to specify and to define access control models. Such a framework provides several levels of specification. First, the considered information system can be described by specifying the security parameters and by defining how to represent states of this system (what is the security information describing a state of the system). Then an access control policy is defined as a means to permit or deny a subject (users, processes, ...) the use of an object (files, processes, ...). This can be done by introducing a predicate allowing to characterise secure states of the system (which are the states satisfying the policy). The next step consists in specifying the syntax and the semantics of a language of requests allowing the system to move from one state to another state. The specification of a policy and a language of requests leads to the notion of access control model. Lastly, our framework allows to describe what are the transition functions (definitions of reference monitors) of a model and what security properties these transition functions have to satisfy (the main properties are concerned with the policy and the semantics of requests). Furthermore, since several transition functions can be defined for an access control model, we introduce a way to compare such transition functions.

As a usage of Focal, we are developing an access control library based on the framework previously described. The architecture of the framework's implementation within Focal is shown in figure 2. As we consider the systems on which we apply access control as state transition systems (reference monitors are tran-sition functions), we see that the species states is the central species of the implementation. Indeed, it is parameterised by the basic components of an access control system (subjects, objects, security parameter, . . . ), and is inherited by the species defining the access control policy (policies), the semantics of requests (semantics requests) and the transition function (models). We also see how we use the framework's implementation in order to implement a particular access control model, this is done by refining the framework's species thanks to inheritance. Those species defining an access control model are the ones ending with a *, where * can be replaced by the name of the access control model implemented. For instance, the library currently offers the Bell & LaPadula, RBAC, HRU, Unix-like and Unforgeable Tickets (capabilities based) models. Hence, this architecture shows some of the strength of Focal which are parameterisation and refinement through inheritance that allow us to follow a quite complex formalisation and to implement access control models by first considering what is common to every models and then focusing on what is particular to a specific one (this way of developing also ease code reusing).

Another major feature of Focal is to allow to write properties and to prove them in order to show the correctness of an implementation. This has currently be done in the access control library for the RBAC and HRU models (our aim is to certify all the implemented models), and we show here an example of such a theorem concerning the correctness of the RBAC transition function. Indeed, the following theorem tau rbac acc secure states the correctness of the RBAC transition function according to the RBAC security predicate (omega). For the sake of simplicity, we only consider here the requests allowing to ask to get or to release an access (the correctness proof taking into account the administrative requests of the RBAC model has also be done). We now show the architecture of its proof. The first step consists to consider the hypothesis needed to do the proof and to express what we want to prove, as we would do in any mathematical proof.

proof :

<1 >1 assume st1 in Self , assume st2 in Self , assume r1 in Req , assume d1 in Dec , assume H1 : t a u _ r b a c _ a c c( r1 , st1 ) = ( d1 , st2 ) , assume H2 : omega ( st1 ) , prove omega ( st2 )

Then, mainly, we need to consider two cases corresponding to the two possible requests, "get an access" (is get) or "release an access" (is rel) and prove our goal. Finally, we are able to conclude this proof thanks to the property get or rel stating that the requests we consider are either "get an access" or "release an access" requests. To summerize, our framework, described in [START_REF] Jaume | Towards a formal specification of access control[END_REF][START_REF] Jaume | Contrôler le contrôle d'accès : Approches formelles[END_REF][START_REF] Jaume | On specifying, implementing and comparing access control models. A Semantical Framework[END_REF][START_REF] Morisset | Sémantique des systèmes de contrôle d'accès[END_REF], has been used to formalise, to implement within Focal and to compare the BLP model [START_REF] Morisset | Sémantique des systèmes de contrôle d'accès[END_REF], the Chinese Wall model [START_REF] Morisset | Sémantique des systèmes de contrôle d'accès[END_REF], the RBAC (role based access control) model [START_REF] Habib | A formal comparison of the bell & lapadula and rbac models[END_REF], and discretionary policies (HRU model, trust management model, unforgeable tickets model) [START_REF] Anseaume | Formalisation, spécification et implantation de politiques de contrôle d'accès avec l'atelier focal[END_REF].

Conclusion

This paper is mostly devoted to Focal which was conceived from the beginning to help constructions of systems highly concerned with safety and security. Its development is based on strong theories such as type theories, denotational and operational semantics, rewriting. But, our methodology for Focal development is to incorporate only parts of these theories which are mandatory for our purposes. For example, the Focal language is indeed a dependent type language but some dependencies available for example in the proof assistant Coq are not offered: for instance, a function cannot depend of a proof. If such a possibility is retained, then treatment of partiality of functions can perhaps be improved but we would have to manage possible logical clashes when redefining a function. It seems to us that this management would be too difficult for engineers and we reject this possibility.

The claim behind Focal is that formal developments tend to increase the confidence in the final code. One of the main characteristics of critical software is that it is subject to the approval of a safety/security authority before its commissioning. These authorities have defined requirements explaining what should be an acceptable software and its related life cycle process for their own domain. For this reason, getting a high confidence in produced code, and making possible for the safety/security authority to acquire this confidence is an important task, for which Focal brings solutions. Very important is the possibility in Focal to have one unique language for specification, implementation and proofs, since it eliminates the errors introduced between each layer, each switch between languages, during the development cycle.

Other frameworks like Atelier B [1] also aims to implement tools for making formal development a reality. Focal doesn't follow the same path, trying to keep the mean of expression close to what engineers usually know: something close to a programming language. Moreover, instead of having its own system for proofs validation, Focal makes use of external tools, leaving the task of handling proof automation and verification outside its scope and keeping benefits from

  species S e t o i d _ p r o d u c t ( A is Setoid , B is Setoid ) inherits Setoid = rep = ( A * B ) ; let ( = ) (x , y ) = and_b ( A !( = ) ( first ( x ) , first ( y ) ) , B !( = ) ( scnd ( x ) , scnd ( y ) ) ) ; let create (x , y ) in Self = basics # crp (x , y ) ; let element = Self ! create ( A ! element , B ! element ) ; proof of refl = by d e f i n i t i o n of ( = ) ; end ;;

  c o l l e c t i o n M o d u l o _ 8 _ w o r k i m p l e m e n t s M o d u l o _ w o r k ( M a c h i n e N a t i v e In tC ol l , M a c h i n e N a t i v e I n t C o l l! f r o m _ s t r i n g ( ' '8 ' ') ;;

  theorem o r d e r _ i n f _ i s _ i n f i m u m: all x y i in Self , ! o r d e r _ i n f(i , x ) -> ! o r d e r _ i n f(i , y ) -> ! o r d e r _ i n f(i , ! inf (x , y ) ) proof :

Fig. 1 .

 1 Fig. 1. Access control into a database

  theorem t a u _ r b a c _ a c c _ s e c u r e : all st1 st2 in Self , all r1 in Req , all d1 in Dec , t a u _ r b a c _ a c c( r1 , st1 ) = ( d1 , st2 ) -> omega ( st1 ) -> omega ( st2 )

*Fig. 2 .

 2 Fig. 2. Architecture of the framework's and access control models' implementation

Acknowledgments This work was partially supported by the French SSURF ANR project ANR-06-SETI-016 (Safety and Security UndeR Focal). Many thanks to James Geater for his careful proofreading.

researches performed aside in these specific domains.


Gaël Pallares

Matthieu George

Laurent Ponson

Stéphane Roux

Matteo Ciccotti
email: matteo.ciccotti@espci.fr

Multiscale investigation of stress-corrosion crack propagation mechanisms in oxide glasses

Keywords: Multiscale mechanical analysis, Stress-corrosion, Atomic Force Microscopy, Digital Image Correlation, Glass Plasticity

Fracture propagation involves the coupling of many length scales ranging from the sample loading geometry to the molecular level. In brittle materials, the length scales of the damage process zone are reduced to a submicrometric scale and the coupling with the macroscopic scale is expected to be the domain of linear elastic fracture mechanics (LEFM). However, although 2D elastic analyses are generally adequate to describe the sample deformation at macroscopic scales, local investigations of failure mechanisms at the sample free surface require the use of 3D mechanical tools due to the crack front local curvature and to the corner point singularities at the intersection between the crack front and the external surfaces of the sample. We present here a thorough multiscale investigation of the slow crack growth of a sharp crack in oxide glasses in the stress-corrosion regime, combining experimental and numerical analyses of the displacement fields from the millimeter scale to the nanoscale range. The principal aim of the study is identifying the length and time scales of the mechanisms of damage and interaction between water and glass, which have been the subject of an extensive debate in the last decades.

Introduction

Glass is a very widespread material due to its excellent transparency and corrosion resistance. It also has indeed excellent mechanical properties, because it is actually very stiff and can be brought to very high strength when it is produced into very thin fibers or layers, by reducing the number and size of defects and taking a particular care of the external surfaces. The main limitation remains the elevated brittleness of glass, i.e. its tendency to initiate and propagate fractures with very low energy dissipation. This can manifest itself in two very different ways. The first one is the well known catastrophic (critical) fracture, occurring upon overcoming some critical static or dynamic (shock) loading, and resulting in propagation velocities close to the sound speed in glass, i.e. several km/s. The second more subtle manifestation is the slow sub-critical propagation of pre-existing flaws under moderate stresses, which can involve very low velocities ranging from mm/s to pm/s and below (although this becomes hardly measurable) and which plays an outstanding role in the life duration of many loaded structures (the so called "static fatigue"). For oxide glasses, subcritical crack growth mainly originates from stress-corrosion mechanisms, which are related to different kinds of stress and temperature enhanced interactions of glass with the local environment at the crack tip, mainly with water molecules in wet or moist environment (cf. recent reviews form [START_REF] Ciccotti | Stress-corrosion mechanisms in silicate glasses[END_REF][START_REF] Freiman | Environmentally enhanced fracture of glass: A historical perspective[END_REF][START_REF] Wiederhorn | Griffith cracks at the nanoscale[END_REF].

The understanding of the mechanisms of glass strength reduction by Griffith cracks [START_REF] Griffith | The phenomena of rupture and flow in solids[END_REF] and the role of stress-corrosion in the static fatigue of glass has lead to important applications concerning reinforcement fibers and telecom optical fibers which approach the theoretical strength of 10 GPa [START_REF] Brambilla | The ultimate strength of glass silica nanowires[END_REF]. When combining high quality surface finish with thermal of chemical tempering to induce compressive stresses on the glass surfaces, very strong flat glasses can also be produced, which allowed the development of very thin and light smartphone displays and a progressive increase of the use of glass as structural material such as in the transparent crosswalk over the Grand Canyon.

Stress-corrosion is a hydrolysis chemical reaction happening at the crack tip, which would normally be very slow on glass at ambient temperature, but is significantly accelerated due to stress concentration. Most ordinary oxide glasses are silicate glasses, where about 80 wt.% is constituted by a densely crosslinked network of silica tetrahedra, SiO 4 , bonded by a common oxygen atom, thus creating Si-O-Si (siloxane) bridges that locally form some rings of radii down to 0.5 nm. The basic corrosion reaction is a three step reaction involving water adsorption on the Si-O bonds, then the hydrolysis reaction itself (exchange of electron and proton), and finally the separation of the bond in two separate silanol groups (Si-OH), which correspond to one step advance of the fracture in the main silicate network of the glass.

The vision of stress corrosion as a sequence of individual bond breakings by stress (and temperature) enhanced hydrolysis was established in the seventies [START_REF] Wiederhorn | Influence of water vapor on crack propagation in soda-lime glass[END_REF][START_REF] Wiederhorn | Stress-corrosion and static fatigue of glass[END_REF][START_REF] Michalske | Slow fracture model based on strained silicate structures[END_REF]. The kinetics of stress corrosion crack propagation can be represented by a three region scheme on a graph describing the logarithm of crack velocity v (spanning from cm/s to pm/s) against the stress intensity factor (SIF) K, when K is smaller than the toughness 𝐾 𝑐 that is of the order of 1 MPa.m 1/2 for most glasses. Michalske and Freiman, 1983). Right: Schematic v(K) diagram for subcritical crack propagation in oxide glasses.

Figure 1. Left: basic mechanisms of the stress-corrosion reactions (from

Region I is the proper stress-corrosion regime, where the stress enhances exponentially crack propagation according to accelerated hydrolysis reactions. Region II is a plateau where crack velocity is limited by the migration of water molecules towards the very confined crack tip. Region III is a very steep region where the SIF is so high that crack can propagate without any contribution from water hydrolysis. In some glasses such as alkali-silicate glasses, an additional region 0 corresponds to a threshold for crack propagation.

The phenomenology of the stress-corrosion regime (region I), consists of an exponential dependence of the crack velocity on the stress intensity factor, an almost proportional dependence on humidity and an increase of crack velocity with temperature. This was experimentally established by Sheldon [START_REF] Wiederhorn | Influence of water vapor on crack propagation in soda-lime glass[END_REF][START_REF] Wiederhorn | Stress-corrosion and static fatigue of glass[END_REF] who also proposed the following model equation:

𝑣 = 𝑣 0 exp(𝛽𝐾) = 𝐴 � 𝑝 𝐻 2 𝑂 𝑝 0 � 𝑚 exp �- ∆𝐸 𝑎 -𝑏𝐾 𝑅𝑇 � (1)
which is based on the chemical reaction rate theory for the hydrolysis of siloxane bonds by water molecules. The dependency on humidity

𝑝 𝐻 2 𝑂 𝑝 0
, the main reactant, is a multiplicative power law with an exponent m close to 1, which is the order of the reaction. The dependency on both temperature T and K appears through an Arrhenius term, where R is the gas constant and the activation barrier ∆𝐸 𝑎 can be reduced by the presence of local tensile stress 𝜎 𝑡𝑖𝑝 at the crack tip of radius ρ (we can write 𝜎 𝑡𝑖𝑝 𝑉 𝑎 = 𝑏𝐾, where 𝑉 𝑎 is an activation volume of molecular dimensions).

Phenomenological equations such as Wiederhorn's (eq. 1) can describe the dependence of crack velocity on stress and on environmental parameters for most typical glasses and are compatible with a thorough consistent modeling based on the sharp-crack atomic-bonding paradigm [START_REF] Lawn | Fracture of brittle solids[END_REF]).

Yet the detailed nature of the stress-corrosion mechanisms that occur at the crack tip have been debated for decades (Marsh 1964b;[START_REF] Maugis | Review: Subcritical crack growth, surface energy, fracture toughness, stick-slip and embrittlement[END_REF][START_REF] Gehrke | Fatigue limit and crack arrest in alkalicontaining silicate glasses[END_REF][START_REF] Tomozawa | Fracture of glasses[END_REF], and a

general disagreement can be found on the relevance of several accessory phenomena that may participate in the stress-corrosion mechanisms at different stages of the process. Stress-corrosion can involve a complex interplay between the diffusion of reactive molecules (mainly water) into the crack cavity and into the glass network, the corrosion (or dissolution) of the network itself, and the migration of weakly bonded alkali ions under chemical or stress gradient [START_REF] Gehrke | Fatigue limit and crack arrest in alkalicontaining silicate glasses[END_REF][START_REF] Bunker | Molecular mechanisms for corrosion of silica and silicate glasses[END_REF]). We note that in pure silica glass the absence of ion migration can lead to significantly different local corrosion mechanisms. All three phenomena are typically very slow under ambient conditions in the unstressed material, but they can significantly accelerate in the highly stressed neighborhood of the crack tip, depending especially on the nature of the environment and of its confinement in the crack tip cavity.

A major objection to the sharp-crack atomic-bonding paradigm comes from the hypothesis of a significant contribution of plastic deformation at the crack tip in the slow crack propagation mechanisms. Since the early works of [START_REF] Dugdale | Yielding of steel sheets containing slits[END_REF] on metals, and the observations of plastic behavior of glass under compression in indentation and scratch marks [START_REF] Taylor | Mechanisms of fracture in glass and similar brittle solids[END_REF]), several investigations have been carried out to track the evidence of plastic behavior in the strong tensile stress field at crack tips in glasses.

The fracture energies measured by [START_REF] Wiederhorn | Fracture surface energy of glass[END_REF] for six glasses in inert environment range between 7 and 10 J/m 2 , a figure which is tenfold higher than twice the typical values of the surface tension of glasses 𝛾 = 0.5 J/m 2 [START_REF] Griffith | The phenomena of rupture and flow in solids[END_REF]) which suggests a significant contribution of irreversible processes in crack propagation. By considering a typical yield stress of 10 GPa for glass, the size of the crack tip plastic region associated to such fracture energies by the Dugdale model would be limited to a few nanometers. In the subcritical stress-corrosion regime, the fracture energies and the estimated sizes of the plastic regions are lower. However, the extent of the penetration of reactive molecules from the environment into the glass network has been much debated [START_REF] Marsh | Plastic Flow and Fracture of Glass[END_REF], Tomozawa 1984) and this can enhance damage and plasticity on larger regions around the crack tip (cf. )micrometer to millimeter scale. A complementary investigation by [START_REF] Bonamy | Scaling exponents for fracture surfaces in homogeneous glass and glassy ceramics[END_REF] was based on the observation of a cutoff length close to 50 nm in the statistical correlation functions of the crack surface morphology measured post-mortem by AFM. This cutoff length was also attributed to the size of the process zone. On the other hand, [START_REF] Guin | Fracture of silicate glasses: ductile or brittle?[END_REF] have observed that the post-mortem recombination of the AFM measurements of the morphology of opposing crack surfaces in silica and soda-lime showed no evidence for the expected traces of the nanocavities in the bulk of the specimen. All these very resolved but seemingly contradictory AFM observations reopened the debate on crack tip plasticity.

The aim of this paper is to show that a coherent interpretation of these AFM nanoscale investigations, which are limited to the external surface of the sample in the close neighborhood of the crack tip, can be achieved by a thorough multiscale analysis of the mechanics of fracture from the macroscopic scale where the loading is applied to the sample, to the submicrometric scale where the crack tip singularity lives.

In most fracture mechanics test samples, the macroscopic aspects are tackled by establishing the expression of the stress intensity factor K as a function of the applied force F, the crack length a and the geometric parameters of the sample through a 2D finite element analysis. This approach conveniently describes the overall energetic balance during crack propagation as well as the inplane elastic displacement fields of the sample at macroscopic scale. However, when considering the local fields close to the crack tip the actual shape of the crack front will play dominant role. Like in most test samples, the crack front shape of the DCDC sample (described in Fig. 3a) used in most of these AFM investigations is bowed into a parabolic shape as shown in figure 3. Since the AFM observations are intrinsically limited to the external surface of the sample, the fact that the crack front is not normal to the external surface breaks the 2D symmetry of the local stress and displacement fields. This prevents one from taking advantage of the classical plane stress or plane strain 2D solutions, especially for what concerns the out of plane displacement field, which is the main observable of AFM measurements. [START_REF] Fett | Finite element analysis of a crack tip in silicate glass: No evidence for a plastic zone[END_REF] showed the inadequacy of the 2D plane-stress solution used by [START_REF] Guilloteau | The direct observation of the core region of a propagating fracture crack in glass[END_REF] and then by Célarié et al. (2003) to represent the elastic out of plane surface displacement near the crack tip with a 1/𝑟 1/2 dependence (figure 4 left). They pointed out that the mechanical solutions to describe the corner singularity of a 3D surface striking crack were provided by [START_REF] Benthem | State of stress at the vertex of a quarter-infinite crack in a half-space[END_REF] and Bažant and Essentoro (1979), and imply the use of a 𝑟 𝜆 dependence (with λ~1/2) to describe the local displacement field. [START_REF] Fett | Finite element analysis of a crack tip in silicate glass: No evidence for a plastic zone[END_REF] showed that using an alternative fit of the data of Célarié et al. (2003) based on a 3D elastic numerical simulation, the deviation of the displacement profiles measured by AFM from the elastic numerical solution is much less obvious (figure 4 right). However, the quality of the fit on the vertical topography profiles is insufficient to drive accurate conclusions, due to the fact that the vertical extent of the out of plane displacement field on AFM images is of the same order of magnitude as the residual roughness (a few angstroms) even after excellent polishing. 2003), along with the 𝟏/𝒓 𝟏/𝟐 fit used therein. Right: a different fit of the same dataset as proposed by [START_REF] Fett | Finite element analysis of a crack tip in silicate glass: No evidence for a plastic zone[END_REF] according to a 3D elastic numerical analysis.

In order to overcome this problem, we developed an extension of the Digital Image Correlation (DIC) Technique to AFM topographical images of in-situ crack propagation in order to separate properly the 3D surface displacement field from the nanoscale surface roughness [START_REF] Han | Measuring nanoscale stress intensity factors with an atomic force microscope[END_REF].

We show here that only when insuring the steady state crack propagation we can interpret in a fully consistent way the nanoscale resolved displacement fields measured by AFM-DIC with the large scale surface displacement measured by optical profilometry (figure 5). The optical profilometry allows for appreciating the millimetric lateral extent of the crack tip surface depression, which is well separated from surface roughness and clearly attributable to an elastic effect at that scale. The different scales of these experimental observations are bridged by a 3D finite element modeling of the whole DCDC sample involving the accurate crack front shape geometry. The overall multiscale strategy is presented in figure 5. The results of this multiscale analysis provide strong evidence that accurate elastic solutions can describe faithfully the mechanics of the DCDC sample from the macroscopic scale where the load is applied down to the resolution limit of the AFM measurements, represented by the 10 nm size of the probe. This is proved both from the consistency of the measured out of plane displacement throughout all the scales and from the identity (within 5% uncertainty) of the stress intensity factor independently obtained by either the macroscopic mechanical analysis of the structural response of the DCDC sample or by the submicroscale measurement of the crack tip asymptotic displacement fields.

Corner point singularity

We dedicate this second section to some theoretical notions on the corner point singularity, i.e. on the 3D nature of the asymptotic crack tip fields surrounding the region where a crack front intersects the external surface of the sample as in figure 6 (where a perpendicular intersection is chosen for simplifying the first description of the double coordinate system). Intensive theoretical and numerical studies, often disregarded, have been devoted to this problem by [START_REF] Benthem | State of stress at the vertex of a quarter-infinite crack in a half-space[END_REF], Bažant and Essentoro (1979), [START_REF] Dimitrov | 3D-corner effects in crack propagation[END_REF], and applied to the DCDC sample by [START_REF] Fett | Finite element analysis of a crack tip in silicate glass: No evidence for a plastic zone[END_REF].

Figure 6. Representation of a crack front perpendicularly intersecting the external surface of a sample, along with the two spherical and cylindrical coordinate sets used to describe the corner singularity (after [START_REF] Dimitrov | 3D-corner effects in crack propagation[END_REF].

The local symmetry of the crack problem around this singular point is rather spherical than cylindrical (as it is the case for a current point along the crack front away from the edge where classical 2D approaches hold). The asymptotic displacement field u should thus be expressed as:

𝒖(𝑟, 𝜃, 𝜑) = 𝐾 𝐶𝑃 𝑟 𝜆 𝑼 � (𝜃, 𝜑) + 𝑼 𝑟𝑒𝑚 (2)
where K CP denotes the corner stress intensity factor (CSIF), (r,θ,φ) are the spherical coordinates around the corner point as in figure 6. The radial dependency (where r is the distance from the corner point) is a power law with a complex exponent λ called corner singularity, 𝑼 � (𝜃, 𝜑)

represents a universal angular function (depending on the exponent λ , on the Poisson's ratio and in general on the angle of incidence of the crack front on the free surface) and U rem is a non singular reminder. We can express this solution in the more classical cylindrical coordinate system (ρ,θ,z) aligned with the crack front (where ρ is the distance from the crack front, cf. figure 6):

𝒖(𝜌, 𝜃, 𝑧) = 𝐾(𝑧)𝜌 1/2 𝒖 �(𝜃) + 𝒖 𝑟𝑒𝑚 (3)
where K(z) represent the evolution of the classical stress intensity factor along the crack front as a function of the distance z from the corner point at the sample surface:

2 / 1 ) ( - λ z K z K CP (4) The classical value 2 / 1 = λ
, typical of 2D solutions, marks a break even point with respect to the limit of . This case is denoted as a "strong-singularity" and it gives rise to enhanced crack propagation near the surfaces even for a very small load. On the other hand, if the real part of the corner singularity λ is larger than 2 / 1 , then the SIF ) (z K will tend to zero for 0 → z . This case is denoted as a "weak-singularity" and it gives rise to a vanishing propagation velocity of the crack corner point even when the crack propagates (away from the specimen surface). For the sake of simplicity we will refer here to λ as the real part only, which determines the main radial scaling of the asymptotic solutions, and we limit our description to a crack plane that is perpendicular to the external surface of the sample and to macroscopic mode I loading. [START_REF] Benthem | State of stress at the vertex of a quarter-infinite crack in a half-space[END_REF] and Bažant and Essentoro (1979) have shown that for a crack front merging perpendicularly to the free surface, the singularity is weak, resulting in a vanishing SIF at the corner point. In the general case, if the crack front strikes the external surface with an angle α (measured from the normal to the external surface, like in figure 3), the corner singularity λ can be expressed as a universal decreasing function of the angle α and an increasing function of the Poisson's ratio ν of the material. Bažant and Essentoro (1979) and subsequently [START_REF] Dimitrov | 3D-corner effects in crack propagation[END_REF] have proposed an important interpretation of the consequences of this corner point singularity on the evolution of the crack front shape during the ensuing crack propagation. Notably, in the case of a strong singularity ( λ < 1/2) the crack will advance faster at the surface than in the bulk, thus inducing a reduction of the crack front angle α, and hence an increase of λ . On the other hand, in the case of a weak singularity ( λ > 1/2) the crack corner point will be arrested and the crack will advance faster in the bulk, thus inducing an increase of the crack front angle α, and hence a decrease of λ . It is thus a reasonable conjecture that the crack will reach a steady state crack propagation only after the corner point singularity has converged to the classical exponent λ = 1/2, when the stress intensity factor K(z) becomes a constant along the crack front. The crack front angle will thus reach a fixed angle α that only depends on the Poisson's ratio. For these reasons the steady state propagation is a very convenient situation to perform a multiscale analysis. We remark that despite the expected corner singularity for steady state propagation has the same exponent λ = 1/2 as for the in plane displacement field in the classical 2D crack tip singularity, the out-of-plane displacement at a corner point should also present a r 1/2 singularity, which is not predicted by 2D solutions neither in plane stress or plane strain. In order to test this conjecture we perform our investigations on two glasses with a different Poisson's ratio.

) (z K for 0 → z , i.e.

In-situ investigations of crack propagation

In the present experiments, fractures were initiated and propagated on a DCDC sample using a precision loading apparatus (based on a Microtest load cell produced by Deben, Woolpit, UK) (cf.

figure 1). The DCDC test set-up is particularly convenient for these studies due to its excellent stability and compactness (Jannsen 1974). Two kinds of oxide glasses were tested: pure fused silica glass (Suprasil 311, Heraeus, Germany,

Young modulus E = (72 ± 2) GPa, Poisson's ratio ν = (0.17 ± 0.01)) and lithium-aluminium-silicate glass (produced by Saint-Gobain and called LAS in the following, with E = (83 ± 2) GPa and ν = (0.22 ± 0.01)), which is the same glass used by Célarié et al. (2003).

All measurements are done after an extensive stabilization consisting of several hours of steady state propagation, so that crack propagation conditions can be considered as stable. We also insure stable environmental conditions of temperature (±1°C) and relative humidity (±1%). The propagation velocity is accurately measured in the range between 10 -5 and 10 -12 nm/s. The details of the setup and techniques can be found in [START_REF] Célarié | Dynamique de fissuration a basse vitesse des matériaux vitreux[END_REF] and [START_REF] Grimaldi | The crack tip : a nanolab for studying confined liquids[END_REF]. The macroscopic value of the stress intensity factor K was computed according to one of the most recent 2D finite element analyses by [START_REF] Pallares | Crack opening profile in DCDC specimen[END_REF]:

R a R w c R w c c R w c R w c c K R               + + +               + + = 2 5 4 3 2 2 1 0 π σ (5)
where σ is the external load, a is the crack length, and the set of parameters is: c 0 =0.3156, c 1 =0.7350, c 2 =0.0346, c 3 =-0.4093, c 4 =0.3794, and c 5 =-0.0257 for 2.5≤w/R≤5 and the range of applicability is w < a < L-2w.

3D macroscopic analyses of the DCDC specimen

Crack front shape

The crack front shape is measured in-situ by means of a CCD camera at different stages of crack propagation. Several high resolution images are stitched to obtain the whole crack front spanning the 4 mm thickness of the sample (cf. figure 8). The crack front can be fitted very accurately by a parabolic shape, providing the value of the terminal angle, α . This angle is found to be independent on the conditions of loading and environment, and it assumes two clearly different values for the two glasses. The average value for silica glass is α = (8.5±1)° , while for the LAS glass it is α = (15±1)°. The dominant increasing dependency of α on the Poisson's ratio is qualitatively consistent with the predictions of Bažant and Essentoro (1979)

Out-of-plane displacement

The measurements of the out-of-plane displacement on the DCDC samples was performed by an optical profilometer (Wyko NT9100, Bruker, California), placed in a metrological room with These results were compared to the out-of-plane displacement field predicted by the 3D finite element simulation (described in detail in section 6), which accounts for the experimentally measured shape of the crack front. An excellent agreement was reached on the whole range of scales spanned by the optical images as illustrated in figure 9 for silica glass. The residual error is less than 10% of the image vertical dynamics and can be attributed to a weak additional mode III loading present in the experiment but not included in the simulation.

Nanoscale analysis of the asymptotic fields

AFM observations are done in tapping mode on a D3100 from Veeco Metrology Inc., Santa Barbara, California. After an extensive stabilization consisting of several hours of steady state crack propagation and imaging, each AFM image series is acquired within a few hours, so that crack propagation conditions can be considered as stable and AFM drifts are minimized. This provides optimal conditions of the application of Digital Image Correlation techniques. A detailed description of techniques can be found in [START_REF] Han | Measuring nanoscale stress intensity factors with an atomic force microscope[END_REF], but we recall here the most relevant information for interpreting the results.

The aim of the technique is to extract the displacement field between two AFM topographic images, the reference image ) (x f  and the deformed image ) (x g  , taken on the same surface at two different times, the crack length increasing during the time interval (cf. figures 10(a) and 10(b)). The generalization of the so-called "optical flow conservation" which relates the two images can be written as:

) ( )) ( ( ) ( x v x u x g x f      + + = (6) where ) (x u  
(respectively, v ) (x  ) denotes the in-plane (respectively, out-of-plane) displacement field. In other words, the roughness of the two surfaces is used to obtain the in-plane displacement field and then the subtraction of the registered images allows obtaining the out-of-plane displacement field by eliminating the contribution of roughness. In order to develop a robust method, we resort to an "Integrated" DIC approach as introduced by [START_REF] Roux | Stress intensity factor measurements from digital image correlation: post-processing and integrated approaches[END_REF]. The

displacement field ( ) (x u   , ) (x v  ) is sought as a combination of a few expected fields ) (x n  Φ : ) ( )) ( ), ( ( 10 1 x a x v x u i i i     Φ = ∑ = (7)
Six of the base fields represent regular transformations such as uniform extension or shear, which allows for the correction of AFM drifts. Additionally, four others represent the linear elastic fracture mechanics in-plane and out-of-plane singular fields on each image. The steady-state crack propagation condition can be used to enforce the identity of the crack tip fields on the two images after a translation along the crack path direction, thus reducing the number of unknowns.

The in-plane component of the crack tip field can be well approximated by the 2D plane stress condition. On the other hand, the out-of-plane component ) (x  ψ of the singular displacement field is not known analytically. According to the conjecture of [START_REF] Dimitrov | 3D-corner effects in crack propagation[END_REF] discussed in section 2 the crack front geometry adjusts itself during steady-state propagation so that the singularity exponent λ becomes 1/2, as for the 2D in-plane components, yet the angular dependence remains unknown. We thus used the trial solution

x x   = ) ( 0 ψ
to register both images, and then we adjusted the residual field by a simple algebraic expression proposed as a systematic Fourier expansion (truncated at very low order) respecting the mode I crack symmetries:

) ( ) ( θ ρ ψ DIC DIC F x x ⋅ =   (8) E K I DIC π ν ρ 2 / ) 1 ( + = (9) ) cos( ) 2 / cos( ) ( θ θ θ DIC DIC DIC DIC c b a F + + = (10)
The analysis on a first image pairs on silica glass provided the coefficients: [START_REF] Han | Measuring nanoscale stress intensity factors with an atomic force microscope[END_REF].

A series of 5 images of the same 1×1µm 2 zone swept by a crack is first analyzed. As an example, we report in figure 10 the steps of the IDIC analysis of the first two AFM height images of the series. The reference and deformed height images are represented in figure 10(a) and (b). The residual map without out-of-plane displacement is shown in figure 10(c) and the corresponding elastic solution is represented in figure 10(d). Figure 10(e) shows that no obvious long-range trend is left in the final residual. The out-of-plane displacement due to the opening of a crack at the origin is shown in figure 10(f). The quality of the IDIC measurement is evaluated by measuring the normalized residual, i.e. the standard deviation of the remaining residual, normalized by the peakto-valley roughness of the original topographic image. In the present cases, even though the kinematic field was adjusted with very few parameters, the normalized residual n is very stable at 1.6%, a remarkably low value which gives confidence in the convergence of the procedure. The measured stress intensity factor values (using the elastic moduli for silica glass: Young modulus of 72GPa and a Poisson's ratio of 0.17) is K DIC = (0.39±0.04) MPa.m 1/2 , which is in excellent agreement with the macroscopic value of (0.39±0.02) MPa.m 1/2 estimated independently. Note the huge difference of length scale used in both estimates (millimeter vs nanometers). A second image series was tested in [START_REF] Han | Measuring nanoscale stress intensity factors with an atomic force microscope[END_REF] after zooming to 200×200 nm 2 images around the crack tip.

Although the residuals of 5% are slightly higher, they still do not show any trend out of a 10 nm distance from the crack tip, which represents the lateral resolution limit of the AFM related to the tip size. Moreover the locally estimated value of K DIC of (0.41±0.05) MPa.m 1/2 is still in excellent agreement with the macroscopic measurement.

3D elastic finite element simulation

The 3D finite element simulation used to represent the linear elastic stress and displacement fields of a realistic DCDC specimen with curved crack fronts is implemented by the finite element code The material's linear elastic response is defined by the Young's modulus E and the Poisson's ratio ν of silica glass as defined in section 3. Thanks to the symmetry of the geometry, we can limit the simulation to one eighth of the specimen by imposing the boundary conditions u x = 0 along the symmetry plan normal to 𝑒 ⃗ 𝑥 and u y = 0 along the symmetry plan normal to 𝑒 ⃗ 𝑦 on the uncracked ligament. The compressive stress σ is applied on the two opposite faces, without imposing any displacement constraints. We thus neglect the effects of friction at the platen/sample surfaces, but they will be negligible if the crack front remains at a sufficiently large distance w away from the end of the sample. The crack has a length a measured from the edge of the hole to the corner point of the crack front. The crack front is curved with a parabolic shape terminating with an adjustable angle α. The gap between the millimeter length scale of the external mechanical loading and the nanometer length scale of the asymptotic crack tip fields close to the corner point singularity requires an adapted mesh with an exponential densification of elements down to 0.01 nm close to the corner point singularity. The mesh is also refined close to the central hole.

To investigate the influence of the geometrical parameters on the corner singularity λ, a series of meshes was designed with twenty five values for the terminal angle α ranging from 6° to 17.5°. The rest of the geometry is kept constant, the external size and hole are as in our test samples, the crack length and loading were the same as for the tests with optical profilometer, in order to reproduce at best the macroscopic behavior of the out-of-plane displacement field. On the other hand, the local asymptotic behavior at the corner point should be independent of the crack length.

We already presented in section 4 (figure 9) the good performance of the 3D simulation against the out-of-plane measurement of the optical profilometer on a 1 mm large image. We will focus here on the description of the corner point singularity in order for the 3D FE simulation to bridge the two scales of experimental observation.

In order to extract the corner point singularity λ, three different indicators are investigated: these consist of the power law fit of the two main components u x and u y of the mode I displacement field and of the 2D stress intensity factor profile K(z) when approaching the corner point. For both components of the displacement fields, the fit is done at the free surface along the crack lips (x > 0, y = 0) in the distance range 1 nm < x < 1 µm from the tip, which according to [START_REF] Pallares | Crack opening profile in DCDC specimen[END_REF] is well included in the region of K-dominance (i.e. dominance of the Irwin square root singularity in a 2D analysis) of the DCDC. The stress intensity factor K(z) is evaluated along the crack front using the J integral estimators included in the code and then fitting a power law exponent according to equation ( 4). The obtained values of the corner singularity exponent λ are shown in figure 12(left) as a function of the terminal angle α. We observe an overall good agreement between the estimates obtained using u x , u y and K(z). By applying the conjecture of a corner singularity exponent λ = 1/2 expected for a steady state crack propagation, the first three indicators would predict a terminal angle α = 7±1°, which is intermediate between the theoretical prediction of 5.1° according to Bažant and Essentoro (1979) and our measured value of 8.5±1° (cf. section 4.1). The agreement is quite satisfactory. Some more precise results may be achieved by refining the mesh along the crack front within the material bulk, but the reach of such a precision is out of the scope of the present investigation aimed at understanding the appropriate bridging over length scales. ). The residuals become larger than 10% only when r > 2000 nm. This remarkable agreement is a further validation of the sound multi-scale reconstruction of the 3D mechanics of the DCDC specimen from the macroscopic scale down to the asymptotic corner singularity field that dominates the in-situ AFM images.

Discussion and conclusion

The present multi-scale investigation offers a consistent mechanical view of the steady state subcritical fracture propagation in a DCDC specimen. The 3D analysis of the crack tip field is shown to be an unavoidable step to link the macroscopic features of the loading and the nanoscale asymptotic crack tip field as measured at the accessible free surface of the sample. The macroscopic loading is transferred to the crack front singular fields through the structural response of the DCDC sample which is essentially captured by a 2D analysis at large to intermediate scales. When approaching the crack front at distances comparable to the sample thickness w, the details of its non straight geometry become dominant, yet locally we can still approximate the neighborhood of the crack front by a 2D fracture field. However, when approaching the incidence of the crack front onto the free surface, the 2D symmetry is essentially broken and a different self-similar corner point singularity emerges with an intrinsic 3D structure. This allows a range of possible local corner singularities, yet it was argued that only the exponent λ = 1/2 is compatible with a steady state propagation of the crack front, inducing a prediction of the terminal angle α as only related to the Poisson's ratio, together with a prescription of r 1/2 fields also for the out-of-plane components of displacement (a result that is strongly different from the 2D predictions in either plane stress or plane strain conditions). Our multiscale experimental and numerical analysis provides a consistent validation of this global picture, and the ultimate proof is that the local stress intensity factor obtained through the DIC analysis of submicrometric sized AFM images close to the crack tip corner point provides a robust and consistent estimation of the macroscopically measured stress intensity factor under different propagation conditions. The key of this success is the quality of the steady state crack propagation. By enforcing several hours of equilibrated slow crack growth in a very stable sample such as DCDC, the crack front progressively finds a shape that remains invariant throughout the entire propagation, equilibrated through all scales and under a very pure mode I loading (thanks to the principle of local symmetry). This allows both to relate the macroscopic and microscopic loading very accurately, and to insure that the crack tip displacement field in a series of subsequent AFM images is substantially identical. This mechanical information is the key to separate this nanometric out-of-plane displacement field from the nanometric surface roughness which has the same order of magnitude, and which generally prevents quantitative evaluation of small displacement fields on AFM images. We underline that although AFM nanoscale measurements have generally a poor metrological content due to the interplay of drifts, tip/sample interactions and imaging feedback details, the use of DIC to extract displacement fields from very similar images can provide very accurate and metrological results, especially when the singular nature of the crack tip fields under study allows a clear separation from the more regular AFM drifts. A second key of this success is the incredible mechanical properties of silicate glasses, which were proved to allow the use of continuum mechanics and linear elasticity down to 10 nm scales from the crack tip, which is by itself an amazing result. Full 3D elastic solutions were used here as a first reasonable guess to establish a connection from the macroscopic scale down to the nanometric neighborhood of the corner point singularity. However, the extremely low values of the residual fields measured by DIC, and especially the absence of any observable trend in the residual fields out of a 10 nm region from the crack tip become a striking evidence of the appropriateness of these elastic solutions to describe the crack tip fields down to the extreme lateral resolution of AFM imaging. This set of measurements constitutes a clear and sound solution to the long debate on the length scales of the inelastic processes acting at the crack tip of glasses during stress-corrosion slow crack propagation [START_REF] Wiederhorn | Griffith cracks at the nanoscale[END_REF].

What about the reported AFM observations suggesting crack tip plasticity at 100 nm scales? As above discussed the crack tip topography as studied by [START_REF] Guilloteau | The direct observation of the core region of a propagating fracture crack in glass[END_REF] and Célarié et al (2003) call for proper 3D corner point solutions to be quantitatively interpreted, and these early experimental results should be revisited within such a framework. [START_REF] Fett | Finite element analysis of a crack tip in silicate glass: No evidence for a plastic zone[END_REF] showed that the apparent nanoscale cavities observed by Celarié et al. (2003) (cf. figure 2 left) could originate from the superposition of the out-of-plane crack tip elastic depression and of the surface roughness which has the same order of magnitude. In a previous investigation [START_REF] Lechenault | Effects of finite probe size on self-affine roughness measurements[END_REF] we also showed that the 20-100 nm cutoff length observed in the correlation functions of the nanoscale roughness of the fracture surfaces can be generated by a subtle non-linear filtering induced by the geometrical interaction of the nanoscale sized AFM tip (subject to wear) and the self-affine nanoscale roughness. These subtle artifacts should be used as an important lesson concerning the danger of misinterpreting very resolved nanoscale investigations. The multi-scale mechanical consistency of the reported study is a precious safeguard against this risk.

Is this the end of the story concerning the active debate on plasticity and damage around the crack tip in glasses? We believe that the question is settled concerning the 100 nm scale, but our present analysis cannot resolve features below the 10 nm scale which is the limit of lateral resolution of AFM in-situ investigations (and even in post-mortem fractographic investigations when looking for a cutoff in the lateral lengths). And indeed when considering the separation of two atoms, nonlinearities of interactions are evidently involved, resulting at least in non-linear elasticity, and most probably in plasticity with irreversible reorganization of the amorphous atomic arrangement.

Moreover, when examining more closely the literature on the evidences of water penetration at the crack tip, we find several experimental evidences of water penetration in regions of a few nanometers (yet no more than 10 nm). These are generally post-mortem investigations of the water concentration depth profile on crack surfaces in silicate glasses performed by resonant nuclear reaction [START_REF] Lanford | Hydration of soda-lime glass[END_REF], optical reflectivity [START_REF] Stavrinidis | Crack healing in glass[END_REF]) and more recently by small angle neutron reflectivity [START_REF] Lechenault | Effects of finite probe size on self-affine roughness measurements[END_REF]. These evidences are very strong, but as in all post-mortem investigations, they do not provide details on the moment where water really penetrated and on the mechanisms of coupling with the stress-corrosion crack propagation. A more recent AFM post-mortem investigation by [START_REF] Wiederhorn | Effect of water penetration on the strength and toughness of silica glass[END_REF] has shown that a possible mechanical coupling between water penetration in the crack tip region and crack propagation in silica glass could come from the induced local swelling of the glass and the consequent build up of local compressive stresses, which can have an effect of shielding crack tip stresses. This mechanism is analogous to the well studied coupling between ion exchange leaching in alkali-silicate glasses and the crack tip stresses [START_REF] Fett | Interpretation of effects at the static fatigue limit of soda-lime-silicate glass[END_REF], which results in the presence of the stress-corrosion threshold of propagation described in figure 1 (right). It is noteworthy that, even in the more highly corrosive context of leachable glasses, the volume affected by leaching and compressive stresses is limited to a region of size well below 10 nm from the crack tip [START_REF] Wiederhorn | Griffith cracks at the nanoscale[END_REF][START_REF] Célarié | Stress-enhanced ion diffusion at the vicinity of a crack tip as evidenced by atomic force microscopy in silicate glasses[END_REF].

In order to discuss the final implications of the present analysis on the understanding of the stresscorrosion mechanisms we recall some recently performed complementary observations thanks to our in-situ AFM investigation technique. By using a complementary AFM imaging technique, called phase imaging, we showed that the crack tip cavity is so sharp that it is filled with a spontaneous water condensation from the ambient moist atmosphere in a submicrometric neighborhood of the crack tip [START_REF] Grimaldi | The crack tip : a nanolab for studying confined liquids[END_REF]. While this condensate was shown to be close to pure water at condensation equilibrium in pure silica glass [START_REF] Pallares | Quantitative analysis of crack closure driven by Laplace pressure in silica glass[END_REF], complementary observations on alkali-silicate-glasses [START_REF] Célarié | Stress-enhanced ion diffusion at the vicinity of a crack tip as evidenced by atomic force microscopy in silicate glasses[END_REF] have shown that the chemical composition of this condensate keeps evolving in time due to the leaching of sodium out from the glass. These observations are of the greatest importance to the understanding of the stress-corrosion kinetics under ordinary moist atmosphere since this condensate constitutes the effective local environmental condition at the crack tip region where the stress-corrosion occurs.

Figure 3 .

 3 Figure 3. Left: Sketch of the DCDC geometry. Right: Side view of the DCDC sample, putting into

Figure 4 .

 4 Figure 4. Left: AFM measurement of the out of plane displacement field in a section crossing the

Figure 5 .

 5 Figure 5. The DCDC test sample is represented on the left along with the regions corresponding to

Figure 7 .

 7 Figure 7. Experimental setup for in-situ AFM imaging of the slow crack propagation in a DCDC

  , although the theoretical values are somehow lower (respectivelyα = 5.1° for silica glass and 7.3° for LAS glass,

Figure 8 .

 8 Figure 8. Experimental in-situ image of the crack front at the free surface (z=0) in a DCDC fused-

.Figure 9 .

 9 Figure 9. Comparison between (a) finite element simulation and (b) optical profilometry

Figure 10

 10 Figure 10. (a) and (b) are respectively the reference and deformed AFM height images for the IDIC

  is developed by CEA-Saclay, France. Reference web page: http://www-cast3m.cea.fr/cast3m/index.jsp . The mesh is constituted of linear elastic isotropic eight nodes elements. The details of the sample loading configuration and the mesh geometry are shown in figure 11.

Figure 11 .

 11 Figure 11. 3D mesh for the finite element simulation of the DCDC sample. Due to symmetry, only 1/8 th of the specimen is meshed. The crack front is curved to a parabolic front with terminal angle α

Figure 12 .

 12 Figure 12. Finite element calculations: Left: Representation of the corner singularity exponent λ as

  in the neighborhood of the corner point. According toDimitrov et al.

				2 1 , then the SIF /	K	(z	)	will tend
	to infinity for	z	→	0

(2006)

, if the real part of the corner singularity λ is smaller than

Acknowledgements

We wish to thank S. Wiederhorn, D. Bonamy, E. Bouchaud, K. Ravi-Chandar, T. Fett, J.P. Guin, and C. Marlière for fruitful scientific discussions, I. Serre and A. Van Gorp for helping us using their optical profilometer, S. Chapuliot and C. Kumar for helping us in the design of the finite element mesh, B. Rufflé for the Brillouin measurements of the Poisson's ratios. All co-authors of this work wish to acknowledge the financial support of ANR Grant "Corcosil" No. ANR -07-BLAN-0261-02.

We can conclude our discussion by stating that the combination of the investigations of crack tip stresses along with the understanding of the local environmental condition is likely to offer an undisputable key to a thorough understanding of the role of glass composition on the measured phenomenological parameters of the stress-corrosion curves [START_REF] Wiederhorn | Griffith cracks at the nanoscale[END_REF]. Another major perspective comes from the recent outstanding developments in the performances of molecular dynamics towards the simulation of stress-corrosion reactions on space and time scales that could soon approach from below the limits of the measurable range accessible by our in-situ AFM experimental investigations [START_REF] Mischler | Water adsorption on amorphous silica surfaces: a Car-Parrinello simulation study[END_REF][START_REF] Du | Molecular dynamics simulation of the structure and hydroxylation of silica glass surfaces[END_REF]Cormack 2005, Kermode at al. 2008) thereby opening a formidable opportunity for a novel experimental/modeling dialog.