Keywords: control flow, static analysis, Java, embedded systems, security flot de controle, analyse statique, Java, systèmes embarqués, sécurité

Vérification de politiques de flot de contrôle sur du bytecode Java

Résumé : Ce rapport présente l'application de politiques de flot de contrôle sur du bytecode Java pour les petits systèmes ouverts. La plupart du temps, l'application de ce type de politiques de sécurité est réalisée par l'observation du système ou l'insertion de code pour assuré en assurer le respect, ce qui n'est pas approprié pour les petits systèmes fortement contraints tels que les téléphones mobiles ou les cartes à puce. Nous présentons une méthode basée sur le proof-carrying code pour faire appliquer ce type de politiques avec une vérification embarquée réalisée au chargement. Notre approche est bien adaptée aux petits systèmes ouverts évolutifs car elle est compositionnelle, pour éviter la revérification du code déjà chargé, et régressive, afin de traiter proprement le déchargement de code déjà installé et vérifié.

Introduction

Ubiquitous devices such as mobile phones and smart-cards are multi-application capable and support post-issuance installation of applications. Applications are also evolving to take advantage of this new trend: they have shifted from standalone designs to a collaborative model where they provide and/or use services of other applications. In this context, operating systems of ubiquitous devices provide few mechanisms to protect themselves, and end-users, against misuses.

In Android for instance, an application can request some permissions at installation such as the ability to read the address book stored in the phone (READ_CONTACTS), or to open network sockets (INTERNET). The end-user can accept or refuse to grant these permissions to an application, but there is no way to control how the application is going to use them: is it going to send my contacts to a third party? If I refuse to grant a permission P to an application, can it collude with some other application that has been granted P ?

Code-signing was the first technique introduced to protect ubiquitous devices against code originated from untrusted entities, but it does not guarantee any security property on the behavior of the loaded code. Code-signing is now also used to ensure integrity of the code bounded together with some metadata describing its security-related behavior. This is for instance the case in model-carrying code (MCC) [START_REF] Sekar | Model-carrying code: a practical approach for safe execution of untrusted applications[END_REF] and security-by-contract (S×C) [START_REF] Bielova | Matching in security-bycontract for mobile code[END_REF][START_REF] Massacci | Simulating midlet's security claims with automata modulo theory[END_REF] models. The embedded metadata are checked at loading time by the device to determine they are compliant with its security policy. However, adequacy between the code and the metadata describing its behavior is enforced at run-time by execution monitoring, which is not appropriate for constrained devices such as smart-cards or mobile phones as it produces variable run-time overheads according to the complexity of the security policy to be enforced. A common approach for the enforcement of security policies using execution monitoring consists in relying on security automata [START_REF] Bauer | Composing security policies with Polymer[END_REF][START_REF] Erlingsson | IRM enforcement of Java stack inspection[END_REF][START_REF] Schneider | Enforceable security policies[END_REF][START_REF] Fong | Access control by tracking shallow execution history[END_REF][START_REF] Vanoverberghe | Supporting security monitor-aware development[END_REF][START_REF] Brown | Synthesising monitors from high-level policies for the safe execution of untrusted software[END_REF][START_REF] Huisman | A formal connection between security automata and JML annotations[END_REF]. While security automata provide a very expressive mean to describe security policies, execution monitoring of the security automaton states implies to react before the policy is violated when some misuse is about to occur: execution can be halted [START_REF] Alpern | Recognizing safety and liveness[END_REF][START_REF] Schneider | Enforceable security policies[END_REF] or control flow can be dynamically altered [START_REF] Ligatti | Edit automata: enforcement mechanisms for run-time security policies[END_REF][START_REF] Ligatti | Enforcing non-safety security policies with program monitors[END_REF][START_REF] Bielova | Do you really mean what you actually enforced[END_REF][START_REF] Talhi | Execution monitoring enforcement for limited-memory systems[END_REF][START_REF] Fong | Access control by tracking shallow execution history[END_REF] in order to make it compliant with the security policy, but both actions strongly impact applications functionality.

McDaniel et al [START_REF] Ongtang | Semantically rich applicationcentric security in Android[END_REF] described a context-sensitive security framework for Android to monitor and to restrict applications behavior. It is for example possible to restrict applications to be granted both READ_CONTACTS and INTERNET permissions, but also for an application to refuse interactions with some application according to its permissions. However, this framework cannot avoid collusion between applications, for instance between one with the READ_CONTACT permission, and the another one with the INTERNET permission. This approach lacks refinement as it can block the installation of "honest" applications (such as a reliable text messenger application in the previous example) without detecting possibly dangerous misuses. Information flow techniques such as [START_REF] Myers | Practical mostly-static information flow control[END_REF] can solve this problem, but they are practically not used because they require an ad hoc run-time environment and developers with a strong understanding of the underlying model to smartly annotate their code. To cope with these problems, McDaniel et al recently proposed another framework [START_REF] Enck | An information-flow tracking system for realtime privacy monitoring on smartphones[END_REF] for Android with run-time enforcement of secure information flow. This approach is obviously not portable to devices more constrained than modern phones, i.e., J2ME or Java Card devices.

Static analysis offers a good alternative to execution monitoring as it does not produce computation overheads at run-time and does not alter code's behavior dynamically. However, static analysis requires high computational and memory resources not available in constrained devices. The Proof-carrying code (PCC) model [START_REF] Necula | Proof-carrying code[END_REF] permits to simplify on-device analysis. A proof of the code's behavior with respect to a given property is pre-computed off-device so that the code's receiver only needs to verify that the proof is correct for the given code. Verifying this proof is actually far more easier and consumes less resources than doing the complete analysis on-device while it offers the same security guarantees, moreover without the need of a trusted entity for signing the code. Proof-carrying code approaches have already been successfully applied in constrained devices, in particular by Rose [START_REF] Rose | Lightweight bytecode verification[END_REF] on Java bytecode. Existing approaches mainly focus on type safety [START_REF] Morrisett | From system F to typed assembly language[END_REF][START_REF] Klein | Verified lightweight bytecode verification[END_REF][START_REF] Rose | Lightweight bytecode verification[END_REF], space/time guarantees [START_REF] Aspinall | Mobile resource guarantees for smart devices[END_REF], safety properties [START_REF] Alpern | Verifying temporal properties without temporal logic[END_REF][START_REF] Walker | A type system for expressive security policies[END_REF][START_REF] Winwood | On the automated synthesis of proof-carrying temporal reference monitors[END_REF], access control and control flow policies [START_REF] Jensen | Verification of control flow based security properties[END_REF][START_REF] Colcombet | Enforcing trace properties by program transformation[END_REF][START_REF] Pottier | A systematic approach to static access control[END_REF]. All aforementioned works are not purely static analysis. For instance, Jensen et al [START_REF] Jensen | Verification of control flow based security properties[END_REF] proposed to enforce a global control flow policy through local run-time checks present in the code. Their approach consists in verifying that these local checks are sufficient to enforce a global control flow policy. This approach is closely related to [START_REF] Colcombet | Enforcing trace properties by program transformation[END_REF] where similar in-line checks are generated just-in-time.

In this paper, we propose a technique in-between security automata [START_REF] Schneider | Enforceable security policies[END_REF], Jensen et al work on the verification of control flow policies [START_REF] Jensen | Verification of control flow based security properties[END_REF] and compositional verification of control flow policies described in [START_REF] Gurov | Compositional verification of sequential programs with procedures[END_REF][START_REF] Mizuno | A security flow control algorithm and its denotational semantics correctness proof[END_REF]. Our main contribution is to propose a purely static and compositional proof-carrying code approach to enforce global control flow policies specified by an automaton devoted to constrained Java-based devices such as mobile phones or smart cards. This paper is structured as follows. Section 2 introduces the formal notations used in the rest of the paper. Section 3 describes the theoretical foundations of our approach: the definition of a global control flow policy of a system, and the definition of a method's footprint, that is its relevant contribution to a global policy. Section 4 details the static analysis of Java bytecode needed to compute method footprints off-device, and how method footprints are efficiently encoded. Section 5 details how proof obligations that are method footprints can be efficiently and incrementally verified on-device upon (un)loading of bytecode. Section 6 draws conclusions and presents future work.

Notations

Object-oriented notations

In this paper, we consider multi-application Java systems. As in any Java system, an application is implemented by a set of classes. However, the notion of application does not correspond to something concrete on most Java sytems. We voluntary use a generic meaning for applications in order to match any Java environment: for traditional Java, an application can simply be a fully qualified package name, while it can correspond to a CAP file on Java Card systems.

We will write M the set of all method names that are fully qualified names, namely elements of the form A.C.m to denote the method m that is available in objects of class C of application A. Note that the method A.C.m might be defined and implemented in a super-class of A.C -which might itself be in some other application -and simply inherited.

We use the following notations for inheritance. The set of classes is equipped with an inheritance relation ≤; C 1 ≤ C 2 means that the class C 1 inherits from C 2 or is C 2 (< for a strict sub-class). The set M is also equipped with an inheritance relation, also written ≤. When a class C 1 of application A 1 inherits from some class C 2 in application A 2 and redefines a method m, we write A 1 .C 1 .m < A 2 .C 2 .m. We use ≤ whenever the method is either inherited or redefined. The method definition def

(A.C.m) of A.C.m is A.C.m if the method m is defined or redefined in A.C, otherwise def (A.C.m) = A ′ .C ′ .m such that A.C < A ′ .C ′ and for each A ′′ .C ′′ such that A.C < A ′′ .C ′′ < A ′ .C ′ , m is neither defined nor redefined in A ′′ .C ′′ .

Graphs of the programs

We consider finite directed graphs with edges labeled by elements of a set L E and unlabeled vertices (as we consider only cases where the labeling function of vertices would have been a bijection). A graph G is given by a pair (V, E) where V is its set of vertices, E ⊆ V × V × L E , and its set of labeled edges.

In the graph G = (V, E), the edge from the vertex u to v, labeled by l is denoted by (u, v, l). Graphs may also have unlabeled edges, which are edges for which labeling is irrelevant and can be ignored, edges of such graphs are written as pairs of vertices (u, v).

For a graph G = (V, E), V ′ ⊆ V and V ′′ ⊆ V :

