Keywords: Static analysis, abstract interpretation, bytecode Java, Coq

Certification de résultat pour l'analyse de programme relationnelle

Résumé : Nous proposons une analyse générique de programme relationnelle pour un langage de bytecode impératif avec pile d'opérande, procédures, tableaux et variables globales. Cette analyse est instanciée avec un domaine abstrait de polyèdres. Elle propose une inférence automatique d'invariants de boucle et de préconditions/postconditions de procédures, ainsi qu'une vérification efficace du résultat de l'analyse par un vérificateur simple. Les invariants, qui peuvent être grands, peuvent être spécialisés pour prouver une propriété de sûreté en utilisant une technique automatique de compression de taille de certificat. Le résultat de l'analyse peut être vérifié efficacement en annotant le programme avec une partie des invariants et quelques certificats d'inclusion de polyèdre, qui permettent d'éviter certaines calculs polyédriques complexes comme le calcul de l'enveloppe convexe de deux polyèdres. Nous obtenons des certificats d'inclusion petits et facilement vérifiables grâce au lemme de Farkas pour prouver l'absence de solution dans un système d'inégalités linéaires. Le vérificateur ainsi obtenu est suffisamment simple pour être entièrement certifié avec l'assistant à la preuve Coq.

Mots-clés : Analyse statique, interprétation abstraite, bytecode Java, Coq

Introduction

Logic-based, static program verification, be it in form of abstract interpretation, symbolic model checking or interactive proving of programs, is used in a number of ways to improve the confidence in safety-critical systems and for protecting host machines from malicious code, as e.g., done by the Java byte code verifier.

As applications and the program logics grow in complexity, an automated technique for verifying program invariants based on a program logics should ideally meet all of the following three requirements:

Automatic Inference: the complexity of both programs and the underlying logic can quickly make it burdensome to conduct program proofs manually. Automatic inference of program properties is necessary to obtain a technique that scales.

Result certification: when inference is available, it often relies on advanced deductive methods for inferring an invariant whose size and complexity make it difficult to ascertain its validity manually. Efficient checking of the result of the inference or of any proposed invariant in general becomes important.

Small Trusted Computing Base (TCB): the result checker becomes the cornerstone of the reliability of the verification framework. In order to reduce the part of the code base that needs to be trusted without proof, the checker should be kept sufficiently simple and small in order to be able to verify the checking algorithmics mechanically.

Program verification based on general Hoare-style program logics may follow the Verification Condition Generator (VCGen) approach of e.g., Extended Static Checking by Flanagan, Leino et al. [START_REF] Cormac Flanagan | Extended static checking for Java[END_REF] or use expressive type systems such as the dependent type systems of Xi and Pfenning [START_REF] Xi | Imperative Programming with Dependent Types[END_REF] for proving properties of programs. The approaches based on VCGens are generally complete for partial correctness and will produce a set of verification conditions which, when satisfied, will allow to conclude that a given program property holds in the logic. Verification conditions often fall into fragments of logic that require them to be proved by dedicated decision procedures or theorem provers. VCGens and the type-based approaches are primarily concerned with invariant checking and discard part of the inference problem by relying on loop invariants and prepost-condition of methods to be provided by the programmer. In terms of small TCB, the VCGens remain complex software which are hard to prove correct in extenso. The machine-checked formalizations e.g., by Nipkow, Wildmoser et al. [START_REF] Wildmoser | Asserting bytecode safety[END_REF][START_REF] Wildmoser | Prototyping proof carrying code[END_REF] show that this is indeed possible to certify an entire VCGen inside a proof assistant but also that this remains a major software certification challenge.

Another strand of program verification is based on abstract interpretation. Abstract interpretation is an automatic technique for inferring program properties in the form of fixpoints of monotone data flow functions. As a theory of proving programs it has strong semantic foundations. At the same time it should be noted that the algorithmics of the domains underlying the more advanced analyses such as polyhedral analysis (initially described by Cousot and Halbwachs [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF]) is highly non-trivial. Checking an invariant is in theory simple as it only requires one more iteration to check that a property is indeed a RR n ¡ 6333 fixpoint but, as said, this computation does in certain cases rely on non-trivial algorithmics that forms part of what must be trusted. In previous work [START_REF] Cachera | Extracting a data flow analyser in constructive logic[END_REF][START_REF] Pichardie | Interprétation abstraite en logique intuitioniste: extraction d'analyseurs Java certifiés[END_REF], some of the authors formalised the theory of abstract interpretation inside the proof assistant Coq and extracted Caml implementations of a variety of program analyses. This Certified Abstract Interpretation approach represents a systematic way of reducing the TCB of static analyzers and fulfills the three requirements listed above. However, a fully mechanised correctness proofs of more advanced program analysers such as an optimised, polyhedral-based analysis would require an enormous effort in terms of program certification.

The purpose of this paper is to demonstrate that by focusing on certifying the result of the analysis rather than the analysis itself, it is possible to develop a verification framework for advanced program properties that satisfies all of the three desired properties and, at the same time, requires a significantly smaller effort in order to be proved correct. This idea was previously used by Wildmoser et al [START_REF] Wildmoser | Bytecode analysis for proof carrying code[END_REF] who use the result of an untrusted interval analysis in a VCGen for byte code and by Leroy [START_REF] Leroy | Formal certification of a compiler back-end or: programming a compiler with a proof assistant[END_REF] in his certification of a compiler back-end where he, rather than certifying the complex graph-coloring algorithms for register allocation, proves the correctness of a checker that verifies a given coloring returned by an untrusted graph-coloring algorithms. Here, we generalise this idea by developing a relational analysis framework together with a certified checker. The basic observation is that an abstract interpretation can be decomposed into an abstract domain of properties, a generic program logic for reasoning about these properties and a fixpoint engine for solving recursive equations over the abstract domains. The inference does not need to use certified abstract domain operations and fixpoint engines, and the checking of invariants does not need to use a fixpoint engine at all. We take advantage of this to design a checker that re-uses the program logic but replaces the more complex domain operations with simpler ones, at the expense of providing some extra information in the certificate accompanying a program.

Overview

In the first part of this paper, we will develop a fully relational, interprocedural analyser which automatically infers an invariant for each control point in the program, a pre-condition that must hold at the point of calling a procedure and a post-condition that is guaranteed to hold when the procedure returns. Relational analyses are useful for finding loop invariants needed for proving program safety, e.g. when verifying the resource usage of programs or verifying safety properties related to safe memory access such as checking that all array accesses are within bounds. We will take Safe Array Access as an example safety policy and illustrate our approach with the Binary Search example given in Fig. 1, showing how the analysis will prove that the instruction that accesses the array vec with index mid will not index out of bounds.

We have annotated the code of Binary Search with the invariants that have been inferred automatically. Invariants refer to values of local and global variables and can also refer to the length of an array. For example, the invariant (I 3 ) asserts among other properties that when entering the while loop, the relation 0 ≤ low < high < |vec| is satisfied. Similarly, the post-condition ensures that the result is a valid index into the array being searched, or -1, indicating that

INRIA // PRE: 0 ≤ |vec 0 | static int bsearch(int key, int[] vec) { // (I 1 ) key 0 = key ∧ |vec 0 | = |vec| ∧ 0 ≤ |vec 0 | int low = 0, high = vec.length -1; // (I 2 ) key 0 = key ∧ |vec 0 | = |vec| ∧ 0 ≤ low ≤ high + 1 ≤ |vec 0 | while (0 < high-low) { // (I 3 ) key 0 = key ∧ |vec 0 | = |vec| ∧ 0 ≤ low < high < |vec 0 | int mid = (low + high) / 2; // (I 4 ) key 0 = key ∧ |vec 0 | = |vec| ∧ 0 ≤ low < high < |vec 0 | ∧ low + high -1 ≤ 2 • mid ≤ low + high if (key == vec[mid]) return mid; else if (key < vec[mid]) high = mid -1; else low = mid + 1; // (I 5 ) key 0 = key ∧ |vec 0 | = |vec| ∧ -2 + 3 • low ≤ 2 • high + mid ∧ -1 + 2 • low ≤ high + 2 • mid ∧ -1 + low ≤ mid ≤ 1 + high ∧ high ≤ low + mid ∧ 1 + high ≤ 2 • low + mid ∧ 1 + low + mid ≤ |vec 0 | + high ∧ 2 ≤ |vec 0 | ∧ 2 + high + mid ≤ |vec 0 | + low } // (I 6 ) key 0 = key ∧ |vec 0 | = |vec| ∧ low -1 ≤ high ≤ low ∧ 0 ≤ low ∧ high < |vec 0 | return -1; } // POST: -1 ≤ res < |vec 0 |
Figure 1: Binary search the element was not found. In addition, the analysis introduces a 0-indexed variable (such as e.g. key 0 in the example) for each parameter (and also for the global variables, of which there are none in the example) in order to refer to its value when entering the procedure. The effect of this is that the invariant on exit of the program defines a relation between the input and the output of the procedure, thus yielding a summary relation for the procedure.

