Nicolas Moro

Karine Heydemann

Emmanuelle Encrenaz

Bruno Robisson

Formal verification of a software countermeasure against instruction skip attacks

. As a consequence, this fault model is a realistic threat for an embedded program.

. On the contrary, performing faults on two instructions separated by a few clock cycles is significantly harder [6] while still possible. Indeed, it requires a much more costly fault injection equipment and very high synchronization capabilities. It is then not yet considered as a realistic threat.

The securing approach proposed in this paper uses an instruction-scale temporal redundancy to ensure a fault-tolerant execution of an embedded program. It is based on the statement that performing two faults on two instructions separated by few clock cycles is hardly feasible. A fault-tolerant replacement sequence for most of the instructions of the whole Thumb-2 instruction set has been designed. We also show how to formally prove the fault tolerance of replacement sequences by using a model-checking tool.

By using such a fine-grained redundancy scheme, it is then possible to strengthen most assembly programs against fault attacks without any specific knowledge about the program itself. In the experimental results, we evaluate the overhead induced by fault tolerance and show that it can be reduced by only applying this countermeasure scheme to the sensitive parts of an implementation.

The rest of this paper is organized as follows. Section 2 introduces our fault model and gives details about some related research papers. Section 3 introduces our countermeasure scheme and details our replacement sequences. Section 4 explains the approach we use for the formal verification. Finally, section 5 evaluates the efficiency of our countermeasure scheme on several implementations.

Related works and fault model

This section is dedicated to related works. First, fault models are discussed in section 2.1. Countermeasure schemes that have previously been proposed are addressed in section 2.2. Section 2.3 presents some related research papers on formal verification.

Introduction

Physical attacks were introduced in the late 1990s as a new way to break cryptosystems. Unlike classical cryptanalysis, they use some weaknesses in the cryptosystems' implementations as a way to break them. Among them, faults attacks were introduced in 1997 by Boneh et al. [START_REF] Boneh | On the importance of checking cryptographic protocols for faults[END_REF]. In this class of attacks, attackers try to modify a circuit's environment in order to change its behaviour or induce faults into its computations [START_REF] Bar-El | The Sorcerer's Apprentice Guide to Fault Attacks[END_REF][START_REF] Barenghi | Injection Technologies for Fault Attacks on Microprocessors[END_REF]. This attack principle was first introduced against cryptographic circuits but can be used against a larger set of embedded circuits. Many physical means can be used to induce such faults: laser shots [START_REF] Trichina | Multi Fault Laser Attacks on Protected CRT-RSA[END_REF], clock glitches [START_REF] Balasch | An In-depth and Black-box Characterization of the Effects of Clock Glitches on 8-bit MCUs[END_REF], chip underpowering [START_REF] Zussa | Investigation of timing constraints violation as a fault injection means[END_REF], temperature increase [START_REF] Skorobogatov | Local heating attacks on Flash memory devices[END_REF] or electromagnetic glitches [START_REF] Dehbaoui | Electromagnetic Transient Faults Injection on a Hardware and a Software Implementations of AES[END_REF].

Among fault attacks, three subclasses can be distinguished: differential fault analysis, safe error and algorithm modifications. Differential fault analysis (DFA) aims at retrieving some ciphering keys by comparing correct ciphertexts with ciphertexts obtained from a faulted encryption [START_REF] Boneh | On the importance of checking cryptographic protocols for faults[END_REF]. Safe-error attacks are based on the fact that a fault injection may have or not have an impact on the output [START_REF] Barenghi | Fault Injection Attacks on Cryptographic Devices: Theory, Practice, and Countermeasures[END_REF]. Finally, algorithm modifications target an embedded processor and aim at injecting faults into an embedded program's control flow [START_REF] Schmidt | A Practical Fault Attack on Square and Multiply[END_REF][START_REF] Balasch | An In-depth and Black-box Characterization of the Effects of Clock Glitches on 8-bit MCUs[END_REF].

Those attack schemes rely on an attacker's fault model which defines the set of faults an attacker can perform [START_REF] Barenghi | Fault Injection Attacks on Cryptographic Devices: Theory, Practice, and Countermeasures[END_REF]. As a consequence, countermeasure schemes must take this fault model aspect into account. On microcontrollers and embedded processors, the fault model in which an attacker can skip an assembly

The final publication is available at Springer via http://dx.doi.org/10.1007/s13389-014-0077-7

Fault model

On embedded processors, a fault model in which an attacker can skip an assembly instruction or equivalently replace it by a nop has been observed on several architectures and for several fault injection means [START_REF] Karaklajić | Hardware Designer's Guide to Fault Attacks[END_REF]. On a 8-bit AVR microcontroller, Schmidt et al. [START_REF] Schmidt | A Practical Fault Attack on Square and Multiply[END_REF] and Balasch et al. [START_REF] Balasch | An In-depth and Black-box Characterization of the Effects of Clock Glitches on 8-bit MCUs[END_REF] obtained instruction skip effects by using clock glitches. Dehbaoui et al. obtained the same kind of effects on another 8-bit AVR microcontroller by using electromagnetic glitches [START_REF] Dehbaoui | Electromagnetic Transient Faults Injection on a Hardware and a Software Implementations of AES[END_REF]. On a 32-bit ARM9 processor, Barenghi et al. obtained some instruction skip effects by using voltage glitches. On a more recent 32-bit ARM Cortex-M3 processor, Trichina et al. were able to perform instruction skips by using laser shots [START_REF] Trichina | Multi Fault Laser Attacks on Protected CRT-RSA[END_REF]. Moreover, this fault model has also been used as a basis for several cryptanalytic attacks [START_REF] Barenghi | Fault Injection Attacks on Cryptographic Devices: Theory, Practice, and Countermeasures[END_REF]. As a consequence, it is considered as a common fault model an attacker may be able to perform [START_REF] Karaklajić | Hardware Designer's Guide to Fault Attacks[END_REF].

A more generic fault model is the instruction replacement model, in which nop replacements correspond to one possible case. In some previous experiments on an ARM Cortex-M3 processor by using electromagnetic glitches, we have observed a corruption of the instructions binary encodings during the bus transfers [START_REF] Moro | Electromagnetic Fault Injection: Towards a Fault Model on a 32-bit Microcontroller[END_REF] leading to such instruction replacements. Actually, instruction skips correspond to specific cases of instruction replacements: replacing an instruction by another one that does not affect any useful register has the same effect as a nop replacement and so is equivalent to an instruction skip. Many injection means enable to perform instruction replacement attacks [START_REF] Moro | Electromagnetic Fault Injection: Towards a Fault Model on a 32-bit Microcontroller[END_REF][START_REF] Balasch | An In-depth and Black-box Characterization of the Effects of Clock Glitches on 8-bit MCUs[END_REF][START_REF] Barenghi | Injection Technologies for Fault Attacks on Microprocessors[END_REF]. Nevertheless, even with very accurate fault injection means, being able to precisely control an instruction replacement is a very tough task and, to the best of our knowledge, no practical attack based on such a fault model has been published yet.

As a conclusion, we consider in this paper the potentially harmful fault model in which an attacker is able to skip a single instruction.

Countermeasure schemes

Several countermeasures schemes have been defined to protect embedded processor architectures against specific fault models. At hardware level, many countermeasures have been proposed. As an example, Nguyen et al. [START_REF] Huu Nguyen | Low-cost recovery for the code integrity protection in secure embedded processors[END_REF] propose to use integrity checks to ensure that no instruction replacement took place.

Software-only countermeasure schemes, which aim at protecting the assembly code, are more flexible and avoid any modification of the hardware. Against fault attacks, the most common software fault detection approach relies on function-level temporal redundancy [START_REF] Bar-El | The Sorcerer's Apprentice Guide to Fault Attacks[END_REF]. For example, this principle applied to a cryptographic implementation can be achieved by calling twice the same encryption algorithm on the same input and then comparing the outputs. For encryption algorithms, an alternative way is to call the deciphering algorithm on the output of an encryption and to compare its output with the initial input. These approaches enable fault detection and involves doubling the execution time of the algorithm. Triplication approaches with voting enabling fault tolerance at the price of tripling the execution time of the whole algorithm have also been proposed [START_REF] Bar-El | The Sorcerer's Apprentice Guide to Fault Attacks[END_REF].

At algorithm level, in [START_REF] Medwed | A Generic Fault Countermeasure Providing Data and Program Flow Integrity[END_REF], Medwed et al. propose a generic approach based on the use of specific algebraic structures named AN+B codes. Their approach enables to protect both the control and data flow.

