Keywords: Flot d'information, analyse statique, bytecode Java, interpretation abstraite, non-interference

Une analyse de dépendence pour le flot d'information

Résumé : Dans ce rapport, nous présentons une analyse de flot d'information pour le bytecode Java. Notre approche consiste à calculer, pour différents points du programme, un graphe de dépendances qui représente l'influence que les valeurs en entrée d'une méthode ont sur les sorties. Ce calcul inclut une analyse de pointeurs (illustrant les dépendances entre objets) à laquelle sont ajoutées les dépendances issues des données de type primitif et du flot de contrôle du programme. La construction de notre graphe est prouvée correcte par un théoreme de non-interference qui énonce qu'une valeur de sortie n'est pas liée à une valeur d'entrée dans le graphe de dépendances si la valeur de sortie ne change pas lorsque la valeur d'entrée varie. À l'inverse de beaucoup de techniques basées sur des systèmes de types, notre approche ne nécessite pas de connaître la politique de sécurité lors du calcul du graphe : le respest d'une politique de "sécurité" en termes de flot d'information sont vérifiés en étiquetant "a posteriori" le graphe de dépendances avec des niveaux de sécurité.

Introduction

Information flow analysis [START_REF] Sabelfeld | Language-based information-flow security[END_REF] detects how data may flow between variables focusing on data manipulations of primitive types. This analysis is used to check data propagation in programs with regards to security requirements and aims to avoid that programs leak confidential information: observable/public outputs of a program must not disclose information about secret/confidential values manipulated by the program. Noninterference defines the absence of illicit information flow by stating that public outputs of a program remain unchanged if its secret values are modified. Data is labeled with security levels, usually high for secret/confidential values and low for observable/public variables. There are information flows arising from assignments (direct flow) or from the control structure of a program (implicit flow). For example, the code l=h generates a direct flow from h to l, while if(h) then l=1 else l=0 generates an implicit flow. If h has security level high and l low, then the examples are insecure and generate an illicit information flow, as secret data can be induced by the reader of l.

In object oriented languages, like Java [START_REF] Lindholm | Java Virtual Machine Specification[END_REF], the analysis of information flow is related to the analysis of references. Points-to analysis [START_REF] Ole | Program Analysis and Specialization for the C Programming Language[END_REF] is a static analysis which computes for every object the set of objects to which it may point to at runtime. Pointsto analysis [START_REF] Salcianu | Pointer and escape analysis for multithreaded programs[END_REF] has been developed for applications such as escape analysis [START_REF] Whaley | Compositional pointer and escape analysis for Java programs[END_REF] or optimizations, but never used as part of information flow analysis even if they are strongly related.

In this paper we propose a sound general flow-sensitive analysis of Java programs that computes a dependency graph including references and primitive types. The graph is a points-to graph extended with primitive values and dependencies raised by control flow. The dependency graph characterizes on one hand how fields of objects point to other objects, and on the other hand the dependencies between primitive values through direct or indirect flow, in the sense of non-interference. This leads to an analysis which is more general than "traditional" information flow analysis as it computes a dependency graph abstracting the dependencies between program data: a node a is related to b if the value of b may influence the value of a. These dependencies are not made explicit in "traditional" information flow analysis and replaced by coarser flows of security levels from a a priori fixed security lattice [START_REF] Denning | A lattice model of secure information flow[END_REF]. This approach has been initiated by the Volpano, Irvine and Smith's model [START_REF] Volpano | A sound type system for secure flow analysis[END_REF].

In our work, we compute these dependencies between values independently of any a priori information like security levels. Therefore, when applied to secure information flow, our approach allows to reuse the same analysis for various security lattices without re-analysing the code.

Note that our dependency graph should not be confused with data dependency graphs such as [START_REF] Chambers | Dependence analysis for Java[END_REF] which represent dependencies among register and memory reads and write and aim to be used for program slicing.

The language we consider is the Java bytecode language: only few papers [START_REF] Barthe | Security types preserving compilation: (extended abstract)[END_REF][START_REF] Kobayashi | Type-based information flow analysis for low-level languages[END_REF]] take into consideration low-level languages, while the Java language is rarely specified. A type-based method for checking secure information flow in Java bytecode is presented in [START_REF] Bernardeschi | Checking secure information flow in java bytecode by code transformation and standard bytecode verification[END_REF], while in [START_REF] Barthe | A certified lightweight noninterference java bytecode verifier[END_REF] Barthe, Pichardie and Rezk define an information flow type system for a sequential JVM-like language and prove that it guarantees noninterference. Some other works [START_REF] Avvenuti | Java bytecode verification for secure information flow[END_REF][START_REF] Genaim | Information Flow Analysis for Java Bytecode[END_REF][START_REF] Andrew | Jflow: practical mostly-static information flow control[END_REF] use static analysis to treat information flow. The main weakness of these approaches is that they are flow insensitive. Recently, Hunt and Sands proposed a family of flow-sensitive type systems [START_REF] Hunt | On flow-sensitive security types[END_REF] for tracking information flow.

RT n°0347

All the previous cited works require the lattice security model of information flow to be known from the very beginning of the analysis. We believe that "traditional" information flow analysis can be recovered as an abstract interpretation of our dependency graphs, this abstract interpretation taking into account the security levels.

The paper is structured as follows: Section 3 presents the concrete model used in the rest of the paper. Section 4 describes the design and construction of our dependency graph during an intra-method analysis of sequential programs. We present the correctness of the construction in Section 5, using a non-interference theorem. Section 6 describes the inter-procedural analysis and adds support for method invocation. Section 7 applies the dependency graph to information flow.

Notations

We consider finite graphs whose vertices and edges are both labelled. Let V, L two sets used respectively as labels for vertices and edges.

A graph G is given by a triple (V, E, ς) where V is its set of vertices (or nodes), E ⊆ V × V × L is its set of labelled edges and the mapping ς associates a label from V with each element of V . In a graph G, the edge from vertex u to v, labeled with l is denoted by (u, v, l), and adj G (u, l) is the set of adjacent vertices of u in G, reached by an edge labeled by l. Further, G.V denotes its set of vertices and G.E its set of edges; the mapping G.ς(v) gives the label of the node v. A node u is a leaf in a graph G if for any node v and label l, (u, v, l) ∈ G.E.

The union of two graphs G 1 ∪ G 2 (assuming that for all u in

G 1 .V ∩ G 2 .V , G 1 .ς(u) = G 2 .ς(u)) is a graph G 3 , having G 3 .V = G 1 .V ∪ G 2 .V , G 3 .E = G 1 .E ∪ G 2 .E and G 3 .ς = G 1 .ς ∪ G 2 .ς. A graph G 1 is included in a graph G 2 (denoted G 1 ⊆ G 2 ) if there exists a subgraph G 2 of G 2 which is isomorphic 1 to G 1 .
For two graphs G 1 , G 2 , we say that G 1 and G 2 are similar (denoted G 1 ≡ G 2 ) if there exists a mapping ς : G 2 .V → V such that for all u in G 2 .V which is a leaf G 2 .ς(u) = ς(u) and G 1 , (G 2 .V, G 2 .E, ς) are isomorphic.

For a graph G, G[u → l] designates the graph that agrees with G but changes the label of the vertex u to l, while G[(u, f ) → v] agrees with G except that all the edges of the form (u, u , f ) in G.E, are replaced by a unique edge (u, v, l).

A vertex v is reachable from u in a graph G if there is a path (a sequence of edges leading) from u to v and we denote by Reach G (u) the set of vertices reachable from u in G. We define G u the subgraph of G given by (Reach G (u), {(v, w, l) | (v, w, l) ∈ G.E and v, w ∈ Reach G (u)}, ς |ReachG(u) ).

Finally, for a function f , by f [x → e] we denote the function f such that f (y) = f (y) if y = x and f (x) = e. For D, a subset of the domain of the function f , f |D is the restriction of f on D.

The Java Virtual Machine model

This section introduces the syntax and the model of the JVM we consider. Due to limited space, we focus on a general and representative subset of the JVM, depicted in Figure 1. Most of the rest of the JVM instructions are similar to the ones of this set (e.g. we give a hint how static variables and arrays can be treated as objects with prim op primitive operation taking two operands, pushing the result on the stack pop pop the top of the stack iconst n push the primitive value n on the stack aconst null push null on the stack new C creates new object of type C in the memory goto a jump to address a ifeq a jump to address a if the top of the stack equals to 0 load x push the content of the local variable x on the stack store x pop the top of the stack and store it into the local variable x getfield f C load on the stack the field f C of the object beeing on the top of the stack putfield f C store the top of the stack in the field f C of an object on the stack invoke m C virtual invocation of method m C areturn return an object and exit the method Figure 1: Instruction set some special fields). We do not address exceptions and threads but take overwritting into account. We assume the bytecode programs to be well-typed and deal only with executions that terminate and do not throw exceptions. We consider a set of class names Class, a set of methods Methods and a set Fields of fields names.

Memory model

We define the memory as a directed graph. The advantage of this representation is the independence between objects and actual locations where these objects are allocated. However, the graph representing the memory is isomorphic to any address assignment in an execution. This independence property is crucial when comparing memories for two executions of the same method for different input values.

A node designates a location and is labeled with an element from Jv, representing the JVM value stored in the location; edges represent field references and are labeled with field names (from Fields). Nodes containing null or primitive values (from Val ) are leaves.

For a graph G, G.V Obj denotes the nodes labeled by some element from Obj (G.V Obj = {v ∈ G.V | G.ς(v) ∈ Obj }) while G.V Val denotes the sets of nodes labelled by some element from Val. We define by Π Obj (G) the subgraph of G restricted to objects as

(G.V Obj , {(u, v, l) | u, v ∈ G.V Obj and (u, v, l) ∈ G.E}, G.ς |G.V Obj ).
For a memory graph G, G.ς is an injective function associating with each vertex (location) the JVM value (from Jv ) it contains, each object value being associated with a unique location. This allows us to make no distinction between a node of G.V Obj and its label. For l in Obj , we freely use G.ς -1 (l) to denote the (unique) vertex labeled by l in G. Moreover, there exists a unique vertex labelled by null. For each primitive field of an object, the memory has a location (vertex) containing (labeled with) the value of the field and this vertex is the target of a unique edge. We consider an allocator function G = new(o, C) which creates a new graph structure for an object named o of type C; o is labelling the root of the graph. The graph G contains the initial values of the new created object (vartices labeled by 0 for fields of primitive type and edges to null for fields of type object).

Figure 2(a) shows the result of the allocator function for A

Operational semantics

For a method m of class C, n m denotes the number of its arguments, χ m its set of local variables, P m its instruction list; P m [i] denotes the ith bytecode of the method m. A (concrete) state of our machine is a pair Q = (fr , G), where fr represents a stack of frames corresponding to a dynamic chain of method calls (with the current frame on the top), and G is the memory graph. A frame has the form (pc, ρ, s), where pc ∈ P m is the program counter, ρ : χ m → Jv represents a value assignment of local variables and s is a stack with elements in Jv . The operational semantics of Java bytecode is presented in Figure 3. The concatenation n :: s denotes a stack having n on top, while f C designates the field f of the class C .

The bytecode putfield has two rules depending on the type of the manipulated field: changing the value of a primitive field means changing the label of a vertex, whereas changing an object field consist in changing the edge to the vertex containing the new pointed object.

Figure 2(b) shows the memory graph after executing the entire code from Figure 2. Affecting the object B 3 1 to the field g of A 1 1 (bytecodes 7-9) consists in creating a new edge labelled by g from A 1 1 to B 3 1 , while the assignment of the value 3 to the field f of A 1 1 (bytecodes 13-15) changes the label of the node reached from A 1 1 with an f-edge. The intra-method control flow graph CF m of a method m is defined as usual: CF m is a graph with P m as set of vertices and edges from i to each elements of succ(i), with succ(i) given by the bytecode semantics, for each i ∈ P m as:

• succ(i) = {a} if P m [i] = goto a, • succ(i) = {a, i + 1} if P m [i] = ifeq a, • succ(i) = ∅ if P m [i] = areturn, • succ(i) = {i + 1} otherwise.
We also use the notation pred(i) = {j | i ∈ succ(j)}. An exit-point in a control flow graph is a node without successor.

For a method m, a block B is a subset of the instruction list P m together with a distinguished instruction, called the entry-point of B (Entry(B)) such that the control flow graph CF B of B is a subgraph of CF m ; all vertices in CF B are reachable from Entry(B) and CF B has a unique exit-point (Exit(B)). We will assume that P m is itself a block by adding a unique (fake) exit-point to its control flow graph. A state Q = ((i, ρ, s) :: f r, G) is a good initial state for a block B, if B[i] is defined and executing the block B starting from the state Q terminates in a state denoted by instr B (Q).