paths(G, V ′ , V ′′ ) = {v 0 v 1 . . . v n ∈ V * | v 0 ∈ V ′ , v n ∈ V ′′ , ∀0 < i ≤ n, (v i-1 , v i ) ∈ E}. A strongly connected component of a graph G = (V, E) is a subgraph G ′ = (V ′ , E ′ ) with V ′ ⊆ V and E ′ ⊆ E, where V ′ is a maximal subset of V such that for each pair v 1 , v 2 of vertices of V ′ , there exists a word v 1 v i 0 . . . v in v 2 in paths(G, V ′ , V ′ ) and each v i k ∈ V ′ (and symmetrically from v 2 to v 1 ).
For a method m, P m is its instruction list. We assume this list to be indexed from 0 to |P m | -1, where |P m | is its size. Hence, we denote by P m [i] the i + 1-th bytecode instruction of the method m.

Let us first define the call graph of a set of methods. To deal with control flow properties, we have to be able to compute for a given method, the set of methods it invokes directly of indirectly. The set is statically computed and thus collects methods that are invoked on static types. Definition 3 (Invoked methods). Let m be a method. Then the set of methods that m invokes is the smallest set of methods such that

I(m) = I direct (m) ∪ I indirect (m) with -I direct (m) = {m ′ | ∃0 ≤ i < |P m |, P m [i] = invoke m ′′ , m ′ ≤ m ′′ } is the set of methods invoked in the bytecode of m, -I indirect (m) = m ′ ∈I direct (m) I(m ′ ), i.e.
, the set of methods (directly and indirectly) invoked by methods directly invoked by m.

It is fairly easy to see that I(m) is exactly the set of all the methods that are reachable (by 1 or more transitions) from m in the call graph of the system (Definition 1).

Formal languages notations

In this section we give additional notations that are used in this paper for finite automata and languages.

Definition 4 (Finite automaton). A finite automaton is a tuple A = (Σ, S, s 0 , ζ, S F ) where Σ is the input alphabet, S is the set of states, s 0 ∈ S is the initial state, ζ : S × Σ -→ S is the transition function, and S F ⊆ S is the set of final states.

Definition 5 (Trimmed automaton).

An automaton A = (Σ, S, s 0 , ζ, S F ) is trimmed if for all state s ∈ S, there exist two words u and v such that ζ(s 0 , u) = s and ζ(s, v) ∈ S F . Definition 6 (Language). Let A = (Σ, S, s 0 , ζ, S F ) be a finite automaton. The language of A, denoted by L(A) is defined by:

L(A) = {a 0 . . . a n ∈ Σ * | ∃(s i 0 , a 0 , s i 1 )(s i 1 , a 1 , s i 2 ) . . . (s in , a n , s i n+1 ) ∀0 ≤ k ≤ n, (s i k , a k , s i k+1 ) ∈ ζ, s i 0 = s 0 , s i n+1 ∈ S F }.
Note that ε denotes the empty word. We now define the factors of a language.

Definition 7 (Factors). Let L be a language of Σ * . Then, the left factors, (regular) factors, and right factors of L are respectively defined by:

lf (L) = {u ∈ Σ * | ∃w ∈ Σ * , uw ∈ L}, fact(L) = {u ∈ Σ * | ∃v, w ∈ Σ * , vuw ∈ L}, rf (L) = {u ∈ Σ * | ∃v ∈ Σ * , vu ∈ L}.
Definition 8 (Projection). Let Σ and Ξ be two alphabets. Let L ⊆ Σ * be a language. The projection onto Ξ is the alphabetical morphism

Π Ξ from Σ to Ξ such that for each x of Σ, Π Ξ (x) = x if x ∈ Ξ and Π Ξ (x) = ε otherwise.

Global control flow policy of a system

In this work, we study the control flow policies in terms of access to methods. We introduce the notion of global policy of a system that defines the control applied on applications by the system. The global policy of a system defines the sequences of method calls that are forbidden. This type of policy can be used for example to restrict applications access to the system api.

Definition of the global policy of a system

At the verification level, the forbidden sequences of calls are described by a finite automaton. This automaton is really simple compared to security automata [START_REF] Schneider | Enforceable security policies[END_REF] as it has no vertex labelling to describe a particular state of the system, and an edge label can only describe a method call. Actually, we show along the rest of the paper that these simplifications are useful to achieve a complete static verification technique especially in open and constrained environments.

Definition 9 (Global policy). Let the global policy of a system G be a finite trimmed automaton G = (Σ, S, s 0 , ζ, {s F }) with Σ ⊆ M and such that:

-there is no (s, a) ∈ S × Σ with ζ(s, a) = s 0 , -there is no (s, a) ∈ S × Σ with ζ(s F , a) = s.
Definition 10 (Conformity to a policy). We say that a system conforms to the policy G if for each execution trace t ∈ M * , conform(t, G) holds with:

conform(t, G) ⇔ (∀v such that Π Σ (t) = uvu ′ , v ∈ L(G)).
Note that we prohibit any transition incoming into the initial state and outgoing of the final state in our global policies. Since a trace is not conforming as soon as it contains a word of the language of the global policy, transitions starting in a final state or leading to the initial state are useless to detect non-conforming traces: on the one hand, the trace was already recognized as invalid the first time s F was reached and on the other hand we can simply chop off the prefix corresponding to the loop from s 0 to s 0 while keeping an invalid trace.

Also note that, only one final state is needed since this state has no outgoing transition: if there were various final states they would be equivalent and could be merged. Consequently, we write in the rest of this document G = (Σ, S, s 0 , ζ, s F ).

Global policy footprint of a method

In this work, we consider open systems that support dynamic application loading. Thus, we aim at a compositional model in which methods can be verified one by one and systems can be extended with new methods without re-verification of already loaded code. In this system, a method m can be valid for a global policy but still contain a part of an invalid trace. If this method is invoked by another one that produces the beginning of a forbidden trace, invokes m, and produces the end of a forbidden trace, then m might participate in the construction of an invalid trace even if all the traces of m are allowed. To track this kind of behaviors, we define in this section the contribution of a method to the current execution with respect to the global policy of a system; we call that contribution the footprint of the method.

Definition 11 (Interprocedural control flow graph). The interprocedural control flow graph of a set of methods M is the graph ICFG

M = (V, E), built from the intraprocedural control flow graphs CF m of the methods m ∈ M , with def (M ) = M ∪ {def (m) | m ∈ M }, such that: -V = {m.i | i ∈ V m , m ∈ def (M ), CF m = (V m , E m )}, -E = {(m.i, m.i ′ ) | m ∈ def (M ) ∧ CF m = (V m , E m ) ∧ (i, i ′ ) ∈ E m ∧P m [i] = invoke m ′ with m ′ ∈ def (M )} ∪ {(m.i, m ′′ .0) | P m [i] = invoke m ′ ∧ m ′ ∈ def (M ) ∧m ′′ ≤ def (m ′ ) ∧ m ′′ = def (m ′′ )} ∪ {(m.i, m ′ .i ′ ) | P m [i] = return ∧ P m ′ [i ′ -1] = invoke m ′′ ∧ m ≤ def (m ′′ )}
Let m be a method. Let us remind that I m is the set of methods called by a method m, directly or indirectly. Then the interprocedural control flow graph of m is ICFG m = ICFG {m}∪Im .

In general, it is not possible to compute statically the exact set of traces of a system or a subsystem, so we compute an over-approximation of that set. In particular, we put in the interprocedural control flow graph the edges between an invoke instruction and all the methods that could be actually invoked, due to method overloading.

As we only consider method calls in the policy, we define a morphism for V * to the set L(M) of languages defined on M that allows us to restrict the traces to method calls, taking care of method definitions to avoid an attacker to bypass the control by overloading a class:

calls : V -→ L(M) m.i -→ {m ′′ | m ′ ≤ m ′′ ∧ def (m ′′ ) = def (m ′ )} if P m [i] = invoke m ′ ∅ otherwise
We now define the set of traces of a method m, that is an over-approximation of its set of execution traces as:

traces(m) = m.calls(paths(ICFG m , {m.0}, {m.i | P m [i] = return})).
We can now define the G-footprint of a method m for a policy G that describes the factors (left, regular and right) of the traces of the policy language that may result from the execution of this method.

Definition 12 (G-footprint of a method). The G-footprint of a method m for a policy

G = (Σ, S, s 0 , ζ, s F ) is foot G (traces(m)) with foot G (L) =            if fact(L) ∩ L(G) = ∅ ( lf (Π Σ (L)) ∩ rf (L(G)), Π Σ (L) ∩ fact(L(G)), rf (Π Σ (L)) ∩ lf (L(G)) )
otherwise We denote by F G the set of footprints for a policy G.

This definition allows us to keep information about the contribution of a method m to creation of forbidden sequences as factors. That contribution is written whenever the method contains an execution trace that is prohibited. Otherwise, it is described as a tuple: the first element of the tuple contains the possible ends of forbidden traces (left factors of complete execution traces of the method); the second element contains the full execution traces of the method that are middle elements of forbidden traces, and the last element of the tuple contains the possible beginnings of forbidden traces. All these factors will be later aggregated with the beginnings and ends of traces of a method that invokes m in order to produce the footprint of this calling method.

Properties of the operations on footprints

In this section, we present the main operations on footprints and their properties, that will be useful to obtain compositionality.

Definition 13 (Union of G-footprints). Let G = (Σ, S, s 0 , ζ, s F ) be a global policy and f 1 and f 2 be two G-footprints. Then the union of f 1 and f 2 is defined depending on their forms:

∪ = ∪ (LF 2 , F 2 , RF 2 ) = (LF 1 , F 1 , RF 1 ) ∪ = (LF 1 , F 1 , RF 1 ) ∪ (LF 2 , F 2 , RF 2 ) = (LF 1 ∪ LF 2 , F 1 ∪ F 2 , RF 1 ∪ RF 2 )
Lemma 1 (foot G distributes over union). Let L 1 and L 2 be two languages, then we have foot

G (L 1 ∪ L 2 ) = foot G (L 1 ) ∪ foot G (L 2 ).
Proof. If one of the languages contains a word with a prohibited factor, its footprint will be , as will be the union of the footprints and the footprint of the union. Otherwise, the result follows from the fact that the set of factors (resp. left or right) of a language is the set containing all the factors (resp. left or right) of its words.

⊓ ⊔ Definition 14 (Concatenation of G-footprints). Let G = (Σ, S, s 0 , ζ, s F ) be a global policy. We define the concatenation of two G-footprints depending on their forms.