At assembly level, in [START_REF] Barenghi | Countermeasures against fault attacks on software implemented AES[END_REF], Barenghi et al. propose three countermeasure schemes based on instruction duplication, instruction triplication and parity checking. Their approach ensures a fault detection for a small number of instructions against instruction skip or transient data corruption fault models. Our scheme enables a fault tolerance only against the instruction skip fault model but for almost all the instructions of the considered instruction set. Moreover, our countermeasure scheme has been formally proven fault tolerant.

Formal verification of software countermeasures

Formal methods and formal verification tools have been used for cryptographic protocols' verification of to check that an implementation could meet the Common Criteria security specifications [START_REF] Chetali | Industrial use of formal methods for a high-level security evaluation[END_REF]. However, to the best of our knowledge, very few formal verification approaches to check the correctness of software countermeasure schemes against fault attacks have been proposed yet. One of the most significant contributions has been proposed by Christofi et al. [START_REF] Christofi | Formal verification of a CRT-RSA implementation against fault attacks[END_REF]. Their approach aims at performing a source code level verification of the effectiveness of a countermeasure scheme on a CRT-RSA implementation by using the Frama-C program analyzer. In this paper, we formally prove all our proposed countermeasures against an instruction skip fault model at assembly level. Another more recent contribution of a formal methodology at algorithm level has been proposed by Rauzy et al. [START_REF] Rauzy | A formal proof of countermeasures against fault injection attacks on CRT-RSA[END_REF]. In their scheme, an attacker can induce faults in the data flow of a target implementation described in a high-level language. This scheme enables them to detect unnecessary countermeasures or possible flaws on several CRT-RSA implementations.

Countermeasure scheme

The proposed countermeasure scheme aims at ensuring a fault-tolerant execution of an assembly code against instruction skip faults. The approach we propose relies on providing a formally proven fault-tolerant replacement sequence for almost all the assembly instructions of a whole instruction set. We chose the ARM Thumb-2 instruction set [START_REF] Arm | ARM Architecture Reference Manual -Thumb-2 Supplement[END_REF] since ARM is a widely used target architecture for embedded processors. In this section, we give some details about the considered instruction set and present some of the replacement sequences we have defined for each instruction. This fine-grained redundancy scheme enables to strengthen most assembly codes against fault attacks without any specific knowledge about them.

The Thumb-2 instruction set

Thumb-2 is actually the successor to both ARM and Thumb instruction sets. Thumb-2 is a variable-length instruction set since it extends the 16-bit Thumb instruction set with some 32-bit instructions. Thus, 16 and 32-bit instructions can be mixed in a single program to combine both code density and performance. However, unlike the ARM instruction set, most 32-bit Thumb-2 instruction do not support direct conditional execution. To achieve such a conditional execution, a new If-Then (it) instruction has been introduced. Moreover, some constant shifts can be applied to one operand of some instructions. Those shifts are : lsl (logical shift left), lsr (logical shift right), asr (arithmetic shift right), ror (rotate right) and rrx (rotate right one bit with extend). The Thumb-2 instruction set was first introduced with the ARMv6-T2 architecture and is now the standard instruction set for ARMv7 architectures.

Instruction classes

We have defined a fault-tolerant replacement sequence for each instruction and each encoding of the Thumb-2 instruction set. This instruction set contains 151 instructions, and each instruction has up to four different encodings. For many instructions, the replacement sequence is very simple. However, this sequence can become much more complex for some specific instructions. According to the replacement sequences found, the instructions in the Thumb-2 instruction set can be divided into three classes. Every class is associated to one kind of replacement sequence. These three classes are summarized in Table 1.

The first class is composed of idempotent instructions which only need to be duplicated to provide fault tolerance. The second class gathers the instructions that are not idempotent but can be replaced by an equivalent sequence of idempotent instructions. The third class gathers some specific instructions that cannot easily be replaced by a list of idempotent instructions but for which a specific replacement sequence is possible. This last class also contains the instructions for which no replacement sequence that ensures fault tolerance and correct execution in any case can be provided. The solution for these instructions is either to avoid the compiler to use them or to use a fault detection approach. The following section gives more details about those classes. Moreover, it provides some examples of replacement sequences for every class. 3.3 Individual instruction replacement sequences

Idempotent instructions

Idempotent instructions are the instructions that have the same effect when executed once or several times. If all the source operands are different from the destination operands, and if the value written into the destination operands does not depend on the instruction's location in the code, then the instruction is said to be idempotent. For such instructions, the countermeasure consists in a simple instruction duplication.

The overhead for such a duplication is twofold: an overhead which equals the instruction size in terms of code size and a performance overhead that is equal to the execution time of the instruction. Table 2 gives some examples of idempotent instructions and their associated replacement sequence.

Separable instructions

Listing 1: Replacement sequence for the non idempotent add r1, r1, r3 instruction 1

; we assume rx is an available register 2 mov rx , r 1 3 mov rx , r 1 4 add r1 , rx , r 3 5 add r1 , rx , r 3

In the considered instruction set, some instructions are not idempotent but can be rewritten by a sequence of idempotent instructions whose execution gives the same result. Once this rewritting is performed, each idempotent instruction of the replacement sequence can then be duplicated. This class gathers the instructions whose destination register is also a source register. To replace these instructions by a sequence of idempotent instructions, some extra registers have to be used. These registers have to be available at this location in the code: any dead register can be used1 . If no dead register is available, the stack can be used to temporarily store the value in a register. Simple separable instructions Listing 1 shows the replacement sequence for an add r1, r1, r3 instruction. For this class of instructions, the overhead cost brought by our countermeasure scheme depends on the instruction to replace. There is an overhead cost in code size, performance and register pressure (since the replacement sequence needs some extra registers). For the add r1, r1, r3 instruction example, one extra register is needed. Moreover, 4 instructions are required instead of 1 and the overhead cost in terms of code size is between 6 and 10 bytes (depending on the encoding used for the initial and the replacement instructions).

Stack manipulation instructions Some memory access instructions can update the address register before or after (stmdb2 /ldmia3 ) a memory access. As a consequence, this address register is both a source and a destination register for such an instruction. This is notably the case of the stack manipulation instructions (push and pop). These instructions respectively write or read on the stack and decrement or increment the stack pointer. Such instructions can be separated into a sequence of instructions that only perform one operation at a time, either a memory access or an address register update. The push instruction can be decomposed into instructions that first write the register to save on the stack and then decrement the stack pointer. As decrementing the stack pointer implies reading and writing the same register, this operation is decomposed into two steps in order to get a sequence of idempotent instructions. Such a replacement sequence for the push instruction is detailed on Listing 2. This replacement requires 1 extra register and has a code size and performance overhead of 5 instructions. umlal instruction The umlal instruction multiplies two source registers and then adds the content of the concatenation of the two 32-bit destination registers. The final result is written into two 32-bit destination registers. As a consequence, this instruction has registers that are both source and destination. However, it can be decomposed. First, a multiply instruction whose result is a 64-bit value can be performed. Then the 64-bit addition has to be decomposed into several instructions. This requires to propagate the carry set by adding the 32 least significant bits (by using an adds instruction) to the addition of the 32 most significant bits by using an adc instruction. However the adds instruction sets the flags whereas the umlal does not: this sequence of instructions is not strictly equivalent to the umlal instruction and may be wrong if the flags are used after the umlal instruction without being set. As a consequence, it is necessary to save the flags before the sequence and restore them afterwards. Instructions with a constant shift As mentioned in Sec. 3.1, several constant shifts can be applied to one source operand of some instructions. Among them, the rrx shift rotates all the bits of the shifted register to the right by 1 and uses the carry to set the most significant bit. The carry is read by a rrx operation. Thus, if the initial instruction also writes the flags, it has to be decomposed. An example of replacement sequence for a subs r1,r2,r3,rrx instruction is provided in Listing 4.

Listing 4: Replacement sequence for a subs r1, r2, r3, rrx instruction

Specific instructions

Some instructions cannot easily be replaced by a list of idempotent instructions. These instructions can still be decomposed into an equivalent sequence of instructions that can be duplicated to enforce a robust execution. There are also some instructions for which no fault-tolerant countermeasure in any case can be found. Some of them can still be replaced by a fault-tolerant sequence under some constraints. In this section, we give details and provide some examples for both kinds of such specific instructions.