INRIA Pm[i] = prim op n = op(n1, n2) ((i, ρ, n1 :: n2 :: s) :: f r, G) -→ ((i + 1, ρ, n :: s) :: f r, G) Pm[i] = goto a F -→ ((a, ρ, s) :: f r, G) Pm[i] = aconst null F -→ ((i + 1, ρ, null :: s) :: f r, G) Pm[i] = pop ((i, ρ, n :: s) :: f r, G) -→ ((i + 1, ρ, s) :: f r, G) Pm[i] = iconst n F -→ ((i + 1, ρ, n :: s) :: f r, G) Pm[i] = new C o = C fresh(C i ,G) i G = new(o, C) F -→ ((i + 1, ρ, G .ς -1 (o) :: s) :: f r, G ∪ G ) Pm[i] = ifeq a n = 0 ((i, ρ, n :: s) :: f r, G) -→ ((i + 1, ρ, s) :: f r, G) Pm[i] = ifeq a n = 0 ((i, ρ, n :: s) :: f r, G) -→ ((a, ρ, s) :: f r, G) Pm[i] = load x F -→ ((i + 1, ρ, ρ(x) :: s) :: f r, G) Pm[i] = store x ((i, ρ, n :: s) :: f r, G) -→ ((i + 1, ρ[x → n], s) :: f r, G) Pm[i] = getfield f C n = null n ∈ adj G (G.ς -1 (n), f C ) ((i, ρ, n :: s) :: f r, G) -→ ((i + 1, ρ, G.ς(n ) :: s) :: f r, G) Pm[i] = putfield f C n = null v ∈ Val n ∈ adj G (G.ς -1 (n), f C ) ((i, ρ, v :: n :: s) :: f r, G) -→ ((i + 1, ρ, s) :: f r, G[n → v]) Pm[i] = putfield f C n = null v / ∈ Val ((i, ρ, v :: n :: s) :: f r, G) -→ ((i + 1, ρ, s) :: f r, G[(G.ς -1 (n), f C ) → G.ς -1 (v)]
)

Pm[i] = invoke m C o = null ((i, ρ, pn m :: • • • :: p1 :: o :: s) :: f r, G) -→ ((0, {0 → o, 1 → p1 . . . nm → pn m }, ) :: (i, ρ, s) :: f r, G) Pm[i] = areturn ((i, ρ, v :: s) :: (i , ρ , s ) :: f r, G) -→ ((i + 1, ρ , v :: s ) :: f r, G)
where F = ((i, ρ, s) :: f r, G). prim op stands for primitive operations with two parameters. The function fresh(c, G) returns a natural k such that c k is not used as a vertex label in G.

Figure 3: A subset of operational semantics rules

We use the notion of postdominance as defined in [START_REF] Ball | What's in a region?: or computing control dependence regions in near-linear time for reducible control flow[END_REF]: in a control flow graph CF B of a block B, a node n post-dominates a node n if n belongs to any path from n to Exit(B). We denote PD(n) the set of post-dominators of n. The immediate post-

dominator of n, ipd (n) ∈ PD(n) satisfies that∀n ∈ PD(n), if n = n , then n ∈ PD(n ).
In a block B with control flow graph CF B , for each conditional instruction B[i] = ifeq a, we define its dependency region as the set of instructions executed under this condition: reg(i) = Reach CFB (i) Reach CFB (ipd(i)). We compute a function cxt : B → ℘(B) representing the context (the set of conditional bytecodes) under which each instruction is executed:

cxt(i) = {j | i = j ∧ i ∈ reg(j)}.

Assumption about programs : "Structured" Blocks

We restrict blocks we consider by means of by a graph grammar G. This grammar allows us to rewrite a graph into another one according to some production rules. These rules have a single node in the left part and a graph in their right part. Nodes in the RT n°0347 left-hand side of transition rules are non-terminals We assume a unique non-terminal B for blocks wich is also the axiom of G. Nodes corresponding to bytecodes are nonterminals and cannot be rewritten.

The grammar G is given by the following set of production rules of Figure 4 (the entry-point in the right-side is the dashed one). Note that in these production rules, for the bytecode ifeq the two children of this node are distinguished, as according to the concrete semantics, they correspond to two different rules. Starting from the axiom B, a derivation is a succession of rewriting steps: a step consists in replacing, according to a production rule B → G , the left-hand side B by the corresponding right-hand side G such that edges are tranfered as follows: each incoming edge of the node B targets now the entry-point of G . There is an edge from the exit-point of G to the successor of B in the original graph (if any). In the resulting graph, the nodes from the right-hand side loose their entry node status (resp. exit node status) is they receive an incoming edge (resp. an outgoing edge).

A graph is produced by the grammar G if it can be obtained by rewriting from the axiom. Note that all the produced graphs have unique (remaining) entry-point and exitpoint. A block is "structured" if its control flow graph is produced by G. From now on, unless specified the blocks we consider are "structured" blocks.

Non-interference

Our analysis will compute an abstraction on how the value of some objects may depend or not on the value of others. We formalize this notion of dependency through noninterference: roughly, at the method level, the non-interference between an object ω and an input value η (of primitive type) can be stated as "changing of value of η does not affect the value of ω". The "value" of an object is defined by the values of its fields of primitive types and recursively, by the "values" of its object fields. An input value of a block is a value of primitive type chosen in the concrete state before the execution of the block; formally:

INRIA Definition 3.1 (Set of input values) Let Q = ((i, ρ, s) :: f r, G) be a state. Then, the set of input values of Q is I(Q) = G.V V al ∪ {x ∈ χ m | ρ(x) ∈ V al}.

Definition 3.2 (Value-change)

The value-change of a state Q = ((i, ρ, s) :: f r, G) and an input value η (η ∈ I(Q)) is a state Q = ((i, ρ , s) :: f r, G ) such that for some value a of primitive type, either

• η ∈ G.V V al , ρ = ρ and G = G[η → a], or • η ∈ {x ∈ χ m | ρ(x) ∈ V al}, ρ = ρ[η → a] and G = G. Definition 3.3 (Non-interference) Let B be a block. Let Q 1 , Q 2 be two states such that Q 2 = instr B (Q 1 ). Let G 1 , G 2 be the memory graphs of Q 1 and Q 2 respectively.
For some input value η from I(Q 1 ) and for any object node ω in G 1 , η does not interfer in B with ω if for Q 1 , a value-change of Q 1 and η, and the state Q 2 (having G 2 for memory graph) equal to instr B (Q 1 ) it holds that

G 2 ω ≡ G 2 ω .

Intra-method abstract dependency

In this section, we present the core of our analysis, that is the design of the dependency graph. The dependency graph is an "abstraction" of the memory graph and contains all possible dependencies between objects and input values. In Section 5, we formalize non-interference: an object and an input value do not interfeer if there is no path between them in the dependency graph.

We present here the intra-method analysis and take in consideration programs without method call: the algorithm consists in computing a dependency graph for each program point of a method. The method invocation and inter-method analysis is discussed in Section 6. Our approach can be context-insensitive or context-sensitive.

The abstract model: Dependency graph

Let us present the abstract model on an example. We consider the example in Figure 5 and the dependency graph obtained after the execution of method m. To help the reader, we refer to Java source code, but our analysis works on Java bytecode.

The dependency graph G at a program point is a representation of the concrete memory such that, when restricted to objects, G and the memory graph are related by an abstraction relation. Then the abstraction G is prolonged with primitive values and implicit flow dependencies. Nodes in this graph contain abstractions of JVM objects, constants and newly created objects as well as initial values of primitive type of the method. For a dependency graph G, G Obj denotes the set of nodes abstracting JVM objects, while G Val denotes the nodes corresponding to primitive values. As for the memory graph, we can define by Π Obj (G) the restriction of a dependency graph G to objects.

Hence, nodes of the graph G are defined to take into account the model:

• n n pc , pc ∈ P m : node modeling all the objects created by the execution of the object allocation instruction pc. We use the object allocation site model as all objects created at the same program statement have the same abstraction, RT n°0347

• n c pc , pc ∈ P m : constant value created at instruction pc. There is a unique node for every constant creation statement in the method,

• n null -1 : special node for null. Static variables can be modeled as fields of a global object, n s -1 , thus instructions dealing with static variables are similar to the ones treating normal objects. Arrays are objects having two fields: length and content, holding all the elements of the array.

0: void m(A p1, A p2, int h){ 1: if(h) 2: v = p1; 3: else 4: v = p2; 5: v.f = 0; 6: } p1 p2 p3 n c 5 p1.f p2.f f , i f , d f , i f , d f , d f , d
Edges represent links between nodes; they are labeled with f, q , where f ∈ Fields is the name of the field ans and q ∈ F = {d, i} is the type of flow: i for implicit flow and d for direct links, with the order relation i d.

Let us present the abstract model on an example. We consider the example in Figure 5 and the dependency graph obtained after the execution of method m. To help the reader, we refer to Java source code, but our analysis works on Java bytecode. The edge labeled f, d between p 1 and n c 5 shows that there is direct flow, arising from an assignment, from n c 5 to the field f of p 1 . The edge labeled f, i between p 1 and p 3 expresses the implicit flow: the value of p 3 might be deduced from the field f of p 1 .

To deal with implicit flows, we use the notion of regions. When executing an instruction i which adds an edge (u, v, f, d ), edges having the form (u, v , f, i ) are also added, where v is the value tested by conditional instructions in cxt(i). The intuition behind is that someone who knows the control structure of the program and can observe the field f of u, is able to deduce the value of v .

To unify the model, we add a special value field ref of primitive type to each object, which stands for the address of the object. When comparing two objects or an object to null, the value tested is the ref field. The code if(o == null) a.x = b generates an implicit flow from the field x of a to the address

ref of o ( (a, o.ref, x, i )).
Implicit flows are from objects modified inside a region to values on which the execution of the region depends. These facts combined with the use of the special field ref , allow us to deduce the properties of a dependency graph:

1. any node u ∈ G.V Val is a leaf, 2. for any edge of type (u, u , f, i ) ∈ G.E), u ∈ G.V Obj \ {n null -1 } and u ∈ G.V Val .
These properties state that edges between two references are always direct edges:

if u 1 , u 2 ∈ G.V Obj and (u 1 , u 2 , f, t ) ∈ G.E then t = d.
Value nodes are always leaves, and implicit edges are always between a reference and a value node. Thus, the edges generated by the information flow and the primitive values are not imprecated in the graph restricted to objects. Our construction is a points-to graph prolonged by edges about primitive values and implicit flows.