. = (LF 1 , F 1 , RF 1 ). = .(LF 2 , F 2 , RF 2 ) = (LF 1 , F 1 , RF 1 ).(LF 2 , F 2 , RF 2 ) =            if RF 1 .LF 2 ∩ L(G) = ∅ ( LF 1 ∪ (F 1 .LF 2 ∩ rf (L(G))), F 1 .F 2 ∩ fact(L(G)), RF 2 ∪ (RF 1 .F 2 ∩ lf (L(G))) ) otherwise
Clearly, the concatenation is not commutative, but it has the following property: Lemma 2. The concatenation of footprints is associative.

Proof. Let us consider three footprints. If one of them is , the result is immediate. Otherwise, we want to show that

((L 1 , F 1 , R 1 ).(L 2 , F 2 , R 2 )).(L 3 , F 3 , R 3 ) = (L 1 , F 1 , R 1 ).((L 2 , F 2 , R 2 ).(L 3 , F 3 , R 3 )).
Let us give names to the two sides:

Res 1 = ((L 1 , F 1 , R 1 ).(L 2 , F 2 , R 2 )).(L 3 , F 3 , R 3 ) Res 2 = (L 1 , F 1 , R 1 ).((L 2 , F 2 , R 2 ).(L 3 , F 3 , R 3 )) We have (L 1 , F 1 , R 1 ).(L 2 , F 2 , R 2 ) = only when R 1 .L 2 ∩ L(G) = ∅. On the other side, if (L 2 , F 2 , R 2 ).(L 3 , F 3 , R 3 ) = , the results will obviously coincide. Otherwise, the left factor of (L 2 , F 2 , R 2 ).(L 3 , F 3 , R 3 ) will contain L 2 so (L 1 , F 1 , R 1 ).((L 2 , F 2 , R 2 ).(L 3 , F 3 , R 3 )) will be forced to be too. The converse is similar. Let us develop further if (L 1 , F 1 , R 1 ).(L 2 , F 2 , R 2 ) = and (L 2 , F 2 , R 2 ).(L 3 , F 3 , R 3 ) = . Res 1 = (L 1 ∪ (F 1 .L 2 ∩ rf (L(G))), F 1 .F 2 ∩ fact(L(G)), R 2 ∪ (R 1 .F 2 ∩ lf (L(G))).(L 3 , F 3 , R 3 ) Res 2 = (L 1 , F 1 , R 1 ).(L 2 ∪ (F 2 .L 3 ∩ rf (L(G))), F 2 .F 3 ∩ fact(L(G)), R 3 ∪ (R 2 .F 3 ∩ lf (L(G)))) If Res 1 = then (R 2 ∪ R 1 .F 2 ).L 3 ∩ L(G) = ∅. Since (L 2 , F 2 , R 2 ).(L 3 , F 3 , R 3 ) = , that would mean R 1 .F 2 .L 3 ∩ L(G) = ∅. This would mean that R 1 .(F 2 .L 3 ∩ rf (L(G))) ∩ L(G) = ∅ so Res 2 = .
The converse is similar. Assuming that Res 1 = and Res 2 = , we finish developing the two terms.

Res 1 = ((L 1 ∪ (F 1 .L 2 ∩ rf (L(G)))) ∪ ((F 1 .F 2 ∩ fact(L(G))).L 3 ∩ rf (L(G))), (F 1 .F 2 ∩ fact(L(G))).F 3 ∩ fact(L(G)), A) Res 2 = (L 1 ∪ (F 1 .(L 2 ∪ (F 2 .L 3 ∩ rf (L(G)))) ∩ rf (L(G))), F 1 .(F 2 .F 3 ∩ fact(L(G))) ∩ fact(L(G)), B)
We first consider factors (second component) of Res 1 and Res 2 :

(F 1 .F 2 ∩ fact(L(G))).F 3 ∩ fact(L(G)) and F 1 .(F 2 .F 3 ∩ fact(L(G))) ∩ fact(L(G)).
In both cases, if u is a word of the language, u is a word of fact(L(G)) that is composed of three factors: u = u 1 .u 2 .u 3 with u i ∈ F i , as fact(L(G)) is closed by fact, we get the equality.

We now consider the left factors (first component) of Res 1 and Res 2 :

(L 1 ∪ (F 1 .L 2 ∩ rf (L(G)))) ∪ ((F 1 .F 2 ∩ fact(L(G))).L 3 ∩ rf (L(G))) = L 1 ∪ (F 1 .L 2 ∩ rf (L(G))) ∪ ((F 1 .F 2 ∩ fact(L(G))).L 3 ∩ rf (L(G)))
and

L 1 ∪ (F 1 .(L 2 ∪ (F 2 .L 3 ∩ rf (L(G)))) ∩ rf (L(G))).
So we have to show that

(F 1 .L 2 ∩ rf (L(G))) ∪ ((F 1 .F 2 ∩ fact(L(G))).L 3 ∩ rf (L(G))) = ((F 1 .L 2 ) ∪ ((F 1 .F 2 ∩ fact(L(G))).L 3 )) ∩ rf (L(G))
and

F 1 .(L 2 ∪ (F 2 .L 3 ∩ rf (L(G)))) ∩ rf (L(G)) = (F 1 .L 2 ∪ F 1 .(F 2 .L 3 ∩ rf (L(G)))) ∩ rf (L(G))
are equal. That can be reduced to show that ((

F 1 .F 2 ∩ fact(L(G))).L 3 ) ∩ rf (L(G)) and (F 1 .(F 2 .L 3 ∩ rf (L(G)))) ∩ rf (L(G)) are equal.
In both cases if u is a word of the language, it is composed of three factors: u = u 1 .u 2 .u 3 with u 1 ∈ F 1 , u 2 ∈ F 2 , and u 3 ∈ L 3 . As u belongs to rf (L(G)), obviously u 2 .u 3 ∈ rf (L(G)), and u 1 u 2 ∈ fact(L(G)).

⊓ ⊔

We now show that foot G is an endomorphism, i.e., it somehow "distributes" over concatenation.

Lemma 3 (Footprint is a morphism). Let L 1 and L 2 be two languages, then we have foot

G (L 1 .L 2 ) = foot G (L 1 ).foot G (L 2 ). Proof. If foot G (L 1 ) = or foot G (L 2 ) = , then foot G (L 1 .L 2 ) = because fact(L i ) ⊆ fact(L 1 .L 2 ). Otherwise, let foot G (L 1 ) = (LF 1 , F 1 , RF 1 ) and foot G (L 2 ) = (LF 2 , F 2 , RF 2 ). If we have foot G (L 1 .L 2 ) = ,
we know that there is a factor of L 1 .L 2 in L(G). That factor must be of the form

u 1 .u 2 , with u 1 ∈ rf (Π Σ (L 1 )), u 2 ∈ lf (Π Σ (L 2 )). Obviously, u 1 ∈ lf (L(G)) and u 2 ∈ rf (L(G)). So u 1 ∈ RF 1 and u 2 ∈ LF 2 which implies that RF 1 .LF 2 ∩ L(G) = ∅ so foot G (L 1 ).foot G (L 2 ) = . If foot G (L 1 .L 2 ) = , we have: foot G (L 1 .L 2 ) = (lf (Π Σ (L 1 .L 2 )) ∩ rf (L(G)), Π Σ (L 1 .L 2 ) fact(L(G)), rf (Π Σ (L 1 .L 2 )) ∩ lf (L(G)))
Let us first consider the factors :

Π Σ (L 1 .L 2 ) ∩ fact(L(G)) = (Π Σ (L 1 ).Π Σ (L 2 )) ∩ fact(L(G)) = ((Π Σ (L 1 ) ∩ fact(L(G))).(Π Σ (L 2 ) ∩ fact(L(G)))) ∩ fact(L(G))
For left factors we have:

lf (Π Σ (L 1 .L 2 )) ∩ rf (L(G)) = lf (Π Σ (L 1 ).Π Σ (L 2 )) ∩ rf (L(G)) = (lf (Π Σ (L 1 )) ∪ Π Σ (L 1 ).lf (Π Σ (L 2 ))) ∩ rf (L(G)) = (lf (Π Σ (L 1 )) ∩ rf (L(G))) ∪ (Π Σ (L 1 ).lf (Π Σ (L 2 )) ∩ rf (L(G))) = LF 1 ∪ (Π Σ (L 1 ).lf (Π Σ (L 2 )) ∩ rf (L(G)))
As all the words of rf (L(G))) are concatenations of factors of L(G))

= LF 1 ∪ ((Π Σ (L 1 ) ∩ fact(L(G))).lf (Π Σ (L 2 )) ∩ rf (L(G))) = LF 1 ∪ (F 1 .lf (Π Σ (L 2 )) ∩ rf (L(G)))
Obviously, we have:

= LF 1 ∪ (F 1 .(lf (Π Σ (L 2 )) ∩ rf (L(G))) ∩ rf (L(G))) = LF 1 ∪ (F 1 .LF 2 ∩ rf (L(G)))
and we can obtain the right factors in the same way.

⊓ ⊔

From Lemma 1 and Lemma 3, we get the following proposition:

Proposition 1. For a language L ⊆ M * and a global policy of the system G = (Σ, S, s 0 , ζ, s F ), we have

foot G (L) = m 0 m 1 . . . mn ∈ L | ∀0 ≤ i ≤ n, m i ∈ M foot G ({m 0 }).foot G ({m 1 }) . . . foot G ({m n }).

Compositionality of the footprint computation

The G-footprints of methods can be computed in a compositional way except in the presence of mutual recursive methods that have to be analyzed together. For a method m, we compute the strongly connected components of the graph CG m . Starting from m, we have a partial order of components as the transitive closure of the relation saying that a component c 1 is lower than a component c 2 if there exists an edge from c 1 to c 2 . Then, the methods of each strongly connected component have to be analyzed together, when all the greater components have been analyzed (i.e., when their footprints are available). The proof of the next proposition is straightforward from Proposition 1.

Proposition 2 (Compositionality). Let us consider a method m and a global policy of the system G = (Σ, S, s 0 , ζ, s F ), and M the set of methods of the strongly connected component of CG m that contains m. Then,

foot G (traces(m)) = compose G,M (calls(paths(ICFG M , m.0, {m.i | P m [i] = return}))) with the morphism compose G,M : M -→ F G m ′ -→ foot G ({m ′ }) if m ′ ∈ M foot G (traces(m ′ )) otherwise