bl subroutine call instruction The subroutine call instruction (bl) performs a jump and writes the return address into the link register (r14). Duplicating a bl instruction would induce two subroutine calls if no attack is performed. A solution is to explicitly put the return address into the link register and then perform an unconditional jump. As the Thumb execution mode requires the last bit of an instruction address to be set, this bit must be set before the unconditional jump to the subroutine code, as shown on Listing 5. Instructions that both read and write the flags Instructions that read and write the flags cannot easily be replaced by a fault-tolerant sequence of instructions. For example, the adsc instruction performs an addition between two source operands (two registers or one register and an immediate value) and the carry flag. The result is written into a destination register and the flags (carry, negative, overflow and zero) are updated. Duplicating such an instruction is not correct since the second adcs would use the carry set by the first adcs instruction instead of the initial carry value. If the flags are alive4 after the adcs instruction, then no simple replacement sequence seems possible, the code has to be modified. Otherwise, if the flags are not alive after the adcs instruction, a replacement sequence exists. Such a sequence consists in saving the flags values before the first adcs instruction and restoring these values before the second adcs instruction. This replacement sequence is illustrated in Listing 6.

Listing 6: Replacement sequence for a adcs r1, r2, r3 instruction it blocks Thumb-2 provides conditional execution of instructions through it blocks. An it instruction specifies a condition and up to the 4 following instructions can be conditionally executed according to this condition or its inverse. it blocks correspond to if-then or if-then-else higher-level constructions and are useful when the branches of a conditional statement are composed of a limited number of instructions. Listing 7 gives an example of such an it block. The simplest solution for such blocks is to first transform the it block into an equivalent classical if-then-else structure such as the one presented on Listing 8 and then apply the countermeasure scheme to each instruction, as illustrated on Listing 9. Other replacement sequence for it blocks We have also designed a specific replacement sequence for it blocks but this replacement has some limitations and can quickly become more costly than its equivalent form with an if-then-else structure. Listing 7 gives an example of such an it block. If the condition NE holds, (i.e. if the Z flag is set), then the two following instructions (addne and eorne) are executed. Otherwise, the last two instructions (subeq and moveq) are executed. The whole it block needs to be considered in order to secure it. The solution we propose is to first apply our countermeasure scheme to every instruction of the it block. Every instruction of a replacement sequence first keeps the same condition as the initial instruction. The first it instruction is then duplicated. The second it instructions specifies one instruction less than the first one. Moreover, both it instructions are to be updated depending on the instructions that result of the replacement sequence of the instuctions of the initial it block. This step is presented in Listing 10. The second step consists in adding some it instructions, since it blocks cannot contain more than 4 instructions, as illustrated in Listing 11. Finally, the conditions set in the it instructions need to be updated to match with the instructions of the it block they define. Listing 12 shows the secure code corresponding to the it block code example given in Listing 7.

Listing 10: First step for replacement of the it block given in Listing 7 Note that an it instruction should not appear in an it block. Thus, in case of a fault targeting one of the duplicated it instructions, the code behaves as if there was only one it instruction. Otherwise, the second it instruction is executed in the it block defined by the first it instruction. The second it instruction has actually no effect and is considered as a nop. However, some compilers may not accept such a construction. In this case, we have to use traditional conditional sequences for if-then or if-then-else constructions and apply our countermeasure scheme to each individual instruction of the resulting code as presented in Section 3.3.3. Moreover, transforming first the it block into a classical if-then-else structure and then applying the countermeasure scheme may induce a smaller overhead cost. Such a construction has been previously presented in Listings 8 and 9.

Other specific instructions For some very specific instructions, defining a replacement sequence cannot really be done. Those specific instructions include the group of instructions for coprocessors (mcr, lcr, ...) or the instructions for synchronization with external systems (sev, yield, ...).

Summary of the defined instruction classes

To sum up, an overview of the defined instruction classes is shown on Table 3. This table shows the different types of instructions that are included in every class and provides a few examples for each type of instructions.

Formal verification of correctness and fault tolerance

In this section, we present how we formally prove the fault tolerance specification for the countermeasure replacement sequences presented in Section 3. Details about the models used for the verification approach are presented in Section 4.1 and verification examples for some replacement sequences are presented in Section 4.2.

State machine model and specification to prove

A program acts as the application of transformations of the values stored in the set of registers or in memory. Each instruction of the program acts like a function whose input is a configuration of registers and memory and produces a new configuration. The program can then be represented as a transition system whose states are configurations of registers and memory, and any transition mimics the state transformation induced by an individual instruction execution.

Individual instruction model

Instead of proving the fault tolerance for a complete program, our model checking approach consists in proving the fault tolerance for each replacement sequence proposed in our countermeasure scheme. Indeed, # input r2, r3, flags # output r1, flags pc_init : add r1, r2, r3 pc_final : next_instruction it is sufficient to certify that the output state (registers and memory configuration) after the replacement sequence execution (with or without a fault injection) is equivalent to the normal output state after the initial instruction execution. As this output state is also the input state for the following instruction, using such a verification approach certifies that the next instruction will start from the right configuration. Moreover, this enables to use model checking while avoiding state-explosion problem.

pc init, pc f inal ∈ L (R, F ) is the current state (R ′ , F ′ ) is the next state t : (R, F ) → (R ′ , F ′ ) with R.pc = pc init R ′ .r1 = R.r1 + R.r2 R ′ .pc = pc f inal

State machine model

As explained before, we can model the execution of a sequence of instructions by a transition system T S. We define this transition system as T S = {S, T, S 0 , S f , L}. S is the set of states, T the set of transitions T : S → S, S 0 and S f are the subsets of S which respectively gather the initial states and final states. The final states from S f are absorbing states. A state from S is defined by the value of the different registers (from the set of registers R which includes the program counter) and processor flags (from the set of flags F ). Each transition from T is defined by the effect of an instruction on the registers and processor flags. L is a set of labels which correspond to the values the program counter can take. An example of such a transition system for the add r1, r2, r3 instruction is shown in Fig. 1. To prove that a countermeasure for an instruction i is robust against a fault, we build two transition systems: one for the initial instruction m(i) and another one for its strengthened replacement sequence m cm (i).

Fault model In any transition system m cm (i), one instruction skip fault may occur. An instruction skip fault is modeled by a transition from a state to any following one. Such a faulty transition only modifies the program counter. We add to the whole transition system a skip instruction faulty transition between every pair of adjacent states. As we assume that only one skip instruction fault injection may occur, every fault transition is guarded with a boolean which identifies that a fault has already occurred.

Flags and registers models

The set of registers is composed of some general-purpose registers (r0-r12), a stack pointer (r13), a link register (r14) and a program counter (r15). The 5 processor flags are: C (carry), N (negative), Z (zero), V (overflow), Q (saturation). These flags can be set by some instructions and are used by several others. The conditional jumps are among the instructions that use those flags. Each flag is modeled as a 1-bit register. All the other registers are modeled as 4-bit registers. This width is sufficient to model the arithmetic and logic operations as well as the flags computations and enables to keep a reasonable complexity for the model checker. Moreover, modeling all the registers is not necessary since an instruction only reads a subset of the registers and writes on the destination registers. Besides, according to our fault model, the registers that are not modified by an instruction cannot be modified by a fault. Thus, for a given m(i) or m cm (i), the set of registers R is only composed of the subset of registers that are manipulated by i or its replacement sequence cm(i). Extra registers used in cm(i) are supposed to be dead after the occurrence of the instruction i in the initial program.

Memory model Since in our fault model we assume the memory cannot be corrupted, modeling the memory is not relevant. To ensure that a write to the memory took place, we only need to ensure that the corresponding instruction has been executed at least once. As explained later in this section, we add a counter variable to m(i) and m cm (i) in order to achieve this. For the loads from the memory, we use symbolic values as the values cannot be corrupted and they also do not matter since the formal verification we use consists in checking the equivalence for any value. The important point is to give the same symbolic Figure 3: Model for an idempotent instance of the str instruction and its countermeasure value to any loads at a given address for the transition system m(i) (when i is a load instruction) and for m cm (i). This is achieved by adding an input variable for each memory address that is read by i and cm(i) to both transition systems. These variables contain the needed symbolic values.

Vis model checker

We have chosen to use the Vis model checker 5 to prove the fault tolerance of our countermeasure scheme. This tool can take as input a transition system described with a subset of the Verilog hardware description language. Using Verilog is convenient to model transition systems which manipulate registers and bit vectors. The Vis model checker supports symbolic model checking techniques which enable to perform the proof in a symbolic way without having to enumerate each value for the registers. In [START_REF] Fox | A trustworthy monadic formalization of the armv7 instruction set architecture[END_REF], Fox et al. proposed a model of the ARMv7 architecture based on the HOL4 interactive theorem prover. However, this tool makes some proofs that are much more complex than the ones we need for the equivalence checking of finite models (the formal approach we propose to use in this paper) and the verification of rather simple properties on those models.

Specification to prove

