Frédéric Besson

Sandrine Blazy

Pierre Wilke

A Precise and Abstract Memory Model for C using Symbolic Values *

Real life C programs are often written using C dialects which, for the ISO C standard, have undefined behaviours. In particular, according to the ISO C standard, reading an uninitialised variable has an undefined behaviour and low-level pointer operations are implementation defined. We propose a formal semantics which gives a well-defined meaning to those behaviours for the C dialect of the CompCert compiler. Our semantics builds upon a novel memory model leveraging a notion of symbolic values. Symbolic values are used by the semantics to delay the evaluation of operations and are normalised lazily to genuine values when needed. We show that the most precise normalisation is computable and that a slightly relaxed normalisation can be efficiently implemented using an SMT solver. The semantics is executable and our experiments show that the enhancements of our semantics are mandatory to give a meaning to low-levels idioms such as those found in the allocation functions of a C standard library.

Introduction

Semantics of programming languages give a formal basis for reasoning about the behaviours of programs. In particular, the correctness guarantee of C compilers [START_REF] Leroy | Formal verification of a realistic compiler[END_REF] and verification frameworks [START_REF] Cohen | VCC: A Practical System for Verifying Concurrent C[END_REF] is stated with respect to the program semantics. However, the C programming language is specified in such a way that certain operations are either undefined, unspecified or implementation-defined. Typically, reading uninitialised memory is an undefined behaviour; the order of evaluation of function arguments is unspecified; the size of the int type is implementation-defined. A C program is strictly conforming if it does not trigger any undefined, unspecified or implementation-defined behaviour.

This leads to an unsettling question: what is the guarantee provided by a compiler when the program is not strictly conforming, i.e. when its semantics is undefined? The short answer is none. The C standard [START_REF] Iso | [END_REF] explains that anything can happen with undefined behaviours: the compiler may fail to compile, but it could -and usually does -produce an executable code. The behaviour of the executable depends on compiler flags, especially optimisation levels. The executable code may behave as expected by the programmer, but it can also ignore the statements that lead to undefined behaviours, or even crash at runtime. For instance, for the sake of optimisation, the compiler may choose to remove pieces of code that result in an undefined behaviour [START_REF] Wang | Undefined behavior: What happened to my code?[END_REF]. In summary, the advantage of undefined behaviours is that they can be exploited by C compilers to optimise the generated code; the downside is that C programs with undefined behaviours may have unexpected results.

In practice, undefined behaviours have been responsible for serious flaws in major open source software [START_REF] Wang | Undefined behavior: What happened to my code?[END_REF] -optimisations triggered by undefined behaviours have introduced vulnerabilities in the target code. Moreover, some lowlevel idioms cannot be expressed without resorting to unspecified behaviours of the C semantics. A compelling example is the memory allocation primitives of the C standard library which are written using the C syntax but do not have a strictly conforming semantics. One reason for this is that the low-level bit manipulation of pointers that is necessary for efficient and robust implementation of memory allocation is implementation defined.

To alleviate the problem, a common approach consists in setting compiler flags to disable optimisations known to exploit undefined behaviours [START_REF] Wang | Undefined behavior: What happened to my code?[END_REF]Section 3.1]. In a sense, flag tweaking is a fragile way to get the desired program semantics. Wang, Zeldovich et al. [START_REF] Wang | Towards Optimization-safe Systems: Analyzing the Impact of Undefined Behavior[END_REF] propose a more principled compiler approach where they identify and report code whose optimisation depends on undefined behaviours. In this work, we advocate for a semantics-based approach and propose an executable extension of a C semantics ruling out unspecified behaviours originating from low-level pointer arithmetic and undefined behaviours due to access to uninitialised data.

The C standard describes only an informal semantics, but several realistic C formal semantics have been defined [START_REF] Norrish | C formalised in HOL[END_REF][START_REF] Blazy | Mechanized Semantics for the Clight Subset of the C Language[END_REF][START_REF] Ellison | An executable formal semantics of C with applications[END_REF][START_REF] Krebbers | An operational and axiomatic semantics for non-determinism and sequence points in C[END_REF]. They describe precisely the defined behaviours of C programs, as well as some undefined behaviours. Yet, none of them accommodates for all low-level pointer manipulations; uninitialised data are only dealt with in a very limited fashion by the semantics of Ellison and Roşu [7, 6.2.2].

One formal semantics is the C semantics used by the CompCert formally verified C compiler [START_REF] Leroy | Formal verification of a realistic compiler[END_REF]. CompCert is equipped with a machine-checked correctness proof establishing that the generated assembly code behaves exactly as prescribed by the semantics of the C source, eliminating all possibilities of compiler-introduced bugs and generating unprecedented confidence in this compiler. Yet, as for any compiler, the guarantee offered by CompCert only holds for programs with a defined behaviour. In general, the CompCert compiler provides a stronger guarantee than an ISO C compiler because its source language Com-pCert C is more defined than the ISO C99 language. Our goal is to extend the semantics expressiveness of CompCert C further by ruling out more undefined or unspecified behaviours.

The contributions of this work can be phrased as follows:

-We present the first formal semantics for CompCert C able to give a meaning to low-level idioms (bit-level pointer arithmetic and access to uninitialised data) without resorting to a concrete representation of the memory.

-The semantics operates over a novel memory model where symbolic values represent delayed computations and are normalised lazily to concrete values. -We demonstrate that the most precise normalisation is decidable and explain how to devise an efficient implementation using an SMT solver. -The semantics is executable and the software development is available at http://www.irisa.fr/celtique/ext/csem/. -We show in our experiments that our extensions are mandatory to give a defined meaning to low-level idioms found in existing C code.

The remainder of this paper is organised as follows. Section 2 introduces relevant examples of programs having undefined or unspecified behaviours. Section 3 defines our extension of CompCert's semantics with symbolic values. Section 4 specifies our normalisation of symbolic values. Section 5 deals with the implementation of the normalisation using SMT solvers over the theory of bitvectors. Section 6 describes the experimental evaluation of our implementation. Related work is discussed in section 7, followed by concluding remarks.

Motivating Examples

An example of unspecified behaviour is the order of evaluation of the arguments of a function call. The relative size of numeric types is defined but the precise number of bits is implementation defined. An undefined behaviour is for instance the access of an array outside its bounds. Unsafe programming languages like C have by nature undefined behaviours and there is no way to give a meaningful semantics to an out-of-bound array access. 1 Yet, certain undefined behaviours of C were introduced on purpose to ease either the portability of the language across platforms or the development of efficient compilers. As illustrated below, our novel memory model gives a formal semantics to low-level idioms such as access to uninitialised memory or low-level pointer arithmetic.

Access to Uninitialised Variables

The C standard states that any read access to uninitialised memory triggers undefined behaviours [10, section 6.7.8, §10]: "If an object that has automatic storage duration is not initialised explicitly, its value is indeterminate." Here, "indeterminate" means that the behaviour is undefined. To illustrate a benefit of our semantics, consider the code snippet of Fig. 1, representative of an existing C pattern (see Section 6.3).

The program declares a status variable and sets its least significant bit using the set function. It then tests whether the least significant bit is set using the isset function. According to the C standard, this program has undefined behaviour because the set function reads the value of the status variable before it is ever written. However, we argue that this program should have a well-defined semantics and should always return the value 1. The argument is that whatever the initial value of the variable status, the least significant bit of status is known to be 1 after the call set(status,0). Moreover, the value of the other bits is irrelevant for the return value of the call isset(status,0) which returns 1 if and only if the least significant bit of the variable status is 1. More formally, the program should return the value of the expression (status|(1≪ 0))&(1≪0) != 0 which evaluates to 1 whatever the value of status. Our semantics constructs symbolic values and normalises them to a genuine value when the evaluation yields a unique possible value.

Low-level Pointer Arithmetic

In ISO C, the bit width and the alignment of pointers are implementation defined. We consider here that pointers are encoded with 4 bytes and that the malloc function returns pointers that are 16-byte aligned (i.e. the 4 least significant bits are zeros). The C standard also states that arithmetic operations on pointers are limited to certain comparisons, the addition (or subtraction) of an integer offset to a pointer and the subtraction of two pointers pointing to the same object. In order to perform arbitrary operations over a pointer, it is possible to cast it to an unsigned integer of type uintptr_t for which the ISO C standard provides the following specification [START_REF] Iso | [END_REF]Section 7.18.1.4].

[The type uintptr_t] designates an unsigned integer type with the property that any valid pointer to void can be converted to this type, then converted back to pointer to void, and the result will compare equal to the original pointer.

Note that this specification is very weak and does not ensure anything if a pointer, cast to uintptr_t, is modified before being cast back. Here, uintptr_t is implemented by a 4 bytes unsigned integer, and a cast between pointers and uintptr_t preserves the binary representation of both pointers and integers (i.e. it is essentially a no-op).

With these assumptions in mind, consider the expected behaviour of the code snippet of Fig. 2. The pointer p is a 16-byte aligned pointer to a heap-allocated integer obtained by malloc. Therefore, it has 4 trailing spare bits. The pointer q is obtained from the pointer p by filling the 4 trailing bits (hence the bitwise and with 0xF) with a hash of the pointer p. Note that this pattern is used in practice as a hardening technique to enforce pointer integrity [START_REF] Lee | A memory allocator[END_REF]. Then, the evaluation of r clears out the 4 trailing bits of q using logical shifts. We argue that r is equal to p and that the program has a well-defined semantics and returns * p (that is 0). Our semantics computes the expected behaviour of this program without resorting to a concrete representation of pointers as machine integers.

Summary of Differences with the ISO C Standard

The ISO C standard leaves certain behaviours implementation defined. Among these, our semantics is parametrised by the size of the pointers and the alignment constraint of malloc. Our semantics also stipulates that pointer and uintptr_t types have the same size and that casts between these types preserve the binary representation of the objects. The ISO C standard states that reading uninitialised memory is undefined behaviour. Our semantics is more flexible and simulates the read of an arbitrary value. Operationally, our semantics propagates a symbolic undefined value through the execution. These extensions are sufficient to give a well-defined (and intuitive) semantics to the previous examples.