Implementation of the footprint computation

Since we target small systems, we need to provide a compact representation of footprints that uses as little memory as possible and that is easy to manipulate. For this purpose, we use sets of pairs of automaton states to represent footprints. Using this representation, we only need one set to describe one footprint since left factors obviously end at s F and right factors obviously start at s 0 .

Definition 15 (G-footprint implementation). Let G be a global policy of the system. The G-footprint implementation is given by the function:

Φ : F G -→ ℘(S × S) -→ {(s i , s j ) | ∀s i , s j ∈ S} (LF, F, RF ) -→ {(s i , s j ) | ∃u ∈ F, ζ(s i , u) = s j } ∪ {(s 0 , s i ) | ∃u ∈ RF, ζ(s 0 , u) = s i } ∪ {(s i , s F ) | ∃u ∈ LF, ζ(s i , u) = s F }
We write F m for the implementation of the G-footprint of a method m, namely F m = Φ(foot G (traces(m))).

We now define the composition of footprint implementations.

Definition 16 (Composition). The composition over ℘(S × S) is defined as, for S 1 and S 2 :

S 1 ⊕ S 2 = {(s i , s F ) | (s i , s F ) ∈ S 1 } ∪ {(s 0 , s i ) | (s 0 , s i ) ∈ S 2 } ∪ {(s i , s j ) | ∃k, (s i , s k ) ∈ S 1 , (s k , s j ) ∈ S 2 or ∃k, (s 0 , s k ) ∈ S 1 , (s k , s F ) ∈ S 2 or (s 0 , s F ) ∈ S 1 ∪ S 2 }
Note that the definition forces the composition to be the full set S ×S as soon as it contains (s 0 , s F ). It is easy to see that {(s i , s j ) | ∀s i , s j ∈ S} is absorbing for ⊕: this corresponds to the element for normal footprints. So we will also write for the full set S × S.

Lemma 4. Let S 1 , S 2 , S 3 and S 4 be elements of ℘(S × S). The composition is monotonic: if S 1 ⊆ S 2 and S 3 ⊆ S 4 then S 1 ⊕ S 3 ⊆ S 2 ⊕ S 4 .

Lemma 5. Φ is a morphism, i.e., Φ(f

1 .f 2 ) = Φ(f 1 ) ⊕ Φ(f 2 ).
Proof.

If f i = , then f 1 .f 2 = and Φ(f i ) = Φ(f 1 .f 2 ) = which will absorb Φ(f 3-i ).
Let us then assume that f 1 = and f 2 = . We write

f 1 = (LF 1 , F 1 , RF 1 ) and f 2 = (LF , F 2 , RF 2 ). Let us first prove that Φ(f 1 .f 2 ) ⊆ Φ(f 1 ) ⊕ Φ(f 2 ). If f 1 .f 2 = , this means that RF 1 .LF 2 ∩ L(G) = ∅. So we have some u = u 1 .u 2 such that u 1 ∈ RF 1 and u 2 ∈ LF 2 and u ∈ L(G), which means that ζ(s 0 , u) = ζ(ζ(s 0 , u 1 ), u 2 ) = s F .
From this, we conclude that (s 0 , ζ(s 0 , u 1 )) ∈ Φ(f 1 ) and (ζ(s 0 , u 1 ), s F ) ∈ Φ(f 2 ) and so that Φ(f 1 ) ⊕ Φ(f 2 ) = since it contains (s 0 , s F ). Let us now assume that f 1 .f 2 = and write f 1 .f 2 = (LF, F, RF ). We consider each of the three sub-sets composing Φ(f i ) separately. We have F = F 1 .F 2 ∩ fact(L(G)). Let us consider some u ∈ F . We know that there exist u 1 and u 2 such that u = u 1 .u 2 , with u 1 ∈ F 1 and u 2 ∈ F 2 . If we consider a pair of states (s i , s j ) such that ζ(s i , u) = s j , we know that ζ(s i , u 1 ) is some state s k and that (s i , s k ) must be in Φ(f 1 ) and that (s k , s j ) must be in

Φ(f 2 ) since ζ(s k , u 2 ) = s j , by definition of Φ. So (s i , s j ) ∈ Φ(f 1 ) ⊕ Φ(f 2 ). We have LF = LF 1 ∪ (F 1 .LF 2 ∩ rf (L(G))
). Let us consider some u ∈ LF and (s i , s F ) a pair of states such that ζ(s i , u) = s F . If u ∈ LF 1 , then (s i , s F ) must be in Φ(f 1 ) by definition of Φ; and so it is preserved by ⊕. Otherwise, we must have u ∈ F 1 .LF 2 so u = u 1 .u 2 with u 1 ∈ F 1 and u 2 ∈ LF 2 . So ζ(s i , u 1 ) must be some state s j with ζ(s j , u 2 ) = s F . By definition of Φ, we have (s i , s j ) ∈ Φ(f 1 ) and (s j , s F ) ∈ Φ(f 2 ) which entails that (s i , s F ) is in Φ(f 1 ) ⊕ Φ(f 2 ). By a similar argument we prove that the image of RF is also included in Φ(f 1 ) ⊕ Φ(f 2 ). Conversely, let us prove that Φ(f 1 ) ⊕ Φ(f 2 ) ⊆ Φ(f 1 .f 2 ). Let us consider for this (s i , s j ) in Φ(f 1 ) ⊕ Φ(f 2 ). We reason over the three definition cases of ⊕.

1. s j = s F and (s i , s F ) ∈ Φ(f 1 ); then there exists some u such that ζ(s i , u) = s F by definition of Φ and so u must be in RF 1 ∪ F 1 ∪ LF 1 . In all three sub-cases, since it is a right factor of L(G) (because it can end in s F ) it must also be in LF 1 . This entails that it is in LF by definition of concatenation so (s i , s F ) is in Φ(f 1 .f 2 ). 2. s i = s 0 and (s 0 , s j ) ∈ Φ(f 2 ). This case is similar to the previous one.

We have again three sub-cases.

-There exists some s k such that (s i , s k ) ∈ Φ(f 1 ) and (s k , s j ) ∈ Φ(f 2 ). So we can find

u 1 ∈ RF 1 ∪ F 1 ∪ LF 1 such that ζ(s i , u 1 ) = s k and u 2 ∈ RF 2 ∪ F 2 ∪ LF 2 such that ζ(s k , u 2 ) = s j . • If u 1 ∈ LF 1 , then s j = s k = s F and u 2 must be ε since there is no transition out of s F . Then u = u 1 is in LF and (s i , s F ) is in Φ(f 1 .f 2 ). • If u 2 ∈ RF 2 , then s i = s k = s 0 and u 1 must be ε since there is no transition to s 0 . Then u = u 2 is in RF and (s 0 , s j ) is in Φ(f 1 .f 2 ). • If u 1 ∈ F 1 and u 2 ∈ LF 2 , then s j = s F and we just need to show that u 1 .u 2 is in rf (L(G)) to prove that u 1 .u 2 is in LF . Since G is trimmed, there must exist some word v such that ζ(s 0 , v) = s i so u 1 .u 2 is indeed a right factor of L(G), which proves that (s i , s F ) is in Φ(f 1 .f 2 ). • If u 1 ∈ F 1 and u 2 ∈ F 2 , since the automaton is trimmed, u 1 .u 2 is a factor of L(G)
and is in the factors of

f 1 .f 2 so (s i , s j ) is in Φ(f 1 .f 2 ). • If u 1 ∈ RF 1 and u 2 ∈ LF 2 then u 1 .u 2 ∈ L(G) so RF 1 .LF 2 ∩ L(G) = ∅ so f 1 .f 2 = in which case (s i , s j ) ∈ Φ(f 1 .f 2 ) = . • If u 1 ∈ RF 1 and u 2 ∈ F 2 ,
then s i = s 0 and there must exist some word v such that

ζ(ζ(s 0 , u 1 .u 2 ), v) = s F since G is trimmed. So u = u 1 .u 2 is a left factor of L(G), so u must be in the right factors of f 1 .f 2 which entails that (s 0 , sj) ∈ Φ(f 1 .f 2 ). -If (s i s j ) is present because there is some k such that (s 0 , s k ) ∈ Φ(f 1 ) and (s k , s F ) ∈ Φ(f 2 )
this means that there is some word u 1 such that ζ(s 0 , u 1 ) = s k with u 1 in the right factors of f 1 (because the factors of f 1 that are in lf (L(G)) are also in the right factors; and if u 1 is in the left factors, then s k = s F so it is also in the right factors) and some

u 2 such that ζ(s k , u 2 ) = s F with u 2 in the left factors of f 2 , so f 1 .f 2 = and (s i , s j ) ∈ Φ(f 1 .f 2 ). -Lastly, if (s 0 , s F ) is in Φ(f 1 ), then we must have f 1 =
by definition of footprints, since it means that a factor of the underlying language of traces is prohibited. Then

f 1 .f 2 = and Φ(f 1 .f 2 ) = so (s i , s j ) ∈ Φ(f 1 .f 2 ). ⊓ ⊔
Φ also distributes over ∪.

Lemma 6. For any f 1 and

f 2 two footprints, Φ(f 1 ∪ f 2 ) = Φ(f 1 ) ∪ Φ(f 2 ).
Proof. Let us consider f 1 and f 2 two footprints. If

f 1 = , Φ(f 1 ∪f 2 ) = Φ( ) = = ∪Φ(f 2 ).
The result is identical if f 2 = . If neither of them is , we write f 1 = (LF 1 , F 1 , RF 1 ) and

f 2 = (LF 2 , F 2 , RF 2 ). f 1 ∪ f 2 = (LF 1 ∪ LF 2 , F 1 ∪ F 2 , RF 1 ∪ RF 2
) and the definition of Φ allows us to conclude.

⊓ ⊔

In the rest of this section, we define a system of equations that allows us to compute the footprint implementation of a method that corresponds to the G-footprint of a method m.

For each method m we consider M the set of methods of the strongly connected component of CG m that contains m. We define the system of equations (S M ) where the rules instr are given on Figure 1:

S m ′′ .i = (m ′ .j,m ′′ .i)∈ICFG M instr P m ′ [j] (S m ′ .j )
with the initial state