To prove the equivalence of the output of an instruction and its replacement sequence, we prove the validity of logic formulas on the two models. To perform such a verification, we use a specific construction in which the two transition systems m(i) and m cm (i) have the same values for the set of registers R (except for the program counter), the set of flags F and the symbolic values (for the memory loads) in their initial states. Such constructions are presented in Fig. 2, 3 and 4. We then need to prove that m(i) and m cm (i) always reach a final absorbing state. Moreover, we also need to prove that, when m(i) and m cm (i) reach a final state, the values for the set of alive registers R ′ (except for the program counter) and flags F ′ are similar. Such properties to check are expressed with the CTL temporal logic. The left part of Fig. 2 shows the state machine corresponding to the transition system for a non-idempotent add r1,r3 instruction. The program counter is updated and depending on the instruction, the registers or the flags may be updated too. The replacement sequence uses a dead register r2 and two extra mov instructions to write the result to the destination register r1. Its transition system is modeled by the state machine on the right part of Fig. 2. To prove that the replacement sequence is fault tolerant against a possible instruction skip, both state machines are fed with the same values for the source registers (r1 and r3) and flags. Then, the validity of three CTL logic formulas has been checked with the Vis model checker. P1 and P2 express the fact that in both state machines any path from an initial state goes to a final state. P3 expresses the fact that in this final state, for all possible values in the source registers, the values in r1 and the flags are identical in m(i) and m cm (i). Fig. 3 presents the transition systems for an idempotent memory write, namely an str r3, [r1, r2] instruction, and its replacement sequence. In this case, as the instruction writes the content of r3 to the memory at the address r1+r2, and as we consider an instruction skip fault model, no proof is needed on the value hold by the registers. We only need to make sure that at least one str instruction has been executed. A counter variable is added to the definition of a state. This counter is set to 0 and is incremented by any transition which corresponds to a str instruction. P1 and P2 express the fact that any path goes to the last state. P3 expresses the fact that the number of writes made by the replacement sequence greater or equal to the number of writes made by the initial instruction (which is equal to 1).

Specific instructions

Subroutine call: the bl instruction Figure 4 shows the state machines for the bl instruction and its replacement sequence. In both corresponding transition systems, we have added a label @f ct to model the target of the subroutine call. Transitions from a state in which P C = @f ct assign the link register to the PC. Such a transition models the return of the function and also increments a counter. Then, properties P1 and P2 to be checked by the model checker express that any path from an initial state goes to a final state. Property P3 expresses the fact that in a final state the number of calls to the function (the counter values) are the same. Validity of property P3 ensures that the function has been executed only once while validity of P1 and P2 ensures that the control flow comes back to the calling function.

Instructions that read and write the flags For the adcs instruction and its replacement sequence, as presented in Listing 6, the CTL properties are the same as the ones that were used for the add instruction. However, the property that deals with the equality of the destination register and the flags is not valid if a fault targets the last adcs instruction. Relaxing the constraint on flags equality (expressed as LIGHT RESULT) makes this property valid as shown with the output of the Vis model checker in Fig. 5. To sum up, this countermeasure can only be used if the flags are not used before being set again after the adcs instruction.

Verification statistics

The verification process is based on modeling the arithmetic and logic operation performed by instructions and modeling their effects on the flags. Thus, the minimal size required to model the registers is the minimal one that enables to precisely model the effects on the flags. As a consequence, modeling registers with a 4-bit size is relevant. However, the verification process leads to the same results (passed or failed) for registers modeled with a 4-bit length or for larger sizes. Moreover, the verification process duration and the size of the transition system are related to the size of the registers. The verification process required less than 1 second per instruction with a 4-bit register size for all the instructions, and less than 1 minute for almost all the instructions with a 16-bit register size. As an example, it needed 29 hours to complete for the most expensive umlal instruction with a 16-bit register size. Moreover, the model checker we used could not build the internal representation or carry out the verification for registers larger than 24 bits for all the instructions.

Application to several implementations

In this section, we applied our countermeasure scheme to several codes. Two of them are implementations of the AES-128 symmetric encryption algorithm, and the last one is an implementation of the SHA-0 algorithm. We developed the first AES implementation, in which every round key is calculated before the associated AddRoundKey operation. The second AES implementation and the SHA-0 implementation come from the MiBench embedded benchmark suite [START_REF] Guthaus | MiBench: A free, commercially representative embedded benchmark suite[END_REF]. We provide an estimation of the overhead cost brought by our countermeasure scheme for those three implementations and perform an exhaustive instruction skip simulation on an ARM Cortex-M3 microcontroller to confirm the effectiveness of our approach. The chosen target is an up-to-date 32-bit microcontroller based on the ARM Cortex-M3 processor [START_REF] Yiu | The Definitive Guide To The ARM Cortex-M3[END_REF]. This microcontroller uses an ARMv7-M Harvard architecture and runs the Thumb-2 instruction set [START_REF] Arm | ARM Architecture Reference Manual -Thumb-2 Supplement[END_REF].

Estimation of the overhead cost

The overhead cost in terms of clock cycles and code size for the three implementations that use our countermeasure scheme is shown on the first three lines of Table 4. For those implementations, the whole code has been strengthened with our methodology and both overhead costs are high.

Another approach consists in applying our countermeasure to a specific chosen part of the algorithm. As an example, in terms of cryptanalysis, fault injections are supposed to be harder to exploit if the fault does not target the last two rounds. Thus, as shown on the fourth line of Table 4, it could be possible to reduce the overhead in terms of clock cycles by applying our countermeasure scheme to the last two rounds only. This last scenario is just a possible example of optimization and some cryptanalysis attacks may still exist. Nevertheless, it aims at showing that the overhead costs can be significantly reduced with a good knowledge about the algorithm to strengthen and about some possible vulnerabilities in its assembly code. It is important to mention that all the instructions from the tested codes could be replaced by using our countermeasure scheme. Moreover enough dead registers were always available for all the replacement sequences that required some extra registers.

To sum up, the overhead cost brought by our countermeasure scheme is high, but remains comparable to the one brought by classical algorithm triplication or other software approaches for fault tolerance. However, unlike such classical algorithm duplication or triplication approaches, our countermeasure scheme should be resistant to double fault attacks in a time interval longer than a few clock cycles.

Conclusion

In this paper, we have presented a countermeasure scheme that enables to strengthen an embedded program and make it tolerant to instruction skip faults. In our countermeasure scheme, we have built a fault-tolerant replacement sequence for almost all the instructions of the whole Thumb-2 instruction set. The instructions can be divided into three classes, which all have their dedicated replacement sequences. We have also provided a formal verification process in order to guarantee the correctness and the fault tolerance of our replacement sequences for each class of instructions.

Finally, we do not claim our scheme enables a full protection against fault attacks. Nevertheless, such an approach enables to add a reasonably good security level to an embedded program, without requiring any extra hardware countermeasure and any specific knowledge about the embedded program. The overhead cost brought by using such a countermeasure is comparable to the extra cost brought by using classical algorithmlevel temporal redundancy approaches and can be reduced with a more accurate knowledge about the sensitive parts that should be protected. Moreover, using a very fine-grained redundancy at the instruction scale makes the multiple fault attacks less practical with a reasonable cost equipment.

Listing 2 : 1 ; 2 ;

 212 Replacement sequence for the push {r1, r2, r3, lr} instruction the push {} instructi o n is equivalent to the stmdb sp ! ,{} instructi o n 3 stmdb sp , { r1 , r2 , r3 , l r } 4 stmdb sp , { r1 , r2 , r3 , l r }

1 rrx ry , r 3 2 rrx ry , r 3 3

 123 subs r1 , r2 , r y 4 subs r1 , r2 , r y

Listing 5 : 5 b 6 b

 556 Replacement sequence for a bl instruction 1 adr ry ,< r e t u r n l a b e l > 2 adr ry ,< r e t u r n l a b e l > 3 add l r , ry , #1 ; Thumb mode requires the 4 add l r , ry , #1 ; last bit of lr to be set <f u n c t i o n > <f u n c t i o n > 7 r e t u r n l a b e l

1 mrs rx , a p s r ; save flags 2 mrs rx , a p s r 3 adcs r1 , r2 , r 3 4 msr a p s r , r x ; restore flags 5 msr a p s r , r x 6 adcs

 123456 r1 , r2 , r 3

Listing 7 : 1 i t t e NE 2 addne r1 , r2 , #10 3 eorne r3 , r5 , r 1 4 moveq r3 , # 10 Listing 8 : 1 b . eq e l s e 2 add r1 , r2 , #10 3 eor r3 , r5 , r 1 4 b c o n t i n u a t i o n 5 e l s e 6 mov r3 , #10 7 c o n t i n u a t i o n Listing 9 : 1 b . eq e l s e 2 b . eq e l s e 3 add

 7123410812345679123 Example of it block Code equivalent to the it block of Listing 7 Code of Listing 8 strengthened with individual instruction countermeasure scheme r1 , r2 , #10