A C Semantics with Symbolic Values

Our semantics is able to model low-level idioms, in particular bit-level manipulation of pointers, while retaining abstraction properties of the current block-based memory model of CompCert. Our approach consists in computing symbolic values lazily delaying evaluation until values are really needed. A symbolic value sv evaluates to a value v if for every possible concrete memory M , sv evaluates to the same value v.

CompCert defines the semantics of a dozen of intermediate languages ranging from CompCert C to assembly. All the languages share the same memory model. The compiler transforms programs from one language to another and proves the correctness of the transformations with respect to that memory model. The two highest-level languages are CompCert C (source language) and Clight, a simpler version of CompCert C with side-effect free expressions. For the sake of presentation, we introduce our new memory model on the Clight semantics. However, our implementation leverages the existing CompCert C interpreter enhanced with our new memory model.

In this section, we first describe our memory model with symbolic values. Then, we show how to enhance the Clight semantics [START_REF] Blazy | Mechanized Semantics for the Clight Subset of the C Language[END_REF] with symbolic values.

The CompCert Memory Model

The semantics of operations involving pointers relies on a memory model defining how values are represented. The most concrete memory model is an array of bytes, where pointers and integers are indistinguishable. It can give a precise semantics, but reasoning on programs at such a low level is cumbersome (e.g. reasoning on forbidden memory accesses to detect buffer overflows). CompCert is using a more abstract block-based model [START_REF] Leroy | The CompCert memory model[END_REF] where memory is divided into disjoint blocks, each block corresponding to an allocated variable. A memory is a collection of blocks, each block being an array of concrete bytes. Intuitively, a block represents a C variable or an invocation of malloc.

Values stored in memory are defined in Fig. 3. They are the disjoint union of 32-bit integers (written as int(i)), 32-bit floating-point numbers (written as float(f)), locations (written as ptr(b,i)), and the special value undef representing the content of uninitialised memory. Locations ptr(b,i) are composed of a block identifier b (i.e. an abstract address) and an integer byte offset i within this block. Pointer arithmetic modifies the offset part of a location, keeping its block identifier part unchanged. Memory chunks appear in memory operations load and store, to describe concisely the size, type and signedness of the value being stored. These functions return option types: we write ∅ for failure and ⌊x⌋ for a successful return of a value x.

The memory is modelled as a map associating to each location an 8-bit elementary memory value of type memval. A memval value is a byte-sized quantity that describes the current content of a memory cell. It can be either Undef to model uninitialised memory; Byte(b) to model a concrete byte b; or Pointer(b, i, n) to represent the n-th byte (n ∈ {1, 2, 3, 4}) of the location ptr(b, i).

A New Memory Model with Symbolic Values

Our memory model is built on top of CompCert's, where we replace the values with symbolic values, defined as follows.

sv ::= v | op τ 1 sv unary arithmetic operation | sv τ op 2 τ sv binary arithmetic operation | sv τ ? sv τ : sv τ conditional expression | (τ )sv τ type cast (to a C type τ )
Symbolic values are annotated by C types that are needed to disambiguate overloaded C operators. Symbolic values are side-effect free and therefore their evaluation is independent of the memory content. To account for alignment properties we associate with each block of the memory a mask that the concrete address of the block needs to satisfy. Formally, the concrete address a of a block with mask msk must be such that a & msk = a. The allocation primitive is modified accordingly, and we add a function that returns the mask of a given block. The primitives load and store now operate over symbolic values instead of values.

alloc(M, lo, hi , msk ) = (M ′ , b) mask(M, b) = msk load(κ, M, b, i) = ⌊sv ⌋ store(κ, M, b, i, sv ) = ⌊M ′ ⌋
We also adapt the memval type to accommodate for symbolic values. To that purpose, we replace the Pointer constructor by a generalised Symbolic(sv , n) constructor which represents the n-th byte of a symbolic value sv .

To perform these memory primitives, we define a key operation extr(sv,i), which extracts the i th byte of a symbolic value. The reverse operation is the concatenation of a symbolic value sv1 with a symbolic value sv2 representing 8 bits. Assuming that the symbolic value represents a 32-bit value, these operations can be defined as

extr(sv,i) = (sv ≫ (8 * i)) & 0xFF concat(sv1,sv2) = sv1 ≪8 + sv2

Parametrised Semantics of Clight Values

Expressions cannot be kept symbolic forever. Our semantics is equipped with a partial normalisation function normalise(M, τ, sv) which converts a symbolic Expressions in l-value position:

G, E ⊢ a, M ⇒ sv normalise(M , type(a), sv ) = ⌊ptr(ℓ)⌋ G, E ⊢ *a, M ⇐ ℓ (1)
Expressions in r-value position:

G, E ⊢ a1, M ⇒ sv1 type(a1 ) = τ G, E ⊢ op 1 a1, M ⇒ op τ 1 sv1
(2) G, E ⊢ a, M ⇐ ℓ (evaluation of an expression in l-value position) G, E ⊢ a, M ⇒ sv (evaluation of an expression in r-value position)

G, E ⊢ a1, M ⇒ sv1 G, E ⊢ a2 , M1 ⇒ sv2 type(a1 ) = τ1 type(a2 ) = τ2 G, E ⊢ a1 op 2 a2, M ⇒ sv1 τ 1 op 2 τ 2 sv2 (3) G, E ⊢ a1, M ⇒ sv1 type(a1 ) = τ1 G, E ⊢ a2, M ⇒ sv2 type(a2 ) = τ2 G, E ⊢ a3 , M ⇒ sv3 type(a3 ) = τ3 G, E ⊢ a1 ? a2 : a3, M ⇒ sv τ 1 1 ? sv τ 2 2 : sv τ 3 3 (4) G, E ⊢ a, M ⇒ sv1 type(a) = τ1 G, E ⊢ (τ )a, M ⇒ (τ )sv τ 1 1 (5)
Compared to the existing Clight semantics [START_REF] Blazy | Mechanized Semantics for the Clight Subset of the C Language[END_REF], expressions are not completely evaluated but mapped to symbolic values. Moreover, the rules explicitly introduce calls to a normalisation function (see Section 4). These calls are inserted when a genuine value is required, i.e. when reading from or writing to memory, when evaluating the condition of a loop or if-then-else statement, or when exiting the program.

For instance, to evaluate * a, rule (1) recursively evaluates the expression a to get the symbolic value sv . To get a genuine location l, rule (1) explicitly normalises sv to get l. Now, l can be used to perform a store memory operation. Rule (2) specifies the evaluation of unary expression op 1 a 1 : it recursively evaluates the expression a 1 to get the symbolic value sv 1 . Instead of evaluating the operator op 1 , the semantics delays the evaluation and constructs the symbolic value op τ 1 sv 1 where τ is the type of the expression a 1 . Similarly, the evaluation of binary expressions (rule (3)), conditional expressions (rule (4)) and cast expressions (rule ( 5)) recursively evaluate their arguments and construct a symbolic value. Note that for the original Clight semantics, two rules are needed to give a semantics to conditional expressions [3, Fig. 6, rules ( 12) and ( 13)] depending on whether the condition holds or not. With symbolic values, we delay the evaluation and therefore have a single rule.

A Sound and Complete Normalisation

Our semantics with symbolic values aims at giving a defined meaning to low-level idioms that are out-of-reach of the current Clight. To do so, we need to instantiate the semantics with an aggressive normalisation function. The existing Clight semantics can be obtained by a suitable normalisation function. This semantics is trustworthy because it has been carefully designed, thoroughly reviewed and intensively tested. However, for more aggressive normalisation (which is what we aim at), this validation methodology does not scale and therefore provides a limited trustworthiness.

In this section, we give a formal specification of the normalise function. We define the notions of soundness and completeness of a normalisation function with respect to a concrete memory model. We will later show (Section 5) how to get efficient executable implementations from this specification.

Soundness of the Normalisation of Symbolic Values

Our semantics is parametrised by the normalisation function normalise. In this part, we describe the soundness conditions that this normalisation should fulfil. Symbolic values denote low-level values of types either Tint or Tfloat. The mapping between high-level C types and low-level types is performed by the function ctyp defined as follows: ctyp(τ ) = Tfloat if τ = Tfloat, and ctyp(τ ) = Tint otherwise. Notice that all the pointer types are mapped to the type Tint. Indeed, at low-level, addresses are not distinguishable from genuine integers. To map locations (b, i) to integers, the low-level evaluation is equipped with a mapping A from block identifiers to concrete addresses, which assigns an address to each memory block and therefore fixes a memory layout. In general, the low-level evaluation of a symbolic value is not a single value but a set because the value undef represents an arbitrary low-level value. Definition 1 formalises the low-level evaluation of symbolic values.

Definition 1 (Low-level evaluation). Let A be an allocation function mapping block identifiers to concrete addresses. The low-level evaluation • τ

A of a symbolic value e of type τ is inductively defined by the following rules.

int(n) ∈ int(n) Tint A float(f ) ∈ float(f ) Tfloat A ctyp(τ ) = Tint int(A(b) + i) ∈ ptr(b, i) τ A ctyp(τ ) = Tfloat float(n) ∈ undef τ A ctyp(τ ) = Tint int(n) ∈ undef τ A v 1 ∈ sv 1 τ1 A eval unop(op 1 , v 1 , ctyp(τ 1 )) = ⌊v ⌋ type(v ) = ctyp(τ ) v ∈ op τ1 1 sv 1 τ A v 1 ∈ sv 1 τ1 A v 2 ∈ sv 2 τ2 A type(v ) = ctyp(τ ) eval binop(op 2 , v 1 , ctyp(τ 1 ), v 2 , ctyp(τ 2 )) = ⌊v⌋ v ∈ sv 1 τ1 op 2 τ2 sv 2 τ A v 1 ∈ sv 1 τ1 A v 2 ∈ sv 2 τ A is true(v 1 , ctyp(τ 1 )) v 2 ∈ sv τ1 1 ? sv τ 2 : sv τ 3 τ A v 1 ∈ sv 1 τ1 A v 3 ∈ sv 3 τ A is false(v 1 , ctyp(τ 1 )) v 3 ∈ sv τ1 1 ? sv τ 2 : sv τ 3 τ A v 1 ∈ sv 1 τ1 A cast(v 1 , ctyp(τ )) = ⌊v ⌋ v ∈ (τ )sv τ1 1 τ A
By construction, the denotation of a symbolic value of type τ is a set of values of type ctyp(τ ). Symbolic values that are not well-typed have an empty low-level evaluation. As a side-remark, notice that the types of symbolic values cannot be uniquely inferred (undef can have an arbitrary type), and are therefore explicitly given. Moreover, the low-level evaluation of a symbolic value is reusing the existing high-level operators eval unop and eval binop with the difference that types are low-level types.