S m.0 ⊇ {(s i , s i ) | s i ∈ S} ∪ {(s i , s j ) | s i , s j ∈ S if s 0 = s F } when m ∈ Σ {(s i , s j ) | s i , s j ∈ S, ζ(s i , m) = s j or ζ(s 0 , m) = s F }} when m ∈ Σ
Note that the last rule of Figure 1 takes the union of the footprint implementations of all the actual methods that could be invoked by the instruction. Proposition 3. The system of equations (S M ) admits a least solution.

Proof. The set (℘(S×S), ⊆, ∪, ∩) is a finite lattice. Lemma 4 implies that the transfer functions instr b are monotonic with respect to ⊆. Thus we can apply Knaster-Tarski theorem. Finally we prove that this least fix-point construction implements footprints.

⊓ ⊔ b = invoke instr b (S) = S b = invoke m ′ and m ′ ∈ Σ and m ′ ∈ M instr b (S) = S ⊕ Φ(foot G ({m ′ })) b = invoke m ′ and m ′ ∈ Σ and m ′ ∈ M instr b (S) = S b = invoke m ′ and m ′ ∈ M instr b (S) = S ⊕ m ′′ ≤m ′ F m ′′
Proposition 4. Let m be a method, M the set of methods of the strongly connected component of CG m that contains Then

F m = i|Pm[i]=return S i
with S i the least solutions of the equations of (S M ).

Note that this property justifies the last rule of Figure 1: the computation of the solution of (S M ) can be based on the footprint implementations of all the methods that are not in the same strongly connected component of the call graph since that will result in the same value. And this proves that the system of equations indeed provides a way to compute the footprint implementations.

Proof. Let us write

U = i|Pm[i]=return

S

and let us first prove that F m ⊆ U .

F m = Φ(foot G (traces(m))) = Φ( t∈traces(m) foot G ({t})) = Φ( m 1 ...mn∈traces(m) foot G ({m 1 }) . . . foot G ({m n })) = m 1 ...mn∈traces(m) Φ(foot G ({m 1 })) ⊕ • • • ⊕ Φ(foot G ({m n }))
Let us consider any pair in F m and some trace t of m so that the pair is in Φ(foot G ({t})). Since traces come from actual execution paths, we consider a path p in CG m such that it produces t. Let us sum up the constraints on (S M ) we obtain by looking at that path p. p can be written as (m j 0 .i j 0 ) . . . (m jq .i jq ) where at each step j k the instruction i j k of method m j k is executed.

Let us reason on the length of p to show that, if we consider a prefix path p ′ of p of any length, the set S m ′ .i ′ must contain Φ(foot G (t ′ )) where t ′ is the part of t corresponding to p ′ . If m ∈ Σ, every trace of m begins with m. In that case we also know that Φ(foot G ({m})) ⊆ S m.0 by definition of the initial state of the system (S M ). Otherwise, S m.0 initially contains simply Φ(foot G ({ε})).

Let us add one instruction to p ′ . For all instruction P m j k [i j k ] along p that is not an invoke, we simply learn that S m j k .i j k ⊇ S m j k -1 .i j k -1 by the rules of Figure 1. Correspondingly, t ′ is not extended by a non-invoke instruction.

If the added instruction is P m j k [i j k ] = invoke m ′ , we have to consider the various possibilities for m ′ :

if m ′ ∈ Σ and m ′ ∈ M , t ′ is left unmodified and S m j k .i j k ⊇ S m j k -1 .i j k -1 ensures the result; -if m ′ ∈ Σ and m ′ ∈ M , m ′ is appended to t ′ and we know that we have

S m j k .i j k ⊇ S m j k -1 .i j k -1 ⊕ Φ(foot G ({m ′ })); by Lemma 4, Φ(foot G ({t ′ })) ⊆ S m j k -1 .i j k -1 entails that Φ(foot G ({t ′ })) ⊕ Φ(foot G ({m ′ })) ⊆ S m j k .i j k ,
if m ′ ∈ M , the fragment t ′′ of the trace that corresponds to the call of m ′ is such that

Φ(foot G ({t ′′ })) ⊆ m ′′ ≤m ′ F m ′′
since t ′′ is a trace of one such method m ′′ ; so, by Lemma 4 we get

Φ(foot G ({t ′ })) ⊕ Φ(foot G ({t ′′ })) ⊆ S m j k -1 .i j k -1 ⊕ m ′′ ≤m ′ F m ′′ ⊆ S m j k .i j k .
We with the fact that

F m = i|Pm[i]=return R m.i .
We can show that, for any edge (m ′ .j ′ , m ′′ .j ′′ ) in ICFG M , R m ′′ .j ′′ ⊇ instr P m ′ [j ′ ] (R m ′ .j ′ ) by cases over the definition of instr b in a similar way to previously shown. Since U is the least solution of (S M ), we directly get that

S m ′ .i ′ ⊆ R m ′ .i ′ for all m ′ .i ′ ∈ ICFG M . Therefore U = i|Pm[i]=return S m.i ⊆ i|Pm[i]=return R m.i = F m ,
which concludes the proof.

⊓ ⊔

This proof uses some property of interest to embed the verification. As we noticed just above, as soon as we have a set of R m ′ .i ′ such that, for any edge (m ′ .j ′ , m ′′ .j ′′ ) in ICFG M , R m ′′ .j ′′ ⊇ instr P m ′ [j ′ ] (R m ′ .j ′ ), then the union of footprints at all return instructions must contain F m , since it is the least such set. This means that checking for those inclusions will provide a low-complexity technique to ensure that a declared footprint for a method m is safe, i.e., it is an over-approximation of F m . This also means that the footprint implementation against which some method bytecode will be verified can be any such over-approximation: to handle method overloading we will only use the union of all the footprints of methods in one class and its subclasses.

On-device verification

The computation of footprints uses a fix-point computation, it is thus too heavy for the computation capabilities of target devices such as mobile phones or smart-card. For this reason, we use a proof-carrying code approach [START_REF] Necula | Proof-carrying code[END_REF] analog to Rose [START_REF] Rose | Lightweight bytecode verification[END_REF] developed for Java bytecode type verification.

Encoding of the embedded proof

Each class file is analyzed off-board, either alone or with the methods of its strongly connected component when needed. Then, metadata have to be shipped with the code. For traditional Java environments, they are added to the class file in the form of class file attributes. Java Card platforms (2.x and 3.x Classic) do not accept class files directly but rely on the CAP file structure that is a specific class files bundle. This structure admits "Custom Components" where footprints can be stored and retrieved during the loading process. Whatever the target platform, we need:

for each method m of the class:

• the over-approximated footprint F m of m, so that every method m ′ such that m ′ ≤ m has a footprint included in F m , • "proof annotations" that is the list of intermediate footprints computed externally for all i such that P m [i] is the target of a jump, proof annotations are encoded in the array proof [i] in Algorithm 5.1, -for each method m that is invoked by methods m 0 , . . . , m n of the class :

• "believed footprint" that is the footprint F m of m that has been used in composition to compute the footprints of the methods m 0 , . . . , m n .

Let us consider a system with a global policy G = (Σ, S, s 0 , ζ, s F ). Footprints are encoded in a binary form, if S contains n elements, s 0 is the initial state, s F is denoted s n-1 , and then we need n × (n -1) bits for a footprint and the bit 0 ≤ i < n × (n -1) encodes the presence of (s i/n , s i mod n ) in the footprint of m. For readability of the rest of this section, we use the array notation and denotes by F m [i] the (i + 1)-th bit of F m .

The empty footprint is encoded by ⊥ (all bits set to zero), and the fully saturated footprint denoted in the formal model is encoded by the footprint value ⊤ (all bits are set to one).

On-device metadata

To manage methods footprints on-device, we use two repositories: R which maps the verified methods to their footprints, and R tmp the temporary repository which maps methods that are not loaded to their believed footprints.

The global policy G = (Σ, S, s 0 , ζ, s F ) is an automaton on a subset of the methods, thus we need to record it on the embedded system and especially Σ and ζ. The global policy G is encoded by an array of footprints G such that:

G[A.C.m] =    ⊥ if m = Σ {(s i , s j ) | ζ(s i , A.C.m) = s j ∨ (ζ(s i , A ′ .C ′ .m ′ ) = s j ∧ A.C.m ≤ A ′ .C ′ .m ′ )} otherwise footprint in R tmp for A ′ .C ′ .m ′ (⊤ by
default) is restricted to its common parts with the believed footprint F A ′ .C ′ .m ′ coming with the currently verified application; since this restriction can only remove factors contributing to invalid traces, it cannot cause methods already loaded and successfully verified with the previous footprint to be rejected if they were re-verified with the restricted footprint. Then, for each believed footprint, we check line 5 if it is valid, if it conforms to the believed ones of the applications already loaded on the system, and if it is compliant with the class hierarchy line 6.

Then, the last part of the algorithm verifies the proof of the footprint of the method without any fix-point computation. For each branching bytecode, we just have to verify that the computed footprint is lower than the proof annotation. To avoid cycles in the verification algorithm, for each bytecode that has a proof annotation, we use it as current state instead of the computed one as seen line 13, after verification that the current state is included in the proof annotation line 12. Only invocation bytecodes have an impact on the footprint: we compose (see Algorithm 5.2) the current footprint with the footprint of the invoked method if it is already verified line 16, with the believed ones otherwise line 18. For the return bytecode, we only have to verify that the current state is compliant with the footprint announced for the method line 19.

Lastly, for branching bytecodes, we have to check that the target bytecode has been annotated and that the current state is included in the proof annotation of the target line 22, and if the bytecode always branches (goto, return, etc.), we have to reset the current state line 23, before analyzing the next bytecode.

Algorithm 5.2 implements the composition in a different way from the formal definition. The composition of F 1 and F 2 computed here is only the union of:

-{(s i , s j ) | ∃k, (s i , s k ) ∈ F 1 , (s k , s j ) ∈ F 2 }, implemented by lines 2 to 5, -{(s 0 , s i ) ∈ F 2 }, line 7, -{(s i , s F ) ∈ F 1 }, line 8.
Instead of saturating the composition as soon as (s 0 , s F ) is found in it, since the actual implementation must directly reject the code, we simply test after this computation whether (s 0 , s F ) was added and fail if this is the case.

1: Let Fres be initialized to 0 2: for all 0 ≤ i < n -1 do 3:

for all 0 ≤ j < n such that F1[i × n + j] == 1 do 4:

for all 0 ≤ k < n such that F2[j × n + k] == 1 do 5:

Fres[i × n + k] = 1 6: for all 0 ≤ i < n do 7:

Fres

[i] = Fres[i]|F2[i] 8:
Fres

[i × n + n -1] = Fres[i × n + n -1]|F1[i × n + n -1]
Algorithm 5.2: Composition of footprint: compose (F 1 , F 2 ).

Extension of the verification to removal of applications

We have proposed a model that allows an issuer to define a global policy of a system, and an incremental verification designed to avoid re-verification of already loaded bytecode. In order to keep this last property while dealing with applications removal, we have to keep additional metadata on-device. When an application A is successfully verified and installed, all the believed footprints of A's methods are removed from the temporary repository R tmp , and the verified footprints of A's methods are stored in R. Moreover, if A invokes some shared methods of other applications not yet installed, then the believed footprints of these methods have been updated to intersect with the believed footprints brought by A. In order to remove A, we have to be able to restore the temporary repository. To achieve this reset, it is mandatory to keep all the individual believed footprints of shared methods, and not only an aggregation of these footprints, brought by applications until there are uninstalled.

Concretely, a new repository F restore is defined to gather the collection of believed footprints coming with each application. We choose to still maintain R tmp in a incremental way (line 3 of Algorithm 5.1) to avoid multiple comparisons (line 5 of Algorithm 5.1) with all believed footprints now stored in F restore . However, R tmp can be removed to reduce memory requirements if necessary, which will conversely increase the number of required comparisons. Indeed, in case R tmp is removed, each expression of the form Upon removal of an application A, the believed footprints of the external methods invoked by A must be restored. This last operation requires to recompute the believed footprints according to the collection of believed footprints of all external methods brought by applications remaining installed, as depicted in Algorithm 5.3. Finally, the removal of an application A must reset the verified footprint of each method of A to its default value ⊥ in R (line 5 of Algorithm 5.3).

Conclusion

In this paper we have proposed a powerful technique to enforce control flow policies on Java bytecode in open and constrained systems. Our approach is purely static so it does not require any execution monitoring, which is a better approach for strongly constrained devices such as smart cards. Moreover, the incremental and compositional verification scheme of our approach permits to efficiently deal with post-issuance (un)installation of applications without the need to re-verify already loaded code. As we use a proof-carrying code approach, no code-signing mechanism is required for the device to be protected against code originating INRIA from an untrusted origin or transmitted through an unsecure communication channel, which is crucial for open devices. The main issue we still have to face is the monolithic security policy stored on-device that impacts security policy updates. Further works will focus on an efficient way to update the security policy on-device.

Fig. 1 .

 1 Fig. 1. Transfer function instr b (S).

  thus easily conclude that Φ(foot G ({t})) ⊆ U and consequently that F m ⊆ U . Let us prove the converse, U ⊆ F m , by considering the set of definitions (R M ): R m ′ .i = p∈paths(ICFG M ,{m.0},{m ′ .i}) Φ(foot G ({m.calls(p)}))

  F A.C.m ⊆ R tmp [A.C.m] has to be replaced by its equivalent: there exist an installed applicationA ′ such that F A.C.m ⊆ F restore [A.C.m][A ′ ].Composition is not done with verified footprints anymore but with the believed ones brought on by the application itself. Thus, we apply the following modifications in Algorithm 5.1:lines 15 -18: -→ F tmp = compose(F tmp , F A ′ .C ′ .m ′ ) line 26: -→ store each F A ′ .C ′ .m ′ in F restore [A ′ .C ′ .m ′ ][A]

1 :Algorithm 5 . 3 :

 153 for all Frestore [A.C.m] do 2: Rtmp[A.C.m] = ⊤ 3: for all A ′ ∈ A do 4: Rtmp[A.C.m] = Rtmp[A.C.m]&Frestore [A.C.m][A ′ ] 5: for all A.C.m do 6: R[A.C.m] = ⊥ Rollback after the removal of an application.

  Definition 2 (Intraprocedural control flow graph). The intraprocedural control flow graph of a method m is an unlabeled graph CF m = (P m , E) such that (i, i ′ ) belongs to E if either (1) i ′ = i + 1 and P m [i] is different from a return bytecode and from goto a, or (2) i ′ = a and P m [i] is equal to goto a or to a comparison (or similar cases) bytecode ifcmp a. Hence, there is no edge going out of the vertex i if P C.m [i] is a return bytecode. An exit-point in a control flow graph is a vertex without successor.

	Definition 1 (Call graph for a set of methods). Let M be a set of methods. A call graph
	for M is a finite graph CG = (M, E), E ⊆ M × M × N, such that: for each m 1 ∈ M , for each instruction P m 1 [i] = invoke 1 m 2 , for all m ′ 2 ≤ m 2 that might be called at run-time by this instruction (m 1 , m ′ 2 , i) ∈ E. 2

RR n°7584

invoke stands for any invocation bytecode like invokevirtual, invokestatic, etc.RR n°7584

The system starts with no application installed, no method has a verified footprint so each method is assigned the encoded empty footprint ⊥. On the contrary, each method is assigned in the temporary repository the fully saturated footprint: this default value denotes the "worst" possible footprint of method; this assumption is mandatory to be able to reject a method during its verification if it invokes another method for which no footprint is known in R or in R tmp . Thus, repositories are initialized such that:

the repository R of verified methods footprints is empty: R[m] = ⊥ for all methods m; -the temporary repository R tmp of methods footprints is set to the maximum value: R tmp [m] = ⊤ for all methods m, since we will restrict it step by step using intersection.

Verification algorithm

The verification algorithm is given by the Algorithm 5.1. For a policy of n states, a footprint is a vector of n × (n -1) bits. Then the basic operations are encoded in the following way:

nonvalid(F m ) is (F m &mask == mask) with mask the vector that encodes {(s 0 , s n-1 )}, i.e., all bits equal to 0 except the bit n -1, for all bytecode i from 0 to end do 11:

if From lines 2 to 3, we check the believed footprints: if a verified footprint for the same method already exists on the device, the shipped one must conform to it, then the believed


MD Merja Kataja-Tuomola
email: merja.kataja-tuomola@thl.fi

Jari Sundell

Satu Männistö

Mikko J Virtanen

Jukka Kontto

Demetrius Albanes

Jarmo Virtamo

2 diabetes in Finnish male smokers

Keywords: Cohort study, diabetes, weight change, weight fluctuation ATBC Study Alpha-Tocopherol, Beta-Carotene Cancer Prevention Study

à 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

Obesity, physical inactivity and smoking are established and modifiable risk factors for type 2 diabetes [START_REF] Paffenbarger | Chronic disease in former college students. XII. Early precursors of adult-onset diabetes mellitus[END_REF][START_REF] Modan | Effect of past and concurrent body mass index on prevalence of glucose intolerance and Type 2 (non-insulin-dependent) diabetes and on insulin response[END_REF][START_REF] Burchfiel | Incidence and predictors of diabetes in Japanese-American men. The Honolulu Heart Program[END_REF][START_REF] Medalie | Major factors in the development of diabetes mellitus in 10,000 men[END_REF][START_REF] Wilson | Epidemiology of diabetes mellitus in the elderly. The Framingham Study[END_REF][START_REF] Feskens | Cardiovascular risk factors and the 25-year incidence of diabetes mellitus in middle-aged men. The Zutphen Study[END_REF][START_REF] Ohlson | Risk factors for type 2 (non-insulin-dependent) diabetes mellitus. Thirteen and one-half years of follow-up of the participants in a study of Swedish men born in 1913[END_REF][START_REF] Helmrich | Physical activity and reduced occurrence of non-insulin-dependent diabetes mellitus[END_REF][START_REF] Manson | A prospective study of exercise and incidence of diabetes among US male physicians[END_REF][START_REF] Ford | Weight change and diabetes incidence: findings from a national cohort of US adults[END_REF]. The risk for developing type 2 diabetes also increases with age [START_REF] Burchfiel | Incidence and predictors of diabetes in Japanese-American men. The Honolulu Heart Program[END_REF][START_REF] Medalie | Major factors in the development of diabetes mellitus in 10,000 men[END_REF][START_REF] Feskens | Cardiovascular risk factors and the 25-year incidence of diabetes mellitus in middle-aged men. The Zutphen Study[END_REF]. When dietary and lifestyle factors were analysed simultaneously in the Nurses' Health Study, the most important risk factor for type 2 diabetes was a higher body mass index (BMI, weight (kg)/ height (m) 2 ) [START_REF] Hu | Diet, lifestyle, and the risk of type 2 diabetes mellitus in women[END_REF].

Weight gain has been associated with the risk for type 2 diabetes [START_REF] Ford | Weight change and diabetes incidence: findings from a national cohort of US adults[END_REF][START_REF] Colditz | Weight gain as a risk factor for clinical diabetes mellitus in women[END_REF][START_REF] Schienkiewitz | Body mass index history and risk of type 2 diabetes: results from the European Prospective Investigation into Cancer and Nutrition (EPIC)-Potsdam Study[END_REF][START_REF] Oguma | Weight change and risk of developing type 2 diabetes[END_REF][START_REF] Koh-Banerjee | Changes in body weight and body fat distribution as risk factors for clinical diabetes in US men[END_REF].

Weight loss can prevent or delay the progression to diabetes in obese patients [START_REF] Holbrook | The association of lifetime weight and weight control patterns with diabetes among men and women in an adult community[END_REF][START_REF] Fx | How effective are lifestyle changes in the prevention of type 2 diabetes mellitus?[END_REF], though some studies have linked weight loss to increased risk for diabetes [START_REF] French | Weight variability and incident disease in older women: the Iowa Women's Health Study[END_REF][START_REF] Noppa | Body weight change in relation to incidence of ischemic heart disease and change in risk factors for ischemic heart disease[END_REF].