Figure 1 :

 1 Figure 1: Transition system for the add r1, r2, r3 instruction

Figure 2 :

 2 Figure 2: Model for a non-idempotent instance of the add instruction and its countermeasure

Figure 4 :Figure 5 :

 45 Figure 4: Transition systems for the bl instruction and its replacement sequence

Table 1 :

 1 Instruction classes in the Thumb-2 instruction set

	Instruction class	Examples	Replacement scheme
	Idempotent instructions mov r1,r8	Instruction duplication
		add r3,r1,r2
	Separable instructions	add r1,r1,#1	Use of extra registers and
		push {r4,r5,r6} decomposition into an idempotent instruction sequence
	Specific instructions	bl <function>	Replacement sequence specific to each instruction
		it blocks

Table 2 :

 2 Replacement sequences for some idempotent instructions

	Instruction	Description	Replacement
	mov r1,r8	Copies r8 into r1	mov r1,r8
			mov r1,r8
	ldr r1,[r8,r2]	Loads the value	ldr r1,[r8,r2]
		at the address	ldr r1,[r8,r2]
		r8+r2 into r1
	str r3,[r2,#10] Stores r3 at	str r3,[r2,#10]
		the address r2+10	str r3,[r2,#10]
	add r3,r1,r2	Puts r1+r2 into r3 add r3,r1,r2
			add r3,r1,r2

  Performing such a saving requires 4 extra instructions. The corresponding replacement sequence for this instruction is given in Listing 3. This countermeasure requires 4 extra registers and replaces the initial instruction by 14 instructions. This replacement sequence is actually the most costly one of the whole instruction set, both in term of extra registers and extra instructions.

	Listing 3: Replacement sequence for umlal rlo, rhi, rn, rm instruction that performs rhi:rlo = rn*rm
	+ rhi:rlo
	1	mrs	r t , a p s r	; save flags
	2	mrs	r t , a p s r
	9 mov	r l o , r z
	10 mov	r l o , r z
	11 mov	r h i , r x
	12 mov	r h i , r x

3 umull rx , ry , rn , rm 4 umull rx , ry , rn , rm 5 adds rz , rx , r l o 6 adds rz , rx , r l o 7 addc rx , ry , r h i 8 addc rx , ry , r h i 13 msr a p s r , r t ; restore flags 14 msr a p s r , r t

Table 3 :

 3 Summary of the defined instruction classes

	Class	Type of instructions	Example
	Idempotent ALU operations	add r1,r2,r3 -subs r1,r2,#8
	instructions Load instructions	ldrh r1,[r2,r3] -ldrb r1,[r2,#8]
			Store instructions	strh r1,[r2,r3] -strb r1,[r2,#8]
			Branch instructions	b <label> -bx lr
			Comparison instructions	cmp r1,#9 -cne r3,r4
	Separable	Instructions with a register both source and destination	add r1,r1,#1 -str r0,[r0,#0]
	instructions Instructions with pre-indexed or post-indexed addressing str r1,[r2,#8]! -str r1,[r2],#8
			Stack manipulation instructions	push {r1,r2} -pop {r1,r2}
			Instructions that use a rrx shift and write the flags	adds r1,r2,r3,rrx
	Specific	Subroutine call instruction	bl <function>
	instructions If-Then (it) blocks	itte NE
			Instructions for synchronization with external systems	sev -yield -svc
			Instructions for coprocessors	mcr p0,#0,r8,r2,r3
			Instructions that both read and write the flags	adcs r1,r2,r3 -rrxs r1,r2
	4	add r1 , r2 , #10
	5	eor r3 , r5 , r 1
	6	eor r3 , r5 , r 1

7 b c o n t i n u a t i o n 8 b c o n t i n u a t i o n 9 e l s e 10 mov r3 , #10 11 mov r3 , #10 12 c o n t i n u a t i o n

Table 4 :

 4 Countermeasures overhead for several implementations

	Implementation	Without countermeasure Clock cycles Code size	Clock cycles	With countermeasure Increase Code size	Increase
	AES	9595	490 bytes	20503	113.7 %	1480 bytes	202 %
	MiBench AES	9294	3372 bytes	26618	186.4 %	9776 bytes	189.9 %
	MiBench SHA0	4738	746 bytes	10558	122.8 %	2076 bytes	178.2 %
	AES with countermeasure	9595	490 bytes	11374	18.6 %	1874 bytes	282.5 %
	on the last two rounds
	4.2 Formal verification for some replacement sequences
	4.2.1 Idempotent and separable instructions

It turns out that, in the ARM calling conventions, the r12 register can be used to hold intermediate values and does not need to be saved on the stack. Thus, this register can be used, if available, as a temporary register for such replacement scenarios.

stmdb stores multiple registers into the memory and decrements the address before each access

ldmia loads a memory segment into multiple registers and increments the address after each access

A register is alive at a given point in an instructions sequence if there is a path to the end in which it is read before being written

http://vlsi.colorado.edu/˜vis/


Y F Zhao

N Perry

H Andriankaja

INFORMATION STRUCTURE FOR MANUFACTURING SUSTAINABILITY ASSESSMENT: STEP FOR LCA

Keywords: manufacturing process, information model, STEP

Environmental performances need product, processes and life cycle modeling and evaluations. There is direct need of assessment tools to monitor and estimate environmental impact generated by different types of manufacturing processes. Indeed, eco design and products optimizations can be done with the manufacturing process choices. But the manufacturing systems are very complex and they are driven by physicals laws that are heavy to model. This research proposes a manufacturing informatics framework for the assessment of manufacturing sustainability based on an EXPRESS information model developed to represent sustainability information. It is the first step of association of sustainability information with product design specification. In the next phase of research, investigation will be conducted to integrate sustainability information model and existing standardized product design model ISO 10303 AP 242.

INTRODUCTION

The manufacturing industry is often cited as the cause of many environmental and social problems, yet it is acknowledged as the main mechanism for change through economic growth (Baldwin 05). Industry is confronted with the challenge of designing sustainable products and manufacturing processes. Many sustainable development strategies have been proposed by government agencies and academia since the late 1990s. Research in sustainable manufacturing field can be categorized into the following four main themes [START_REF] Mayyas | Design for sustainability in automotive industry: A comprehensive review[END_REF][START_REF] Ashby | Life-cycle cost analysis: Aluminum versus steel in passenger cars[END_REF][START_REF] Barker | Organizing reuse managing the process of design for remanufacture (DFR)[END_REF][START_REF] Govetto | End-of-life vehicle recycling based on disassembly. Determining the Environmental Impact of Disposal[END_REF][START_REF] Perry | Improving design for recycling -Application to composites[END_REF][START_REF] Vijayaraghavan | Automated energy monitoring of machine tools[END_REF]): a) Life-Cycle Assessment (LCA), b) design-for-X principles and design for sustainability, c) end-of-life studies, and d) energy efficiency monitoring and studies. But it remains a lack of manufacturing system and sustainability information integration hampers the widespread adaptation of the best sustainability practices in the manufacturing industry.

INFORMATION MODELS OF PRODUCT DESIGN AND MANUFACTURING PROCESSES

In recent years, information technology has become increasingly important in the manufacturing enterprise. Effective information sharing and exchange among computer systems throughout a product's life cycle has been a critical issue (ITM 1995, Lee 1999). An information model is a representation of concepts, relationships, constrains, rules, and operations to specify data semantics for a chosen domain of discourse. Amongst these information models, the STEP and STEP-NC information models are the most advanced and standardized ones, developed by ISO committee to provide the basis for product design, machining standardization, and integration of part inspections with machining. The information is modeled in EXPRESS language. STEP Application Protocol (AP) 203 editions 1 & 2 (ISO10303 19941 & 2 (ISO10303 , 20071 & 2 (ISO10303 & 2009) ) (Configuration Controlled 3D Designs of Mechanical Parts and Assemblies) provides the data structures for the exchange of configuration-controlled 3D designs of mechanical parts and assemblies. AP 203 comes from ISO 10303 product data standard, and is not a data standard for configuration management of a product throughout its entire life cycle. The AP is centered on the design phase of mechanical parts and the high-level information entities.

PROPOSED MANUFACTURING INFORMATICS FRAMEWORK FOR THE INTEGRATION OF LCA AT DESIGN STAGE