Compressing invariants

Abstract interpretations may give you more information than you need for proving a particular property. In the case of the Binary Search example, if we are only interested in proving the validity of array accesses, there are a number of relations between variables in the invariants that can be forgotten. Reducing the number of constraints and the number of variables under consideration can lead to a significant gain in execution time when it comes to checking a proposed invariant. For example, pruning the invariants in Fig. 1 with respect to this property yields the simpler invariant shown in Fig. 2: Notice that the inferred loop invariant I 3 is close to what a specifying programmer of Binary Search might have come up with, but here produced automatically. We explain pruning of procedures in Section 7.

Analysing a stack-based language

Polyhedral analysis of While languages is well understood but we want our framework to be able to analyse byte code programs and not only source code. We could in theory avoid the problem by transforming the program into threeaddress code and treat each stack location as a local variable but this transformation is expensive from an algorithmic point of view, as it increases the number of times that the relation has to be updated. Instead, we achieve the effect of this transformation by defining an analysis for stack-oriented byte code

RR n ¡ 6333 // PRE: T rue static int bsearch(int key, int[] vec) { // (I 1 ) |vec 0 | = |vec| ∧ 0 ≤ |vec 0 | int low = 0, high = vec.length -1; // (I 2 ) |vec 0 | = |vec| ∧ 0 ≤ low ≤ high + 1 ≤ |vec 0 | while (0 < high-low) { // (I 3 ) |vec 0 | = |vec| ∧ 0 ≤ low < high < |vec 0 | int mid = (low + high) / 2; // (I 4 ) |vec| -|vec 0 | = 0 ∧ low ≥ 0 ∧ mid -low ≥ 0∧ // 2 • high -2 • mid -1 ≥ 0 ∧ |vec 0 | -high -1 ≥ 0 if (key == vec[mid]) return mid; else if (key < vec[mid]) high = mid -1; else low = mid + 1; // (I 5 ) |vec 0 | = |vec| ∧ -1 + low ≤ high ∧ 0 ≤ low ∧ 5 + 2 • high ≤ 2 • |vec| } // (I 6 ) 0 ≤ |vec 0 | return -1; } // POST: -1 ≤ res < |vec 0 |
Figure 2: Binary search after invariant pruning that combines relational abstract interpretation with symbolic execution, following an idea previously used for analysing Java byte code by Xi and Xia [START_REF] Xi | Towards Array Bound Check Elimination in Java Virtual Machine Language[END_REF] and Wildmoser et al [START_REF] Wildmoser | Bytecode analysis for proof carrying code[END_REF]. This technique abstracts the environment of local variables by a relation (e.g., a polyhedron) and replace the operand stack with a stack of symbolic expressions used to "decompile" the operations on the operand stack. For example, the comparison of variables low and high will be compiled to the byte codes below, which are analysed in a state consisting of the relation I 2 as defined in Fig. 1 More generally, with the abstract stack of expressions, only the comparisons and assignment to variables require updating the relation. In a polyhedron-based analysis this is a substantial saving.

Result checking with certificates

Checking an invariant obtained by computing a post-fixpoint of an abstract interpretation is in theory simple as it only requires one more iteration to check that it is indeed a post-fixpoint. In addition, only invariants at certain program points such as loop headers are required for re-building an entire invariant in one iteration. Lightweight Bytecode Verification by Rose [START_REF] Rose | Lightweight bytecode verification[END_REF] and the more general Abstraction-Carrying Code by Albert, Puebla and Hermenegildo [START_REF] Albert | Abstraction-carrying code[END_REF] exploit this to construct efficient checkers for invariant-based program certificates. For the code in Fig. 2, only I 2 is required. The inference of invariants using our relational analysis uses an iterative fixpoint solver over an abstract domain of polyhedra and is in principle amenable to the same technique. However, despite efficient implementations of basic polyhedral operations, the algorithmic complexity of operations such a computing the least upper bound (i.e. the convex hull) of two polyhedra remains high, and certifying them in a proof assistant would be a major undertaking.

Instead, we propose an enriched certificate format which has the virtue of being simpler to check, at the cost of sending more information than in basic fixpoint reconstruction. We exploit that, for the checker, the only important property of the convex hull operators is that it produces an upper bound of two polyhedra and therefore can be replaced by inclusion checks with respect to an upper bound that is proposed by the certificates. Upper bounds are computed at join points so in Fig. 2 we would also supply I 5 .

Safety checks also reduces to inclusions of polyhedra as verifying the array access vec[mid] amounts to ensuring that I 4 implies 0 ≤ mid < |vec|. By simple propositional reasoning, this reduces to proving that the linear systems of constraints -mid -1 ≥ 0 ∧ I 4 and mid -|vec| ≥ 0 ∧ I 4 have no solution. Due to a result by Farkas, such problems can be checked efficiently using certificates by a simple matrix computation. The key insight is that unsolvability follows from the existence of a positive combination of the constraints which yield a strict negative constant. This would lead to a contradiction because the sum and product of positive quantities cannot be strictly negative. The certificate is therefore a vector which records the coefficients of the positive combination. For example, the certificate [2; 2; 0; 0; 1; 2] proves that the constraints mid-|vec| ≥ 0 ∧ I 4 are unsatisfiable, as the expression

2 • (mid -|vec|) + 2 • (|vec| -|vec 0 |) + 0 • • • • + 0 • • • • + 1 • (2 • high -2 • mid -1) + 2 • (|vec 0 | -high -1) RR n ¡ 6333
evaluates to -2. We explain these certificates in detail in Section 8.

Certified certificate checkers

The result checking technique explained above already drastically reduces the TCB of the analysis result which only rely on the result checker. To further reduce the TCB, we have machine-checked the result checker of our analysis in the Coq proof assistant. The main components of the formalisation are 1. a predicate Safe:program→Prop which models the safe programs with respects to the the semantics described in Section 4, 2. a function checker:program→certificate→bool, which checks the safety of a program using a certificate containing a (partial) result of an analysis and some inclusion certificates, 3. a machine checked proof establishing the correctness of the checker:

Theorem checker_correct : ∀ p cert, checker p cert = true → Safe p.
The Trusted Computed Base is hence reduced to the Coq type checker and the formal definition of program safety.

Once the certified result checker is verified (by the Coq type checker) and installed by the code consumer, two scenarios can be envisaged to verify the safety of programs sent by producers. In the first one, the consumer may use an efficient Ocaml version of the checker, extracted from the Coq version thanks to the Coq extraction mechanism. The other alternative is related to proof by reflection. For each program p and certificate cert the consumer may build a foundational Coq proof of Safe p. To do so he only has to check in Coq the term checker_correct p cert refl_eqtrue where refl_eqtrue denotes a proof of true=true. It is the role of the Coq reduction engine to verify during type checking if true=true is equivalent to checker p cert = true by running the checker inside Coq. In this way we combine two desirable features which are often difficult to reconcile in state-of-the art Proof Carrying Code: foundational proofs and small certificates.

Notations

Let A and B be sets. If A and B are disjoint then A + B is the disjoint sum of A and B. We write