The normalisation of a symbolic value s should return a defined value v (v = undef) such that s evaluates to v for all possible concrete valid memory layouts. Definition 2 specifies valid memory layouts.

Definition 2 (Valid memory layout). An allocation A from blocks to concrete addresses is a valid memory layout for memory M (written A ⊢ M ) iff:

1. addresses from distinct blocks do not overlap, 2. the address of a block satisfies its mask, i.e. ∀b, A(b) & mask(M, b) = A(b) 3. addresses are not equal to zero.

With the previous definitions we are ready to state what it means for a normalisation to be sound.

Definition 3 (Sound normalisation).

A normalisation function is sound iff for any symbolic value sv , it returns a value v (normalise(M, τ, sv ) = ⌊v ⌋) such that v is not undef ; v has type τ and v has the same evaluation as sv for any valid allocation layout i.e. ∀A ⊢ M.

sv τ A = v τ A .
Note that because v differs from undef, v τ A is necessarily a singleton. Yet, certain symbolic values containing undef can nonetheless be normalised, for instance, normalise (M,Tint,undef & 0x0)= ⌊0⌋.

Reconstructing the Original Clight Semantics

The more precise the normalisation, the more defined the semantics. There is a hierarchy of normalisations of different precision. We therefore aim at identifying a normalisation which is not only precise but also tractable. The least precise normalisation, which always returns ∅, is sound but useless: it fails to provide a semantics to any expression. The original Clight semantics can be modelled by a normalisation function which recursively evaluates symbolic values.

type(v) = τ normalise(M, τ, v) = ⌊v⌋ normalise(M, τ 1 , e 1 ) = ⌊v 1 ⌋ eval unop(op 1 , v 1 , τ 1 ) = ⌊v⌋ type(v) = τ normalise(M, τ, op τ1 1 e 1 ) = ⌊v⌋ normalise(M, τ 1 , e 1 ) = ⌊v 1 ⌋ normalise(M, τ 2 , e 2 ) = ⌊v 2 ⌋ eval binop(op 2 , v 1 , τ 1 , v 2 , τ 2 ) = ⌊v⌋ type(v) = τ normalise(M, τ, e 1 τ1 op 2 τ2 e 2 ) = ⌊v⌋
As explained in the introduction, this normalisation is unable to give a semantics to low-level pointer operations (e.g. ptr(b,i) & 0x0) or expressions with undefined sub-terms (e.g. undef & 0x0). The original Clight semantics could be enriched to cope with these simple expressions. However, dealing with arbitrarily complex expressions using ad hoc simplifications would not be manageable.

Completeness of the Normalisation of Symbolic Values

Whenever possible, the most precise normalisation should always return some value. Yet there are rare cases where distinct values are sound normalisations. This is illustrated by Example 1.