In order to integrate LCA information into the product design stage, necessary information must be properly represented and associated to the product PLM information. In the proposed research, a case study was first conducted to examine what LCA information should be modeled. Composite parts give interesting examples on a simple piece such as a pedal crank developed with recycled carbon fibers for thermoset organic matrix composite as shown in Figure 3. During the design, product models have to integrate materials information such as matrix composition, reinforcement type (glass, carbon, aramid, and natural), their architecture (unidirectional, woven) and the structure composition (orientations of the different layers in the depth of the product). Other information like inserts or coating completes the bill of material. Currently in STEP AP 203, only very limited material information is modeled as shown in the following entities in table 1. To associate composite material information to a product design, the following entities were developed in this research. The new entities are written in bold-italic. Manufacturing data must also been included in order to ensure the product / material / process combined design in the case of composite parts. Promoting recycled carbon fibers eco-design [START_REF] Perry | Knowledge integration based on road mapping and conceptual framework approach to ease innovation management[END_REF] imposes to access to material data (from end of life scenario and properties) at the early stage of the design. It means developing specific data storage for material properties (depending to the recycling process) and properties models prediction (based on the different type of fibers) as illustrated on Figure 2. Figure3:Proposed information framework for integrating LCA in product design stage Currently in STEP AP 203, the limited material information, shown above in unbolt entities, is not associated to design geometry. The material information is defined only for annotation display. In order to fully integrate material information with design process, the association between product geometry and its material must be semantic. Today no integrated environment allows taking all these facets into consideration. And the next step is to compare, for an expected set of functions, the n-plet [START_REF] Mayyas | Design for sustainability in automotive industry: A comprehensive review[END_REF]) in order to optimize both technically, but also environmentally with specific focus such as material resources minimization (mix of less material and improved end of life possibilities), energy optimization and/or pollution reduction. These multi objective optimization needs to handle all these data, models, life stages, functional unit definition in a coherent environment and at the early stage of product development. STEP and STEP-NC is the most suitable information structure framework that needs to be enriched by the environmental aspects of the product/process data as shown in Figure 3. Eventually, with the proposed information framework, LCA related information is integrated to the design and process planning aspects of product development. The LCA knowledge and data accumulated throughout a product life cycle can be fed back to the product design stage to improve new product development and to reduce environmental impact.

FUTURE WORK AND CONCUSIONS

The research reported in this paper is the very beginning stage of developing an information framework to support the integration of LCA at the product design stage. A simple case study was conducted to examine what composite material information should be defined in association with product design information. The next steps of the proposed research are for the data structure level: i) identify the Product Life Phases needs in terms of environmental data versus the existing data into STEP, ii) identify a dynamic ontology of environmental data for product development, iii) structure the data and evaluation models to propose, usable simulation results for decision making, and iv) propose a STEP extension for End of Life support. For the data acquisition level: i) low level implementation (at the process level for the manufacturing phase) in order to enrich STEP with environmental concepts and start creating data base for process evaluation and optimization, ii) develop design approach and integrated tools specification based on STEP.

Sustainable product design and manufacturing is the future of today's manufacturing industry. The lack of manufacturing system and sustainability information integration hampers the widespread adaptation of the best sustainability practices in the manufacturing industry. In order to provide product designer with comprehensive material and environmental related information at the design stage, a complete information structure must be developed to associate sustainability information with product design information and product manufacturing process. This research proposes to develop such an information framework based upon STEP and STEP-NC information models. An initial case study was conducted to identify composite material information that should be defined for product design.

Figure 1 :

 1 Figure 1: pedal crank made with recycled Carbon Fibers (developed at I2M) (Perry 2012)]

Figure2:

  Figure2: Recycling End of Life scenario and product/material properties evaluation tool.