INRIA (ρ, v1 :: v2 :: s, G) (ρ, v1 ∪ v2 ∪ TVΓ :: s, G) prim op (ρ, s, G) (ρ, { n n i , d } ∪ TVΓ :: s, G) new i C (ρ, s, G) (ρ, s, G) goto a (ρ, s, G) (ρ, {(n null -1 , d)} ∪ TVΓ :: s, G) aconst null (ρ, v :: s, G) (ρ, s, G) ifeq a (ρ, s, G) (ρ, {(n c i , d)} ∪ TVΓ :: s, G) iconst iv (ρ, v :: s, G) (ρ, s, G) pop (ρ, s, G) (ρ, ρ(x) ∪ TVΓ :: s, G) load x (ρ, u :: s, G) (ρ[x → u ∪ TVΓ :: s, G) store x (ρ, u :: s, G) (ρ, {(e, t) | e ∈ adjG(e , f C , t ) ∧ e ∈ V u d } ∪ { e, i | e ∈ V u i } ∪ TVΓ :: s, G) getfield f C (ρ, v :: u :: s, (V, E)) " ρ, s, " V, E ∪{(e, e , f C , t )| e, d ∈ u, e = n null -1 , e , t ∈ v} ∪{(e, e , f C , i )| e, d ∈ u, e = n null -1 , e ∈ Γ ∪ V u i } «« putfield f C with V u d = {e | e, d ∈ u} V u i = {e | e, i ∈ u} TVΓ = { e, i | e ∈ Γ}

Abstract semantics

Building the dependency graph requires to approximate local variables and stack contents, and to deal with implicit flow, we must know the conditions under which the local variables and the stack are modified. Thus, elements from stack and local variables have the form u, t where u ∈ G.V and t ∈ F. Hence, an abstract state is of the form Q = (ρ, s, G) where G is the dependency graph, ρ is a mapping from χ m to ℘(G.V × F) and s is the stack with elements in ℘(G.V × F).

For every type of bytecodes b, we define a transformation rule Q = instr b (Q, Γ) where Γ is the set of nodes u corresponding to values on which depends the execution of the bytecode, reflecting the impact of the implicit flow. The semantics of transformation rules is presented in Figure 6.

To reflect the impact of control regions on stack and local variables array, every instruction modifying the last two (push for stack or store for local variables array) takes into consideration the values in the context. For example, the instructions new and iconst push on the stack new abstract values but also the context under which the operation takes place. The store bytecode, stores in the local variable array not only the top of the stack, but also the nodes in Γ, as the writing is done under its control.

The instruction getfield pushes on the stack the adjacent of u , if u is an object reference, or keeps u on the stack if it is primitive value arising from implicit flow.

The most significant bytecode is putfield, as it modifies the dependency graph. Apart edges from direct nodes in u (having the form (e, d)) to elements in v, implicit flow edges from the nodes e ((e, d) ∈ u) to nodes in Γ, the instruction adds implicit flow edges from nodes e ( (e, d) ∈ u) to implicit nodes e ((e , i) ∈ u). The presence of nodes like (e , i) in u signifies that the objects in u depend on e . Thus, we propagate the implicit dependencies of an object to every field being modified of that object.

RT n°0347

Algorithm

From now on, we assume that a method or a block is represented by its control flow graph.

Our analysis is flow sensitive as it computes a dependency graph at each program point. The analysis is defined in the context of a monotone framework [START_REF] Nielson | Principles of Program Analysis[END_REF] for data flow analysis. To comply with the framework, we define an order relation and a join operator on the property space S (the set of pairs (Q, Γ)) and the execution of a method as a set of equations using the transformation rules instr b .

Definition 4.1 (Ordering relation on S)

Let S 1 = ((ρ 1 , s 1 , G 1 ), Γ 1 ) ∈ S and S 2 = ((ρ 1 , s 1 , G 1 ), Γ 2 ) ∈ S be two states. Then, S 1 is said to be smaller than S 2 , i.e. S 1 S 2 if and only if s 1 s 2 , ρ 1 ρ 2 , G 1 ⊆ G 2 and Γ 1 ⊆ Γ 2 .
To order the local variables ρ 1 and ρ 2 we use the classical point-wise ordering relation between functions. Given two stacks s 1 and s 2 , s 1 is said to be smaller than s 2 , i.e. s 1 s 2 , if both stacks are empty or if

s 1 = v 1 :: s 1 and s 2 = v 2 :: s 2 with v 1 ⊆ v 2 and s 1 s 2 .
The join operator is defined as follows:

(Q 1 , Γ 1 ) (Q 2 , Γ 2 ) = (Q 1 Q 2 , Γ 1 ∪ Γ 2 ). The join operator on two states (ρ, s, G) = (ρ 1 , s 1 , G 1 ) (ρ 2 , s 2 , G 2 ) is a component wise operator (s = s 1 s 2 , etc).
Then, (S, , ) forms a semi-joint lattice which satisfies the Ascending Chain Property [START_REF] Nielson | Principles of Program Analysis[END_REF] (all increasing sequences in S become eventually constant) required by the monotone framework.

We can now define the analysis of a block of instructions B ⊆ P m of a method m as an equation system E B , starting from a given initial state (Q 0 , Γ 0 ) (remind that we consider terminating executions without exception and we consider here initial states that allow such executions).

For every node i in the control flow graph of B, (Q i , Γ i ) represent the state and the context (required by the implicit flow) under which the instruction i is executed: It represents, the conditions tested (the top of the stack) by the instructions in cxt(i). Thus, for all nodes i in CF B :

(Q i , Γ i ) =        (Q 0 j∈pred(i) instr B[j] (Q j , Γ j ), if i = Entry(B) Γ 0 ∪ {u | u, t ∈ v with Q k = (ρ, v :: s, G), k ∈ cxt(i)}) ( j∈pred(i) instr B[j] (Q j , Γ j ), otherwise {u | u, t ∈ v with Q k = (ρ, v :: s, G), k ∈ cxt(i)}) (4.1)
The transformation rules are monotone with respect to the ordering relation , thus we can solve the system (4.1) using standard methods for monotone dataflow analysis.

Lemme 4.2 (Monotonicity of the transformation rules) For every instruction b, the transformation rule instr b is monotone with respect to the ordering relation .

The Proof of this Lemma is made by case analysis on each instruction b, based on the transformation rules in Figure 6, it is given in Appendix A.

Our algorithm is a forward dataflow may-analysis [START_REF] Hind | Interprocedural pointer alias analysis[END_REF], as the computed dependency graph for a given program point is the union of graphs created by all the execution paths reaching that point.

For a block B and a pair (Q, Γ), we define instr B (Q, Γ) as the state instr B[e] (Q e , Γ e ) where e = Exit(B) and (Q e , Γ e ) is obtained in the least solution of the system of equations E B starting from the initial state (Q, Γ).

Relations between abstract and concrete worlds

We now relate formally abstract and concrete semantics. We consider abstraction functions to relate restrictions of our memory graphs to nodes representing objects and dependency graphs. Because of the allocation site model, it is possible to relate concrete nodes to abstract nodes in a non ambiguous manner. For complete graphs (including nodes representing values), we cannot define an abstract relation since it is not possible to associate uniquely a concrete node value with an abstract one in the model we use. Let us consider the example of Figure 7. The execution of the method m leads to the memory graph 7(a). Anyway, as we aim at capturing the flow between data, our analysis produces the dependency graph 7(b) for m. For example, it is not possible to decide which node to associate with the concrete dashed node: n c 1 , n c 2 , or n c 3 since the value 1 is the result of a calculus that implies several values. This is the reason why the abstraction relation is only defined for the restriction of graphs to their object part.

Definition 4.3 (Abstraction of a memory graph) Let V and V be two sets of nodes.

A relation α from V to V is an abstraction function if it is a mapping that respects the allocation site model: for all k, all the C k i are mapped to n n i , and for all u ∈ V such that ς(u) = null, α(u) = n null -1 . This relation is canonically extended to graphs defined over sets of nodes V and V. Let G be a memory graph with G.V = G.V Obj ⊆ V. Then α(G) is the graph

({α(u) | u ∈ G.V Obj }, {(α(u), α(v), e, d ) | u, v ∈ G.V Obj ∧ (u, v, e) ∈ G.E}).

Definition 4.4 (α-abstraction) Let G be a memory graph and G be an abstract graph. Then, G is an

α-abstraction of G, denoted by G α G if α(Π Obj (G)) ⊆ Π Obj (G).
The abstraction function must be defined between the full state manipulated by the program instructions. The stack abstraction is a component-wise operation. The local variables abstraction is defined similarly.

Definition 4.5 (Stack abstraction)

Let α be an abstraction function. Let G be a memory graph and G be an abstract graph such that G α G. An abstract execution stack s is the α-abstraction of a concrete execution stack s (denoted by s α s), if s,s are both empty or if s =v :: s 1 , s =v ::

s 1 , s 1 α s 1 , and (α(G.ς -1 (v)), d) ∈ v if v ∈ G.V Obj .
= (ρ, s, G), Q is an α-abstraction of Q (denoted by Q α Q) if G α G, s α s, and ρ α ρ. RT n°0347

Soundness of the intra-method analysis

We now prove the correctness of the construction presented in the previous section with respect to non-interference: if there is no dependency (path in the abstract graph) between an object and an input value, then changing the input value in the concrete graph will not affect the concrete graph of the object. Thus, this section is devoted to the proof of a non-interference theorem. Definition 5.1 (α-abstraction extension) Let Q = ((i, ρ, s) :: fr , G) be a concrete state, and

Q = (ρ, s, G) such that Q α Q. Then, α Q : I(Q) -→ ℘(G.V V al ) is the unique extension of α in Q if ∀η ∈ I(Q) ∩ G.V V al , α Q (η) = {η | ∃(α(u), η, f, d ) ∈ G.E, with(u, η, f ) ∈ G.E} ∀η ∈ I(Q) ∩ χ m , α Q (η) = {e | e, t ∈ ρ(η))} Definition 5.2 Let α be an abstraction function. Let Q = ((i, ρ, s) :: fr , G) be a concrete state, Q = (ρ, s, G) such that Q α Q. Let β ⊆ G.V V al . For any v ∈ G.V Obj , we have f ree α (v, β, Q) if one of the following conditions holds: • ∃ (u, v, f ) ∈ G.E, with u ∈ G .V Obj and β ∩ adj G (α(u), f ) = ∅, • ∃x such that (α(v), d) ∈ ρ(x) and ∃(η, i) ∈ ρ(x) with η ∈ β, • ∃i such that (α(v), d) ∈ s[i] and ∃(η, i) ∈ s[i] with η ∈ β. Theorem 5.3 (Non-interference) Let B be an instruction block. Let Q 1 be a concrete state, Q 1 such that Q 1 α Q 1 , Q 2 = instr B (Q 1 ), and Q 2 = instr B (Q 1 , Γ 1 )
. Let G 1 be the memory graph of Q 1 and G 2 be the abstract graph from Q 2 . For an object node ω in G 1 .V Obj and an input value

η from I(Q 1 ) such that free α (ω, α Q1 (η), Q 1 ), if Reach G2 (α(ω)) ∩ α Q1 (η) = ∅ then η does not interfer with ω in B.
The first step of the proof consists in the soundness of the pointer analysis contained in our analysis. After defining the notion of state-variation which describes how states can be affected by the modification of input values, we complete the proof of soundness for our analysis by the non-interference theorem. As we compare, in this section, concrete and abstract worlds, we denote by e a concrete element and by e an abstract element. Note that e is just an abstract element, and not necessarily the abstraction of e.

Abstraction correctness

We show that when the dependency graphs are restricted to references, our analysis is a sound points-to analysis. We rely on the dataflow framework which is slightly adapted to take into account the flow information of the Γ's.

(Q) α instr b (Q, Γ).
The proof is done by case analysis on each bytecode instruction and can be found in Appendix B.1.

We now want to establish the following property.

INRIA Proposition 5.5 (Points-to correctness) Let B be a block, Q be a good initial (concrete) state for B, α be an abstraction function, and Q be an abstract state. Then, for any set of abstract values Γ,

Q α Q implies instr B (Q) α instr B (Q, Γ).
The proof relies on the general theorem stating the correctness of the global soundness provided that the local correctness holds. However, our system of equations is defined for a pair (Q, Γ) and the computation of the values of Γ's is not performed structurally on the control flow graph but based on regions instead.

Our proof will simply show that the restriction to objects of dependency graphs from the computed abstract states Q are independent from the Γ's. Therefore, we will be able to define a new system of equation E B for a block B that differ from E B only on the interpretation of the functionals appearing in the system, that becomes independent of Γ. But it turns out that the points-to graphs in the states computed for E B and E B are identical.

For two dependency graphs G, G , we write G . = G iff G, G are equal when restricted to their object part, ie Π Obj (G) = Π Obj (G ). This relation .

= is also defined on sets of typed-flow vertices as :

S 1 . = S 2 if {e | e, d ∈ S 1 ∧ e ∈ V Obj } = {e | e, d ∈ S 2 ∧ e ∈ V Obj }, where V Obj is a set of vertices. This relation is extended to abstract as follows: Q = (ρ, s, G) . = (ρ , s , G ) = Q if G . = G and • for all x in χ m , ρ(x) . = ρ (x)
• either s = s = ε or s = u :: s t , s = u :: s t , u . = u and s t . = s t .

Proposition 5. [START_REF] Bernardeschi | Checking secure information flow in java bytecode by code transformation and standard bytecode verification[END_REF] For any concrete state Q, for any abstract states

Q, Q , if Q α Q and Q . = Q then Q α Q . Proof. Let Q = ((i, ρ, s) :: f r, G), Q = (ρ, s, G) and Q = (ρ , s , G ). From the definition 4.6 of state abstraction, Q α Q , if s α s , ρ α ρ and G α G . By hopthesis, Q α Q thus s α s, ρ α ρ and G α G. Moreover Q . = Q thus s . = s , ρ . = ρ and G . = G . Let us first prove that G α G . From G . = G we have Π Obj (G) = Π Obj (G ). Since G α G, α(Π Obj G) ⊆ Π Obj G = Π Obj G . Thus G α G .
Let us now prove that s α s . Let s = u :: s t , s = u :: s t and s = u :: s t . As s α s, thus s t α s t and (α(G.ς

-1 (u)), d) ∈ u if u ∈ G.V Obj . If u ∈ G.V Obj , then α(G.ς -1 (u)) ∈ G.V Obj .
= relation if {e | e, d ∈ u ∧ e ∈ G.V Obj } = {e | e, d ∈ u ∧ e ∈ G .V Obj }. Thus, if α(G.ς -1 (u)) ∈ G.V Obj and (α(G.ς -1 (u)), d) ∈ u then (α(G.ς -1 (u)), d) ∈ u . Hence s α s .
The proof for local variables array is similar.

Proposition 5.7 For all states

Q 1 , Q 1 , Q 2 , Q 2 , • if Q 1 . = Q 2 and Q 1 . = Q 2 then Q 1 Q 1 . = Q 2 Q 2 ,
• for any bytecode b, for any

Γ 1 , Γ 2 , if Q 1 . = Q 2 then instr b (Q 1 , Γ 1 ) . = instr b (Q 2 , Γ 2 ) RT n°0347
Proof. For the first point, as is defined component-wise for stacks and mappings ρ, the only part to be proved is for graphs.

If Q 1 .G . = Q 2 .
G then the two graphs are equal when restricted to their object part, thus

Π Obj (Q 1 .G) = Π Obj (Q 2 .G). Moreover, Π Obj (Q 1 .G) = Π Obj (Q 2 .G), hence Π Obj (Q 1 .G) ∪ Π Obj (Q 1 .G) = Π Obj (Q 2 .G) ∪ Π Obj (Q 2 .G). We must prove that Π Obj (Q 1 .G∪Q 1 .G) = Π Obj (Q 2 .G∪Q 2 .G). It is enough to prove that, for two dependency graphs G and G, Π Obj (G ∪ G ) = Π Obj (G) ∪ Π Obj (G ).
The proof lies on the property of dependency graphs stating that any node u ∈ G.V V al is a leaf. Thus, a dependency graph contains only edges between two objects or edges from an object to a value: there is no edge from a value to an object node. When making the union of two dependency graphs, the only edges between objects can come from the two dependency graphs. Thus, give restriction to objects part of the union of two graphs is equal to the union of the restrictions of the two graphs to objects:

Π Obj (G ∪ G ) = Π Obj (G) ∪ Π Obj (G ).
For the second point, we make a case analysis on each bytecode instruction: details can be found in Appendix B.2.

Let us consider the system of equations E B . Each right-hand side can be seen as a functional over (Q i , Γ i ), the unknowns. Let us define the system E B with (Q 0 , ∅) for initial state:

(Q i , Γ i ) =        (Q 0 j∈pred(i) instr B[j] (Q j , Γ j ), if i = Entry(B) {u | u, t ∈ v with Q k = (ρ, v :: s, G), k ∈ cxt(i)}) ( j∈pred(i) instr B[j] (Q j , Γ j ), otherwise {u | u, t ∈ v with Q k = (ρ, v :: s, G), k ∈ cxt(i)})
We define for a block B and the system E B , the mapping instr B (Q, Γ) as we did for instr B (Q, Γ) and E B .

Obviously, for the least solution of E B , we have that Γ i = ∅ for all i. Therefore, the functionals in the right-hand side and thus, the solution of the system are independent from the Γ . As Lemma 5.4 establishes the local soundness for all Γ's, in particular for ∅, we have that the global soundness holds for the system E B , that is

Q α Q implies instr B (Q) α instr B (Q, ∅) (5.1)
However, the system E B involves the Γ's which influence on the values of the Q's but not on their object part as we show now. Proposition 5.8 Provided that their respective initial states satisfies Q . = Q , then for the respective least solution of E B and E B , we have that

Q i . = Q i for all i.
Proof. We rely here on the iterative construction of the least solution of equation systems. Starting from the valuation assigning the least value of the lattice to all the unknowns, that is the Q i , Γ i 's and the Q i , Γ i 's respectively, we compute a new value for these valuations (at the left-hand side of equalities) by using the old values in the right-hand side. Eventually, a fixed point is reached during that computation.

Then, the proof goes by induction on n, the minimal number of iteration required to reach a fixed point in both system using Proposition 5.7 for the induction step.

INRIA Proposition 5.9 For any block B, for any

Γ 1 , Γ 2 , if Q 1 . = Q 2 then instr B (Q 1 , Γ 1 ) . = instr B (Q 2 , Γ 2 )
Proof. Straightforward from Propositions 5.8 and 5.7.

By combining the global soundness (5.1), Propositions 5.9 and 5.6, we get Proposition 5.5 as result. This ensures correctness for dependency graph restricted to references. The points-to analysis is a flow-sensitive may-analysis, similar to previous work [START_REF] Salcianu | Pointer and escape analysis for multithreaded programs[END_REF][START_REF] Whaley | Compositional pointer and escape analysis for Java programs[END_REF]. In the next subsection, we prove the correctness of the primitive edges (implicit and direct flow) as a non-interference theorem relying on the correctness for the points-to analysis.

Analysis correctness

To prove the non-interference theorem, according to Definition 3.3, we need to make values vary at some program point according to Definition 3.2 and to check the impact of this variation on objects at another program point. Thus, we first define the notion of state variation that captures how a concrete execution state, corresponding to a program point i, might change when a value η has changed in the past of this execution. Definition 5.13 contains an over estimation of the set of states that the JVM can reach after this change: the main impact is on the memory graph, but the local variables and stack can also be affected. The correctness of the definition is proved later in Proposition 5.15.

Definition 5.10 (Graph variation) Let α be an abstraction function. Let

Q = ((i, ρ, s) :: fr , G) be a concrete state, Q=(ρ, s, G) such that Q α Q. Let β ⊆ G.V V al
be a set of nodes of primitive type. Then G is a graph variation of G with respect to G and β, denoted G = υ(G, G, β), if it is obtained from G applying one of the following rules:

1. G = G[v → x] with x ∈ V al, if ∃(u, v, f ) ∈ G.E, ∃η ∈ β and t ∈ F such that (α(u), η, f, t ) ∈ G.E 2. G α G st for all v ∈ G.V Obj if f ree α (v, β, Q) then v ∈ G .V Obj and for all (u, v, f ) in G.E, with u ∈ G .V Obj , if β ∩ adj G (α(u), f ) = ∅, then (u, v, f ) ∈ G .E.

Definition 5.11 (Stack variation) Let α be an abstraction function. Let

Q = ((i, ρ, s) :: f r, G) be a concrete state, Q = (ρ, s, G) such that Q α Q. Let β ⊆ G.V V al
be a set of nodes of primitive type. Then s is a stack variation of s with respect to s and β, denoted by s = υ(s, s, β), if it is obtained from s applying one of the following rules:

1. s = s[i → x] with x ∈ Val , if s[i] ∈ Val and ∃η ∈ β, t ∈ F such that (η, t) ∈ s[i] 2. s = s[i → ς(o)], if ∃η ∈ β such that (η, i) ∈ s[i] ∧ (o, d) ∈ s[i] ∧ o ∈ G .V Obj ∧ o ∈ α -1 (o)
Definition 5.12 (Local variables array variation) Let α be an abstraction function.

Let Q = ((i, ρ, s) :: f r, G) be a concrete state, Q = (ρ, s, G) such that Q α Q. Let β ⊆ G.V V al
be a set of nodes of primitive type. Then ρ is a local variables array variation of ρ with respect to ρ and β, denoted by ρ = υ(ρ, ρ, β), if it is obtained from ρ applying one of the following rules:

RT n°0347 1. ρ = ρ[i → x] with x ∈ Val, if ρ(i) ∈ Val and ∃η ∈ β, t ∈ F such that (η, t) ∈ ρ(i) 2. ρ = ρ[i → ς(o))], if ∃η ∈ β such that (η, i) ∈ ρ(i) ∧ (o, d) ∈ ρ(i) ∧ o ∈ G .V Obj ∧ o ∈ α -1 (o)
Based on the definition of stack variation and local variables array variation, we redefine the state variation: Definition 5.13 (State variation) Let α be an abstraction function. Let Q = (ρ, s, G) be a concrete state, Q = (ρ, s, G) an abstract state such that

Q α Q. Let β ⊆ G.V V al be a set of nodes of primitive type. Then Q is a state variation of Q with respect to Q and β, denoted by Q = ((i, ρ , s ) :: f r, G ) = υ(Q, Q, β), if G = υ(G, G, β), s = υ(s, s, β) and ρ = υ(ρ, ρ, β).
A state variation captures the impacts of the modification of a value in the past of the execution on the current state. The main impact we are interested in concerns the changes of the memory graph according to Definition 5.10. Anyway, the modification of a value in the past of a state also impacts the stack and the local variables, according to definitions 5.11 and 5.12. Rule 1 of Definition 5.11 and rule 1 of Definition 5.12 capture possible variations due to immediate use of a value corresponding to β while rule 2 of Definition 5.11 and rule 2 of Definition 5.12 capture the impact of the changes of a value corresponding to β to the objects that depend on it by an implicit flow.

From the definition of state variation, we can state that the variation of a state regarding to a set β, does not impact the objects ω which have no dependence to any node of β. Lemme 5.14 Let α be an abstraction function, Q = ((i, ρ, s) :: f r, G), and Q = (ρ, s, G) with Q α Q. Let β ⊆ G.V V al , and ω ∈ G.V Obj such that there exists no path from α(ω) to any node of β in G. Then, in any state variation

Q = υ(Q, Q, β) = ((i, ρ , s ) :: f r, G ), if ω ∈ G .V Obj , we have G ω ≡ G ω .
Proof. The differences between G and G are given by rules of Definition 5.10. If ω ∈ G .V Obj , then, for any object node v of the subgraph rooted by ω, there exists an edge (u, v, f ) ∈ G.E such that u belongs to the subgraph rooted by ω with:

• β ∩ adj G (α(u), f ) = ∅ because Reach G (α(ω)) ∩ β = ∅,
• u ∈ G .V Obj because either u = ω, or u belongs to G .V Obj for the same reason.

Thus, v ∈ G .V Obj and (u, v, f ) ∈ G .E For the leaves of the subgraph rooted by ω, rule 1 randomizes the value of v if there is an edge (u, v, f ) ∈ G.E and a flow from α(u) to a element of β labelled by f in G.

As by hypothesis, there is no path from α(ω) to any element of β in in G, it is obvious that this modification does not affect the subgraph rooted by ω.

Proposition 5.15 states the state variation correctness, by claiming that changing an input value and executing a block with a state variation leads us to a state variation.

Proposition 5.15 (State variation correctness) Let B be an instruction block

, Q 1 a concrete state, Q 1 with Q 1 α Q 1 , Q 2 = instr B (Q 1 ), and Q 2 = instr B (Q 1 , Γ 1 ). If Q 1 = υ(Q 1 , Q 1 , β) and Q 2 = instr B (Q 1 ) then Q 2 = υ(Q 2 , Q 2 , β). INRIA Proof.
Proof. We split the proof in two parts: first we prove the theorem holds for blocks containing a single instruction, this is done by case analysis in Appendix B.3. Let us prove now the state variation correctness for "structured" blocks. The grammar G defines precisely what are "structured" blocks and will be used in this proof. The proof goes by induction on k the number of steps required to produce the control flow graph of the block B by the grammar G. Let G be a CFG (that does not contain the non-terminal B anymore) for some block B such that B → k G for some natural k. Let us show that G (and thus, B) satisfies the state variation property.

For k = 1: Only production rules (bytecode) are concerned. In this case, we rely on the correctness established for each bytecode in the previous section.

For k, the property holding for all k < k: in this case, there exists some graph G such that B → G → k-1 G. Depending on the rule used for B → G : we analyse the different cases in Appendix B.4.

We can now conclude with the proof of the non-interference theorem.

Proof of Theorem 5.3. Let B be an instruction block. Let Q 1 = ((i, ρ 1 , s 1 ) ::

f r 1 , G 1 ) be a concrete state, Q 1 = (ρ 1 , s 1 , G 1 ) such that Q 1 α Q 1 , Q 2 = instr B (Q 1 ), and Q 2 = instr B (Q 1 , Γ 1 ). Let ω ∈ G 1 .
V Obj be an object node and η ∈ I(Q 1 ) be an input value. Let us consider a value-change

Q 1 = ((i, ρ 1 , s 1 ) :: f r 1 , G 1 ) of Q 1 and η. According to Definition 3.2, either η is a value node of G 1 and then G 1 = G 1 [η → v], or η is a local variable and then ρ 1 = ρ 1 [η → v] (for some v ∈ V al).
Let us denote β = α Q1 (η), then, the first case corresponds to the rule 1 of Definition 5.10, the second case to the rule 1 of Definition 5.13, thus

Q 1 = υ(Q 1 , Q 1 , β). We denote Q 2 = instr B (Q 1 )
. According to Proposition 5.15, we have Q 2 = υ(Q 2 , Q 2 , β). As f ree α (ω, α Q1 (η), Q 1 ), rule 2 of Definition 5.10 says that ω ∈ G 1 .V , thus ω ∈ G 2 .V . As by hypothesis, Reach G2 (α(ω)) ∩ α Q1 (η) = ∅, by applying Lemma 5.14, we obtain G 2 ω ≡ G 2 ω (for G 2 , G 2 the memory graphs of resp. Q 2 , Q 2 ), ie η does not interfer with ω in B.

Inter-method analysis

In the previous section we show non-interference for methods without invocation. That is to say, for a method m that does not contain any invocation, we know that the noninterference theorem holds. In this section, we add a support for a context-insensitive or a context-sensitive analysis with the same semantics rules. The differences between the two ones are the construction of the inter-procedural control flow graph and the node naming strategy.

Abstract semantics of the method invocation