Example 1. Consider the normalisation of the symbolic value ptr(b, 0)+2 31 -1 for a pointer type τ in a memory M made of an unaligned block b with bounds [0, 2 31 -1[ and a 2-byte aligned block b ′ with bounds [0, 2 31 [. Because the maximum capacity of the memory is 2 32 -1 bytes (0 is not a valid address), the memory is full. Moreover, the alignment constraint of b ′ prevents it from being allocated at address 1. It follows that the only valid memory layout of

M is A = [b → 1; b ′ → 2 31 ].
As we have ptr(b, 0) + 2 31 -

1 τ A = ptr(b, 2 31 -1) τ A = ptr(b ′ , 0) τ A = {int(2 31
)}, both ptr(b, 2 31 -1) and ptr(b ′ , 0) are sound normalisations.

In this example, the normalisation ptr(b ′ , 0) is more valuable because it represents a valid address (i.e. within the bounds of the allocated block). Definition 4 formalises what it means for a normalisation to be complete by stipulating an ordering ≺ M on values such that ptr(b ′ , 0) ≺ M ptr(b, 2 31 -1).

Definition 4 (Complete normalisation).

A normalisation function norm is complete if for all sound normalisations norm ′ , we have:

norm(M, τ, e) M norm ′ (M, τ, e)
where M is the reflexive closure of the ordering ≺ M inductively defined below and < is an arbitrary total order over locations.

⌊v⌋ ≺ M ∅ (6) i ∈ bound(M, b) i ′ / ∈ bound(M, b ′ ) ⌊ptr(b, i)⌋ ≺ M ⌊ptr(b ′ , i ′ )⌋ (7) i ∈ bound(M, b) i ′ ∈ bound(M, b ′ ) (b, i) < (b ′ , i ′ ) ⌊ptr(b, i)⌋ ≺ M ⌊ptr(b ′ , i ′ )⌋ (8) i / ∈ bound(M, b) i ′ / ∈ bound(M, b ′ ) (b, i) < (b ′ , i ′ ) ⌊ptr(b, i)⌋ ≺ M ⌊ptr(b ′ , i ′ )⌋ (9)
Rule ( 6) ensures that a complete normalisation is maximally defined and as much as possible does not return ∅. Rules ( 7), ( 8) and ( 9) ensure that a complete normalisation should, as much as possible, return a valid address. There are memories M for which there is no valid memory layout A. The simple case is when the size of the allocated memory exceeds 2 32 -1 bytes. In general, reasoning about the size of the allocated memory is not enough because the memory can be fragmented due to alignment constraints. In such cases, Definition 4 is not sufficient to ensure that there is a unique sound and complete normalisation function. The reason is that when there is no valid memory layout, any value v is a correct normalisation. Moreover, as the order ≺ M is not total, Definition 4 does not rule out these spurious cases. The good news is that all sound and complete normalisations compute the same result as soon as there exists a valid memory layout. Our normalisation algorithm (see Section 5) checks the existence of a valid memory layout and fails to normalise when there is none.

Evaluating Symbolic Values using an SMT solver

We have adapted the CompCert C semantics and its executable interpreter to work with symbolic values. As already demonstrated for the Clight semantics, the addition of symbolic values is not very intrusive and reuses most of the semantics infrastructure of the existing interpreter.

The difficulty lies in the implementation of the normalisation function. Given a memory M , there are finitely many valid memory layouts A. It is thus decidable to compute a sound and complete normalisation and the naive algorithm consists in enumerating over the valid memory layouts and checking that the symbolic values always evaluate to the same values. Yet, this is not tractable. As shown below, the normalisation can be recast as a decision problem over the logic of bitvectors. However, implementing (and proving) in Coq an efficient decision procedure for this logic would require a substantial engineering effort. Therefore, our current implementation leverages an external Satisfiability Modulo Theory (SMT) solver, Z3 [START_REF] De Moura | Z3: An Efficient SMT Solver[END_REF].

An Executable Semantics of Symbolic Values

We have adapted the CompCert C interpreter to work with symbolic values. The modification requires to change the type of values to the type of symbolic values and to replace the existing memory model by our implementation accommodating for symbolic values. As it is illustrated for Clight, the evaluation of C operators now builds symbolic values and calls to the normalise function are placed at certain points, as discussed below.

Our memory model stores (resp. reads) symbolic values to (resp. from) memory but the address needs to be a location (b,i). Therefore, we apply the normalisation function before calling the store and load primitives of the memory model. The normalisation is also called to compute the target of conditional jumps (e.g. for, while or if statements). A last normalisation is applied before ending the program because the program status needs to be a genuine integer. If the normalisation succeeds and returns some value, then the execution continues normally. Otherwise, the semantics gets stuck and the interpreter returns that it encountered an undefined behaviour. We detail in Section 6 some representative programs of our benchmarks.

Normalisation as a Satisfiability Problem

The normalisation function is axiomatised and implemented by an external (trusted) call to the SMT solver Z3 [START_REF] De Moura | Z3: An Efficient SMT Solver[END_REF]. As stated earlier, the problem of computing the most precise normalisation is decidable. Yet, a naive approach does not provide a tractable algorithm. A better solution consists in encoding the normalisation problem as an SMT problem over the logic of bitvectors and uninterpreted function symbols. A bitvector of size n is the logic counterpart of a machine integer with n bits. This logic is therefore a perfect match for reasoning about machine integers.

First, we axiomatise the memory and define a logical function size mapping each block to its size and a logical function mask mapping each block to the mask to be verified by the concrete address. Next, we axiomatise the valid memory layout relation by directly translating Definition 2 in first-order logic.

(b) =    4 if b = b 1 8 if b = b 2 0 otherwise Block masks: mask (b) =    0xFFFC if b = b 1 0xFFFF if b = b 2 0xFFFF otherwise No overlap: ∀b, b ′ , o, o ′ .    b = b ′ o < size(b) o ′ < size(b ′ ) ⇒ A(b) + o = A(b ′ ) + o ′ Addresses are not 0: ∀b, o.o < size(b) ⇒ A(b) + o = 0 Alignment : ∀b, A(b) & mask (b) = A(b)
We process the symbolic value e to be normalised into a logical symbolic value e * and replace occurrences of undef by distinct fresh logical variables thus modelling that undef may take any value.

Normalising into an integer. To normalise into an integer, we generate the SMT query: e * = i, where i is a fresh logical variable. Suppose the formula is satisfiable for a value v for logical variable i. This means that there exists a valid memory layout such that e is evaluated as the value v. However, this value v is only a sound normalisation if it is the evaluation for every possible valid memory layout. To ensure this, we generate the second SMT query: e * = i ∧ i = v. If this is unsatisfiable, then we will return v as the normalisation of e.

Normalising into a pointer. Getting the normalisation of a pointer value is more complicated by the fact that there are several ways of decomposing an integer into a location made of a base and an offset. Yet, as we are only interested in valid addresses (i.e. with an offset inside the bounds of the block), there is only a single choice. Therefore, we generate the following SMT query:

e * = A(b) + o ∧ o < size(b).
Given a model (b ′ , o ′ ) for location (b, o), we have to ensure that the evaluation of the expression is independent from the memory layout. Since blocks do not overlap, there is only one block such that the pointer is valid, so we just need to check that b ′ is the only possible block that makes a valid pointer, i.e. that the following formula is unsatisfiable: We process e into a logical expression e * by replacing undef by the fresh variable x 1 :

e * = A(b) + o ∧ o < size(b) ∧ b = b ′
e * = A(b 1 ) + 1 -A(b 2 ) -2 + A(b 2 ) + 4 + x 1 &0x0
Notice that the two occurrences of A(b 2 ) cancel out each other, and that we have ∀x, x&0x0 = 0. As a result, we can simplify this expression e * into A(b 1 ) + 3.

Normalising into an integer. We need to solve the following SMT query, with i the unkown: A(b 1 ) + 3 = i. We then get a first solution (e.g. v = 19, with A(b 1 ) = 16). However, this is not the only possibility because we get a second solution with A(b 1 ) = 32 for example, which yields v = 35. This expression has therefore no normalisation as an integer.

Normalising into a pointer. Now, the SMT query we need to solve is:

A(b 1 ) + 3 = A(b) + o ∧ o < size(b)
A solution is b ′ = b 1 and o ′ = 3, and we can see that this is the only solution to this equation. Therefore the expression e is normalised into the location ptr(b 1 , 3).

Relaxation and Optimisation of the SMT Encoding

The previous encoding of the memory depends on the number of allocated blocks. Thus, as the memory gets bigger, the normalisation would get slower. In practice, we observe that the size of the memory has a dramatic (negative) impact on SMT solvers. To tackle the problem, we propose a relaxation of the SMT query that is independent of the number of allocated blocks and only depends on the size of the symbolic value to be normalised.

A key observation is that a symbolic value can only be normalised if the corresponding SMT query has a unique solution. As a result, it is always sound to relax the SMT query and generate a weaker one (i.e. with potentially more solutions) provided the initial formula is satisfiable. Indeed, if there are more solutions, the normalisation will fail -this is always sound.

In our relaxation, we do not fully axiomatise the memory but only specify the bounds and masks of the memory blocks B that appear syntactically in the symbolic value to be normalised. When normalising a symbolic pointer, we also state explicitly in the SMT query that the normalisation, if it exists, should be a location (b, i) such that b ∈ B. This relaxation will only miss a normalisation if the memory is almost full and blocks b ∈ B cannot be allocated at certain addresses because of bound or alignment constraints of other blocks b ′ / ∈ B. This is illustrated by Example 4. The normalisation of Example 4 requires a full axiomatisation of the memory and cannot be obtained using our relaxation. In practice, we have never encountered such a pathological case.

As stated earlier, we have adapted the CompCert C interpreter so that we could test our semantics on real programs. This required only minor changes to get it to work with symbolic values. However, we put slightly more effort in designing stubs in the interpreter to model system calls such as mmap that are used e.g. in the source code of the malloc implementation we used. This system call is mapped to the alloc primitive of our memory model. Other system calls such as open, read or write are resolved using the OCaml equivalent functions.

We have tested our C semantics with symbolic values on the CompCert benchmarks. Their size ranges between a few hundreds and a few thousands lines of code. We checked the absence of regression: when the CompCert interpreter returns a defined value, our interpreter enhanced with symbolic values returns the exactly same value.

We have also run our interpreter over Doug Lea's memory allocator [START_REF] Lee | A memory allocator[END_REF] and on parts of the NaCl cryptographic library [START_REF] Bernstein | The Security Impact of a New Cryptographic Library[END_REF], which are challenging programs because they perform low-level pointer arithmetic; their size is about a few thousands lines of code. For this experiment, we model the system call mmap by a call to the alloc primitive of our memory model with a mask specifying the alignment of a page. Our interpreter succeeds in giving a semantics to memory management functions, such as malloc, memalign or free, built on top of mmap. As there is no other formal C semantics able to deal with low-level pointer arithmetic, we checked that the result of our interpreter was matching the output of gcc. Programs reading uninitialised variables have undefined semantics and gcc could exploit this to perform arbitrary computations. Yet, the output of gcc and our interpreter agree on examples similar to Fig. 1. In the following, we detail some interesting patterns found in the benchmarks.

Pointer Arithmetic Using Alignment and Bitwise Operations

The malloc function sometimes needs to check a pointer's distance to an alignment boundary. This is equivalent to getting the last bits of the pointer. For instance, this is done with the C expression p & 15, which gets the 4 last bits of pointer p. For our experiments, pointers are allocated by mmap and are therefore known to be aligned on more than 16 bytes boundaries. For a pointer p=ptr(b,3), our SMT encoding models that the last 4 bits of b are zeros and the code evaluates to 3&15 (i.e. 3). In general, with the previous alignment constraints, we have that the symbolic value ptr(b,o) & 15 returns the offset o of the pointer.

A similar example is the function memalign(al,nb), where al must be a power of two (i.e. al = 2 n ). The function dynamically allocates a nb-byte region, and ensures that the address returned has the n last bits to zero. When called with al = 32, the function computes checks such as p&31 == 0 to check that the 5 last bits are zeros. The left-hand side of the comparison is evaluated in the same manner as the example above, and the comparison is computed trivially.

Comparison Between Pointers and -1

Several system calls, such as mmap or sbrk, are expected to return pointers but return -1 on error. When a function calls mmap for example, there is typically a check that the system call succeeded (i.e. the returned value is not -1).

void * p = mmap(...); if (p == -1) { ... } Our normalisation gives a semantics to this programming pattern using the following reasoning. We know that pointers returned by mmap are aligned on a page boundary (2 12 in our implementation, i.e. the 11 last bits of the pointer are zeros). When the allocation succeeds, the pointer can therefore never be -1 (in binary 0 xFFFFFFFF) thus allowing to evaluate this comparison.

Operations on Undefined Values

The example shown is Fig. 1 is a simplified version of a C expression that appears in real-life programs. For example, the memalign function described above features this kind of operations on undefined values.

The memory managed by the dynamic allocation functions is organised in memory chunks, which consist of two 32-bit words of meta-data and the memory chunk itself. The second word of meta-data stores the size of the chunk and two bits of other information. Initialising the meta-data is done with the C code * p = ( * p & 0b1)|size|0b10 (the 0b prefix applies to constants in binary format). When the memory pointed by p is undefined, this ends up with the symbolic value (undef & 0b1)|size|0b10. It does not evaluate as a value, because the last bit is still undefined.

However, our semantics enables us to keep a symbolic value holding information about all the other bits instead of getting stuck. For instance, the symbolic value ((undef & 0b1)|size|0b10) & 0b10 has the well-defined normalisation 0b10 and retrieves the second last bit of the meta-data. This reasoning is made possible by the fact that size is a multiple of 4 (i.e. the last two trailing bits of size are zeros).

Copying Bytes between Memory Areas with memmove

Our semantics requires the target of jump instructions to be unique. This is a consequence of the fact that a symbolic value representing a conditional should normalise to some fixed boolean value. In other words, a program whose controlflow depends on the memory layout has an undefined behaviour. This dependance on the memory layout (e.g. on the memory allocator) is a portability bug that is detected by our semantics. Indeed, in our experiments, we have encountered this situation for the memmove function (see Fig. 5) which implements a memory copy even when the origin and destination memory regions do overlap. To cope with this situation, the memmove function performs the pointer comparison dest <= src. If the pointers dest and src point to distinct memory blocks, this comparison depends on the memory layout and is therefore undefined for our memory model. We have solved the issue by replacing the original condition dest <= src with the more involved condition src <= dest & dest < src + n. This condition explicitly tests whether the memory regions overlap using the integer n which is the number of bytes to be copied. Notice that we use on purpose the bitwise & operator (and not the lazy boolean && operator). A && would force the evaluation of src <= dest which cannot be normalised. The new condition with a & constructs a symbolic value which is independent from the memory layout and has therfore always a defined normalisation. In particular, if the pointers are from distinct blocks, the condition is always false because locations from distinct blocks cannot overlap.

Related Work

Wang et al. have shown that undefined behaviours of the ISO C standard have a negative impact on the security of software [START_REF] Wang | Undefined behavior: What happened to my code?[END_REF]. To tackle the problem Wang et al. propose a compiler-based approach to identify pieces of code whose optimised generated code exploit undefined behaviours [START_REF] Wang | Towards Optimization-safe Systems: Analyzing the Impact of Undefined Behavior[END_REF]. We adopt a semantics-based approach that aims at giving a meaning to programs that do not have a defined behaviour according to the ISO C standard.

Memory models have been proposed to ease the reasoning about low-level code. The VCC system [START_REF] Cohen | VCC: A Practical System for Verifying Concurrent C[END_REF] generates verification conditions using an abstract typed memory model [START_REF] Cohen | A Precise Yet Efficient Memory Model For C[END_REF] where the memory is a mapping from typed pointers (p ∈ T × B |u64| ) to structured C values. This memory model is not formally verified. Using the Isabelle/HOL proof assistant, the Autocorres tool [START_REF] Greenaway | Bridging the Gap: Automatic Verified Abstraction of C. In ITP[END_REF][START_REF] Greenaway | Don't sweat the small stuff: formal verification of C code without the pain[END_REF] constructs provably correct abstractions of C programs. Following Tuch et al. [START_REF] Tuch | Types, bytes, and separation logic[END_REF], a concrete memory is abstracted by an abstract memory m ∈ ′ a ptr → ′ a option where ′ a represents the type of the pointer. The memory models of VCC [START_REF] Cohen | A Precise Yet Efficient Memory Model For C[END_REF] and Autocorres [START_REF] Greenaway | Don't sweat the small stuff: formal verification of C code without the pain[END_REF] ensure separation properties of pointers for high-level code and are complete with respet to the concrete memory model. For the CompCert memory model [START_REF] Leroy | The CompCert memory model[END_REF], separation properties of pointers are for free because pointers are modelled as abstract locations l ∈ block × offset. For our symbolic extension, the completeness (and correctness) of the normalisation is defined with respect to a concrete memory model and therefore allows to reason about low-level idioms.

Several formal semantics of C are defined over a block based memory model where pointers are modelled by a location l ∈ block × offset [START_REF] Ellison | An executable formal semantics of C with applications[END_REF][START_REF] Krebbers | An operational and axiomatic semantics for non-determinism and sequence points in C[END_REF][START_REF] Leroy | Formal verification of a realistic compiler[END_REF]. The different models differ upon their precise interpretation of the ISO C standard. The CompCert C semantics [START_REF] Blazy | Mechanized Semantics for the Clight Subset of the C Language[END_REF] provides the specification for the correctness of the CompCert compiler [START_REF] Leroy | Formal verification of a realistic compiler[END_REF]. CompCert is used to compile safety critical embedded systems [START_REF] Bedin França | Formally verified optimizing compilation in ACG-based flight control software[END_REF] and the semantics departs from the ISO C standard to capture existing practices. Our semantics extends the existing CompCert semantics and benefits from its infrastructure.

Krebbers also extends the CompCert semantics but aims at being as close as possible to the C standard and proposes a formalisation of sequence points in non-deterministic programs [START_REF] Krebbers | An operational and axiomatic semantics for non-determinism and sequence points in C[END_REF] and of strict aliasing restrictions in union types of C11 [START_REF] Krebbers | Aliasing restrictions of C11 formalized in Coq[END_REF]. These aspects are orthogonal to the focus of our semantics which gives a meaning to implementation defined low-level pointer arithmetic. Ellison and Roşu [START_REF] Ellison | An executable formal semantics of C with applications[END_REF] propose an executable C semantics using the K framework [START_REF] Lucanu | K Framework Distilled[END_REF]. Unlike our semantics with symbolic values, they do not model low-level pointer arithmetic and only have a partial symbolic support for uninitialised values [7, Section 6.2.2].

Conclusion

We propose an executable semantics for C programs that augments the block based memory model of CompCert with the ability to reason about low-level pointer arithmetic and uninitialised values. The key insight is the use of symbolic values that represent delayed computations: symbolic values are only normalised when a concrete value is really needed. The normalisation is executable and efficient in practice thanks to the use of SMT solvers.

As future work, we shall investigate how to adapt the correctness proof of the CompCert compiler to our new memory model. A difficulty is that our model makes explicit that the memory is finite as the normalisation exploits the fact that pointers are indistinguishable from C integers. Moreover, our memory model is general enough and should be helpful to add in CompCert new target architectures where integer and float values are not so clearly separated in memory or in registers (e.g. SIMD architecture).

As another line of research, we intend to study how to ground security analyses upon our enhanced memory model. A feature of our memory model is that the normalisation, seen as an SMT query, implicitly enumerates all the possible concrete memory configurations. We shall investigate how to augment the axiomatisation of the memory to assess the consequences of a memory violation (e.g. use-after-free), and perform detailed vulnerability analyses.

Fig. 1 .Fig. 2 .

 12 Fig. 1. Undefined behaviour: reading the uninitialised variable status

  Memory locations: l ::= (b, i) (block, integer offset) Values: v ::= int(i) | float(f ) | ptr(l) | undef Memory chunks: κ ::= Mint8signed 8-bit integers | Mint8unsigned | Mint16signed 16-bit integers | Mint16unsigned | Mint32 32-bit integers or pointers | Mfloat32 32-bit floats Operations over memory states: alloc(M, lo, hi) = (M ′ , b) Allocate a fresh block with bounds [lo, hi[. free(M, b) = M ′ Free (invalidate) the block b load(κ, M, b, i) = ⌊v⌋ Read consecutive bytes (as determined by κ) at block b, offset i of memory state M . If successful, return the contents of these bytes as value v. store(κ, M, b, i, v) = ⌊M ′ ⌋ Store the value v as one or several consecutive bytes (as determined by κ) at offset i of block b. If successful, return an updated memory state M ′ . bound(M, b) Return the bounds [lo, hi[ of block b.

Fig. 3 .

 3 Fig. 3. CompCert's memory model

Fig. 4 .

 4 Fig. 4. Semantics of Clight with symbolic values (excerpt)

Example 2 .

 2 Consider a memory M restricted to two blocks b 1 and b 2 , with b 1 of bounds [0, 4[ aligned on word boundaries (i.e. the 4 trailing bits are zeros) and b 2 of bounds [0, 8[ with no alignment constraint. The axiomatisation of M is given by the following formulae. Block sizes: size

Example 3 .

 3 Consider again the memory M of Example 2 and the symbolic value e = ptr(b 1 , 1)ptr(b 2 , 2) + ptr(b 2 , 4) + undef&0x0.

Example 4 .

 4 Consider a memory with 3 unaligned blocks b 1 , b 2 and b 3 of size 1 and a last block b 4 of size 2 32 -4 that is 4-byte-aligned, i.e. the last two bits are zeros. Because of alignment and size constraints, the block b 4 can only be allocated at address 4 while other blocks can be allocated at the remaining addresses (i.e. 1, 2 and 3). As a result, the symbolic value ptr(b 1 ,0)+ptr(b 2 ,0)+ptr(b 3 ,0) evaluates to 6 which corresponds to the valid location (b 4 , 2).

Fig. 5 .

 5 Fig. 5. memmove with an undefined semantics

Typed languages detect illegal accesses and typically throw an exception.

* This work was supported by Agence Nationale de la Recherche, grant number ANR-12-INSE-002 BinSec.


Frédéric Besson

Thomas Jensen

Pierre Vittet Inria

SawjaCard: a static analysis tool for certifying Java Card applications

This paper describes the design and implementation of a static analysis tool for certifying Java Card applications, according to security rules defined by the smart card industry. Java Card is a dialect of Java designed for programming multi-application smart cards and the tool, called SawjaCard, has been specialised for the particular Java Card programming patterns. The tool is built around a static analysis engine which uses a combination of numeric and heap analysis. It includes a model of the Java Card libraries and the Java Card firewall. The tool has been evaluated on a series of industrial applets and is shown to automate a substantial part of the validation process.

Introduction

Security plays a prominent role in the smart card industry, due to their extensive use in banking and telecommunication. Hence, certification of smart cards has become accepted industrial practice. Traditional certifications (e.g., against the Common Criteria [START_REF]Common Criteria for Information Technology Security Evaluation[END_REF]) focus primarily on the protection mechanisms of the card's hardware and operating system. More recently, attention has been drawn to the increasing number of applications that execute on the cards and the smart card industry has elaborated a set of secure coding guidelines [START_REF] Le Pallec | Cardlet Development Guidelines[END_REF][START_REF]GlobalPlatform Card Composition Model Security Guidelines for Basic Applications[END_REF] that apply to basic applications. Basic applications are granted limited privileges and the goal of the guidelines is to ensure that they do not interfere with more sensitive (e.g., banking) applications. The verification of these guidelines is done by an independent authority that analyses the code and issues a certificate of conformance (or pinpoints failures of compliance). In collaboration with a company from the smart card industry we have developed the static analysis tool Saw-jaCard that can significantly simplify and automate the validation of smart card basic applications.

We consider applications written in the Java Card language -a dialect of Java dedicated to smart cards. To be validated, an application must respect a series of secure coding rules. SawjaCard is designed for the certification procedure proposed by AFSCM, the French industry association for Near Field Communication (NFC) technology providers, which consists of around 65 rules in total. These rules impose requirements on how an application is programmed, how it uses the resources of the card, and what kind of exceptions are acceptable.

Our main contribution is the implementation of the first static analysis tool able to automate the validation of basic applications according to AFSCM rules.

Our experiments show that SawjaCard proves automatically 87% of the properties. This work also demonstrates that precise but informal security guidelines can be mapped to formal properties that can be checked by harvesting a static analysis result. The design of the static analysis engine is a contribution of its own: we exploit the characteristics of Java Card but also constraints imposed by guidelines to get a precise yet efficient analyser. In terms of static analysis, the main contribution is a novel abstract domain for identifying a variant of the object-oriented singleton object pattern, where the nullity of a field is used to control the execution of an allocation instruction (Section 4.2).

We first present Java Card, highlighting the features relevant for security validation such as the Java Card firewall. The security requirements are described, and we explain how they can be verified on the model obtained through static analysis. We then present the main features of the analysis engine that is at the core of the tool. This includes the above-mentioned domain for detecting singleton objects and the use of trace partitioning for identifying file accesses. The tool has been evaluated against a series of industrial applications. We explain how the tool has significantly improved the certification procedure by automating a large part of the code verification.

Java Card

Java Card is a software development framework dedicated to multi-application smart cards. It includes a reduced version of Java, and has its own binary code format dedicated to devices with limited memory and processing capabilities. Like in Java, a Java Card application or library is written as a set of packages containing classes. After a standard Java compilation, Java Card converts all the classes belonging to the same package into a so-called CAP file. The CAP file is optimised to be small and meet smart card constraints, e.g., fields, methods and classes are referred via token integers in order to reduce the size of the file.

Java Card keeps the class-based object oriented model of Java. Class inheritance, interfaces and the resolution mechanism for virtual and static calls is the same as in Java. Primitive types are restricted to the Java boolean, byte, short and optionally integer (might not be supported by every platform and the use of integer is also forbidden in some security guidelines). Arrays are limited to single-dimensional arrays. Strings are not available, neither as a primitive type, nor as a provided library class. Garbage collection is not required by the Java Card specification and it is still common not to have a garbage collector in a smart card. As memory is precious, application are expected to allocate data only during their installation phase and as parsimoniously as possible. Security guidelines emphasise this aspect (e.g., allocation in a loop is forbidden).

The bytecode language is close to the Java bytecode language but with some noticeable differences. It is still a stack-based language with basically a reduced instruction set. However there are some differences which makes the Java Card bytecode more than a strict subset. For example, the operand stack contains 16 bits values and the standard operations work on such short values. Hence, each arithmetical operation is semantically different from its Java counterpart.

Modelling the Java Card runtime and its libraries

Our static analysis tool performs a whole program analysis. It takes a single application CAP file but also expects additional CAP files representing all the used libraries. The core Java Card libraries are usually not available for analysis. They are i) proprietary; ii) card dependent; iii) and (partly) implemented using native code. To get a portable and card independent whole program, we have implemented the core Java Card libraries and standard extensions such as Glob-alPlatform or ETSI standard UICC [START_REF]ETSI Project Smart Card Platform[END_REF] using pure Java Card code extended by specification methods that are built-ins of the analyser: RANDOM, ASSUME and ASSERT. As we are not interested in proving functional correctness but security properties, the model of a method is usually simple and is based on the informal specification of the libraries. The model initialises system resources of the Java Card runtime. For instance, it allocates singleton exceptions objects that are owned by the Java Card runtime or global system input/output buffers. The model is also responsible for simulating the different phases of the applet life cycle. The install phase consists in initialising the applet state. The applet is also assigned its Application IDentifier (AID) and is registered within the Java Card runtime. The process phase is an infinite event loop where the applet processes commands. Eventually, the applet enters the uninstall phase where it is removed from the card.

Modelling the Java Card firewall

The Java Card security architecture relies on a firewall which strongly limits inter-applet communication. The firewall mechanism guarantees that an interapplet communication triggers a dynamic run-time check whose success depends on the owner of the object and the running context of the code. Every created object is assigned an owner, which is the context of the applet performing the object allocation. Each method is assigned the context of its enclosing applet. At runtime, the virtual machine ensures that an applet can only manipulate objects in its context and raises a SecurityException otherwise.

Communication between applets is achieved through Shareable interfaces. Using a specific method of the runtime, an applet A receives a shareable request from an explicitly identified applet B. The applet A can accept the request depending on the identity of B and return an object o implementing a Shareable interface. When applet B calls a method of object o, a context switch occurs and the method runs with the context of A.

Our Java model makes explicit the security checks performed by the Firewall using built-in API calls to obtain the owner of objects GET_OWNER or the running contexts GET_CALLER_CONTEXT (see Fig. 1). The owner/context properties are directly modelled by the abstract domains: each abstract object in the heap is assigned a owner and the abstract call stack is tagged by running contexts.

Validation of Java Card applications

The validation of Java Card applications is based on several sets of coding guidelines, edited by industrial stakeholders. The main source of guidelines comes from the AFSCM [START_REF] Le Pallec | Cardlet Development Guidelines[END_REF], a French association of companies working in the area of NFC and contact-less smart cards. The AFSCM guidelines consists of 65 coding rules that specify properties that an applet must obey in order to be validated. Rules from the Global Platform [START_REF]GlobalPlatform Card Composition Model Security Guidelines for Basic Applications[END_REF] initiative have also been integrated. Some rules (such as "The interactions between different interfaces must be clearly defined.") are not amenable to automatic verification. Others are not considered because they concern the Java source ("A switch statement must always include a default case."). Eliminating duplicates, we extracted 55 verifiable rules from the guidelines mentioned above, and classified them as shown in Fig. 2.

The rules vary significantly in granularity and type of property. Some properties are purely syntactic ("An application must not contain a nop instruction", or "An application shall not use an AID already registered.") whereas others require information about the dynamic behaviour of the application ("no null pointer exceptions" or "no array-out-of bounds exceptions"). Some rules specify Figure 2: Classification of the rules (from AFSCM [START_REF] Le Pallec | Cardlet Development Guidelines[END_REF] and Global Platform [START_REF]GlobalPlatform Card Composition Model Security Guidelines for Basic Applications[END_REF]).

restrictions on how library methods can be called, and with what arguments.

Most of these rules cannot be verified as is, exactly due to the undecidability of the underlying semantic property, and approximations are called for. As mentioned above, an important feature of these rules is that certain rules simplify the verification of others. E.g., knowing that the rules "Recursive code is forbidden" and "Arrays must be allocated with a determined size" are satisfied means that the analyser can strive for more precision without running into certain complexity and computability issues. In the following, we explain how the validation of the rules can be done by mining the static analysis result.

Numeric values: In Java Card, resources are often accessed using integer identifiers and managed by calling methods with a fixed set of flags. Many rules specify that those integers must be constant or range over a set of legitimate values. Our analyser is computing an abstraction of numeric values and therefore of method arguments. The abstraction of the method arguments is checked for compliance with the rules.

Array values: Some resources can be coded by arrays of integers. For instance, files are identified by an array [i 1 ;...;i n ] which represents the file name i 1 /.../i n . Menu entries (i.e., strings) are coded by arrays of bytes. As with numeric values, validation rules often require those arrays to be constant. Files are an exception. File names are constructed by a sequence of calls fh.select(d 1 ) . . . fh.select(d n ) where fh is a FileView object and the d i are typically constants, identifying directories. Our analyser does not track sequences of events but our model of the class FileView is an array representing the current working directory that is updated by calls to the select method. Our analyser models arrays and provides for each index a numeric abstraction of the content. This abstraction is queried in order to validate rules about resources encoded as arrays.

Control-flow:

The validation rules impose constraints on the control-flow graph of the application-especially during the installation phase. For instance, most memory allocations are required only to take place during the install phase, identified by a call to the install method. The analysis is constructing an abstract control-flow graph corresponding to the inlined control-flow graph of the application. Constraints over the control-flow graph can therefore be checked by exploring the abstract control-flow graph. For the particular case of memory allocation, we traverse the graph and make sure that memory allocation primitives e.g., new statement, are only accessible from the install method.

Exceptional behaviour: Validation rules are strict about exception handling. Run-time exceptions such as ArrayOutOfBounds, NullPointerException and ClassCastException are strictly forbidden. In our bytecode intermediate representation, run-time exceptions correspond to explicit instructions and we generate verification conditions for all those instructions. For obvious reasons, security exceptions (SecurityException) are also forbidden. The abstraction of the heap is designed to model object ownership and can be used to ensure that the security checks performed by the Java Card Firewall do no raise Securi-tyException. There are other rules about exceptional behaviours which can be interpreted as coding guidelines. The analysis is precisely modelling the flow of exceptions. In particular, it collects for each handler the caught exception and for each method call the escaping exceptions. This information is sufficient for checking all the rules regarding exceptions.

Overview of the static analysis engine

Our static analysis engine is designed specifically for Java Card and its particular programming style. Existing general purpose analysis frameworks for Java e.g., [START_REF] Vallée-Rai | Soot -a Java bytecode optimization framework[END_REF][START_REF] Ibm | Watson Libraries for Analysis[END_REF][START_REF] Hubert | Sawja: Static Analysis Workshop for Java[END_REF] cannot be applied directly to Java Card. Firstly, existing frameworks do not provide a CAP front-end -this is a non-negligible engineering issue. Although CAP files are compiled from class files, the inverse transformation is far from obvious. For instance, the instruction set is different and dynamic method lookup is compiled using explicit virtual tables. Secondly, our static analysis engine exploits fully the fact that Java Card programs are relatively small, forbid recursion and allocate few objects. Standard Java analyses designed to scale for object-oriented programs cannot exploit this. Finally, the Java Card firewall which has no Java counterpart is also modelled directly at the analysis level.

Our analyser operates on a 3-address code intermediate bytecode representation A3Bir [START_REF] Demange | A Provably Correct Stackless Intermediate Representation for Java Bytecode[END_REF] that is obtained by pre-processing the binary CAP file. This representation is adapted from the Sawja framework [START_REF] Hubert | Sawja: Static Analysis Workshop for Java[END_REF] and has the advantage of making explicit the different runtime checks performed by the Java Card Virtual Machine. An example of such intermediate code is given Fig. 4.

The static analysis engine implements an inter-procedural scheme which consists in a dynamic inlining of method calls. The benefit is a precise interprocedural scheme that mimics the behaviour of a concrete interpreter. In terms of abstract domains, the domain of the inter-procedural analysis is D * given that D is the domain for the intra-procedural analysis. This approach is effective for two reasons that are specific to Java Card: recursion is forbidden and the programs are relatively small.

Combining intervals, constant sets and symbolic equalities

To abstract numeric values, the analyser is using a combination of three abstract domains: intervals, finite sets and symbolic equalities. The code snippet of Fig 3 illustrates their collaboration. The abstract domain of intervals Int is very popular but is not precise enough if used alone. At Line 4 of Fig. 3, the interval [0;5] is used to abstract the non-consecutive values 0 and 5. As many Java Card methods take as arguments integer flags or return integer flags that are in general not consecutive, this is a common source of imprecision. To deal with this issue, we use a domain Fin = P(Cst) ∪ {⊤} where Cst is the set of constants that appear in the program text. For efficiency, information about these constants is lost after arithmetic operations and reductions with the interval domain are limited to the cases of ⊥ and singletons i.e., abstract elements with represent a single concrete value. For Line 4, the product Int × Fin gives a precise invariant but would still be unable to infer that at Line 6 the value of i can only be 5. To get this result, it is necessary to propagate through the test j==0 the knowledge that j equals i. This is a known weakness of non-relational domains which compute an abstraction for each variable independently. There are well-known numeric relational domains e.g., convex polyhedra [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF], octagons [START_REF] Miné | The octagon abstract domain[END_REF]. These domains are very expressive but are also computationally costly. Our analyser is using a more cost-effective weakly relational domain [START_REF] Miné | Symbolic Methods to Enhance the Precision of Numerical Abstract Domains[END_REF] computing for each program point and each local variable x an equality x = e where e is a side-effect free expression of our intermediate representation i.e., an expression built upon variables, arithmetic operators and field accesses. At Line 5, we have the equality j==i. Hence, when j==0, i is also 0 and when j != 0, j have value 5 and so has i. Combined, the three domains are able to compute the precise invariant of Line 6.

Symbolic expressions improve the precision of numeric abstractions but also significantly contribute to ruling out spurious null pointers. This is illustrated by Fig. 4. Our goal is to verify that bar is called with a non-null argument. At source level, this property is obvious. However, the cumulative effect of Java compilation, CAP conversion and the re-construction of our analyser intermediate representation introduces temporary variables. Without symbolic expressions, at Line 3, we only know that the temporary variable t0 is not null but this variable is not used anymore. Symbolic expressions keep track of equalities between variables t0, t1, t2, the constant null and the value of field this.foo. Using the theory of equality, we can deduce at Line 2 that this.foo is not null. This information is propagated at Line 4 where we deduce that t2 is also not null. Therefore, at the call in Line 5, t2 is still not null.

Points-to analysis with detection of singleton objects

Our heap abstraction is flow-sensitive and takes the form of a points-to graph [START_REF] Hind | Pointer Analysis: Haven't We Solved This Problem Yet[END_REF]. A node in the graph is an abstract object identified by a call-stack and the creation point of the new statement, or a special node representing the null value.

Object creation is done with parsimony in Java Card, and most new statements only ever allocate one object. In other words, most abstract objects are singletons representing a single concrete object. If an abstract object is a singleton, the analyser can precisely model side effects and perform strong updates.

Abstract counting of the number of allocations of an abstract object o ∈ AO is a standard technique for identifying singletons objects. The properties "not allocated", "allocated at most once" and "allocated many times" are encoded by the numeric domain {0, 1, ∞}. Our domain is therefore Cnt = AO → {0, 1, ∞}. In Java Card most objects are allocated during the install phase. This phase is loop-free and abstract counting therefore precisely identifies singleton objects. However, abstract counting fails at identifying singleton objects that are allocated during the process command loop.

To improve precision we propose a novel abstract domain able to capture variants of the so-called object-oriented singleton pattern. The idea behind the singleton pattern is that a field fd is either i) null and the singleton object is not allocated or ii) not null and the singleton object is allocated. To capture such conditional invariants, our singleton domain maps each field to a valuation of the abstract allocation counters. The abstract domain is therefore Sgton = Field → Cnt. Consider sgton ∈ Sgton and a field fd . The intuition is that sgton(fd ) only provides information about abstract counters under the condition that the field fd is null. When the points-to ensures that a field fd is definitely not null, the condition does not holds and sgton(fd ) can be set arbitrarily, in particular it can be strengthened to ⊥. When the points-to ensures that a field fd is definitely null, the condition holds and sgton(fd ) can be used to strengthen the current abstract counters. If the condition cannot be decided, the information sgton(fd ) remains dormant but becomes useful after e.g., a test fd = null or would be updated after an assignment to the field fd .

Formally, given a concretisation γ Cnt : Cnt → P(Heap) for the Cnt domain, the concretisation γ : Sgton → P(Heap) is defined by:

h ∈ γ(sgton) iff fd h(fd ) = null ⇒ h ∈ γ Cnt (sgton(fd )).
Fig. 5 illustrates how the reduced product [START_REF] Cousot | Systematic Design of Program Analysis Frameworks[END_REF] of a points-to, Sgton and Cnt analyses can ensure the singleton property. Before the loop (Line 1), the object o is not allocated, the field fd is definitely null and the conditional property (fd = null ⇒ (o → 0)) holds. At the head of the loop (Line 4), the object o is a singleton, the field fd is either null or points to the object o. The singleton domain holds the key invariant: the object o is not allocated when the field fd is null. After the test fd == null (Line 6), we refine our points-to and conclude that fd is definitely null. Therefore, the conditional property of the singleton domain holds: we can exploit the right hand side of the condition and refine the and fd points to o. Hence, fd is definitely not null. This is where the conditional singleton domain becomes useful. Because the condition fd = null now no longer applies, the abstract counters can be strengthened to ⊥. For simplicity, say that the abstract state after the (empty) else branch is the abstract state of the loop head of Line 4. At the end of the conditional, after the join, we get the same abstract state as at the loop head, which is therefore a fixpoint. In practice, our Sgton domain also maintains conditions over instance fields and numeric fields (false plays the role of null). For our Java Card applications, those enhancements allow a precise identification of all singleton objects.

/* fd = null & (fd = null ⇒ (o → 0)) & o → 0 */ [...] while(true){ /* fd ∈ {null, o} & (fd = null ⇒ (o → 0)) & o → 1 */ if (fd == null) /* fd = null & (fd = null ⇒ (o → 0)) & o → 0 */ fd = new o(); /* fd = o & (fd = null ⇒ ⊥) & o → 1 */ }

File system access: a case for trace partitioning

Trace partitioning [START_REF] Rival | The trace partitioning abstract domain[END_REF] is a generic technique for locally improving the precision of a static analysis. It consists in partitioning an abstract state depending on a history of events. Suppose that the original abstract state is D ♯ , after trace partitioning, the abstract state is (Event * × D ♯ ) * where Event is an arbitrary set of syntactic events (e.g., a call to a specific method) or semantic events (e.g., the variable x has value v). We have successfully used trace partitioning for precisely determining the files accessed by an application.

As explained in Section 3, Java Card comes with a hierarchical file system. In our model, the current directory i 1 /.../i n is coded by an array of short [i 1 ;...;i n ] that is stored in the path field of a file handler object fh implementing the FileView interface. Moving to the i n+1 directory is done by the method call fh.select(i n+1 ). Therefore, determining the accessed files requires a precise analysis of the array content.

Consider the code of Fig. 6 that is representative of how files are accessed in Java Card. Suppose that before calling the cd method, the field fh is either null or points to an object ofh such that ∀i, ofh.path[i] = 0. At the method return, with our base abstraction, the effect of the three paths is merged. We loose precision and get res = fh ∈ {null; ofh}∧ofh.path

[0] ∈ [0; 1] ∧ ofh.path[1] ∈ [0; 20].
However, the precise post-condition of the cd method is P 1 ∨ P 2 ∨ P 3 where each

P 1 △ = res = null ∧ fh = null ∧ ofh.path[0] = 0 ∧ ofh.path[1] = 0 P 2 △ = res = null ∧ fh = ofh ∧ ofh.path[0] = 1 ∧ ofh.path[1] = 0 P 3 △ = res = ofh ∧ fh = ofh ∧ ofh.path[0] = 1 ∧ ofh.path[1] = 20
Even for Java Card, the disjunctive completion [START_REF] Cousot | Systematic Design of Program Analysis Frameworks[END_REF] of our base abstract domain does not scale. Trace partitioning [START_REF] Rival | The trace partitioning abstract domain[END_REF] offers a configurable trade-off between efficiency and precision. In particular, it allows a fine-grained control of when abstract states should be merged or kept separate. Our trace partitioning strategy is attaching to abstract states the trace of the encountered select calls. A trace event is therefore of the form select i where i identifies uniquely the method call in the control-flow graph. At the end of the cd method, we obtain: [] : P 1 [select 3 ] : P 2 [select 3 ; select 5 ] : P 3 . The security guidelines mandate that the applet install phase and the processing of a single command of the process phase should terminate. We exploit this information and merge traces at those specific events. This strategy is precise and terminating for all the Java Card applications we have analysed.

Experimental evaluation

We have evaluated SawjaCard on 8 industrial Java Card applets. For confidentiality reasons, we are required to keep them anonymous. The applications are representative of basic applications. There are loyalty applets but also phone applications. They require few privileges but access nonetheless certain nonsensitive part of the file system. The characteristics of the applets can be found in Fig. 7. For each applet, we provide the number of instructions of the application and the number of instructions taking into account the libraries used by the application. To give a finer estimate of the complexity of the code, we also provide the number of nodes in the inlined control-flow graph constructed by SawjaCard. However, this is still a coarse-grained measure of code complexity which is weakly correlated with the analysis time. For instance, applet A1 executes more instructions than applet A2, has fewer CFG nodes but takes longer to analyse. The analysis time is obtained using a laptop with a Intel Core i7 processor and 8 GB of memory. Fig. 8 summarises the analysis results for the 8 applets. We made a selection of the properties that can be evaluated in a fully automatic way i.e., the result is either boolean or can be expressed as a percentage of alarms. An entry in Fig. 8 reads as follows. A denotes a fully verified property. A property is marked x if it is a true violation according to our manual inspection of the code. A ? denotes a false positive. A number denotes a percentage. For instance, 90 means that the property holds for 90% of the program points relevant for the property -percentages are rounded from below. If it is in bold red, the remaining alarms are true violation. Otherwise, we could not ascertain the absence of false positives. For 75% of the properties, SawjaCard reports no alarm and thus those properties are automatically validated. We have investigated the remaining alarms manually. For 12% of the properties, we have concluded that the alarms were all genuine violations of the properties. Therefore, the verdict of SawjaCard is precise for 87% of the properties. For the remaining 13%, there are false positives. For instance, we identified that certain ArrayOutOfBounds alarms were due to a lack of precision of the analysis. However, on average, SawjaCard validates nonetheless about 87% of array accesses. For the remaining alarms, there are false positives but also real alarms. In the following, we explain in more details a selection of the properties of Fig 8.

NullPointerException 1 The precision of our null pointer analysis is satisfactory as SawjaCard validates 98% of reference accesses. Moreover, for 4 of the applets, we could conclude after manual inspection that the remaining alarms were real errors. For the other 4, the reasoning is more intricate and there might still be false positives. A typical error we found consists in ignoring that certain APIs can (according to the official specification) return a null pointer in some unusual cases. For instance, the method getEntry of the class uicc.toolkit.ToolkitRegistrySystem may return null if the server does not exist or if the server returns null. None of the analysed application performs the necessary defensive check to protect itself against such a null pointer.

ArrayOutOfBounds2 SawjaCard validates 87% of array accesses. The remaining accesses are sometimes false positives. In particular, we have identified an access whose verification would require a relational numeric analysis. However, a simple rewrite of the code would also resolve the problem. Other array accesses rely on invariants that are not available to the analyser. For instance, certain array indexes are read from files. More precisely, when reading a file, certain applications first read a special segment, which is the file status. The full size of the file is a field of this file status. As the content of the file cannot be known, it is impossible to track this length.

CatchIndividually3 This rule corresponds to a strict coding discipline that is almost syntactic: each type of exception should be caught by a different handler. This property is responsible for numerous alarms. All the reported alarms correspond to true violations of the rule. For instance, the following not compliant code snippet catches all the different exceptions with a single handler. CatchNonISOException 4 All the applets trigger alarms for this property. The alarms correspond to violations of the property. The exceptions that are ignored correspond to exceptions that are not thrown by the application itself but escape from library code. It might very well be that the proprietary implementations never raise these exceptions. Nonetheless, their possibility is reflected by our model of the API which is based on the Java Card API specification.

Other properties. The AFSCM rules forbid the classic Java exceptions: Class-CastException, NegativeArraySize and ArrayStoreException. For all the applets, SawjaCard proves their absence. Thanks to our modelling of Java Card Firewall, SawjaCard is also able to rule out SecurityExceptions. The rule AppletInStat-icFields specifies that applet objects should not be stored in static fields. This property is validated for all the applets. The next two rules concern values that should be constant: array sizes and menu entries. Those rules are also validated for all the applets. The rule SDOrGlobalRegPriv is about privileges that should be granted to access certain APIs. Applet 1 requires certain privileges and therefore raises an alarm. The rules SWValid and ReplyBusy specify the range of the status word return by applets. The rule is verified for all the applets except applet 1. This is probably a false alarm given that the applet is using a non-standard way of computing the status word. The last rule concerns certain method calls returning handlers that should be protected by try-catch blocks. SawjaCard raises an alarm for all the applets. This rule is indeed violated.

DeadCode5 For all the applets, SawjaCard detects some dead code which is due to the Java compilation. Consider the following method which unconditionally throws an exception. The return instruction is not reachable but is required by the Java compiler. The Java compiler also enforces that method should list the exceptions they might raise using a throws clause. However, the algorithm for checking this clause is purely syntactic. To make Java Card compile, a defensive approach consists in adding handlers for all the potential exceptions. For certain calls, SawjaCard proves that certain exceptions are never thrown and that the handlers are therefore dead code. For compliance with the rule, a workaround would be to remove the useless handlers and add to the throws clause of the method all the exceptions that are proved impossible.

File handling 6 There is a significant number of properties concerning files. Some of them are simple and do not lead to false positives (such as CreateFile, CreateFilesAtInstall, FileResizing which only require to check arguments for specific method calls). Other properties are more complex and require a precise identification of the files that are read or written. Using trace partitioning (see Section 5), we can precisely identify files paths that are constructed by a sequence of select instructions with constant arguments. However, certain applets make the assumption that the AID of a particular application is stored at a specific position in a system file. The AIDs is thereafter used to access the root of the sub file system owned by the application AID. Our model of the file system is too coarse to encode this assumption and therefore we cannot handle this pattern.

Allocation 7 The alarms are real violations. Most applets allocate objects after the install phase. Yet, more relaxed rules allow the allocation of singleton objects. This rule is still violated by applet 6 which repeatedly tries to get a handler. In our model of the library, each unsuccessful try allocates an intermediate object and is therefore responsible for a memory leak. For the other applets, our singleton domain is precise and ensures that memory allocation is finite.

Related work

For analysing Java programs, there are mature static analysis frameworks such as Soot [START_REF] Vallée-Rai | Soot -a Java bytecode optimization framework[END_REF] and Wala [START_REF] Ibm | Watson Libraries for Analysis[END_REF]. Based on Wala, the Joana tool [START_REF] Graf | Using JOANA for Information Flow Control in Java Programs -A Practical Guide[END_REF] is able to prove security properties based on information-flow. Information-flow analyses would probably benefit from the Java Card restrictions. Currently, AFSCM guidelines do not consider such properties and are limited to safety properties.

Algorithms tuned for Java are usually not well-fitted for the constraints of Java Card. In particular, state-of-the-art algorithms for constructing control-flow graphs of Java programs are based on context-sensitive flow-insensitive pointsto analyses [START_REF] Lhoták | Evaluating the benefits of context-sensitive points-to analysis using a BDD-based implementation[END_REF][START_REF] Smaragdakis | Pick your contexts well: understanding object-sensitivity[END_REF]. For Java Card, our analyser demonstrates that a contextsensitive flow-sensitive points-to analysis is viable. It dynamically inlines methods calls and therefore literally computes an ∞-CFA. The Astree analyser is using a similar strategy for handling function calls [START_REF] Cousot | The ASTRE É Analyzer[END_REF]. In their context, the programs are large and function calls are rare. Java Card programs are comparatively tiny but method calls are ubiquitous.

For Java, Hubert et al., [START_REF] Hubert | A non-null annotation inferencer for Java bytecode[END_REF] show how to infer the best @NonNull annotations for Fähnrich and Leino type system [START_REF] Fähndrich | Declaring and checking non-null types in an object-oriented language[END_REF]. The static analyser Julia [START_REF] Spoto | The Nullness Analyser of julia[END_REF][START_REF] Spoto | Precise null-pointer analysis[END_REF] implements a more costly but also more precise null pointer analysis that can be efficiently implemented using BDDs. Because our objects are singletons, our flow-sensitive points-to analysis performs strong updates and is therefore precise enough to precisely track null pointers and rule out NullPointerExceptions.

Might and Shivers [START_REF] Might | Improving flow analyses via GammaCFA: abstract garbage collection and counting[END_REF] show how to improve abstract counting of objects using abstract garbage collection. Their analysis can prove that an abstract object corresponds to a single live concrete object. Our singleton domain is based on a different program logic and can ensure that an abstract object is only allocated once. As Java Card usually does not provide garbage collection, we really need to prove that there are only a finite number of allocated objects.

Semantics [START_REF] Siveroni | Operational semantics of the Java Card Virtual Machine[END_REF][START_REF] Éluard | An Operational Semantics of the Java Card Firewall[END_REF] and analyses [START_REF] Hansen | Towards Verification of Well-Formed Transactions in Java Card Bytecode[END_REF][START_REF] Éluard | Secure Object Flow Analysis for Java Card[END_REF] have been proposed for Java Card. Huisman et al., [START_REF] Huisman | Checking Absence of Illicit Applet Interactions: A Case Study[END_REF] propose a compositional approach to ensure the absence of illicit applet interactions through Shareable interfaces. For basic applications such interactions are simply forbidden. Our tool verifies that applets do not expose Shareable interfaces and therefore enforces a simpler but stronger isolation property. A version of the Key deductive verification framework [START_REF] Ahrendt | The KeY system: Integrating Object-Oriented Design and Formal Methods[END_REF] has been successfully applied to Java Card [START_REF] Mostowski | Formalisation and Verification of Java Card Security Properties in Dynamic Logic[END_REF]. JACK [START_REF] Barthe | JACK -A Tool for Validation of Security and Behaviour of Java Applications[END_REF] is another deductive verification tool dedicated to Java Card that is based on the specification language JML [START_REF] Leavens | A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java[END_REF]. However, deductive verification is applied at the source level and requires annotations of the code with pre-(post-)conditions. This methodology is not applicable in our validation context which needs to be fully automatic for binary CAP files.

Conclusions

The validation process for smart card applications written in Java Card involves around 55 rules that restrict the behaviour of the applications. This process can benefit substantially from static analysis techniques, which can automate most of the required verifications, and provide machine-assistance to the certifier for the rest. The SawjaCard validation tool contains a static analysis which combines analysis techniques for numeric and heap-based computations, and which is further enhanced by specific domain constructions dedicated to the handling of the file system and Java Card firewall. A substantial part of building such a validation tool involves the modelling of libraries for which we propose to build a series of stubs whose behaviour approximates the corresponding APIs sufficiently well for the analysis to be accurate. Benchmarks on a series of industrial application shows that the tool can analyse such applications in a reasonable time and eliminate more than 80% of the required checks automatically.

The development of the tool suggests several avenues for further improvements. The properties for which the tool could be improved are ArrayOutOf-BoundException and file properties. The numeric analysis is only weakly relational, and it would be possible to increase its precision by using a full-blown relational domains such as polyhedra or octagons. An effective alternative to significantly reduce the number of alarms would be to impose stricter coding rules (for example defensive checks for narrowing down the range of non constant indexes). Our model of the file system could also be improved. To get a precise and scalable analysis, our assessment is that file system specific abstract domains should be designed. Certain properties are also simply not provable because they depend on invariants that are established by the personalisation phase of the application. This phase happens after the install phase and corresponds to commands issued, in a secure environment, by the card manufacturer. Currently, the end of this phase has no standard specification and cannot be inferred from the applet code. For the others properties we have satisfactory results: when the tool emits an alarm, it corresponds to a real error in the application. The tool has been recently transferred to industry where it will be used as part of the validation process.

Figure 3 :

 3 Figure 3: Collaboration between numeric abstract domains

2 / 4 /Figure 4 :

 244 Figure 4: Left: Source code Right: A3Bir representation

Figure 5 :

 5 Figure 5: Singleton pattern

Figure 6 :

 6 Figure 6: Typical code for accessing files

Figure 7 :

 7 Figure 7: Applet characteristics

Figure 8 :

 8 Figure 8: Analysis results -selected properties.

1 try{buffer=

 1 JCSystem.makeTransientByteArray((short)140,CLEAR_ON_RESET);} 2 catch (Exception e) {buffer = new byte[(short)140];}

1

  void dead_code (short val){ SystemException.throwIt(1); return; }

From AFSCM rules: A basic application shall not include any code that leads to NullPointerException, whatever this exception is caught or not.

From AFSCM rules: An application must not include any code that leads to Array-OutOfBoundException, caught or not.

From Global Platform rules: The Application should catch each exception defined by the used APIs individually in the application code and should explicitly rethrow the exception to the card runtime environment if needed.

From AFSCM rules: All exceptions thrown during the execution from any defined entry point must be caught by the application, except ISOException that are thrown in response to a command.

From AFSCM rules: dead code must be deleted/removed from the code.

From AFSCM rules: The file system provides access to files that are under the control of the Mobile Network Operator. These files shall not be accessed by applications, except for a few exceptions.

From Global Platform rules: A basic application should not perform instantiations in places other than in install() or in the applet's constructor.

Acknowledgements. We thank Delphine Demange, Vincent Monfort and David Pichardie for their contributions to the development of the tool.