ENTITY composite_matrix ABSTRACT SUPERTYTPE OF (ONEOF (mud, cement, polymers, metals, ceramics)); name

	(Anisotropic_material,	continuous_fibre_reinforced));
	Braided_assembly,	name:	STRING;
	Coating_layer,	direction:	fibre_directions;
	Isotropic_material,	END_ENTITY;
	Laminate_table,
	Part_view_definition,
	Substance_view_definition,
	Woven_assembly
	Composite_material);
	END_TYPE;
	ENTITY Material_identification;
	material_name : STRING;
	items : SET[1:?] OF material_item_select;
	END_ENTITY;	:	STRING;
		END_ENTITY;
	TYPE material_item_select = SELECT
	(Anisotropic_material,	ENTITY composite_resin
	Braided_assembly,	ABSTRACT SUPERTYPE OF (ONEOF
	Coating_layer,	(polyester_resin, vinylester_resin,
	Isotropic_material,	epoxy_resin, shape_memory_polymer_resin));
	Laminate_table,	name:	STRING;
	Part_view_definition,	material_property: STRING;
	Substance_view_definition,	END_ENTITY;
	Woven_assembly);
	END_TYPE;	ENTITY composite_reinforcement
		ABSTRACT SUPERTYOP OF (ONEOF (glass_fibre,
	ENTITY Composite_material_identification	carbon_fibres, aramid_fibres,
	SUBTYPE OF (Material_identification);	boron_fibres));
	DERIVE	name:	STRING;
	composite_material_name : STRING :=	architecture:	fibre_architecture;
		END_ENTITY;
	SELF\Material_identification.material_name;
	END_ENTITY;	ENTITY fibre_architecture;
		ABSTRACT SUPERTYPE OF (ONEOF
	TYPE material_item_select = SELECT	(short_fibre_reinforced,

ENTITY fibre_directions; SUPERTYPE OF (ONEOF (continuous_aligned, discontinuous_aligned, discontinuous_random, unidirectional, woven)); END_ENTITY;Table 1 :

 1 STEP AP203 entities enriched with composites material information


J Le Duigou

A Bernard

N Perry

J C Delplace

Generic PLM system for SMEs: Application to an equipment manufacturer

Keywords: Product Life cycle Management, Meta Model, Axiomatic Design

For several years, digital engineering has increasingly taken a more important place in the strategic issues of mechanical engineering companies. Our proposition is an approach that enables technical data to be managed and used throughout the product life-cycle. This approach aims to provide assistance for costing, development and industrialization of the product, and for the capitalization, the reuse and the extension of fundamental knowledge. This approach has been experimented within several companies. This paper presents the case in a company environment that designs and produces families of ship equipment parts.

Introduction

In the present industrial context, mechanical engineering industries are facing growing challenges. After having refocused on their primary business in order to increase their production by increasing efficiency, they are now asked to acquire more diversified skills. Market globalisation and an increase in customer demands has forced companies to produce more complex and individualized products in a shorter lead-time. To solve this paradox, companies have adapted by regrouping in order to pool their mutual skills. 'Virtual enterprise' arose for short-term collaborations focused on a specific project, whereas 'extended enterprise' sets up for longer and deeper collaborations between companies [START_REF] Browne | Extended and virtual enterprises -similarities and differences[END_REF].

One of the key points of the success of such kind of enterprise structures is the ability to communicate about and around the product. Products generate a large amount of information, so the classical communication systems phone/fax/email used by 90% of companies are not structured enough to enable efficient cooperation. For many years, software as PLM was developed to pool all this information.

Within this context, Cetim (French industrial technical centre that represents 7000 companies in the field if mechanical engineering industries) launched a survey in 2007 on digital and collaborative engineering for the mechanical engineering companies [START_REF] Cetim | Enquête de besoin sur le travail collaboratif[END_REF]. This survey showed that only 5% of SMEs of fewer than 100 people use a PLM system to manage their technical data. Moreover, more than 70% of these same SMEs consider as important the reuse of knowledge, the sharing of information in the company and with the outside, the security of information access and storage and the follow-up of modifications. These are the exact functionalities offered by the PLM software tools.

Recent surveys evaluate the main difficulties in the implementations of PLM systems in SMEs [START_REF] El Kadiri | Current situation of PLM systems in SME/SMI: Survey's results and analysis[END_REF]. Combined with previous studies in mechanicals SMEs [START_REF] Cetim | Enquête de besoin sur le travail collaboratif[END_REF] [START_REF] Balocco | Innovare e competere con le ICT -Il ruolo delle tecnologie dell'informazione e della comunicazione nella crescita delle PMI[END_REF], it results that the main difficulties that arise for the implementation of PLM system for SMEs are:

• The gap between the functionalities proposed by the actual software and the needs of some kind of enterprise, especially the raw part makers.

• The difficulty of modelling business processes and data models. The modelling skills are not sufficiently present in SMEs.

• The lack of interoperability between PLM and CAD, ERP and PLM of partner companies. Section 2 focuses on the scientific studies that enable to establish the starting point of the approach. In section 3, the working method is presented. In section 4, the industrial case study, an equipment manufacturer, will be described.

PLM: from concept to data model

For many years, the software providers have extolled the merits of PLM and the return on investment of that information systems. But PLM is first of all an enterprise strategy [START_REF] Stark | Product Lifecycle Management: Paradigm for 21st century Product Realisation[END_REF]. It involves managing all the data concerning a product, throughout its lifecycle, and all the internal and external actors involved in the development of this product. An acceptable definition of PLM is: "A strategic business approach that applies a consistent set of business solutions in support of the collaborative creation, management, dissemination and use of product definition information across the extended enterprise from concept to end of life -integrating people, processes, business system, and information" (CIMData, 2003).

Nevertheless, in an extended enterprise context, it is necessary for these different models being able to interoperate together. Different possibilities exist as the use of standardized models that enable sharing and communication between companies. Much work was done in different sectors to increase the interoperability of data models with the standards [START_REF] Subrahmanian | Product lifecycle management support: a challenge in supporting product design and manufacturing in a networked economy[END_REF], using mainly the STEP (STandards for the Exchange of Product model data) ISO norm (ISO 10303), [START_REF] Chambolle | Un modèle produit piloté par les processus d'élaboration : Application au secteur automobile dans l'environnement STEP[END_REF][START_REF] El Khalkhali | An information infrastructure to share product models using STEP standard[END_REF]. The AP214 (ISO 10303-214, 1998) is widely used in the automobile sector, whereas the AP239 (ISO 10303-239, 2005;[START_REF] Pratt | ISO 10303, the STEP standard for product data exchange, and its PLM capabilities[END_REF] focuses more on the aeronautic sector. Those models are not fully interoperable, despite having common integrated resources. The main reason is that the objects and the attributes are different depending on the sector of application. Hence, the creation of PDM Schema (PDM Schema, 2001) that tries to unify the different information models of STEP APs using their common objects.

Much work has been done in this field, especially in the aeronautic and automobile sectors in order to propose technical data management methods [START_REF] Bacha | De la gestion des données techniques pour l'ingénierie de production. Référentiel du domaine et cadre méthodologique pour l'ingénierie des systèmes d'information techniques en entreprise[END_REF][START_REF] Mcmahon | Information management for through life product support: the curation of digital engineering data[END_REF][START_REF] Nguyen | System engineering for collaborative data management systems: Application to design/simulation loops[END_REF], but also in smaller companies, such as foundries [START_REF] Delplace | L'Ingénierie numérique pour l'amélioration des processus décisionnels et opérationnels en fonderie[END_REF]. Numerous projects, like Promise (Promise, 2007) or Bridge (Bridge, 2009), propose methods and models exploiting the whole product lifecycle information in so called closed-loop PLM. It includes the phases of use, maintenance and end of life in the collection of data. The produced data for the whole lifecycle are now available. For example RFIDs, embedded systems and wireless communication allows collecting information during the use or maintenance phases. Those projects lead to describe data models adapted to the encapsulation of knowledge and data from the product all over the lifecycle. Those models and ontologies, like in [START_REF] Matsokis | An Ontology-based Approach for Product Lifecycle Management[END_REF], include the product definition "as designed" but also "as built" and "as maintained". The goal of those models, like in [START_REF] Cassina | Development of an Extended Product Lifecycle Management through Service Oriented Architecture[END_REF] is to improve the interaction between the enterprise and the customer.

These models are more adapted to some kind of companies, especially in a business to consumer (B to C) economic model, than to the mechanical SMEs present in our work, like equipment part manufacturers. Indeed the closed-loop PLM is more valuable when the interaction is direct between the company and the end user of the product. In the case of a second or third rank supplier, this interaction seems to be more difficult. Moreover those methods and data models are very complex and require investment and skills that are not yet available in all mechanical SMEs.

The next section will present our research approach to create a modelling framework based on a bottom-up method to obtain a generic model for SMEs.

Research approach

The proposed method specifies PLM system to be implemented in mechanical SMEs. It is a four steps method that gives functional needs of the company, processes to implement to solve these needs and business objects used in these processes. A final step automates some processes to validate the previous models.

• Identify needs: the analysis phase is done by interviewing and observing the experts.

The implicit and explicit needs about PLM have to be identified. The explicit needs could be identified by the interviews but the implicit needs need the observation or the realization of the task by an external person, the modeler. The observation of the experts show how the technical data are use in the company, their purposes, their processes… the realization of some tasks of the experts permits to the modeler to fill the different gaps in the processes of creation and transformation of the technical data. The needs could be express through a SysML requirement diagram or a less formal language to facilitate the exchange with the experts, like a mind map. • Modeling the processes to realize the identified needs: the goal of this step is to formalize the "to be" business processes that will respond to the identified needs. The language to model the processes could be SADT, IDEF0, BPMN or an UML sequential diagram. In this work, the selected language is SADT because it is the only one that the experts already know in the mechanical SMEs of our study.

• Extraction of the business objects: the extraction of the business object allows

creating the right data model that will be integrated to the PLM system. The objects are extracted from the "to be" processes. The objects are the inputs and outputs of those processes. To represent the data model, the UML class diagram is chosen. This language does not have to be understood only by the experts, but also by the database engineers for the implementation of the PLM system. UML is one of the most known languages in both domains. • Automation: Before implementing the data model, a automation is done to validate the good understanding of the requirements and their resolution through the "to be" processes supported by the data model. A demonstrator is created to respond to requirements automating a process. The confrontation of this demonstrator with the appropriated experts allows validating the three first stages.

The next section is a case study at an equipment manufacturer.

A equipment manufacturer: PSL Concept

This case study must enable us to put into practice methods of technical data structuring and management, adapted to this specific company. In order to do this, the method begins by analysing the needs of the company in terms of PLM. Then it proposes an approach to improve on the initial situation. Finally, it validates the models by automating the analysed process on a product family.

Description of the company and needs analysis

PSL Concept produces and sells equipment for ships. Among these products, there are reserve rudders, pulleys and tackles, sheaves, jam cleats and various accessories. This company organizes the main part of their products into families. In fact, as many system integrators, their products starts from standard products, on which options and modifications are added to meet customer needs. The chosen family is a major and wellknown family of products for the company: the pulleys.

A standard pulley (Figure 1) is composed of two flanges (1), of one or more sheaves (2), of fastening and of different accessories as for example a jam cleat. To translate the movement, the fag end (a sailboat string) moves onto the sheave's groove. The flanges have many options such as adding guides (4) to maintain the contact between fag end and sheave in special use conditions or beckets (5) and different kinds of openings (3) to fix the pulley. Various processes are used to produce the parts, the composite carbon blocks are polymerised, then cut by milling, and are finally manually assembled with the other parts. After an audit of the company, the main needs in terms of PLM are as follows:

• Knowledge capitalisation: an improvement of design, resulting from customer feedback, a set of tests or the optimization of the designer, are not reproduced on the other products of the family without the involvement of the designer on each product. This process is lengthy and is a source of error. • Bill of Material (BoM) management: the BoM are manually edited and have to be updated if a modification appears on the product design. • Reference management: the product references are hard to manage efficiently due to large number of referenced products (1200 only for pulleys). • Quote: no detailed process is available at the early design and quotation phases. That makes difficult to know, for example, the quantities of raw materials and the manufacturing time before the detailed design of the product. • Archive management: when a client comes back with a product, it is not always easy to find the original drawings of the product that has exactly been sold with the references of the different parts.

Business processes modelling

The families in PSL Concept could be organized by main functions of the products. It seems that an organisation of technical data by function could be the most efficient way of being able to link the design parameters and the functions of the product. With this organisation, the technical data are globally managed depending on the functions of the family.

Suh [START_REF] Suh | The Principle of Design[END_REF] proposes the Axiomatic Design that links the functional parameters to the design parameters. He divides the design into four domains (customer, functional, physical, process). Each domain contains specific design objects (customer needs (CNs), functional requirements (FRs), design parameters (DPs) and process variables (PVs)).

The functional requirements defines the minimum data that fully complete the customer needs. The design process moves on by breaking down the hierarchical upper level and zigzagging between functional, physical and process domains. Axioms guide the designers within the choices. Two design axioms have been defined as follows:

First axiom -independency axiom: maintain the independence of functional requirements.

Second axiom -information axiom: minimize the information content (of the design). Design matrix representing the links between FRs and DPs enable the design to be visualized and optimized by applying axioms.

The design matrixes show the relation between the FRs and the DPs at a given level of the design hierarchy. There are three natures for the design matrix: it can be a triangular matrix, known as decoupled matrix, a diagonal matrix, known as uncoupled matrix or any other kind of matrix, known as coupled matrix (Figure 2). This principle is adapted and declined into the technical data structuring and management of a products family. The different functions of the family are broken down, and create a set of functional dimensioning parameters for the products in order to link those parameters to the different functions (Figure 3). To create the link between the functional parameters and the design parameters, the design matrix of the product are needed. The equations are solved to link the FRs to the DPs when the matrix is decoupled or uncoupled ("good design" in the axiomatic design theory).

Thus, if the customer does not require a function, and if this function is only linked to a single sub-product, then this sub-product will not be present in the final product. The word sub-product is for a part in an assembly and for a part of a part. Moreover, the modification of a functional parameter leads to the modification of the design parameters that are linked to it.

On this basis, several functionalities are developed to meet the needs in terms of PLM for this company.

• Knowledge capitalisation: when a modification of the design is made, this modification is implemented on all the products of the family that use the function concerned by the modification. There is no longer information loss when a product is improved because if the function or the definition of the design parameter is modified, all the products of the family will be automatically modified and so have the benefit of the improvement. • Reference management: in order not to have to open a large number of references without producing the referenced product, a system of referencing based on the functions of the product family is introduced. This system enables that a new product (an unseen combination of functions) automatically obtains a reference link to the specified functions, without having to open all the possible references beforehand. • Quote: The price of a product is linked to the functions of this product. So ascertaining empirically the relation between the price and each function, a price for a product is obtained from its functional definition.

• Archive management: by registering the modification dates of functional parameters and the former values of these parameters, the exact CAD of a past product can be found, by using the parameters at the product sale date.

Business objects extraction

Analyzing inputs and outputs of the processes, the following documents have been extracted: functional requirements, assembly CAD files, component CAD files, 2D drawings, BoM... To create the generic model, the following method is applied: • Select the documents that deal with PLM.

•

Group documents by theme and identify the concepts and the objects representing each group. This phase is performed by a cognitive analysis of the modeller based on a semantic analysis.

•

Detail the objects. This step is performed by an extraction of the intersection of attributes and methods.

•

Link the different objects. This is done by identifying the various links between documents of different groups. This process is applied to the documents extract from the analysed processes. The result is the following data model (Figure 4).

Customer

The customer sends an order. The order describes the different customer needs. The order is linked to functions. The function is connected to the product, as a technical function or a service function, via the selected link. The product is composed of products, which may be optional. A product (component) can have alternative products (components) in an assembly context. When it is a bought product, it is connected to a supplier. Finally, the product is linked to the order.

Automation of the approach

A software program, made using Visual Basic and Solidworks API (Application Programming Interfaces), was implemented to automatically construct the CAD file of a pulley from the functional requirements.

To create this program the functionalities of a pulley is broken down (Figure 5) into a list of functions and functional parameters. Then options are defined and linked to those functions (Table 1) to obtain discreet values for the functional parameters. A functional dimensioning of the different parts of the pulley was implemented in the CAD model. The parameters were grouped according to the different functions of the pulley aimed to link the functions of the pulley and the parameters of the CAD model (Table 2). The values of those parameters are calculated according to the specific craft rules defined by the firm and the values of the functional parameters. Other dimensions are also needed to obtain the full CAD model, but they are a pro rata of the previous parameters of Table 2. As a result an only CAD file represents the whole pulley family. All the parameters and their definitions are temporarily stored in a spreadsheet. They will be stored in the PLM database. An example for a specific function is detailed: the function "to keep the contact between the fag end and the sheave" (Figure 6) when the parameter "angle of traction" is greater than 90°. If the maximum angle of traction is greater than 90°, guides are added to the flanges with a screw between the two flanges (reference 4 in Figure 1). The fag end passes between the sheave and the screw and is forced to stay in contact with the sheave. On the CAD model, the feature "guide extrusion" passes automatically from a suppressed state to a resolved state. The construction parameters of the guide are then downloaded and filled in, according to the function requirements (Figure 6 and Table 3). When one of guide parameters is changed, all the pulleys that have an "angle of traction" functional requirement greater than 90° will be modified. No more need to change the value of the parameters, because the change affects directly their definition. If the fag end is often jammed between the screw of the guide and the sheave (cause by an accumulation of impurities), then the definition of the parameter "gap with the sheave" is changed from "fag end diameter +4mm" to "fag end diameter +5mm". Then all the new pulleys with a maximum angle of traction greater than 90° will have 1mm more in the gap between the screw and the sheave, so the impurities will no longer jam the end fag.

Conclusions on the case study

First, the software carries out a needs analysis. Then it produces the CAD model for the specific pulley, shows the quote, opens a reference if necessary and creates the layouts and the BoM. The design time for a new pulley has gone from hours to minutes.

Moreover there is now a single CAD file to manage, with an associated table of parameter definitions for the 1200 pulley references. With the record of modifications of the parameter definitions and the functional requirements of each sold product, an old version of a pulley is recreated directly from this CAD file.

An approach is proposed to meet the specific PLM needs of this company. The implementation of the software based on this approach and the results obtained prove that the approach is in phase with the needs of this kind of company. Nevertheless, a family of well-known products was chosen. What about the feasibility of this approach if a new range of products is chosen. Many parameter definitions were obtained with an empirical value, and it could be difficult to assume those coefficients for a new product range.

Conclusions and prospects

An approach to meet PLM needs of an equipment manufacturer is proposed and implemented. The results obtained confirm that this solution meets the needs in terms of PLM of this type of company. But, in an extended enterprise, the approach could not be limited to one type of company and on one functionality (here design) in the network. It must be possible to link integrators, detail parts producers and mould makers or machine tool producers in order to bring a modern industrial project to fruition. That is why our other portfolio of industrial cases is made of different kind of enterprises. For example the other test cases integrate an elementary part producer and a machine tool producer. That will enable us to underline the specific problems of the other type of companies and of the other life-cycle steps.

In parallel the structure of a meta-model of the PLM for SMEs in Mechanical Manufacturing is built. All the elementary cases study brings together the basics bricks of a more complete software and information system solution. As a conclusion, the case study allow us to built from the experiment a information system to fit with the SMEs requirements in term of PLM. Each case gives us also the possibility to apply and improve the predefine methodology.

Figure 1

 1 Figure 1 Description of a pulley.

Figure 2

 2 Figure 2 Design matrix a) coupled, b) uncoupled, c) decoupled