To deal with method invocation, we add abstract semantics rules for invoke and areturn bytecodes. In static analysis of inter-procedural programs, one of the main problems is that the size of the call stack in the concrete execution is not bounded: the abstract rule for invoke cannot sketch the operational one otherwise, we would have RT n°0347 an infinite abstract domain. Some works of the literature propose an abstraction of the call stack [START_REF] Jeannet | Abstracting call-stacks for interprocedural verification of imperative programs[END_REF]. We propose to keep the same abstract domain than in the intra-method analysis, in which we occult the call stack and only consider the current frame of the method: the method invocation can be added to the framework used. Thus, the new abstract semantics rules are given by Figure 8 where ζ is a special value. Using these rules, we do not registered the current context before the call and use instead a bytecode transformation before the analysis. We replace each invoke bytecode by an "if" region as described by Figures 9(a This transformation is syntactical: we insert some code and rename the following bytecode numbers with a function h. It does not change the semantics of the program since we only add dead code: bytecodes b 0 to b nm+2 will never be executed. We obtain the control flow graph for which it is obvious to see that any concrete execution

Q 0 Q 1 . . . Q i-1 Q i Q Pm[0] . . . Q Pm[j] Q i+1 of the original program correspond to an execution Q 0 Q 1 . . . Q i-1 Q i Q a0 Q c0 Q Pm[0] . . . Q Pm[j] Q h(i+1) with Q i+1 = Q h(i+1) .
Thus, if we obtain an abstract state Q h(i+1) that is correct for Q h(i+1) , it is also correct for Q i+1 . Moreover, we keep the usual Java properties: the stack is well typed and has always the same size at each program point. This transformation is only used for technical reasons in the analysis of the abstract model: the path b 0 . . . b nm+2 (that is never executed in any concrete execution) is used to "transmit" the current context we had before the invocation to the immediate successor of the invocation, thus sketching the context save and reload that occur the concrete INRIA execution of an invocation. The equivalent of a context reload is done by the join operator when computing Q h(i+1) . We extend the operator to the case where the local variables have the special value ζ:

Q b 0 = (ρ, u nm-1 :: • • • :: u 0 :: s, G) Qc 0 = ({0 → u 0 , . . . , nm → un m }, , G) Q h = (ρ, null :: s, G) i a0 Qa 0 b0 bn m bn m+1 bn m+2 Qa 0 Q b 0 (ρ, s, G) Q h c0 Pm[0] Pm[j] Qa 0 Qc 0 h(i + 1) Q h (ζ, u, G ) (c) Transformed Control Flow
(ζ, u, G) (ρ, v :: s, G ) = (ρ, v :: s, G ) (ζ, u, G) = (ρ, u :: s, G G ), thus Q h(i+1) = (ρ, u :: s, G ) (since G G = G ),
which contains the local variables of Q a0 , the stack of Q a0 increased with the return value of m, and the memory resulting from the execution of m. This is exactly the state we would obtain by saving the calling context and reloading it after the method execution. Note that the extension of the join operator does not affect the previous uses of the operator since we only introduce the special value ζ in the areturn rule. Moreover to have a complete definition of , we can define the last case:

(ζ, u, G) (ζ, u , G ) = (ζ, u u , G G ).
Thus, we perform an analysis without any abstraction of the call stack, and keep the same finite abstract domain as previously. We now have to define the inter-procedural control flow graph that we use.

Inter-procedural control flow graph

We use the same framework and the same equation system than for the intra-method analysis to perform a context insensitive or several context sensitive inter-method analyses. We only have to define the pred function, that is to say the inter-procedural control flow graph (ICFG i ): the parameter i of this graph defines the precision of the analysis.

To built the ICFG, we have to extend our naming strategy to keep disjoint instruction number sets for methods and a unique node name in the dependency graph to respect the allocation site model. Thus, each instruction i of a method m is now named m i (with m the fully qualified name of the method and m ≤ m if m is a method that overwrites m.), and we use copies of method call graphs including informations about the call sites. For example the node m i 1 m j 2 m k 3 of the ICFG 3 denotes the k th bytecode of method m 3 that has been called in the context of line j of method m 2 , that has itself been called at line i of m 1 . The larger the parameter of the ICFG is, the more accurate is the analysis but the larger is the number of states of the ICFG. Then, the ICFG k of a set of methods M is a graph with:

ICF G k M .V = {m i 0 0 m i 1 1 . . . m i k k | ∀0 ≤ i ≤ k, mi ∈ M, i k ∈ Pm k , ∀0 ≤ j < k, Pm j [ij ] = invoke mj+1} ICF G k M .E = {(m i 0 0 . . . m i k-1 k-1 m i k , m i 0 0 . . . m i k-1 k-1 m j k ) | (i, j) ∈ CFm k .E, Pm k [i] = invoke m} ∪ {(m i 0 0 . . . m i k-1 k-1 m i k , m j 0 0 . . . m j k-1 k-1 m 0 ) | Pm k [i] = invoke m, m ≤ m} ∪ {((m i 0 0 . . . m i k-1 k-1 m i k , m j 0 0 . . . m j k k ) | Pm k [i] = areturn, P m k [j k -1] = invoke m, m k ≤ m}
The ICFG 0 produces a context-insensitive analysis, ICFG 1 a usual context-sensitive analysis, and so on. Note that in node names of the dependency graph like n c pc and n n pc , pc now encodes the name of the node of the ICFG in which the constant or new object is created. Note that our construction also takes into account overwritten methods, it can be more precise when the dynamic types of objects can statically be computed by only branching on the first instruction of the exact method.

Soundness

In order to show that the extended abstract model is sound with respect to the noninterference, we prove that the abstract semantics rules for invoke and areturn have the same properties as the rest of bytecode. We only have to define an extension of the relation α for an abstraction relation α taking into account the new value ζ.

= (ρ, s, G), Q is an α-abstraction of Q (denoted by Q α Q) if G α G and: • v α s with s = v :: s if ρ = ζ • s α s, and ρ α ρ, otherwise.
The extension is necessary for the areturn bytecode, in order to prove the relation α for the value returned by the invoked method. This definition is sufficient, since the relation α for the rest of the calling context is being insured by the code transformation presented in Subsection 6.1.

For the same reasons, we need to define an extension for the state variation definition: for the areturn bytecode, and thus the special value ζ, the state variation must hold only for the returned value. The detailed proof is in Appendix C.

Definition 6.2 (State variation (extension)) Let α be an abstraction function. Let

Q = ((pc, ρ, s) :: f r, G) be a concrete state, Q = (ρ, s, G) its S 0 -may-abstraction such that Q α Q. Let β ⊆ G.V V al be a set of nodes of primitive type. Then Q is a state variation of Q with respect to Q and β, denoted by Q = ((i, ρ , s ) :: f r, G ) = υ(Q, Q, β), if G = υ(G, G, β) and: • v = υ(v,

Secure information flow

All the previous works on non-interference require the lattice security model of information flow to be known from the beginning. The dependency graph contains points-to and control flow dependency information. Once computed, the dependency graph can be labeled with security levels and non-interference checked. We can consider any kind of "programs", let us for example consider a method m (with n parameters), for which we want to check non-interference. We have to define a initial abstract state

Q m init = ({0 → n p 0 , . . . , n → n p n }, , G init )
for the analysis such that G init .V contains all the nodes required by the allocation site model, constants and nullvalue, nodes representing static variables, and nodes representing formal parameters. For each parameter i, n p i denotes the i th parameter of the method. We add to G init the minimal subgraph rooted by n p i , G p i . This graph represents the parameter and all of its content. To avoid infinite graphs, we use a parameter h, which is called the height of the analysis, and represents how depth we unfold the recursive data structures. The graph G p i is the minimal graph that contains n p i such that ∀u ∈ G p i .V Obj , for each field f 1 of T ype(u):

INRIA • either there exists a path u 1 1 u 1 2 . . . u 1 k u 2 1 u 2 2 . . . u 2 k . . . u h 1 u h 2 . . . u h k u labeled by ( f 1 , d f 2 , d f 3 , d . . . f k , d ) h in G p i such that ∀1 ≤ i ≤ h, 1 ≤ j ≤ h, T ype(u i l ) = T ype(u j l ), then (u, u h 1 , f 1 , d ) ∈ G p i .E. • or u.f 1 ∈ G p i .V and (u, u.f 1 , f, d ) ∈ G p i .E.
Then, we use that description of "formal" initial state. Let (L, , ) be a lattice of security levels; for example, L = {low, high}. Then, we can define security levels on types: let λ t : Fields × Class → L be a function that associates a security level with a field of a class. A security function is a function that associated security levels to inputs values and to return values (denoted by the set Ret):

λ i : 0≤i≤n G p i .V Val ∪Ret → L such that if v is the field f of a class C, then λ i (v) = λ t (f, C).
We say that a method is secure if values accessible from parameters, return value or static variables on paths contain at least a field of higher security level than their own. Theorem 7.1 (Secure information flow) Let m be a method, and λ i a security function. Let Q = (ρ, u ::

s, G) = instr m (Q init , ), and Ret = {v ∈ G.V | ∃(v, t) ∈ u}.
The method has secure information flow with respect to L if for every node v ∈ G.V Val and every path o 0 f1,t1

→ o 1 . . . o k f k ,t k → o k+1 with o 0 ∈ Ret∪{v ∈ G.V |= n s -1 ∨v = n p i }, ∃i such that λ i (v) λ t (f i , Type(o i )).
The advantage of our approach is that security annotations must not be known a priori. Changing a security level does not require a new analysis. Note that we can also have more precise policies on instances: if o and o have the same type, o.f and o .f can be given different security levels using a function λ e : G init .E → L instead of λ t . It is more precise but require the user to precise all the policies.

Conclusion

Information flow analysis aims to avoid that programs leak confidential information: observable/public outputs of a program must not disclose information about secret/private values manipulated by the program. Motivated by information flow analysis for Java bytecode, we propose an algorithm to compute dependency graphs, which tracks, at different program points, how input values may influence the outputs. Such a graph is a points-to graph extended with primitive values and flows arising from the control structure of a program. We prove the soundness of our construction by giving a non-interference theorem: a node a is related to a node b if the value of b may influence the value of a.

In contrast with usual information flow techniques, our approach is flow-sensitive and the security levels are not required to be known during the graph computation. Changing a security level does not require reanalyzing of the code.

Our main goal is to provide an algorithm which can be use for information flow. In the same time, as the dependency graph includes the points-to graph, our framework can be exploited for any points-to application in program analysis, such as escape analysis and optimization.

Further works includes increasing of accuracy by considering strong update or path-sensitivity in the analysis and studying relationships with existing information flow analysis by considering further abstractions of our analysis algorithm. Actual work concentrates on making our analysis compositional, which will better fit the Java paradigm of dynamic class loading. We consider two pairs (Q 1 , Γ 1 ) and (Q 2 , Γ 2 ) from the property space S such that

(Q 1 , Γ 1 ) (Q 2 , Γ 2 ), and let Q 1 = instr b (Q 1 , Γ 1 ) and Q 2 = instr b (Q 2 , Γ 2 ). We prove that Q 1 Q 2 .
We make a proof by case analysis on each instruction b, based on the transformation rules in Figure 6.

Case: b = prim op Let Q 1 = (ρ 1 , v 1 :: v 1 :: s 1 , G 1 ) and Q 2 = (ρ 2 , v 2 :: v 2 :: s 2 , G 2 ). Since Q 1 Q 2 , we also have ρ 1 ρ 2 , s 1 s 2 , G 1 ⊆ G 2 , v 1 ⊆ v 2 and v 1 ⊆ v 2 . Hence, (v 1 ∪ v 1 ) ⊆ (v 2 ∪ v 2 ). From the transformation rule, Q 1 = (ρ 1 , v 1 ∪ v 1 :: s 1 , G 1 ) and Q 2 = (ρ 2 , v 2 ∪v 2 :: s 2 , G 2 )
, and as the partial order relation holds on each component, we can conclude with

Q 1 Q 2 . Case: b = pop or b = ifeq a Let Q 1 = (ρ 1 , v 1 :: s 1 , G 1 ) and Q 2 = (ρ 2 , v 2 :: s 2 , G 2 ), Q 1 = (ρ 1 , s 1 , G 1 ) and Q 2 = (ρ 2 , s 2 , G 2 ). From hypothesis, (ρ 1 , v 1 :: s 1 , G 1 ) (ρ 2 , v 2 :: s 2 , G 2 ), and thus (ρ 1 , s 1 , G 1 ) (ρ 2 , s 2 , G 2 ).

Case: b = goto a

The abstract semantics rules do not change the input, thus

instr b (Q 1 , Γ 1 ) = Q 1 and instr b (Q 2 , Γ 2 ) = Q 2 . Since Q 1 Q 2 , we can conclude straightforward with instr b (Q 1 , Γ 1 ) instr b (Q 2 , Γ 2 ). Case: b = iconst n or b = newiC o b = aconst null
The instruction adds an abstract element on the stack (the same element for Q 1 and Q 2 ). Thus, the monotonicity is preserved.

Case: b = load x From hypothesis, (ρ 1 , s 1 , G 1 ) (ρ 2 , s 2 , G 2 ). Thus, ρ 1 (x) ⊆ ρ 2 (x) and (ρ 1 , ρ 1 (x) :: s 1 , G 1 ) (ρ 2 , ρ 2 (x) :: s 2 , G 2 ). Case: b = store x Let Q 1 = (ρ 1 , u 1 :: s 1 , G 1 ), Q 2 = (ρ 2 , u 2 :: s 2 , G 2 ), instr b (Q 1 , Γ 1 ) = (ρ 1 [x → u 1 ], s 1 , G 1 ), where u 1 = u 1 ∪ {(t, i) | t ∈ Γ 1 }], and instr b (Q 2 , Γ 2 ) = (ρ 2 [x → u 2 ], s 2 , G 2 ), where u 2 = u 2 ∪ {(t, i) | t ∈ Γ 2 }]. To prove the monotonicity, we must show that u 1 ⊆ u 2 . As Q 1 Q 2 and Γ 1 ⊆ Γ 2 (from hypothesis), we also have u 1 ⊆ u 2 and {(t, i) | t ∈ Γ 1 } ⊆ {(t, i) | t ∈ Γ 2 }. Hence, u 1 ⊆ u 2 and instr b (Q 1 , Γ 1 ) instr b (Q 2 , Γ 2 ). Case: b = getfield f C Let Q 1 = (ρ 1 , u 1 :: s 1 , G 1 ), Q 2 = (ρ 2 , u 2 :: s 2 , G 2 ), instr b (Q 1 , Γ 1 ) = (ρ 1 , u 1 :: s 1 , G 1 ) and instr b (Q 2 , Γ 2 ) = (ρ 2 , u 2 :: s 2 , G 2 ).
To prove the monotonicity, we must show that u 1 ⊆ u 2 , where

u 1 = {(e, d) | e ∈ adj G1 (e , f C , d ) ∧ (e , d) ∈ u 1 } ∪ {(e, i) | (e, i) ∈ u 1 }. From u 1 ⊆ u 2 , obviously, {(e, i) | (e, i) ∈ u 1 } ⊆ RT n°0347
{(e, i) | (e, i) ∈ u 2 }. Let us denote by u 1 the first set in u 1 . We now show that u 1 ⊆ u 2 , where

u 1 = {(e, d) | e ∈ adj G1 (e 1 , f C , d ) ∧ (e 1 , d) ∈ u 1 } u 2 = {(e, d) | e ∈ adj G2 (e 2 , f C , d ) ∧ (e 2 , d) ∈ u 2 }.
Since G 1 ⊆ G 2 and u 1 ⊆ u 2 , all the adjacents labeled by f C of e 1 (where (e 1 , d) ∈ u 1 ) are also adjacents of e 2 (where (e 2 , d) ∈ u 2 ). Thus u 1 ⊆ u 2 and u 1 ⊆ u 2 .

Case

: b = putfield f C Let Q 1 = (ρ 1 , v 1 :: u 1 :: s 1 , (V 1 , E 1 )), Q 2 = (ρ 2 , v 2 :: u 2 :: s 2 , (V 2 , E 2 )). Moreover, let instr b (Q 1 , Γ 1 ) = (ρ 1 , s 1 , (V 1 , E 1 )) and instr b (Q 2 , Γ 2 ) = (ρ 2 , s 2 , (V 2 , E 2 )).
To prove the monotonicity, we must show that E 1 ⊆ E 2 . From putfield abstraction transformation rule in Figure 6,

E 1 = E 1 ∪ E 1 ∪ E 1 ,
where

E 1 = {(e, e , f C , t )|(e, d) ∈ u, (e , t) ∈ v 1 }, E 1 = {(e, e , f C , i )|(e, d) ∈ u 1 , e ∈ Γ ∪ V u1 i }, V u1 i = {e | e, i ∈ u 1 }. The definition of E 2 is similar. By hypothesis, u 1 ⊆ u 2 and v 1 ⊆ v 2 , thus E 1 ⊆ E 2 . Moreover, as Γ 1 ⊆ Γ 2 , the inclusion E 1 ⊆ E 2 also holds. Thus, E 1 ⊆ E 2 .

B Soundness of the intra-method analysis

Proof.

By case analysis on each bytecode instruction. Except for the new bytecode, the other intructions do not add new nodes to memory graph and do not change the location of abjects. Thus, for a state

Q and Q = instr b Q, Q.G.V Obj = Q .G.V Obj and hence Q.G.ς(u) = Q .G.ς(u), for all u ∈ Q.G.V Obj .
For simplicity, we denote by ς(u) the value of Q.G.ς(u) and Q .G.ς(u).

Case: b = prim op

From the operational semantics of prim op (Figure 3), Q = ((i, ρ, v 1 :: v 2 :: s) :: f r, G) and instr b (Q) = ((i + 1, ρ, op(v 1 , v 2 ) :: s) :: f r, G). From the abstract rule of prim, Q = (ρ, v 1 :: v 2 :: s, G) and instr b (Q, Γ) = (ρ, v 1 ∪ v 2 :: s, G). From hypothesis, we have G α G, ρ α ρ, s α s and since v 1 , v 2 are not objects we also have (op(v 1 , v 2 ) :: s) α (v 1 ∪ v 2 :: s), and hence we can conclude with instr b (Q) α instr b (Q, Γ).

Case: b = pop or b = ifeq a From operational semantics, Q = ((i, ρ, n :: s) :: f r, G) and instr b (Q) = ((j, ρ, s) :: f r, G), where j is i + 1 or a. From the abstract rules, Q = (ρ, v :: s, G) and ) pushed on the concrete stack. The concrete graph G is enlarged with the new object, while the dependency graph already containts the abstract node (we remind that we suppose that all abstract values are computed from the begining).