Unintentional weight regain frequently follows intentional weight loss, thus leading easily to weight cycling, which appears to enhance subsequent weight gain and may predispose one to obesity [START_REF] Blackburn | Weight cycling: the experience of human dieters[END_REF][START_REF] Saarni | Weight cycling of athletes and subsequent weight gain in middleage[END_REF][START_REF] Kroke | Recent weight changes and weight cycling as predictors of subsequent two year weight change in a middle-aged cohort[END_REF][START_REF] Field | Weight cycling and the risk of developing type 2 diabetes among adult women in the United States[END_REF]. Findings concerning the association between weight fluctuation or cycling and the risk for type 2 diabetes remain controversial; three studies have found weight fluctuation to increase the risk for diabetes [START_REF] Holbrook | The association of lifetime weight and weight control patterns with diabetes among men and women in an adult community[END_REF][START_REF] French | Weight variability and incident disease in older women: the Iowa Women's Health Study[END_REF][START_REF] Morris | Long-term weight fluctuation and non-insulindependent diabetes mellitus in white women[END_REF], but other three studies have found no significant association [START_REF] Field | Weight cycling and the risk of developing type 2 diabetes among adult women in the United States[END_REF][START_REF] Hanson | Rate of weight gain, weight fluctuation, and incidence of NIDDM[END_REF][START_REF] Brancati | Body weight patterns from 20 to 49 years of age and subsequent risk for diabetes mellitus: the Johns Hopkins Precursors Study[END_REF].

We studied the association of various weight change patterns, specified as weight gain, weight loss, and weight fluctuation, with the risk for type 2 diabetes in Finnish male smokers who participated in the Alpha-Tocopherol, Beta-Carotene Cancer Prevention Study (ATBC Study).

Methods

The ATBC Study

The primary aim of the ATBC Study was to examine whether supplementation with alpha-tocopherol, beta-carotene, or both would reduce the incidence of lung cancer and other cancers. The study was a randomized, double-blind, placebo-controlled clinical trial with a 2x2 factorial design [START_REF] The | The Alpha-Tocopherol, Beta-Carotene Lung Cancer Prevention Study: design, methods, participant characteristics and compliance[END_REF][START_REF] The | The effect of vitamin E and betacarotene on the incidence of lung cancer and other cancers in male smokers[END_REF]. The participants were screened from among the total male population between the ages of 50 and 69 living in southwestern Finland (n = 290,406). Men were excluded if they smoked fewer than 5 cigarettes per day, had prior cancer or a serious disease limiting long-term participation or used vitamin E, vitamin A or beta-carotene supplements in excess of predefined doses or anticoagulants. A total of 29,133 eligible men were enrolled from 1985 through 1988, and the trial continued until April 1993 (median intervention time: 6.1 years), with the cohort followed up through national registers thereafter. The institutional review boards of the National Public Health Institute, Finland, and the U.S. National Cancer Institute approved the ATBC Study. All subjects provided their written, informed consent prior to randomization.

Subjects and case ascertainment

In Finland, patients needing medical treatment for diabetes are entitled to reimbursement for the cost of medication according to the sickness insurance legislation. This requires a medical certificate from the attending physician. The certificate of every case is verified to fulfill the diagnostic criteria for diabetes at the Social Insurance Institution which maintains a central register of all patients receiving drug reimbursement.

This study included those men (n = 20,952) who had their weight measured at baseline and three times thereafter, one year apart after which the follow-up for diabetes began [Fig. 1]. During a follow-up period of up to 9 years, 535 incident cases of diabetes were diagnosed. 5 97 98 99

Data collection

At baseline, data on medical history, smoking, alcohol consumption and physical activity were collected with questionnaires. Height and weight were measured, and BMI was calculated. Blood pressure was measured with a mercury sphygmomanometer from the right arm with the subject sitting, and the lower reading of the two measurements taken at least one minute apart was recorded. A blood sample was drawn and serum stored at -70°C. Serum glucose was determined with the enzymatic hexokinase method using an Optima analyzer (ThermoFischer, Vantaa, Finland). Serum total and high-density lipoprotein (HDL) cholesterol concentrations were determined enzymatically [START_REF] Kattermann | Multicentre study of a new enzymatic method of cholesterol determination[END_REF][START_REF] Kostner | Enzymatic determination of cholesterol in high density lipoprotein fractions prepared by polyanion precipitation[END_REF].

The participants made a followup visit three times annually, and weight was measured once a year.

Statistics

Person years were calculated from the date of the fourth annual weight measurement to the date of diabetes occurrence, death, or the end of the follow-up period (December 1997), whichever came first. The average trend in weight change was assessed through the slope of the regression line fitted to four weight measurements taken one year apart. The slope was categorized into three classes: below -1.33 (kg/year) for weight loss, between -1.33 and 1.33 for stable weight, and over 1.33 for weight gain. The 1.33 kg/year corresponded to an average weight change of 4 kg over three years. This was similar to a two-year net weight reduction of 2.7 kg, which associated with a 58% reduction in diabetes risk in the Finnish Diabetes Prevention Study [START_REF] Tuomilehto | Prevention of type 2 diabetes mellitus by changes in lifestyle among subjects with impaired glucose tolerance[END_REF].

To examine the association of risk for diabetes with weight fluctuation, we calculated the root mean square error (RMSE) using annual weight deviations from the 6 corresponding estimated regression line [START_REF] French | Weight variability and incident disease in older women: the Iowa Women's Health Study[END_REF][START_REF] Lissner | Body weight variability in men: metabolic rate, health and longevity[END_REF][START_REF] Iribarren | Association of weight loss and weight fluctuation with mortality among Japanese American men[END_REF]. This variable was divided into Stratified analysis was performed in order to assess the possible effect modifications, and the significance of interactions was tested using the likelihood ratio test.

Differences between the groups were tested using analysis of variance (ANOVA).

Analyses were carried out with the R statistical program [START_REF] Ihaka | A language for data analysis and graphics[END_REF]. All p values were twosided.

Results

At baseline, men who gained on average at least 4 kg of weight during the subsequent three years, were slightly younger and had a lower serum total cholesterol concentration than did those whose weight was stable or who lost at least 4 kg of weight (Table 1). Men whose weight fluctuated the most during the subsequent three years (fifth quintile) were younger and less physically active during leisure time, had a higher BMI, but lower serum total cholesterol and HDL cholesterol levels than did men of the four lowest quintiles.

7

The multivariate-adjusted risk for diabetes was higher in men who gained at least 4 kg during three years than in those whose weight was stable (RR = 1.77, 95% CI 1.44-2.17) [Fig. 2]. When compared to those with stable weight, weight loss of at least 4kg was not associated with the risk for diabetes (RR = 1.17, 95% CI 0.90-1.53). Neither BMI, number of cigarettes, years of smoking, alcohol consumption nor physical activity modified the association between short-term weight change and the risk for diabetes. Age, however, did modify the risk for diabetes (p = 0.0067 for weight gain and p = 0.0036 for weight loss). Among those 60 and older at baseline, weight gain as well as weight loss were associated with higher risk for diabetes than among those of stable weight (RR = 3.42, 95% CI 1.70-6.88, and 2.07, 95% CI 1.08-3.99, respectively), whereas among those younger than 60, no association was observed (RR = 1.25, 95% CI 0.90-1.73 and RR = 0.74, 95% CI 0.55-1.01, respectively).

The risk for diabetes in the four lowest quintiles of weight fluctuation was similar, whereas in the highest quintile the risk was higher than in the lowest quintile (RR = 1.64, 95% CI 1.24-2.17) [Fig. 2]. Neither age, BMI, nor number of cigarettes significantly modified the association between short-term weight fluctuation and the risk for diabetes. Leisure time physical activity did modify the risk of diabetes with weight fluctuation (p = 0.02); among those of light leisure time physical activity, large weight fluctuation was associated with increased risk for diabetes (RR = 1.95, 95% CI 1.28-2.98 for the highest vs. lowest quintile), whereas among those with moderate or heavy leisure time physical activity we found no such association (RR = 1.38, 95% CI 0.95-2.00). In addition, years of smoking modified the risk for diabetes (p = 0.04); among those who had smoked less than 36 years, large weight fluctuation increased the risk for diabetes (RR = 1.91, 95% CI 1.27-2.88), whereas among those who had smoked at least 36 years, the association was weaker (RR = 1.43, 95% CI 0.98-2.09).

Finally, the association of weight fluctuation to diabetes risk was stronger in men who consumed on average 11g or more of alcohol daily (RR = 2.17, 95% CI 1.36-3.45) than in men consuming less alcohol (RR = 1.58, 95% CI 1.10-2.28; p = 0.0001).

Both short-term average weight change (slope) and weight fluctuation remained independent risk factors for diabetes when simultaneously adjusted for in the multivariate model: RR = 1.69, 95% CI 1.37-2.07, for a weight increase of at least 4 kg compared with stable weight, and RR = 1.55, 95% CI 1.17-2.06, for the highest vs. lowest weight fluctuation quintile, respectively. Weight gain of at least 4kg in three years, either steady or fluctuating, increased significantly the risk of diabetes about two-fold compared with those whose weight changed less than 4kg and fluctuated only moderately (Table 2). Among men whose weight changed less than 4kg, large weight fluctuation increased the risk of diabetes 1.47-fold, 95% CI 1.14-1.91. Steady loss of weight of at least 4kg was associated non-significantly with decreased risk of diabetes, RR = 0.73, 95% CI 0.47-1.15. However, if weight loss was associated with large weight fluctuation, the risk of diabetes was two-fold compared with those of stable weight and moderate fluctuation, RR = 2.04, 95% CI 1.47-2.83 (Table 2).

Discussion

Short-term weight gain and fluctuation associated with a higher risk for diabetes. The observation is in line with those of other epidemiological studies [START_REF] Ford | Weight change and diabetes incidence: findings from a national cohort of US adults[END_REF][START_REF] Koh-Banerjee | Changes in body weight and body fat distribution as risk factors for clinical diabetes in US men[END_REF]. In the Health Professionals Follow-up Study, weight gain during the preceding ten years was associated with a 1.9 times higher risk for diabetes (95% CI 1.4-2.7) among those 9 who gained 9 kg or more of weight than among those with a stable weight (± 2 kg) [START_REF] Koh-Banerjee | Changes in body weight and body fat distribution as risk factors for clinical diabetes in US men[END_REF]. A parallel observation resulted in the National Health and Nutrition Examination Survey Epidemiologic Follow-up Study, where participants who gained weight at least 5 kg during 9 years had up to 3.85 times the risk for diabetes compared with participants whose weights remained relatively stable [START_REF] Ford | Weight change and diabetes incidence: findings from a national cohort of US adults[END_REF].