Figure 3

 3 Figure 3 Decomposition of a product family through Suh domains

Figure 4

 4 Figure 4 PSL Concept data model.

Figure 5

 5 Figure 5 Partial functional decomposition of a pulley.

Figure 6

 6 Figure 6 Sketch of the guide on the flange.

Table 1

 1 Design parameters and associate options

	Functions	Options	Choice
	General operations	Fag end diameter 6/ 8/ 10/ 12
		Type of sheave	Big/ Small/ Fiddle
		Number of sheave Simple/ Double/ Triple
	Enable to fix the pulley	Type of opening	Shackle/ swivel/ shafing/ mat/ clinch
	Keep the contact between the fag end and the sheave Becket	Yes/No
		Guide	Yes/No

Table 2

 2 Link between functions and options

	Parameter	Value Unit	Associate function
	Plate length	300	mm	Blank parameters
	Plate breadth	300	mm
	Plate thickness	3.5	mm
	Sheave diameter	84	mm	Fag end parameters
	Number of hole sheave 8	Unit
	Becket radius1	10	mm	Becket parameters
	Becket radius2	11	mm
	Becket fillet	12	mm
	Guide angle	70	°	Guide parameters
	Guide distance	8	mm
	Guide fillet	8	mm
	Swivel distance	5.45	mm	Opening of the
	Shackle distance	4	mm	flange
	Clinch distance	8	mm
	Clinch length	16	mm
	Clinch breadth	8	mm
	Shafing mat distance	8.3	mm
	Shafing mat length	8	mm
	Shafing mat breadth	16	mm
	Evacuation radius1	12	mm	Evacuation
	Evacuation radius2	8	mm	parameters
	Evacuation fillet1	3	mm
	Evacuation fillet2	3	mm
	Screw diameter	3.2	mm	Fastening
	Washer diameter	7.1	mm	parameters

Table 3

 3 Design parameters of the guide.

	Guide parameters	Angle of the	Gap with the	Diameter of	Diameter of	Radius of the
		guide	sheave	the screw	the washer	fillet
	Definition in	180° -angle of	Fag end	Constant	Constant	Fag end
	function of the FRs	traction + 10°	diameter +			diameter +
			4mm			4mm

Acknowledgement

We would like to thank PSL Concept for allowing us to carry out our study in and for their technical support.