instr b (Q, Γ) = (ρ, s, G). As we have Q α Q from hypothesis, it is obvious that instr b (Q) α instr b (Q, Γ).
Case: b = load x Let Q = ((i, ρ, s) :: f r, G) and Q = (ρ, s, G). From the operational semantics rule of load x (Figure 3), we have instr b (Q) = ((i + 1, ρ, ρ(x) :: s) :: f r, G). From the abstract transformation rule of load x (Figure 6), we have instr b (Q, Γ) = (ρ, ρ(x) :: s, G). By hypothesis, we have Q α Q, thus by definition, we have s α s, ρ α ρ and G α G The local variables array abstraction relation ρ α ρ implies that for all x such that ρ(x) ∈ Obj, for all n ∈ α(ς -1 (ρ(x))) we have (n, d) ∈ ρ(x). Since s α s, the definition of stack abstraction gives us (ρ(x) :: s) α (ρ(x) :: s). We can conclude with instr b (Q) α instr b (Q).

Case: b = store x From the concrete semantics rule, if Q = ((i, ρ, n :: s) :: f r, G), then instr b (Q) = ((i + 1, ρ ⊕ {x → n}, s) :: f r, G). From the abstract rules, if Q = (ρ, u ::

s, G), then instr b (Q, Γ) = (ρ[x → u ∪ {(t, i) | t ∈ Γ}], s, G).
The α-abstraction on stack and graphs is straightforward. From hypothesis and the α-abstraction definition on stack, we have that α(ς -1 (n)) ∈ u, thus ρ[x] ∈ ρ[x], and, as the other elements of the local variable array do not change, ρ α ρ. Moreover, by hypothesis s α s and G α G, thus the local soundness holds.

Case: b = putfield f C Let Q = ((i, ρ, v :: u :: s) :: f r, G) and Q = (ρ, v :: u :: s, G). We consider the case when v / ∈ V al (the case v ∈ V al is straightforward, as the edges between references do not change and neither does the stack and local variables array).

From the operational semantics rule of putfield (Figure 3), we have instr b (Q) = ((i + 1, ρ, s) :: f r, G ). From the abstract transformation rule of putfield (Figure 6), we have instr b (Q, Γ) = (ρ, s, G ). From the hypothesis, s α s, ρ α ρ.

RT n°0347

We still need to prove that G α G . Since G α G and because we only add and never delete edges to/from G, all we need to prove is that the edge added by instr b respects the abstraction property i.e. the abstraction of the edge added by instr b in G must be in G.

As, by definition

, G = G[(ς -1 (u), f C ) → ς -1 (v)], the only edge added to G is (ς -1 (u), ς -1 (v), f C ). From Q α Q
and the stack abstraction definition, we have:

(α(ς -1 (v)), d) ∈ v (α(ς -1 (u)), d) ∈ u
The abstract transformation rule of putfield adds to G edges having the form (n , n, f C , d ), ∀n ∈ u and ∀n ∈ v.

Thus, it adds also the edge

(α(ς -1 (u)), α(ς -1 (v)), f C , d ). Thus G α G . Case: b = getfield f C
From the semantics rules of getfield, the local variables array and the memory do not change. Thus, we have to prove the α-abstraction for the stack. Let Q = ((i, ρ, n :: :: f r, G) and Q = (ρ, u :: s, G).

By concrete and abstract semantics rules, instr b (Q) = ((i + 1, ρ, ς(n ) :: s) :: f r, G) and instr b (Q, Γ) = (ρ, u :: s, G). By hypothesis, we have s α s, hence we still need to show that the α-abstraction is preserved for the top of the resulted stack (between ς(n ) and u).

We have two cases: the field f C is of primitive type or is an object. For the first case, ς(n ) ∈ Val and thus the α-abstraction is preserved, as it does not apply on primitive values. We consider the second case, in which ς(n ) ∈ Obj . From Definition 4.5 of stack abstraction, we must prove that (α(n ), d) ∈ u, where n ∈ adj G (ς -1 (n), f C ). From the abstract semantics in Figure 6, Q 1 = (ρ 1 , v 1 :: s 1 , G 1 ) and instr b (Q 1 , Γ 1 ) = (ρ 1 , s 1 , G 1 ). As the only operation performed by these bytecodes is a pop from the stack, obviously instr From hypothesis, (ρ 1 , s 1 , G 1 ) . = (ρ 2 , s 2 , G 2 ). Thus, ρ 1 (x) . = ρ 2 (x) and thus (ρ 1 , ρ 1 (x) :: Case

b (Q 1 , Γ 1 ) . = instr b (Q 2 , Γ 2 ).
(Q 1 , Γ 1 ) = Q 1 and instr b (Q 2 , Γ 2 ) = Q 2 . Since Q 1 . = Q 2 , we can conclude straightforward with instr b (Q 1 , Γ 1 ) . = instr b (Q 2 , Γ 2 ).
s 1 , G 1 ) . = (ρ 2 , ρ 2 (x) :: s 2 , G 2 ). Case: b = store x Let Q 1 = (ρ 1 , u 1 :: s 1 , G 1 ), Q 2 = (ρ 2 , u 2 :: s 2 , G 2 ), instr b (Q 1 , Γ 1 ) = (ρ 1 [x → u 1 ], s 1 , G 1 ), where u 1 = u 1 ∪ {(t, i) | t ∈ Γ 1 }], and instr b (Q 2 , Γ 2 ) = (ρ 2 [x → u 2 ], s 2 , G 2 ), where u 2 = u 2 ∪ {(t, i) | t ∈ Γ 2 }].
(t, i) | t ∈ Γ 1 } to objects in ∅. Hence, instr b (Q 1 , Γ 1 ) . = instr b (Q 2 , Γ 2 ). Case: b = getfield f C Let Q 1 = (ρ 1 , u 1 :: s 1 , G 1 ), Q 2 = (ρ 2 , u 2 :: s 2 , G 2 ), instr b (Q 1 , Γ 1 ) = (ρ 1 , u 1 :: s 1 , G 1 ) and instr b (Q 2 , Γ 2 ) = (ρ 2 , u 2 :: s 2 , G 2 ).
: b = putfield f C Let Q 1 = (ρ 1 , v 1 :: u 1 :: s 1 , (V 1 , E 1 )), Q 2 = (ρ 2 , v 2 :: u 2 :: s 2 , (V 2 , E 2 )), instr b (Q 1 , Γ 1 ) = (ρ 1 , s 1 , (V 1 , E 1 )) and instr b (Q 2 , Γ 2 ) = (ρ 2 , s 2 , (V 2 , E 2 )). To prove the relation . =, we must show that (V 1 , E 1 ) . = (V 2 , E 2 )
, thus the putfield rule must add the same edges btween objects in E 1 and in E 2 .

From abstraction transformation rule in Figure 6,

E 1 = E 1 ∪ E 1 ∪ E 1 , where E 1 = {(e, e , f C , t )|(e, d) ∈ u, (e , t) ∈ v 1 } and E 1 = {(e, e , f C , i )|(e, d) ∈ u 1 , e ∈ Γ ∪ V u i }, V u1 i = {e | e, i ∈ u}.
. = v 2 , thus E 1 . = E 2 . Thus, (V 1 , E 1 ) . = (V 2 , E 2 ).

B.3 Proof of Proposition 5.15 (State variation correctness for single instruction block)

By case analysis on each instruction.

Case: b = prim op

The local variables array and the memory / dependency graphs are not affected by the execution of this bytecode, thus we still need to prove the state variation for the stack.

Let Q 1 .s = n 1 :: n 2 :: s, Q 1 .s = n 1 :: n 2 :: s, Q 1 .s = n 1 :: n 1 :: s . From the operational semantics rule of prim op in Figure 3, we have