A ⊥ the set A + {⊥}. For f ∈ A → B ⊥ , dom(f ) = {a ∈ A | f (x) = ⊥}. Let f ∈ A → B, f [x → v] is the function identical to f everywhere except for x for which it returns v. The notation [x 1 → v 1 ; . . . ; x n → v n ] stands for a function f of domain {x 1 , . . . , x n } such that f (x i ) = v i . A * is
the set of lists of elements of A. We write [] for the empty list and a 0 :: . . . :: a n-1 is a list l of length n (|l| = n) whose head (resp. tail) is a 0 (resp. a n-1 ). l[i] is the i-th element of l. We write a i the list that is the repetition of a, i times. Let V , W be totally ordered sets. For x ∈ V , ι V (x) is the index of x in set V and ι -1 V is the inverse function. We abuse notations and identify A |V | with V → A i.e., given a finite ordered set, V = {x 1 , . . . , x n } such that x 1 < . . . < x n , we identify the finite mapping [

x 1 → v 1 , . . . x n → v n ] with the n-tuple (v 1 , . . . , v n ). INRIA We will write A V to denote both A |V | and V → A. Let ρ ∈ A V and V ⊆ V , ρ |V ∈ A V is the restriction of e over the variables of V such that for all x ∈ V , ρ |V (x) = e(x). Given V and W disjoint set of variables, ρ 1 ∈ A V and e 2 ∈ A W , we write ρ 1 ⊕ ρ 2 ∈ A V +W for the finite mapping such that (ρ 1 ⊕ ρ 2 ) |V = ρ 1 and (ρ 1 ⊕ ρ 2 ) |W = ρ 2 . Let W and W ordered sets of same cardinality. If ρ ∈ A V +W , then ρ W →W ∈ A V +W is obtained by renaming the variables of W to the variables in W . Formally, we have ρ W →W (x) = ρ(x) if x ∈ V and ρ W →W (x) = ρ(ι -1 W (ι W (x))) if x ∈ W .
To make the distinction clear between syntactic expressions and values, syntactic expressions are bracketed ( • ). For example, we write 1 + e a syntactic expression built by applying the + operator to the constant 1 and the syntactic expression e.

A byte code language and its semantics

We use a simple stack-based byte code language to illustrate our ideas. Features include integers, dynamically created (unidimensional) array of integers, static methods (procedures) and static fields (global variables).

Programs are lists of methods and a method consists of a name, a number of arguments and a list of instructions. In the following, f ranges over the set S of static field names, r ranges over the set R = {r 0 , . . . , r |R| } of local variables and id ranges over the set MethId of method names. Moreover, i and n range over N or Z depending on the context and p is used for control points.

P ∈ P rog = M eth * m ∈ Meth = Sig × Code Sig = M ethId × N c ∈ Code = Instr * instr ∈ Instr instr ::= Nop | Ipush n | Iinc r n where n ∈ Z Pop | Dup | Ineg | Iadd | Isub | Imult | Idiv Load r | Store r Getstatic f | Putstatic f Newarray | Arraylength | Iaload | Iastore Goto p | If icmp cond p where cond ∈ {=, =, <, ≤} Invoke sig where sig ∈ Sig Iinput | Return
The instruction set has operators for integer arithmetic and for manipulating local variable, static fields and an operand stack. Instructions on arrays permit to create, obtain the size of, access and update arrays. The flow of control can be modified unconditionally (with Goto), and conditionally with the family of conditional instructions If icmp cond which compare the top elements of the run-time stack and branch according to the outcome. Input of data is modelled with the instruction Iinput. The inter-procedural layer of the language contains an instruction Invoke for invoking a method and an instruction Return which transfers control to the calling method, and, at the same time returns the top of the operand stack as result by pushing it onto the operand stack of the caller (see the operational semantics below).

RR n ¡

6333

A program state is composed of a frame stack, the value of static fields and a heap of arrays and has the form <(m, p, s, l) * , g, h>. Each frame is a triple composed of a method m, a control point p to be executed next, an operand stack s local to a frame and l a partial mapping from local variables to values. The global heap h is used for storing allocated arrays and is modelled as a partial function from memory locations to arrays. A special error state Error models the run-time error arising from indexing an array outside its bounds.

ref ∈ Location v ∈ Val = Z + Location s ∈ Stack = Val * l ∈ LocVar = R → Val a ∈ Array = Z * h ∈ Heap = Location → Array ⊥ g ∈ Static = S → Val Frame = Meth × N × Stack × LocVar State = Frame * × Static × Heap + {Error }
The byte code language is given an operational semantics via a transition relation → between states. Some of the rules of the definition of → are shown in Fig. 3. In the semantics, for a method m = ((id, n), c), we write m[p] for c[p]. Note that the language is untyped: registers and fields may (and will) point successively to values of different types during execution. Instructions that require arguments with a certain type get stuck in case of error. Also, the number of registers |R| is the same for all methods. Unused registers and uninitialised fields have the value 0. Finally, we only consider states <st, g, h> such that every location appearing in st, g is in dom(h), which is clearly preserved by the semantics in Fig. 3.

Relational analysis of byte code

In this section, we describe a generic, relational analysis for byte code, parameterised with respect to a numeric relational domain used to abstract the values of the local and global variables of the program.

Symbolic analysis of the stack

Rather than treating each stack location as a new local variable and include this variable in the numeric abstraction describing the state, we integrate a symbolic de-compilation into the analysis that abstracts a stack location by a symbolic expression describing how the value at that stack location is computed from the values of the local variables. The operand stack is hence abstracted by a stack of symbolic expressions which represents relation between operands, static fields and local variables.

The following definition of expressions and guards has two purposes: they form the basis of the abstract domain for stacks (Expr only), which is specific to stack-based byte code, and they serve as the interface with the numeric relational domain, which is parametric. Note that those two aspects of the analysis are

INRIA s, l, g, h

Ipush n -→ n :: s, l, g, h n 2 :: n 1 :: s, l, g, h The expression ? represents an unknown value and is responsible for the nondeterministic evaluation of expressions. Analyses will use this expression to model interactive inputs and abstract away numeric quantities not in the scope of the analysis. For instance, our analysis will not keep track of values stored in arrays.