An average weight loss of 4 kg in three years was not associated with a lower risk for incident diabetes. This differs from the findings of several prospective cohort and intervention studies where even modest weight loss was associated with a significantly reduced risk for diabetes [START_REF] Colditz | Weight gain as a risk factor for clinical diabetes mellitus in women[END_REF][START_REF] Tuomilehto | Prevention of type 2 diabetes mellitus by changes in lifestyle among subjects with impaired glucose tolerance[END_REF][START_REF] Wannamethee | Overweight and obesity and weight change in middle aged men: impact on cardiovascular disease and diabetes[END_REF][START_REF] Resnick | Relation of weight gain and weight loss on subsequent diabetes risk in overweight adults[END_REF][START_REF] Smith | Incidence of type 2 diabetes in the randomized multiple risk factor intervention trial[END_REF][START_REF] Hamman | Effect of weight loss with lifestyle intervention on risk of diabetes[END_REF][START_REF] Will | Intentional weight loss and 13-year diabetes incidence in overweight adults[END_REF]. In the Finnish Diabetes Prevention Study a net loss of 3.5 ± 5.5 kg by the end of the second year decreased risk of diabetes for 58 % [START_REF] Tuomilehto | Prevention of type 2 diabetes mellitus by changes in lifestyle among subjects with impaired glucose tolerance[END_REF]. In the Nurse's Health Study women who lost more than 5.0 kg reduced their risk for diabetes at least 50% compared to those who maintained a steady weight [START_REF] Colditz | Weight gain as a risk factor for clinical diabetes mellitus in women[END_REF]. In the Diabetes Prevention Program (DPP) study, a 5 kg weight loss accounted for a 55 % reduction in risk of incident diabetes over the mean of 3.2 years of follow-up [START_REF] Hamman | Effect of weight loss with lifestyle intervention on risk of diabetes[END_REF]. Participants with intentional weight loss in the Cancer Prevention Study had a reduction of incident diabetes of about 25% compared with participants with no-intentional weight loss [START_REF] Will | Intentional weight loss and 13-year diabetes incidence in overweight adults[END_REF]. The unintentional weight loss may be an effect of diabetes per se, not a cause of diabetes.

We found that age did modify significantly the association between weight loss and risk of diabetes. Among men 60 years or older weight loss is associated with increased risk, whereas among men younger than 60 years no such an association was evident. In the Iowa Women's Health Study of women aged 55-69 years and in a Swedish study of middle-aged women, weight loss associated with increased risk of diabetes, but effect modification by age was not studied in these materials [START_REF] French | Weight variability and incident disease in older women: the Iowa Women's Health Study[END_REF][START_REF] Noppa | Body weight change in relation to incidence of ischemic heart disease and change in risk factors for ischemic heart disease[END_REF].

The association of weight loss in our study was, however, different depending on whether the weight decreased smoothly or fluctuating. If the weight diminished smoothly, the risk of diabetes was decreased, though not significantly (RR = 0.73, 95% CI 0.47-1.15), which is in line with other studies. The small number of men with smooth weight loss may be the reason why the decrease in risk remained nonsignificant. If the weight loss was associated with large weight fluctuation, it was associated with increased risk of diabetes.

Our results support the hypothesis that weight fluctuation is associated with higher risk for diabetes. In the Iowa Women's Health Study, weight cycling (an increase of ≥ 10% of body weight during a ten-year period and a loss of ≥ 10% of weight during another ten-year period, regardless of order) increased significantly the risk for diabetes (RR = 1.70, 95% CI 1.25-2.29) [START_REF] French | Weight variability and incident disease in older women: the Iowa Women's Health Study[END_REF]. A similarly increased risk was found in an adult community where the adjusted rate ratio for diabetes risk was 1.7 (p < 0.01) for the weight fluctuation (both weight gain and losses of 4.5kg between ages 40 to 60 vs. all others) [START_REF] Holbrook | The association of lifetime weight and weight control patterns with diabetes among men and women in an adult community[END_REF]. In an other cohort study among women, an index of weight fluctuation based on weights in different phases of life associated with diabetes with standardized odds ratio of 1.10 (95% CI 1.07-1.14) [START_REF] Morris | Long-term weight fluctuation and non-insulindependent diabetes mellitus in white women[END_REF]. Supportive evidence comes from the Baltimore Longitudinal Study of Aging, where body weight variability associated with a decrease in glucose tolerance [START_REF] Lissner | Body weight variability in men: metabolic rate, health and longevity[END_REF]. Some studies, however, have found no association between weight fluctuation and the risk for diabetes. In a six-year follow-up of the Nurses' Health Study II, neither mild nor severe weight cycling predicted diabetes [START_REF] Field | Weight cycling and the risk of developing type 2 diabetes among adult women in the United States[END_REF]. In a prospective study among Pima Indians in Arizona, weight fluctuation was not associated with the incidence of diabetes in either sex [START_REF] Hanson | Rate of weight gain, weight fluctuation, and incidence of NIDDM[END_REF]. In the Johns Hopkins Precursors Study the variability in BMI before age 50 predicted incident diabetes only marginally [START_REF] Brancati | Body weight patterns from 20 to 49 years of age and subsequent risk for diabetes mellitus: the Johns Hopkins Precursors Study[END_REF].

Leisure time physical activity modified the association between weight fluctuation and risk of diabetes. Large weight fluctuation increased the risk of diabetes two-fold if only light exercise were taken during leisure time whereas no association was found if exercise was moderate or heavy. This is in keeping with the knowledge that physical activity can prevent diabetes. Regular exercise induces various adaptations in the body resulting in improved muscle and whole body insulin sensitivity, fuel partitioning and cardiovascular function leading to prevention of metabolic disease [START_REF] Christ-Roberts | Exercise training increases glycogen synthase activity and GLUT4 expression but not insulin signaling in overweight nondiabetic and type 2 diabetic subjects[END_REF][START_REF] Perseghin | Increased glucose transport-phosphorylation and muscle glycogen synthesis after exercise training in insulin-resistant subjects[END_REF].

The strengths of our study include the prospective study design, with up to 9-year follow-up for incident diabetes, and data available for several possible risk factors.

Weight and height were measured by trained staff at study centres, not self-reported.

The cases were retrieved from a nationwide register with strict criteria for inclusion.

The trial supplementation had no effect on the incidence of diabetes [START_REF] Kataja-Tuomola | Effect of alpha-tocopherol and beta-carotene supplementation on the incidence of type 2 diabetes[END_REF]. Some limitations should be kept in mind, however, when interpreting these results.

We were able to identify only patients receiving medication for treatment of diabetes, not individuals treating their disease with dietary changes. This will attenuate our estimate between weight indicators and risk of diabetes towards unity. The drug reimbursement register for diabetes contains no data on the type of diabetes.

However, almost all of our diabetes cases would be of type 2 diabetes based on the age of the participants at baseline: 50 to 69 years [START_REF] Laakso | Age of onset and type of diabetes[END_REF]. Some [START_REF] Manson | A prospective study of cigarette smoking and the incidence of diabetes mellitus among US male physicians[END_REF][START_REF] Will | Cigarette smoking and diabetes mellitus: evidence of a positive association from a large prospective cohort study[END_REF] but not all studies [START_REF] Beziaud | Cigarette smoking and diabetes mellitus[END_REF] suggest that smoking cessation may associate with lower risk of diabetes. About 21 % of the ATBC participants stopped smoking during the trial [START_REF] The | The effect of vitamin E and betacarotene on the incidence of lung cancer and other cancers in male smokers[END_REF]. But we do not have smoking data from drop-outs and post-trial follow-up. Thus the possible effects of smoking cessation on our results remain unclear.

For short-term weight change, we had only four weight measurements at intervals of one year and were thus unable to detect weight variations occurring over a shorter period of time. No information on intentionality of weight changes was recorded. In addition, RMSE may have misclassified participants with continuous non-linear weight gain without real weight fluctuation [START_REF] Vergnaud | Weight fluctuations and risk for metabolic syndrome in an adult cohort[END_REF].

The ATBC Study was designed to test whether alpha-tocopherol or beta-carotene could reduce the incidence of lung or other cancers in male smokers, thus our results may not be generalizable to women or non-smokers.

Globally, over one billion adults are overweight, of whom at least 300 million are obese [START_REF]Obesity and overweight Geneva: WHO[END_REF]. If epidemic obesity increases worldwide, the disease burden of type 2 diabetes and cardiovascular diseases will be enormous. Our results confirm that even a short-term weight gain is a risk factor for type 2 diabetes. They also contribute to previous work by demonstrating a significant association between weight fluctuation and higher risk for diabetes. The association between weight fluctuation and risk for diabetes may raise concerns about health-promoting weight-control programs that could result in such cycling. A key target could then be to maintain not only a normal, but a stable body weight in order to optimally lower the risk for diabetes. Footnote to Figure 2 Adjusted for age, intervention (alpha-tocopherol, beta-carotene, both, and placebo), body mass index, smoking, blood pressure, serum total and high density lipoprotein cholesterol, alcohol consumption and leisure time physical activity.

The root mean square error (RMSE) is calculated using annual weight deviations from the corresponding estimated regression line and this variable is divided into quintiles (Q). Q1: -0.54, Q2: 0.55-0.84, Q3: 0.85-1.17, Q4: 1.18-1.67, Q5: 1.68.

  quintiles. Weight fluctuation and weight change were also considered as combined variable, in which case the weight fluctuation was categorized into two classes: Q1-Q4 for minor fluctuation and Q5 for large fluctuation. The association between weight indicators (short-term weight change and weight fluctuation) and the incidence of type 2 diabetes was estimated with the Cox proportional hazards regression as relative risks (RR) and 95% confidence intervals (CI). The basic model was adjusted for age and supplementation group. The model was further adjusted for BMI, years of smoking, number of cigarettes smoked daily, systolic and diastolic blood pressure, serum total and HDL cholesterol, alcohol consumption and leisure time physical activity (sedentary and moderate-heavy).

14 Figure 1 .Figure 2 .

 1412 Figure 1. Diagram of flow of participants through the study

bTable 2 .

 2 Weight change is based on the slope of the regression line fitted to the four weight measurements taken one year apart c Weight fluctuation is the RMSE around the slope Risk for diabetes by weight change and weight fluctuation in three years, in the Alpha-Tocopherol, Beta-Carotene (ATBC) Cancer Prevention Study cohort.

Table 1

 1 Trial baseline characteristics by weight changes during the subsequent three years in the ATBC Cancer Prevention Study

	cohort

Adjusted for baseline age, intervention (alpha-tocopherol, beta-carotene, both and placebo), BMI, smoking, blood pressure, serum total and HDL cholesterol, alcohol consumption and leisure time physical activity a The total number of participants is 20,952 divided in quintiles.