Q 2 .s = op(n 1 , n 2 ), Q 2 = op(
1 .s = Q 1 .s[0 → x] with x ∈ V al. Thus, Q 2 .s = Q 2 .s[0 → op(x, n 2
)], which corresponds to rule 1 of Definition 5.11, as (η, t) belongs to the top of the stack in Q 2 .s ((η, t) ∈ n 1 and obviously (η, t)

∈ (n 1 ∪ n 2 )). Thus Q 2 .s = υ(Q 1 .s, Q 1 .s, β).

Case: b = pop

In both concrete and abstract semantics, the instructions pop a value from the stack. The rest of the stack, the local variables array and the memory/dependency graph remain unchanged. Thus, if Q 1 is the state variation of Q 1 with respect to Q 1 and β, and

Q 2 = instr b (Q 1 ) and Q 2 = instr b (Q 1 , Γ), then Q 2 is a state variation of Q 2 with respect to Q 2 and β. Case: b = goto a
The proof is similar with the one for pop bytecode, as the instruction does not change local the variables and memory / dependency graph and moreover, does not change the stack.

Case: b = iconst n or b = newiC or b = aconst null A constant value is pushed on the stack (for both states Q 1 and the state variation Q 1 ). The rest of the frame remains unchanged, thus the proof is straightforward.

Case

: b = load x Let Q 1 = (ρ, s, G), Q 2 = (ρ, ρ (x)
:: s, G) (from the abstract tranformation rules in Figure 6), Q 1 = ((i, ρ, s) :: f r, G) and Q 2 = ((i + 1, ρ, ρ(x) :: s) :: f r, G) (from the semantics rule in Figure 3).

Let Q 1 = ((i, ρ , s ) :: f r, G ) be the state variation , and

Q 2 = ((i + 1, ρ , ρ (x) :: s ) :: f r, G ).
The bytecode only pushes an element on the stack, thus the graph and local variables array do not change. From hypothesis, we have G = υ(G, G, β), thus the dependency graph in Q 2 is a state variation of the graph in Q 2 with respect to the graph in Q 2 and β. The same reasonement applies to the local variables. We still need to prove the state variation for stacks. q We know that s is a state variation of s with respect to s and β. The top of the stack in Q 2 (ρ (x)) respects the rules 1 and 2 of Definition 5.12 of local variables array variation, and thus is a state variation of the top of the stack in Q 2 (ρ(x)) with respect to the top of the stack in Q 2 (ρ 2 ) and β.

(α(Q 1 .G.ς -1 (u)), η, f C , i ) and (o, η, f C , i ) in Q 2 .
G. At the concrete level, the semantics will change the value of adjacent of α -1 (o) and not Q 1 .G.ς -1 (u), which respects the rule 1 of graph variation definition.

We consider now the case when the field f C is of type reference (v ∈ Obj ).

The idea is the same as the previous case, when v ∈ Val: we will make a case study based on the values of v and u, depending on β. We distinguish the following possibilities:

• for v ∈ Obj :

-either ∃η ∈ β such that (η, i) ∈ v -or ∀η ∈ β, (η, i) / ∈ v.
• for u ∈ Obj :

-either ∃η ∈ β such that (η , i) ∈ u -or ∀η ∈ β, (η , i) / ∈ u.
Case I: ∀η ∈ β, (η, i) / ∈ v and ∀η ∈ β, (η , i) / ∈ u In this case, the rules of the state variation do not apply on v and u, thus v = v and u = u. Since putf ield is executed on the same objects, the same edges are added and since Q

1 .G = υ(Q 1 .G, Q 1 .G, β), the conclusion is obvious Q 2 .G = υ(Q 2 .G, Q 2 .G, β).
(α(Q 1 .G.ς -1 (u)), η, f C , d ) and (α(Q 1 .G.ς -1 (u)), o, f C , d ) in Q 2 .G.
At the concrete level, the semantics will add the edge

(Q 1 .G.ς -1 (u), α -1 (o), f C ) in Q 2 .
G and not (Q 1 .G.ς -1 (u), v, f C ), as in Q 2 .G. The α-abstraction is still preserved for Q 2 .G and Q 2 .G, as the (α(u), o, f C , d ) ∈ Q 2 .G.E. Thus Q 2 .G α Q 2 .G, and, according to rule 2 of Definition 5.10, we obtain the graphe variation: Case IV: ∀η ∈ β, (η, i) / ∈ v and ∃η ∈ β such that (η , i) ∈ u This case is a simplification of the previous one, thus the proof is similar.

Q 2 .G = υ(Q 2 .G, Q 2 .G, β).

INRIA

Remind that instr B and Γ e is computed from E B and instr B1 , Γ e1 and instr B2 , Γ e2 are computed from E B1 , E B2 respectively. From these definitions and the fact that due to the definition of contexts, Γ e1 is computed independently of E B2 , one can see that instr B (Q, Γ) is instr B2 (instr B1 (Q 1 , Γ 1 ), Γ e1 ) where Γ e1 is computed for E B1 with (Q 1 , Γ 1 ) as initial state.

-As k 1 is strictly smaller than k, by induction hypothesis, we have for G 1 (and thus, B 1 ) that for any concrete state Q 1 , any abstract state

Q 1 such that Q 1 α Q 1 , Q 2 = instr B1 (Q 1 )
, and Q 2 = instr B1 (Q 1 , Γ 1 ).

If Q 1 = υ(Q 1 , Q 1 , β) and Q 2 = instr B2 (Q 1 ) then Q 2 = υ(Q 2 , Q 2 , β).
-As k 2 is strictly smaller than k, by induction hypothesis, we have for G 2 (and thus, B 2 ) that for any concrete state Q 2 , any abstract state

Q 2 such that Q 2 α Q 2 , Q 3 = instr B2 (Q 2 )
, and

Q 3 = instr B2 (Q 1 , Γ 1 )
.

If Q 1 = υ(Q 1 , Q 1 , β) and Q 2 = instr B2 (Q 1 ) then Q 2 = υ(Q 2 , Q 2 , β).
Hence, by combining these two results, one has that for any concrete state Q 1 , any abstract state Q 1 such that Q 1 α Q 1 , any Γ 1 , denoting Q 3 the abstract state instr B2 (instr B1 (Q 1 , Γ 1 ), Γ e1 ), For any concrete state Q 1 , any abstract state Q 1 such that Q 1 α Q 1 , we consider Q 1 = υ(Q 1 , Q 1 , β). We assume that the execution of B on Q 1 leads to execute the block B 1 , that is the top of the stack s 1 in Q 1 is equal to 0 (the other case is dual can be be treated similarly). Let Q 2 = instr ifeq a (Q 1 ), Q 3 = instr B1 (Q 2 ) and Q 4 = instr B3 (Q 3 ). Now depending on the top of the stack s 1 in the abstract state Q 1 :

if Q 1 = υ(Q 1 , Q 1 , β) and instr B2 (instr B1 (Q 1 , Γ 1 ), Γ e1 ), then Q 3 = υ(Q 3 , Q 3 , β).
-there is no η from β such that η, i ∈ s 1 [0]: by definition of state variation, the top of the stack s 1 in Q 1 is equal to 0. Let us consider Q 2 = instr ifeq a (Q 1 ); as s 1 [0] = 0, it is easy to see due to the semantics of the bytecode ifeq a, Q 2 = υ(Q 2 , Q 2 , β) where Q 2 = instr ifeq a (Q 1 , Γ 1 ). Now, by induction hypothesis for the block B 1 , we have

Q 3 = υ(Q 3 , Q 3 , β)
where

Q 3 = instr B1 (Q 2 ) and Q 3 = instr B1 (Q 2 , Γ 1 ). Let us denote Q 4 = instr B2 (Q 2 )
. By weakening the state variation, one has

Q 3 = υ(Q 3 , Q 3 Q 4 , β)
. By induction hypothesis for the block B 3 , denoting Q 4 = instr B3 (Q 3 ), we have

Q 4 = υ(Q 4 , instr B3 (Q 3 Q 4 , Γ e1 ), β)
We conclude simply by using the definition of instr B .

INRIA

-there exists some η from β such that η, i ∈ s 1 [0]: assume Q 1 = ((i, ρ, v :: s) :: f r, G), the state variation Q 1 is of the form ((i, ρ , v :: s ) :: f r, G ).

Let us consider Q 2 = instr ifeq a (Q 1 ) = ((k, ρ, s) :: f r, G) and Q 2 = instr ifeq a (Q 1 ) = ((k , ρ , s ) :: f r, G ). If k = k then this case is similar to the previous case. So, we assume that k = k ; Let Q 3 = instr B1 (Q 2 ) and Q 3 = instr B2 (Q 2 ); we are going to show first that

Q 3 = υ(Q 3 , instr B1 (Q 2 , Γ e1 ) instr B2 (Q 2 , Γ e1 ), β).
Let u be the top of the stack in Q 1 . Then, for all i in both B 1 and B 2 , we have that all e such that e, i ∈ u belong to Γ i . Intuitively, due to the abstract semantics, this implies that all the modified position (memory, local variables, stack) in concrete states can be identified in abstract states, and are concern by state variation. Thus, they can vary to show that

Q 3 = υ(Q 3 , Q 3 Q 3 , β)
. Now, we can use the induction hypothesis for the block B 3 to conclude using the definition of instr B and of instr B .

• (if then) -(if else) : these cases are treated similarly to the (if then else) case.

• (while) : let us name respectively B 1 , B 2 , the non-terminals in the right-hand side, B 1 being the block within the loop and B 2 the end block of the loop. Let G 1 , G 2 the graphs without non-terminals such that in the derivation producing G, B 1 → k1 G 1 and B 2 → k2 G 2 Let B 1 , B 2 be the blocks corresponding to G 1 , G 2 respectively. Let B be the block composed by the if eq node and B 1 .

For a concrete state Q 1 = ((i 1 , ρ 1 , s 1 ) :: f r, G 1 ), let us denote Q 2 = instr B (Q 1 ) = ((i 2 , ρ 2 , s 2 ) :: f r, G 2 ) for some Γ 1 , and let us consider an abstract state

Q 1 such that Q 1 α Q 1 , we consider Q 1 = υ(Q 1 , Q 1 , β) and Q 2 = instr B (Q 1 )
with Q 1 = ((i 1 , ρ 1 , s 1 ) :: f r, G 1 ) and Q 2 = ((i 2 , ρ 2 , s 2 ) :: f r, G 2 ). Let us denote Q 2 such that Q 2 = instr B (Q 1 , Γ 1 ) for some Γ 1 and Q 2 α Q 2 .

If the state variation does not impact the top of the stack in Q 1 then the control flow in the concrete execution is not modified and we are in the same situation than for the (if then else).

If the top of the stack is impacted by the variation. Due to the abstract semantics that adds elements from Γ 1 to any manipulation of the state in B 1 , any node or edge of G 2 that differs from G 1 is such that is mapping in G 2 is linked by implicit flow to elements of Γ 1 . The same goes for G 1 and G 2 . Thus, everything in the ntersection of G 2 and G 2 comes from G 1 and the rest is linked to elements of β either because it has been modified in the loop or because it has been modifed by the initial variation. In both cases it can vary under β and then G 2 = υ(G 2 , G 2 , β). We can treat similarly local variables and the stack: the specification of Java bytecode tells us that s 2 and s 2 have the same size, even if the block B may have been executed different numbers of times to lead to Q 2 and Q 2 .

• (repeat) -(while not) -(repeat not) : these cases are treated similarly to the (while) case.

C Soundness of inter-procedural analysis

We have to add the cases of the two new bytecodes (invoke and areturn), to the proofs that have been done by case analysis on each bytecode.

RT n°0347

  For two classes B, C, B ≤ C if and only if B = C or C is a super class of B. The function T ype : Obj → Class returns the type of an object. The set of JVM values is defined as Jv = Val ∪ Obj where Val is the set of primitive values, and Obj the set of objects, including the special value null.

Figure 2 :

 2 Figure 2: Memory Example

Figure 4 :

 4 Figure 4: Graph grammar

Figure 5 :

 5 Figure 5: A Dependency Graph

Figure 6 :

 6 Figure 6: Subset of the abstract transformation rules

Figure 7 :

 7 Figure 7: Relations Example

Definition 4 . 6 (

 46 State abstraction)Let α be an abstraction function. Given a concrete state Q = ((pc, ρ, s) :: f r, G) and an abstract state Q

Lemme 5 . 4 (

 54 Local Soundness) Let α be an abstraction function. Let Q be an execution state and Q an abstract state such that Q α Q. Then for any bytecode b, for any set of abstract values Γ, instr b

Figure 8 :

 8 Figure 8: Abstract semantics rules for method invocation

  ) and 9(b).

  b nm +2 : goto h(i + 1) c 0 : invoke m h(i + 1) : ... (b) Transformed code Qa 0 = (ρ, un m :: • • • :: u 0 :: s, G)

Figure 9 :

 9 Figure 9: Bytecode transformation

Definition 6 . 1 (

 61 State abstraction (extension))Let α be an abstraction function. Given a concrete state Q = ((pc, ρ, s) :: f r, G) and an abstract state Q

  s, β) with s = v :: s and s = v :: s if ρ = ζ • s = υ(s, s, β), and ρ = υ(ρ, ρ, β), otherwise.

RT n°0347 14 5 . 1 17 6-method analysis 19 6 . 1 BINRIAA Proof of Lemma 4 . 2 (

 51176142 Abstraction correctness . . . . . . . . . . . . . . . . . . . . . . . . . 14 5.2 Analysis correctness . . . . . . . . . . . . . . . . . . . . . . . . . . InterAbstract semantics of the method invocation . . . . . . . . . . . . . . 19 6.2 Inter-procedural control flow graph . . . . . . . . . . . . . . . . . . . 21 6.3 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Soundness of the intra-method analysis 28 B.1 Proof of Lemma 5.4 (Local soundness) . . . . . . . . . . . . . . . . . 28 B.2 Proof of Proposition 5.7 . . . . . . . . . . . . . . . . . . . . . . . . . 30 B.3 Proof of Proposition 5.15 (State variation correctness for single instruction block) 32 B.4 Proof of Proposition 5.15 (State variation correctness for blocks) . . . 35 C Soundness of inter-procedural analysis 37 C.1 Addition to proof of Lemma 4.2 . . . . . . . . . . . . . . . . . . . . 38 C.2 Addition to proof of Lemma 5.4 . . . . . . . . . . . . . . . . . . . . 38 C.3 Addition to proof of Proposition 5.7 . . . . . . . . . . . . . . . . . . 39 C.4 Addition to proof of Proposition 5.15 . . . . . . . . . . . . . . . . . 39 Monotonicity of the transformation rules)

B. 1

 1 Proof of Lemma 5.4 (Local soundness) Lemme B.1 (Local Soundness) Let α be an abstraction function. Let Q be an execution state and Q an abstract state such that Q α Q. Then for any bytecode b, for any set of abstract values Γ, instr b (Q) α instr b (Q, Γ).