Iadd -→ n 1 + n 2 :: s, l, g, h l(r) = n s, l, g, h Iinc r i -→ s, l[r → n + i], g, h s, l, g, h Load r -→ l(r) :: s, l, g, h v :: s, l, g, h Store r -→ s, l[r → v], g, h s, l, g, h Getstatic f -→ g(f ) :: s, l, g, h h(ref ) = ⊥ n ≥ 0 n :: s, l, g, h Newarray -→ ref :: s, l, g, h[ref → 0 n ] h(ref ) = a 0 ≤ i < |a| i :: ref :: s, l, g, h Iaload -→ a[i] :: s, l, g, h h(ref ) = a ¬ 0 ≤ i < |a| i :: ref :: s, l, g, h Iaload -→ Error m[p] = instr s, l, g, h instr -→ s , l , g , h <(m, p, s, l) :: st, g, h> → P <(m, p + 1, s , l ) :: st, g , h > m[p] = If icmp cond p' n 1 cond n 2 <(m, p, n 2 :: n 1 :: s, l) :: st, g, h> → P <(m, p , s, l) :: st, g, h> m[p] = If icmp cond p' ¬ n 1 cond n 2 <(m, p, n 2 :: n 1 :: s, l) :: st, g, h> → P <(m, p + 1, s, l) :: st, g, h> m[p] = Invoke (mn,n) m = ((mn, n), c) ∈ P <(m, p, (v n-1 :: . . . :: v 0 :: s), l) :: st, g, h> → P <m , 0, [], [r 0 → v 0 ; . . . ; r n-1 → v n-1 ; rn → 0; . . . ; r |R| → 0] :: (m, p,
The semantics e ρ and t ρ of expressions and guards with respect to an environment ρ ∈ V → Z are given below.

n ρ = {n} x ρ = {ρ(x)} ? ρ = Z e 1 e 2 ρ = {n 1 n 2 | n 1 ∈ e 1 , n 2 ∈ e 2 } e 1 e 2 ρ ⇐⇒ ∃ n 1 ∈ e 1 ρ , n 2 ∈ e 2 ρ n 1 n 2
Note that this is not the whole concretisation function for symbolic expressions, which is described later (see Fig. 4).

Symbolic stacks Concrete operand stacks are abstracted by lists of symbolic expressions. To deal correctly with values which are returned after a method

RR n

¡ 6333 call we use auxiliary variables in a given set A, so the symbolic abstract domain for stacks is Expr * R+S+A .

Numeric relational domain specification

Apart from symbolic expressions stacks, the byte code analysis is specified with respect to an abstract numeric relational interface (defined below) that can be instantiated with standard relational abstract domains. We thus assume a domain D parameterised over a (finite) totally ordered set of variables V .

Language independent operators An abstract element is mapped to a set of environments in Z V by the concretisation function γ :

D V → P(Z V ).
To manage sets of variables, D is equipped with a projection operator ∃ V :

D V +V → D V , an extension operator E V : D V → D V +V and a renaming operator • W →W : D V +W → D V +W .
The abstract domain is also equipped with a partial order ⊆ D V × D V and meet and upper bound operators , : D V × D V → D V . These components are language-independent.

Language dependent operators

The abstract assignment of an expression e ∈ Expr V to a variable x ∈ V is modelled by the operator x := e : D V → D V . A guard t ∈ Guard V may be abstracted by two operators assume (t), ensure (t) : D v : the assume operator computes an over-approximation of the guard, while ensure computes an under-approximation.

D V → P(Z V ), a decidable ordering relation ⊆ D V × D V such that d d ⇒ γ(d) ⊆ γ(d ), a projection ∃ V : D V +V → D V , an extension E V : D V → D V +V and a renaming • W →W : D V +W → D V +W operators such that: γ(∃ V (d)) = {ρ |V | ρ ∈ γ(d)} γ(E V (d)) = {ρ | ρ |V ∈ γ(d)} γ(d W →W ) = {ρ W →W | ρ ∈ γ(d) } , a meet operator : D V × D V → D V such that γ(d d ) = γ(d) ∩ γ(d ),
an upper bound operator :

D V × D V → D V such that γ(d d ) ⊇ γ(d) ∪ γ(d ), INRIA an abstract assignment operator x := e : D V → D V s.t. γ( x := e (d)) ⊇ {ρ[x → v] | ρ ∈ γ(d) ∧ v ∈ e ρ }, assume , ensure : Guard V → D V such that γ(ensure (t)) ⊆ {ρ | t ρ } ⊆ γ(assume (t)).
With the operator assume # of the numerical domain we define the abstract test t : D V → D V of a guard t ∈ Guard V by: e e (l ) = assume (e e ) l if ∈ {=, <, ≤, >, ≥} e =e (l ) = (assume (e <e) l ) (assume (e<e ) l )

The specific rule for = is necessary to ensure a good precision with convex polyhedra.

Analysis specification

The byte code analysis is defined by specifying for each byte code an abstract transfer function which maps abstract states to abstract states (for non-jumping intraprocedural instruction at least). The abstract states are pairs of the form (s , l ) where l is a relation between local, global and auxiliary variables and s is an abstract stack whose elements are symbolic expressions built from these variables. More precisely, the analysis manipulates the following sets of variables: of methods in the symbolic operand stack Moreover, we use a "primed" version X of the variable set X for renaming purposes. For each method the analysis computes a signature Pre → Post whose meaning is if the method is called with in a context where its arguments and the static fields satisfy the property Pre then if the method returns, then its result, its arguments, and the initial and final values of static fields satisfy the property Post.

Preconditions are actually chosen by over-approximating the context in which each method may actually be invoked. Additionally the analysis computes at each control point of each method a local invariant between the current (R) and initial (R 0 ) values of local variables, the current (S) and initial (S 0 ) values of static fields, and some auxiliary variables (A) which are used temporarily to remember results of method calls which are still on the stack ∃ S +{res} aux j := res

0 @ l S→S ∃ R 0 " n-1 i=0 assume (e i = r old i ) S→S Post (sig, c ) S 0 →S « 1 A 1 C C A Loc(m, p + 1)
where p is the index of the j-th Invoke in m m[p] = Return Loc(m, p) = (e :: s , l )

∃ R+A ( res := e (l )) Post(m) (m, n, c) ∈ P |S|-1 i=0 assume (f i = f old i ) n-1 i=0 assume (r old i = r i ) Pre(m) Loc(m, 0) ((main, 0), c) ∈ P Pre((main, 0), c)
State # = Meth → D R0+S0 × Meth → D R0+S0+S+{res} × Meth × N → Expr R+S+A × D R0+S0+R+S+A ⊥
The analysis is specified as a solution of a constraint (inequation) system associated to each program. The constraint system is formally defined

INRIA in Fig 4.
Note that extensions are left implicit. For non-jumping intraprocedural instructions, the constraint is defined via a transfer function in Expr × D R0+S0+R+S+A → (Expr × D R0+S0+R+S+A ) ⊥ . We (ab)use notation and write (e :: s , l ) → e :: e :: s , l for the function that maps a state of the form (e :: s , l ) to the resulting state e :: e :: s , l and other states to ⊥. The analysis maintains a symbolic version of the operand stack and most of the transfer functions are defined as symbolic executions. The transfer functions for the stack operations Nop, Pop and Dup mimic the semantics of those operations so e.g., Dup will duplicate the expression on top of the (abstract) operand stack and hence is abstracted by the function (e :: s , l ) → e :: e :: s , l . The abstraction of the instruction Load r for fetching the value of local variable r just pushes the expression r onto the abstract stack (rather than projecting an abstract value of r from the relation describing the local variables). Similarly, the abstraction of the addition operation Iadd pops the two topmost expressions e 1 and e 2 from the abstract stack and replaces them with the symbolic expression e 2 + e 1 .

The transfer function for the Store r operation updates the abstract environment of local variables with the constraint that r is now equal to the value given by the expression e on top of the abstract stack top. Formally, this is done using the operation x := e provided by the interface of the relational domain. By the same token, all occurrences of the sub-expression x in the abstract stack become invalid, as r now (potentially) has changed value, and are replaced by the "don't know" expression ? . The analysis abstracts arrays references by the length of the referenced array, so the transfer functions for Newarray(which takes the length as argument and returns a reference to the created array) becomes the identity function. Similarly for Arraylength.

For all non-jumping instructions, we generate a constraint saying that the state following the instruction should include the result of applying the transfer function of the instruction to the state preceding the instruction. For the conditional If icmp cond p', we use the abstract tests provided by the relational domain to take the outcome of the test into account, so e.g., at program point p we know that the condition cond holds between the two top elements of the stack. If these are given by expressions e 1 and e 2 then we know that the symbolic expression e 1 cond e 2 evaluates to true in the current environment. The expression e 1 cond e 2 (l ) in the rule for conditionals updates the environment of local variables (l to take this information into account. A similar constraint is generated for the program point p + 1 using this time the negation cond of the condition cond.

The analysis of method calls is the most complicated part. The complications partly arise because we have several kinds of variables (static fields, local and auxiliary variables) whose different scope must be catered for. The analysis gives rise to two constraints: one that relates the state before the call to the pre-condition of the method and one that registers the impact of the call on the state immediately following the call site.

When invoking a method m from method m, we compute an abstract state that holds before starting executing m and which constrains the P re(m ) component of the abstract element describing m . This state registers that the n topmost expressions e 1 , . . . , e n on the abstract stack corresponds to the actual arguments that will be bound to the local variables of the callee m , by inject-

RR n ¡ 6333
Besson, Jensen, Pichardie & Turpin ing the constraints e i = r old i into the relational domain and adding them to the current state as given by l . Care must be exercised not to confound the parameters R 0 of the caller with the parameters of the callee, hence the projecting out of R 0 before joining the constraints. Furthermore, the local variables R, the initial values of static fields S 0 and the auxiliary variables A of method m have a different meaning in the context of method m and are removed from the abstract state at the start of m too. Finally, the current value of static fields S in m at the point of the method call becomes the initial value of the static fields when analysing m , hence the renaming of S into S 0 . The entire start state for m is thus described by the expression

∃ R+S0+A i assume (e i = r old i ) ∃ R0 (l ) S→S0
The second rule for Invoke describes the impact of the method call on its successor state. We use an auxiliary variable aux j (chosen to be free in s # ) to name the result of a method call which is pushed onto the stack. This variable is constrained to be equal to the variable res which receives the value returned by m . The rest of the left-hand side expression of the constraint

l S→S ∃ R0 i assume (e i = r old i ) S→S Post(m ) S0→S
serves to link the post-condition Post(m ) of the method with the state l of the call site. These are linked via the local variables x i constrained to be equal to the argument expressions e i and via the global static fields S. Again, some renaming and hiding of variables is required: e.g., the initial values of the static fields in m , referred to by S 0 , correspond to the values of the static fields before the call in the state l and in the expressions e i , referred to by S. The renamings S 0 → S and S → S , respectively, ensures that these values are identified. Two rules are used to initiate the analysis of a method (constraint on Loc(m, 0)) and of the entire program (constraint on Pre((main, n), c)). To initialise the analysis of a method m, the precondition Pre(m) is conjoined with the constraints linking the variable f old i to the current value of the static field f i and linking the parameters r old i with the local variables r i , in accordance with how parameters are handled in e.g. Java byte code. The analysis of the main method starts in the completely unconstrained state .

Inference

The constraint system presented in the previous section can be turned into a post-fixpoint problem by standard techniques. Consequently, the solutions of the system can be characterised as the set of post-fixpoints {x | F (x) x} of a suitable monotone operator F ∈ State → State operating on the global abstract domain State of the analysis. Assuming that State is a complete lattice1 we know that the least solution lfpF of this problem exists and can be over-approximated by any post-fixpoint of F . Computing such a postfixpoint is the role of chaotic iterations [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixpoints[END_REF] which operate on the equation system associated with the constraint system and choose a suitable iteration strategy [START_REF] Bourdoncle | Efficient chaotic iteration strategies with widenings[END_REF]. Iteration is sped up by using widening on well-chosen control points. Neither the iteration strategy nor the widening operators belong to the TCB since the validity of the result can be checked with a post-fixpoint test.

Safety checks

Once the analysis has inferred correct invariants, this information is used to check if they enforce the suitable safety policy. In a context of array bound checking we must check that each array access is within the bounds of the array. As a consequence, for each occurence of an instruction Iaload or Iastore at a program point (m, pc), we test if the local invariant Loc(m, pc) computed by the analysis ensures a safe array access.

Soundness of the analysis

Fig. 5 gives the concretisation functions for the abstract domains. The auxiliary abstraction function β maps everything to an integer, abstracting arrays by their length. γ expr defines concretisation of a symbolic expression with respect to an environment. γ Pre maps pre-conditions to sets of calling contexts, γ Post maps post-conditions to relations between calling contexts and return contexts, and γ Loc maps local invariants to relations between calling contexts and local program states. Note that concretisations contain only states such that all locations that are being referenced are defined in the heap.

Definition 5.4 (Reachable states). For a method m in a program P , a heap h, a static heap g, a set of local variables l, a frame stack st, the set P m h,g,l,st of reachable state from an execution of m starting in an initial configuration (h, g, l, st) is defined by The purpose of ≥st --→ * P is to collect only the states in between the start and the end of the execution of a particular stack frame.

P m h,

RR n

¡ 6333 β V : Heap × (V → Val) → (V → Z ⊥ ) (h, z) → λx. z(x) if z(x) ∈ Z |h(z(x))| if z(x) ∈ dom(h) γ expr h,g,l,a : Expr R+S+A → P(Val), h ∈ Heap, g ∈ Static, l ∈ LocVar and a ∈ Val → Z e → e β R+S+A (h,l⊕g⊕a) ∪ n ref ∈ dom(h) ˛|h(ref )| ∈ e β R+S+A (h,l⊕g⊕a) o γPre : DR 0 +S 0 → P(Static × Heap × LocVar ) pre → ˘(g0, h0, l0) | βR 0 +S 0 (h0, l0 ⊕ g0) ∈ γ(pre) γPost : D R 0 +S 0 +S+{res} → P((Static × Heap × LocVar ) × (Static × Heap × Val )) post →  ((g0, h0, l0), (g, h, v)) | β S 0 +R 0 +S+{res} (h0, g0 ⊕ l0 ⊕ g ⊕ [res → v]) ∈ γ(post) ff γLoc : Expr × DR 0 +S 0 +R+S+A → P " (Static × Heap × LocVar ) × (Static × Heap × Stack × LocVar) « (e1 :: • • • :: en, loc) → 8 < :
((g0, h0, l0), (g, h, v1 :: Let P be a program and (Pre, Post, Loc) a solution of the constraint system associated with P . If Loc satisfies all safety checks then every method m in P is safe wrt. to Pre(m). In particular, <(((main, n), c), 0, [], λr.0) :: [], λf.0, λref .⊥ > → P Error Proof. The proof is divided into two parts. We first prove that each reachable intermediate state at a point (m, p) satisfies the property γ Loc (Loc(m, p)), that each method m is called in a context satisfying γ Pre (Pre(m)) and that its return value (if it exists) satisfies γ Post (Loc(m)). In the second part we prove that if a state at some point (m, p) satisfies γ Loc (Loc(m, p)) as well as the abstract safety check associated with this point, then no error happens in the next semantic step. To deal with the steps corresponding to procedure calls, the proof makes use of an intermediate big-step operational semantics. Details are omitted for lack of space.

• • • :: vn, l)) | ∃a ∈ A → Z, ∀i ∈ 1, n , vi ∈ γ expr h,g,l,a (ei) ∧ βS 0 +R 0 +S+R+A(h0, g0 ⊕ l0 ⊕ g ⊕ l ⊕ a) ∈ γ(loc) 9 = ;

Polyhedral analysis

We now instantiate the relational analysis framework using linear relations in the form of convex polyhedra. Polyhedral program analysis has a well-established theory [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] with several implementations [START_REF] Bagnara | The Parma polyhedral library user's manual[END_REF][START_REF]Jeannet and the Apron team[END_REF]. Here, we recall the basics of this theory. Definition 6.1. Convex polyhedra of dimension n (P n ⊆ Q n ) are (convex) subsets of Q n that can be expressed as a finite intersection of half-planes of Q n . Polyhedra can be represented as sets of linear constraints. It is desirable to keep these sets in normal form i.e., without redundant constraints. For this purpose, polyhedra libraries maintain a dual representation of polyhedra based on generators in which a convex polyhedron is the convex hull of a (finite) set of vertices, rays and lines. Vertices, rays and lines are respectively extremal points, infinite directions and bi-directional infinite directions of the polyhedron. Fig. 6 shows a a polyhedron with four constraints whose dual representation is made of three vertices (s 1 ,s 2 ,s 3 ) and two rays (r 1 ,r 2 ).

The efficiency of the algorithm that maintains the normal form of the double description is of crucial importance. For this task, state-of-the-art polyhedral libraries [START_REF] Bagnara | The Parma polyhedral library user's manual[END_REF][START_REF]Jeannet and the Apron team[END_REF] use Chernikova's algorithm [START_REF] Chernikova | Algorithm for finding a general formula for the nonnegative solutions of a system of linear inequalities[END_REF]. In the worst case, the number of generators is exponential in the number of constraints (and vice-versa) but, in practise, the double description offers a good performance. To alleviate further the cost of normalising polyhedra, these libraries switch lazily from one representation to the other.

Polyhedral cannot directly handle expressions that fall outside the linear fragment. It would be sound but unsatisfactory to abstract those expressions towards an arbitrary value i.e., the ? expression. More information can be retained by linearising expressions [START_REF] Miné | Symbolic methods to enhance the precision of numerical abstract domains[END_REF]. For instance, the precise analysis of Binary Search (Fig. 1) requires a precise model of euclidean divisions. Given an integer constant n, the guard y = x/n is abstracted by the linear guards 0 ≤ xn • y < n. Multiplications can also be linearised by using the range of variables.

We now briefly explain how polyhedral algorithms implement the abstract numeric relational domain specified in Definition 5.1. To be implemented efficiently, the double description of polyhedra is needed, using Chernikova's algorithm to reconstruct the coherence of the double representation.

The convex polyhedron can directly be cast into an abstract numeric domain by mapping variables of the domain to dimensions of the polyhedron. Hence, we get D V = P |V | and the concretisation:

γ(P ) = {ρ ∈ Z V | ρ ∈ P ∩ Z V }
Renaming of variables consists in applying a permutation to the dimensions of polyhedron. The extension operation which add new variables consists in inserting new unconstrained dimensions at the relevant indexes. Projections can be efficiently performed on the generator description of polyhedra in linear time. Each generator is projected by erasing the now irrelevant dimensions.

RR n ¡

6333

Intersections are computed by taking the union of the constraints of each polyhedron. The convex hull, i.e., least upper bound, is computed by taking the union of the generators of both polyhedra. An assignment x := e is modelled by the linear transformation (if e is linear) that keeps all the variables unchanged except x which is mapped to e. The transformation is applied to the generators. Inclusion tests are using both representation at once. Checking the containment of two polyhedra (P Q) amounts to verifying that the generators of P satisfy the constraints of Q. Widening operators are used by the fixpoint iterator to ensure convergence. For convex polyhedra, there exist various widening operators [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF][START_REF] Bagnara | Precise widening operators for convex polyhedra[END_REF]. Assume and ensure operators are responsible for interpreting guards of the target language. If the guard t is linear, a polyhedron is built from it and no abstraction takes place. Otherwise, t has to be linearised. In the worst case, universal (resp. empty) polyhedra can be used as sound (though very imprecise) fallbacks.

Fixpoint pruning

The result of the polyhedral byte code analysis will be a fixpoint of the transfer functions, representing an invariant of the program under analysis. This invariant will often contain more information than necessary for proving a particular safety policy such as absence of indexing outside array bounds. In the following we show how to prune an invariant with respect to a given safety policy, resulting in an invariant that is smaller and cheaper to verify.

Witnesses and pruning

We have applied the technique described in [START_REF] Besson | Small witnesses for abstract interpretation based proofs[END_REF] for pruning constraint-based invariants, with some adaptations allowing to handle our interprocedural polyhedral analysis on byte code better. First we recall the definition of witnesses for this particular analysis. Definition 7.1. A witness for a program P is a solution (Pre, Post, Loc) to the constraint system associated with P that satisfies the safety checks of P (see Definition 5.3).

We use this as the basis for building certificates, relying on the fact that if there exists a witness for P then P is safe (see Theorem 5.6). Part of the witness is sent to the checker in the constraint representation only (see Section 6), so we aim at extracting a weaker witness with fewer linear constraints than the one produced by the inference algorithm of Section 5.4 (if the analysis is accurate enough for the program). Pruning leaves the symbolic expression stacks of the witness unchanged because the checker recomputes them (and hence nothing is transmitted about this part).

It is easy to see that there is generally no unique weakest witness nor a unique witness with the minimum number of constraints (because the analysis is not distributive). Also, the idea of starting from the safety requirements to compute backward a witness that satisfies them cannot achieve the same precision as a forward analysis, because intuitively it would have to guess the invariants that a forward analysis naturally discovers. For these reasons we use a technique of pruning that removes as many linear constraints as possible from a given witness.

Abstract algorithm

We use a variation of the greedy heuristic presented in [START_REF] Besson | Small witnesses for abstract interpretation based proofs[END_REF]. In the following we identify polyhedra with sets of constraints. We use

Var = {pre m | m ∈ P } ∪ {post m | m ∈ P } ∪ {loc m,p | m ∈ P, m = ((mn, n), c), p < |c|}
to denote the set of unknowns of the constraint system associated with P . For an abstract element x = (P re, P ost, Loc) we define the set of linear constraints of x:

x = m∈P {(loc m,p , k) | Loc(m, p) = (s # , l # ), k ∈ l # } ∪ {(pre m , k) | k ∈ Pre(m)} ∪ {(post m , k) | k ∈ Post(m)} For V ⊆ Var we define x |V = {(var, k) ∈ x | var ∈ V } and x |V is defined accordingly.
Recall that the constraint system for P is a set of constraints of the form F (x) x |{v} where v ∈ Var . For a constraint c we note x, y C if F (x) y |{v} (we can do so since the expression stacks are fixed) and x C for x, x C. We will overload the notation and write also x C if x satisfies the safety check C. Then, for every such constraint C, we define a set dep(C) ⊆ Var that represents the dependencies of this constraint, in the sense that if x, y C then

x |dep(C) , y C. The definition of dep is straightforward. For example, if C is the constraint F instr (Loc(m, p))
Loc(m, p + 1) corresponding to an nonjumping intraprocedural instruction (see the first part of Fig. 4), then dep(C) = {loc m,p }. For the constraint . . . Loc(m, p + 1) of an Invoke sig instruction, dep(C) = {loc m,p , post (sig,c) } where (sig, c) ∈ P .

The pruning algorithm is shown in Fig. 7. The main issue in this nondeterministic algorithm is the choice of the subset x: we obviously want a minimal one in the sense of set inclusion (achievable in reasonable time by monotonicity), but it is not unique.

RR n ¡ 6333

Efficient pruning for polyhedral byte code analysis

Our strategy is to take a minimal such x that almost minimizes a cost function taking into account the number of linear constraints, the number of non-null coefficients in them, and, for Invoke, the number of post constraints (as opposed to loc). This allows us to obtain a witness with simpler invariants and signatures. The heuristic blindly applies the definition of while labelling (part of) the search space. The dependency function dep helps by reducing the number of linear constraints to be considered at each step.

Finally, we face a problem specific to the polyhedra domain when pruning an invariant: in order to keep things small, the polyhedra are usually represented in a minimal form in which the relation between a set of dimensions does not necessarily appear as a dedicated linear constraint, but often as a consequence of several other relations. For example, the constraint x ≤ z is implicit in x ≤ y ≤ z. For the purpose of finding a small invariant, we may benefit from being able to include such constraints. Our solution is to add some implicit constraints to the invariant before pruning it. More precisely, for a polyhedron in D V , we add all the projections ∃ V \V (see Section 6) where V is a subset of V of cardinality at most n. For the maximal number n of dimensions in the implicit constraints to be generated, ∞ seems too costly for non-trivial programs, and unnecessary. It turns out that 3 is enough for all of our examples, which is not surprising because very few correctness proofs actually rely on linear invariants involving more than three variables.

Result checking of polyhedral analysis

A result checker for abstract interpretation based static analysis can be reduced to an (optimised) fixpoint checker [START_REF] Albert | Abstraction-carrying code[END_REF], with the downside that the abstract domains are still part of the TCB. Formally certifying optimised polyhedral libraries [START_REF] Bagnara | The Parma polyhedral library user's manual[END_REF][START_REF]Jeannet and the Apron team[END_REF] is feasible but would require an enormous certification effort. Instead, we propose a lightweight verifier of polyhedral analyses using a result checking methodology which has two advantages: i) the TCB is small, and ii) the checking time is optimised.

The polyhedral domain revisited

Chernikova's algorithm is at the origin of the computational complexity of convex polyhedra operations, so a first approach would be to design a result checker for Chernikova's algorithm i.e., a normal form checker. This has the inconvenience that most of the polyhedral operations would be annotated with their result together with a certificate attesting that it is in normal form. Instead, we develop a checker which only uses the constraint representation of polyhedra and which never need to normalise. Moreover, projections are not computed but delayed using a set of extra existential variables. More precisely, our polyhedra are represented by a list of linear expression over two disjoint sets of variables V and E. Variables in v ∈ V are genuine variables while e ∈ E are (existential) variables that represent dimensions which have been projected out. Definition 8.1. Let V and E be disjoint sets of variables.

P V = Lin * V +E

INRIA

where

Lin V +E = { c 1 × x 1 + • • • + c n × x n | c i ∈ Z ∧ x i ∈ V + E}.
Given es ∈ P V , the concretisation function is defined by

γ V (es) = {ρ |V | ∀k ∈ es, k ≥ 0 ρ }
In the following, we show how to implement the polyhedral operations using (only) polyhedra in constraint form. Renaming simply consists in applying the renaming to the expressions within the polyhedron. Because the existential variables belong to a disjoint set, no capture can occur. In addition, for this encoding, extension is a no-op because unused variables have no impact on the internal representation.

es ∈ P V ⇒ ∀W ⊇ V, es ∈ P W Using Fourier-Motzkin elimination (see e.g.), [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF], projections can be computed directly over the constraint representation of polyhedra However, in the worst case, the number of constraints grows exponentially in the number of variables to project. To solve this problem, we delay the projection and simply register them as existentially quantified. This is done by renaming these variables to fresh variables. To compute intersections, care must be taken not to mix up the existential variables. To avoid capture, existentially variables are renamed to variables that are fresh for both polyhedra. Thereafter, the intersection is implemented by taking the union of the expressions. To implement the assume and ensure operators, the involved expressions are first linearised and the obtained linear inequality is put into the form e ≥ 0 which now belongs to the set Lin defined above. For convex polyhedra, assignment is efficiently implemented as an atomic operation. However, it can be expressed in terms of the previous operators: given x a fresh variable, an assignment can be defined as follows.

x := e (P ) = ∃ {x} P assume (x = e) {x }→{x} It is this latter definition that we use. Widening operators are only used during the fixpoint iteration, and are not needed at checking time. Convex Hull is the typical operation that is straightforward to implement using the generator representation of polyhedra. Using a relaxation technique, it is possible to express the convex hull as the projection of a polyhedron of higher dimension [START_REF] Backer | A clp language handling disjunctions of linear constraints[END_REF] but since this requires to compute projections this does not scale. Even with our delaying of projections, the size of the polyhedron doubles. Instead of computing a convex hull, we follow the result certification methodology and provide a certificate polyhedron that is the result of the convex hull computation. Furthermore, our result checker need not check that the result is exactly the convex hull but only that it is an upper bound by doing a double inclusion test.

Result certification for polyhedral inclusion

Farkas lemma (Lemma 8.2) is a theorem of linear programming (see for instance [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF]) which gives a notion of emptiness certificate for polyhedra. In this part, we show how this result can be i) lifted to obtain an inclusion checker; ii) extended further to deal with existential variables. Our inclusion checker check takes as input a pair of polyhedra (P, Q) and an inclusion certificate. It will only return true if the certificate allows to conclude that P is indeed included in Q (P Q). Lemma 8.2 (Farkas Lemma). Let A ∈ Q m×n and b ∈ Q n . The following statements are equivalent:

For all x ∈ Q n , ¬(A • x ≥ b) There exists ic ∈ Q m satisfying A t • ic = 0 and b t • ic > 0.
The soundness (⇐) of certificates is the easy part and is all that is needed in the machine-checked proof. It follows that the existence of a certificate ensures the infeasibility of the linear constraints and therefore that the polyhedron made of these constraints is empty.

Thus, an inclusion certificate ic is a vector of Q m and checking a certificate consists of 1) computing a matrix-vector product (A t • ic) 2) verifying that the result is a null vector; 3) computing a scalar product (b t • ic); and 4) verifying that the result is strictly positive. All in all, the certificate checker runs in quadratic-time in terms of arithmetic operations.

Certificates generation can be recast as a linear programming problem that can be efficiently solved by either the Simplex or interior point methods. The set of certificates is characterised by the convex polyhedron

Cert = ic ic ≥ 0 ∧ b t • ic > 0 ∧ A t • ic = 0
As a result, finding an extremal certificate amounts to solving a linear optimisation problem. For instance, the solution of the linear program min{c t • 1 | c ∈ Cert} minimises the sum of the coefficients of the certificate. In theory, such a minimisation might not yield a compact certificate because the optimisation is done over the rationals -there are very small rationals that require many bits. However, in practise, the technique is sufficiently efficient.

From emptiness to inclusion Lemma 8.3 states that in the absence of existential variables an inclusion check amounts to emptiness checks. Lemma 8.3. Given P, P ∈ P V +E , we have ∀e ∈ P , γ V +E (-e -1 :: P ) = ∅ if and only if γ V +E (P ) ⊆ γ V +E (P ).

Proof. By construction, polyhedra in P V +E do not have existential variables. Hence, we have γ V +E (P ) = e ∈P γ V +E (e ::[]). Moreover, the complement of a linear constraint e ≥ 0 is -e -1 ≥ 0. These facts allow to reduce inclusion to a set of emptiness tests.

INRIA

Lemma 8.4 states that to do an inclusion test, it is sound to drop existential variables.

Lemma 8.4. Let P and P be polyhedra in constraint form.

γ V +E (P ) ⊆ γ V +E (P ) ⇒ γ V (P ) ⊆ γ V (P )
Proof. The Lemma follows from the definition of γ and the fact that the restriction operator on environments is monotone.

Together, Lemma 8.3 and Lemma 8.4 allow the design of a sound result checker for inclusion tests of form P ⊆ P . In general, the checker is incomplete but this only shows up in cases where P has existential variables. However, inclusions only need to be certified when P is a polyhedron computed by the analyser and such a P does not contain existential variables, so the inclusion checker is always used in a context where it is complete.

Implementation and Experiments

The relational byte code analysis has been implemented in Caml and instantiated with the efficient NewPolka polyhedral library [START_REF]Jeannet and the Apron team[END_REF] as its relational abstract domain. As the language presented in Section 4 is compatible with Java byte code, we analyse programs that are compiled from genuine Java programs. The result checker for polyhedral analysis described in Section 8 has been implemented in the Coq proof assistant.

The analyser computes a solution to the constraint system generated from a program and passes it on to the fixpoint pruning algorithm. From the compressed invariants, loop headers and join points are extracted and the inclusion certificates required by the checker are produced using the Simplex algorithm. A binary form of loop headers, join point invariants and their inclusion certificates constitute the final program certificate.

In Fig 8, we give a table of some of the benchmarks used by Xi to demonstrate the dependent type system for Xanadu [START_REF] Xi | Imperative Programming with Dependent Types[END_REF]. HeapSort and QuickSort are particularly good illustrations of the capacities of our analysis for analysing automatically programs mixing recursive procedures and loops. The programs and the analysis results can be found at http://www.irisa.fr/lande/polycert.html.

. automatically. Second, the checking time is small, especially given that the checker is extracted from its Coq specification and thus is a purely functional implementation of a polyhedral domain. Third, pruning can halve the number of constraints to verify. This reduction can sometimes but not always produce a similar reduction in checking time. The benchmarks are relatively modest in size and it is well known that full-blown polyhedral analyses have scalability problems. Our analyser will not avoid this but can be instantiated with simpler relational domains such as e.g., octagons, without having to change the checker.

Related work

A number of relational abstract domains (octagons [START_REF] Miné | The octagon abstract domain[END_REF], convex polyhedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF], polynomial equalities [START_REF] Müller-Olm | Precise interprocedural analysis through linear algebra[END_REF]) have been proposed with various trade-offs between precision and efficiency, and intra-procedural relational abstract interpretation for high-level imperative languages is by now a mature analysis technique. However, to the best of our knowledge the present work is the first extension of this to an inter-procedural analysis for byte code. Dependent type systems for Javastyle byte code for removing array bounds checks have been proposed by Xi and Xia [START_REF] Xi | Towards Array Bound Check Elimination in Java Virtual Machine Language[END_REF]. The analysis of the stack uses singleton types to track the values of stack elements, achieving the same as our symbolic stack expressions. The analysis is intra-procedural and does not consider methods (they are added in a later work [START_REF] Xi | Imperative Programming with Dependent Types[END_REF] which also adds a richer set of types). The type checking relies on loop invariants. We have run our analysis on the example Xanadu programs given by Xi and have been able to infer the invariants necessary for verifying safe array access automatically.

The area of certified program verifiers has been an active field recently. Wildmoser, Nipkow et al. [START_REF] Wildmoser | Asserting bytecode safety[END_REF] were the first to develop a fully certified VCGen within Isabelle/HOL for verifying arithmetic overflow in Java byte code. The certification of abstract interpreters has been developed by Cachera, Pichardie et al. [START_REF] Cachera | Extracting a data flow analyser in constructive logic[END_REF][START_REF] Pichardie | Interprétation abstraite en logique intuitioniste: extraction d'analyseurs Java certifiés[END_REF]. for a variety of analyses including class analysis of Java byte code and interval analysis. Lee et al. [START_REF] Lee | Towards a mechanized metatheory of standard ml[END_REF] have certified the type analysis of a language close to Standard ML in LF and Leroy [START_REF] Leroy | Formal certification of a compiler back-end or: programming a compiler with a proof assistant[END_REF] has certified some of the data flow analyses of a compiler back-end. Leroy also observes that for certain, more involved analyses such as the register allocation, it is simpler and sufficient to certify a checker of the result than the analysis itself. The same idea is used by Wildmoser et al. [START_REF] Wildmoser | Bytecode analysis for proof carrying code[END_REF] who certifies a VCGen that uses untrusted interval analysis for producing invariants and that relies on Isabelle/HOL decision procedures to check the verification conditions generated with the help of these invariants. Their technique for analysing byte code is close to ours in that they also use symbolic expressions to analyse the operand stack and the main contribution of the work reported here with respect to theirs is to develop this result checking approach for a fully relational analysis.

The idea of removing useless parts from an invariant was developed independently by Besson et al. [START_REF] Besson | Small witnesses for abstract interpretation based proofs[END_REF] and by Yang et al. [START_REF] Yang | Goal-directed weakening of abstract interpretation results[END_REF] who call it abstract value slicing. Both works deal with intra-procedural invariants and both are based on a dependency computation that selects, for every constraint F (X) Y of the constraint system of P and every subset of an abstract state Y , a sufficient subset of X that satisfies the constraint. The two methods differ in the way that this choice is done but both have been shown viable for intra-procedural pruning of INRIA relational invariants. The present work is an extension of the principles underlying the non-deterministic algorithm in [START_REF] Besson | Small witnesses for abstract interpretation based proofs[END_REF] to handle the pre-/post-conditions arising from the interprocedural analysis. Finally, it should be noted that the fixpoint compression is orthogonal to and compatible with the optimisation of iteration strategies for fixpoint checking underlying Lightweight Bytecode Verification [START_REF] Rose | Lightweight bytecode verification[END_REF] and the more general abstraction-carrying code [START_REF] Albert | Abstraction-carrying code[END_REF][START_REF] Besson | Proof-carrying code from certified abstract interpretation and fixpoint compression[END_REF]. Our checker combines both techniques.

Conclusions and future work

This paper demonstrates the feasibility of an interprocedural relational analysis which automatically infers polyhedral loop invariants and pre-/post-condition for programs in an imperative byte code language. The machine-generated invariants can be pruned wrt. a particular safety policy to yield compact program certificates. To simplify the checking of these certificates, we have devised a result checker for polyhedra which uses inclusion certificates (issued from a result due to Farkas) instead of computing convex hulls of polyhedra at join points. This checker is much simpler to prove correct mechanically than the polyhedral analyser and provides a means of building a foundational proof carrying code that can make use of industrial strength relational program analysis.

Future work concerns extensions to incorporate richer domains of properties such as disjunctive completion of polyhedra or non-linear (polynomial) invariants. The certificate format and the result checker can accommodate the disjunctive completions, the inclusion certificates from Section 8.2 can be generalised to deal with non-linear inequalities as well [START_REF] Besson | Fast reflexive arithmetic tactics: the linear case and beyond[END_REF]. However, the analyses for inferring such properties are in their infancy. On a language level, the challenge is to extend the analysis to cover the object oriented aspects of Java byte code. The inclusion of static fields and arrays in our framework provides a first step in that direction but a full extension would notably require an additional analysis to keep track of aliases between objects.

A promising domain of application for our relational analysis technique is to verify the dynamic allocation and consumption of resources and in particular to ensure statically that a program always acquires a necessary amount of resources before consuming them. The approach of Chander et al. [START_REF] Chander | Enforcing resource bounds via static verification of dynamic checks[END_REF] relies on the programmer to provide loop invariants and pre-and post-conditions for methods in order to link program variables to the amount of resources available and perform powerful transformations such as hoisting resource allocations out of loops. Our inter-procedural byte code analyser could infer the necessary invariants and pre-/post-conditions and in the same vein provide the checker for integrating this into a mobile code resource certification scheme.

  s, l) :: st, g, h> m[p] = Return <(m, p, v :: s, l) :: (m , p , s , l ) :: st, g, h> → P <(m , p +1, v :: s , l ) :: st, g, h>

Figure 3 :

 3 Figure 3: Operational semantics of the byte code language

Definition 5 .

 5 1 states formally the requirements over the operators of abstract domain D V . Definition 5.1. An abstract domain D is a family of sets D V with: a concretisation function γ :

R

  : set of local variables r 0 , . . . , r |L|-1 of methods, R 0 : set of old local variables r old 0 , . . . , r old |P |-1 of methods, representing their initial values t the beginning of method execution, S: set of static fields f 0 , . . . , f |S|-1 of the program S 0 : set of old static fields f old 0 , . . . , f old |S|-1 of the program used to model values of static fields at the beginning of method execution A: set of auxiliary variable aux 0 , . . . , aux |A|-1 used to keep track of results

- 1 i=0

 1 l ) → (s , l ) Ipush n (s , l ) → `n :: s , l Ṕop (e :: s , l ) → `s , l Dup (e :: s , l ) → `e :: e :: s , l Íadd (e 2 :: e 1 :: s , l ) → ` e 2 + e 1 :: s , l Ísub (e 2 :: e 1 :: s , l ) → ` e 2 -e 1 :: s , l Ímult (e 2 :: e 1 :: s , l ) → ` e 2 × e 1 :: s , l Ídiv (e 2 :: e 1 :: s , l ) → ` e 2 /e 1 :: s , l Íneg (e :: s , l ) → ` 0 -e :: s , l Íinput (s , l ) → (? :: s, l ) Load r (s , l ) → ` r :: s , l Śtore r (e :: s , l ) → `s [?/r], r := e (l ) Ǵetstatic f (s , l ) → ` f :: s , l Ṕutstatic f (e :: s , l ) → `s [?/f ], f := e (l ) Íinc r n (s , l ) → `s [ r -n /r], r := r + n (l ) Ńewarray (e :: s , l ) → `e :: s , l Árraylength (e :: s , l ) → `e :: s , l Íaload (e 2 :: e 1 :: s , l ) → `? :: s , l Íastore (e 3 :: e 2 :: e 1 :: s , l ) → `s , l ḿ[p] = instr ∈ {Goto p', If icmp cond p', Invoke sig, Return} F instr (Loc(m, p)) Loc(m, p + 1) m[p] = Goto p Loc(m, p) Loc(m, p) m[p] = If icmp cond p' Loc(m, p) = (e 2 :: e 1 :: s , l ) `s , e 1 cond e 2 (l ) ´ Loc(m, p ) m[p] = If icmp cond p' Loc(m, p) = (e 2 :: e 1 :: s , l ) " s , e 1 cond e 2 (l ) " Loc(m, p + 1) m[p] = Invoke (mn,n) ((m',n),c') ∈ P Loc(m, p) = (e n-1 :: • • • :: e 0 :: s , l ) " ∃ R+S 0 +A " nassume (e i = r old i ) ∃ R 0 (l ) mn , n), c ) m[p] = Invoke sig (sig,c') ∈ P Loc(m, p) = (e n-1 :: • • • :: e 0 :: s , l ) j :: s [?/aux j ],

Figure 4 :

 4 Figure 4: Relational byte code analysis with stack de-compilation

Definition 5 . 3 (

 53 Abstract safety checks). We say a set of local invariant Loc ∈ (N → (Expr × D P +S0+L+S+A ) ⊥ ) verifies all safety checks of a program if and only if ∀m ∈ P, pc ∈ N, m[p] = Iaload ⇒ Loc(m, pc) = (e 2 :: e 1 :: s , l ) ⇒ l ensure ( 0 ≤ e 2 ) ∧ l ensure ( e 2 < e 1 ) ∧ m[p] = Iastore ⇒ Loc(m, pc) = (e 3 :: e 2 :: e 1 :: s , l ) ⇒ l ensure ( 0 ≤ e 2 ) ∧ l ensure ( e 2 < e 1 )

P

  g,l,st = s | <(m, 0, [], l ) :: st, g, h> ≥st is the reflexive transitive closure of → P restricted to states who have a form < . . . :: (m, . . .) :: st, . . . >.

Figure 5 :

 5 Figure 5: Concretisation functions

INRIA

2 Figure 6 :

 26 Figure 6: Dual representation of polyhedra

Figure 7 :

 7 Figure 7: Witness pruning algorithm

  isU pperBound(P, Q, UB ) ≡ P UB ∧ Q UB To implement inclusion tests, we push the result certification methodology further and use inclusion certificates. The form of certificates and their generation are described below. RR n ¡ 6333

  The two checking times in the last column give the checking time with and without fixpoint pruning Three things are worth noticing. First, invariants that had to be produced manually for the Xanadu examples are now inferred

		class	certificates	checking time
	Program		before after before	after
	BSearch	515	22	12	0.005	0.007
	BubbleSort	528	15	14 0.0005 0.0003
	HeapSort	858	72	32	0.053	0.025
	QuickSort	833	87	44	0.54	0.25
	Figure 8: Class files in bytes, certificates in number of constraints, time in
	seconds
	RR n

¡ 6333

For the polyhedra abstract domain this assumption is too strong but we can relax it by considering a complete lattice containing State and all its upper bounds[START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF].INRIA

RR n¡