INRIA 1 .

 1 Case: b = goto a Let Q = ((i, ρ, s) :: f r, G) and instr b (Q) = ((a, ρ, s) :: f r, G). The abstract semantics of goto instruction does not change the input state Q, and thus instr b (Q, Γ) = Q. The concrete semantics rule makes a jump to adress a and leaves unchanged the rest of the frame Q. Hence the α-abstraction relation is preserved, and instr b (Q) α instr b (Q, Γ).Case: b = iconst nThe bytecode adds a primitive value on top of the stack, thus since primitive values are not concerned by α-abstraction, we have instr b (Q) α instr b (Q, Γ).Case: b = aconst nullThe bytecode adds pushes null on the concrete stack and n null -1 on the abstract stack. By definition, α(ς -1 (null)) = n null -Case: b = new CThe instruction pushes a new object on the stack. By construction, due to the allocation site model, the value pushed by the abstract rule (n n i ) is the abstraction of the concrete object (C fresh(Ci,G) i

B. 2 7

 27 By hypothesis, we also have G α G, which means that α(ΠObj (G)) ⊆ G. By definition, α(G).E = {(α(v), α(v ), e, d ) | v, v ∈ G.V Obj ∧ (v, v , e) ∈ G.E}. As α(G).E ⊆ G.E and (n, n , f C ) ∈ G.E, we have (α(n), α(n ), f C , d ) ∈ G.E,and from the value of u from the abstract transformation rule of getf ield, we can conclude with (α(n ), d) ∈ u . Proof of Proposition 5.Details of the case analysis for the proof of the Proposition 5.7. Case: b = prim op The instruction pops two operands from the stack and pushes back the result of op on these operands. The operands are of primitive types. Thus the relation . = holds for the resulted stack. The local variables array and the graph are not changed. Case: b = pop or b = ifeq a

INRIA Case: b = goto a

  The transformation rules do not change the input, thus instr b

Case: b

 b = iconst iv or b = aconst null or b = new iC The instruction adds an abstract element on the stack, either n c i , d or n null -1 , d or n n i , d , which is always the same for Q 1 and Q 2 . Thus, the . = relation is preserved. Case: b = load x

1 . = u 2 , where u 1 =

 121 To prove the relation . =, we must show that u 1 . = u 2 , where u 1 = {(e, d) | e ∈ adj G1 (e , f C , d ) ∧ (e , d) ∈ u 1 } ∪ {(e, i) | (e, i) ∈ u 1 }. The elements in {(e, i) | (e, i) ∈ u 1 } refer to value nodes, thus they do no present interest. Let us denote by u 1 the first set in u 1 . We now show that u {(e, d) | e ∈ adj G1 (e 1 , f C , d ) ∧ (e 1 , d) ∈ u 1 } u 2 = {(e, d) | e ∈ adj G2 (e 2 , f C , d ) ∧ (e 2 , d) ∈ u 2 }. Since G 1 . = G 2 and u 1 . = u 2 , all the adjacents labeled by f C of e 1 (where (e 1 , d) ∈ u 1 ) are also adjacents of e 2 (where (e 2 , d) ∈ u 2 ). Thus u 1 . = u 2 and u 1 . = u 2 .

INRIA

  Case III: ∃η ∈ β such that (η , i) ∈ u According to the rule 2 of Definition 5.11 of stack variation, u = u and u = ς(α -1 (o), with (o, d) ∈ u. The transformation rule of putfield creates the links

  Case II: ∃η ∈ β such that (η, i) ∈ v and ∀η ∈ β, (η , i) / ∈ u According to the rule 2 of Definition 5.11 of stack variation, v = v and v = ς(α -1 (o)), with (o, d) ∈ v. The transformation rule of putfield creates the links

  Case III: ∃η ∈ β such that (η, i) ∈ v and ∃η ∈ β such that (η , i) ∈ uAccording to the rule 2 of Definition 5.11 of stack variation, u = u and u= ς(α -1 (o)), with (o, d) ∈ u. In the same way, v = v and v = ς(α -1 (o )), with (o , d) ∈ v.The transformation rule of putfield creates the links(α(u), η, f C , d ), (o, η, f C , d ) and (α(u), o , f C , d ) and (o, o , f C , d ) in Q 2 .G.At the concrete level, the semantics will add the edge(α -1 (o), α -1 (o ), f C ) in Q 2 .G and not (u, v, f C ), as in Q 2 .G. The α-abstraction is still preserved for Q 2 .G and Q 2 .G, as the (o, o , f C , d ) ∈ Q 2 .G.E. Thus Q 2 .G α Q 2 .G,and, according to rule 2 of Definition 5.10, Q 2 .G = υ(Q 2 .G, Q 2 .G, β).

  This allows us to conclude this case due to the definition of instr B . • (if then else) : let us name respectively B 1 , B 2 , B 3 the non-terminals in the right-hand side, B 1 being the "then" block, B 2 the "else" and B 3 the junction block. Let G 1 , G 2 , G 3 the graphs without non-terminals such that in the derivation producing G, B 1 → k1 G 1 , B 2 → k2 G 2 and B 3 → k3 G 3 . Let B 1 , B 2 , B 3 be the blocks corresponding to G 1 , G 2 , G 3 respectively. Let e, e 1 , e 2 , e 3 be the exit points of B, B 1 , B 2 , B 3 respectively.

  To prove the relation . =, we must show that u 1 . = u 2 , which holds because , from hypothesis, we have u 1 . = u 2 and the restriction of set {

  The definition of E 2 is similar. Edges in E 1 are between objects and values, thus are not considered by . =. We must refer only to E 1 and E 2 . From hypothesis, u 1 . = u 2 and v 1

  n 1 , n 2 ) and, from the abstract transformation rule, Q 2 .s = (n 1 ∪ n 2 ) :: s. As n 1 and n 2 must be primitive values (n 1 , n 2 ∈ Val), only the rule 1 of Definition 5.11 (stack variation) can be applied to them.If there exists η ∈ β, t ∈ F such that (η, t) ∈ n 1 , then the value on the top of the stack is randomize and Q

The graph isomorphisms we consider take in consideration both vertex and edge labelling.INRIA

RT n°0347

Case: b = store x

The instruction stores the top of the stack in the local variable x. The proof is similar to the load x bytecode: the top of the stack in the state variation Q 1 respects the rules 1 and 2 of stack variation definition, thus the local variable x in Q 2 respects the rules 1 and 2 of local variables array variation.

Case: b = putfield f C Let Q 1 .s = v :: u :: s, Q 1 .s = v :: u :: s, Q 1 .s = v 1 :: u 1 :: s 1 .

Since putfield does not affect the local variables and only pops elements from the stack, we have:

By hypotesis, Q 1 .ρ = υ(Q 1 .ρ, Q 1 .ρ, β), thus replacing Q 1 .ρ by Q 2 .ρ and Q 1 .ρ by Q 2 .ρ, we obtain the variation for local variables: Q 2 .ρ = υ(Q 2 .ρ, Q 2 .ρ, β). We apply the same resonement for the stack: s = Q 2 .s and s 1 = Q 2 .s. From the hypotesis, Q 1 .s = υ(Q 1 .s, Q 1 .s, β), thus s 1 = υ(Q 2 .s, s, β). By replacing s by Q 2 .s and s 1 by Q 2 .s, we obtain the variation for the stack:

To completely prove the state variation correctness, we still need to prove the graph variation:

Depending on the type of the top of the stack v, there are two semantics rules for the putfield instruction (as depicted in Figure 3). We consider each case: v is a primitive value or an object.

Let us first consider that the field manipulated is of primitive type (v ∈ Val ).

We will make a case study based on the values of v and u, depending on β. We distinguish the following possibilities:

• for u ∈ Obj :

Based on the combination of cases presented above, we distinguish the following cases for the abstract stack, thus the following possibilities to compute the state Q 1 .

Case I: ∀η ∈ β, t ∈ F, (η, t) / ∈ v and ∀η ∈ β, (η , i) / ∈ u In this case, the rules of the state variation do not apply on v and u, thus v = v and u = u. Since putfield is executed on the same objects, the same edges are added and since

Case II: ∃η ∈ β, t ∈ F such that (η, t) ∈ v and ∀η ∈ β, (η , i) / ∈ u We have a new value for v and u is not affected by the state variation (u = u ). According to the concrete semantics,

Thus, the graphs Q 2 .G differs from Q 2 .G according to rule 1 of the definition 5.10 of Graph variation. Thus, Q 2 .G is a graph variation of Q 2 .G with respect to Q 2 .G and β.

RT n°0347

Case: b = getfield f C

The intruction pops an object and pushes the field f C on the stack. Thus, to prove the state variation correctness, we must refer only to the new object/value pushed on the stack (the field f C ) and prove that it can change only accordingly to rules 1 or 2 of Defition 5.11.

Let Q 1 .s = u :: s, Q 1 .s = u :: s, and Q 1 .s = u :: s be the state variation, with u ∈ Obj . Moreover, let Q 2 .s = v :: s, Q 2 .s = v :: s, and Q 1 .s = v :: s .

We can have two cases: 1) for all η ∈ β , (η, i) / ∈ u or 2) there exists η ∈ β such that (η, i) ∈ u.

1) Let us consider the first case: rule 2 does not apply to the top of the stack in Q 1 , thus u = u. The getfield bytecode pushes on the stack the adjacent of

We have again two cases (we denote by u the node containing the object u; u = Q 1 .G.ς -1 (u)):

In the second case, the adjacent labeled f C of u does not change (conform to rule 2 of graph variation definition), thus the instruction pushes the same object/value on the stack for both

We consider now the first case (α(u ) has an adjacent in β in Q 1 .G ). Than there exists η ∈ β and t ∈ F and an edge

If the field f C is of primitive type, the value of adj Q1.G (u , f C ) might change according with the rule 1 of graph variation definition (Definition 5.10). Thus, the value pushed on the stack in Q 1 .G will differ from the one in Q 1 .G, but it will respect the rule 1 of Definition 5.13, since the abstract value (η, t) will be pushed on the abstract stack in

If the field f C is of type reference, the adjacent of u might change according to the rule 2 of graph variation definition. Since Q 1 .G α Q 1 .G and from the points-to correctness (Proposition 5.5), we have

Hence the stack respects the rule 2 of stack variation definition.

2) Let us consider now the case when there exists η ∈ β such that (η, i) ∈ u. Thus the rule 2 of Defition 5.11 applies to u, and u = α -1 (o), with (o, i) ∈ u. From the abstract semantics of getfield, (η, i) is kept on the stack ((η, i) ∈ v). Thus, the value of v will change, but it will respect the rules 1 or 2 of stack variation definition (the proof is similar with the previous case, depending on the type of f C , primitive or reference).

B.4 Proof of Proposition 5.15 (State variation correctness for blocks)

C.1 Addition to proof of Lemma 4.2

We must show that the abstract semantics rules are monotone. We consider two pairs

By case analysis on each instruction b, based on the transformation rules in Figure 8.

Case: b = invoke m

Let Q 1 = (ρ, u nm :: • • • :: u 0 :: s, G) and Q 2 = (ρ , u nm :: • • • :: u 0 :: s , G ). From the semantics of invoke,

Case: b = areturn

Let Q 1 = (ρ, u :: s, G) and Q 2 = (ρ , u :: s , G ). From the semantics of areturn,

C.2 Addition to proof of Lemma 5.4

We show here the local soundness of the extended model, that is the abstract semantics rules for invoke and areturn (defined in Figure 8) respect the local soundness, as defined in Theorem 5.4, in respect with the state abstraction extension (Definition 6.1).

Case: b = invoke m

From the operational semantics of invoke m (Figure 3), we have

From the abstract rule of invoke m (Figure 8), (ρ, u nm ::

From hypothesis, we have G α G, p 0 α u 0 . . . p nm α u nm . Moreover, the stacks are empty and α . Thus, instr b (Q) α instr b (Q, Γ) according to definition 6.1 .

INRIA

Case: b = areturn From the operational semantics of areturn in Figure 3, we have Q = ((i, ρ, v :: s) :: (i , ρ , s ) :: f r, G)

From the abstract rule of areturn:

From hypothesis, Q α Q, hence G α G, ρ α myabsρ, v α myabsu and s α s.

) according to definition 6.1 if G α G and v α u which holds by hypothesis.

C.3 Addition to proof of Proposition 5.7

We prove the second point of the Proposition for both bytecodes, invoke m and areturn: for any

.

Case: b = invoke m

Let Q 1 = (ρ, u nm :: • • • :: u 0 :: s, G) and Q 2 = (ρ , u nm :: • • • :: u 0 :: s , G ). From the semantics of invoke in Figure 8,

Case: b = areturn

Let Q 1 = (ρ, u :: s, G) and Q 2 = (ρ , u :: s , G ). From the semantics of areturn in Figure 8,

C.4 Addition to proof of Proposition 5.15

Case: b = invoke m

From the operational semantics of invoke m (Figure 3), we have

From the abstract rule of invoke m (Figure 8),

Let Q be the state variation and

From hypothesis, we have Q .G = υ(Q.G, Q.G, β). The stack are empty, thus the state variation relation holds. We need to prove the state variation for the local variables array. In Q , p 0 varies according to rules 1 and 2 of Definition 5.11 in function of β and u 0 (the corresponding value on the abstract stack). In instr b (Q ), the value of local variable 0 (which is p 0 ) is a variation of the local variable 0 in the abstract state instr b (Q, Γ) (which is u 0 ) and of β, thus it respects the rules 1 and 2 of Definition 5.12 which define the definition of local variables. We apply the same reasoment on the rest of the local variables, and we obtain the state variation for local variables array.

Thus instr b (Q ) = υ(instr b (Q), instr b (Q, Γ), β).

Case: b = areturn

From the operational semantics of areturn (Figure 3), we have Q = ((i, ρ, v :: s) :: (i 0 , ρ 0 , s 0 ) :: f r, G) instr b (Q) = ((i 0 + 1, ρ 0 , v :: s 0 ) :: f r, G).

From the abstract rule of areturn: