=Paper= {{Paper |id=Vol-1431/paper6 |storemode=property |title=An Approach for Formal Verification of Updated Java Bytecode Programs |pdfUrl=https://ceur-ws.org/Vol-1431/paper6.pdf |volume=Vol-1431 |dblpUrl=https://dblp.org/rec/conf/vecos/LounasML15 }} ==An Approach for Formal Verification of Updated Java Bytecode Programs== https://ceur-ws.org/Vol-1431/paper6.pdf
         An Approach for Formal Verification of
          Updated Java Bytecode Programs


                          Razika Lounas1,2                                    Mohamed Mezghiche
           1
           University of M’hamed Bougara of Boumerdes            University of M’hamed Bougara of Boumerdes
             Facutly of Sciences, LIMOSE Laboratory                Facutly of Sciences, LIMOSE Laboratory
          Avenue de l’independance, 35000 Boumerdes              Avenue de l’independance, 35000 Boumerdes
                               Algeria                                              Algeria
                       2
                         University of Limoges                         mohamed-mezghiche@umbb.dz
        123 Avenue Albert Thomas, 87700 Limoges, France
                      razika lounas@umbb.dz
                                                 Jean-Louis Lanet
                                                  INRIA LHS-PEC
                                     263 Avenue Général Leclerc, 35000 Rennes
                                                       France
                                              jean-louis.lanet@inria.fr



   This paper deals with formal specification and verification of Java bytecode update. Programs update for
   java applications has gained a wide interest since it is used for several purposes: transforming semantics
   of a program, adding features to a program or performing optimizations. In this paper, we focus on
   program transformations for java programs at the bytecode level. Because these transformations may
   introduce errors, our goal is to provide a formal way to verify the update and establish its correctness.
   Our approach for formal specification and verification of updated Java bytecode programs is based on four
   ingredients: a formal interpretation of the semantics of update operations, a functional representation of
   bytecode, bytecode annotation and predicate transformation calculus. We use the concept of Hoare predicate
   transformation to derive a specification of an annotated bytecode. Annotations are used to express update
   operations within the code. A functional representation is used to model annotations and bytecode. The
   approach derives then a new specification for the annotated bytecode using a weakest precondition calculus
   defined to deal with update operations. Verification conditions are then generated and proved to establish
   the correction of the update.

               Bytecode transformation, formal semantics, weakest precondition calculus, bytecode verification.

1. INTRODUCTION                                                 some cases, the source code is not available (or
                                                                not distributed). Transforming a program at bytecode
During their life cycle, programs need to be                    level is an interesting alternative since several
updated in order to alter their semantics, perform              languages like Java or Java Card are based on
optimizations or add features. Several techniques               virtual machines executing bytecode. Transforming
were presented for this purpose in literature, for              programs at bytecode level offers some advantages:
example, (Neamtiu et al. (2006) and Gupta et al.                it does not require to recompile which can be a time
(1996)) present systems for C programs updating                 consuming task as in the case of transformations
and (Orso et al. (2002), Hlopko et al. (2013))                  at source code level. On the other hand, bytecode
present systems to update Java programs.                        level transformation is more complex than source-
                                                                level manipulation for the users because they have
Updating programs leads to the transformation                   to know bytecode language very well and because
of their elements such as code, data structures                 of the many low-level details one needs to use.
and state. We focus on the transformation of
Java codes. In this context, several tools were                 Java bytecode transformation is used in several
developed, for example, Java Syntactic Extender                 applications and several tools were developed to
(JSE) (Bachrach and Playford (2001)) and ixj                    manipulate Java bytecode programs such as BCEL
(Boshernitsan and Graham (2004)). However, in
                                            ••


(Dahm (1999)) and RuggedJ (McGachey et al.               the following contributions: the definition of a new
(2009)). In (Sakamoto et al. (2000)), the authors        weakest precondition calculus as the base of the
developed an algorithm to ensure portable thread         verification process, a formal interpretation of the
migration in Java. This algorithm is based on            semantics of the update operations, a functional
bytecode transformation. Bytecode is transformed in      representation of bytecode programs and bytecode
order to enable programs to save and restore their       annotation. The choice of functional representation
execution state after migration through the network.     is motivated by our interest in capturing the behavior
Another purpose for bytecode transformation is           of the initial bytecode and the updated version and
presented in (Binder and Hulaas (2005)) where            the mature existing tools for formal reasoning about
a framework based on bytecode transformation is          functional programming languages.
developed in order to enable Java applications to
perform CPU management.                                  This paper is organized as follows: in section 2
                                                         we give an overview of embedDSU. Section 3
In some cases, the transformation occurs at runtime.     introduces the language and the formal semantics of
The update is then said to be dynamic (Dynamic           the updates. In section 4, we present an overview
Software Update: DSU). In (Noubissi (2011)) and          of our approach in its steps. We present the
in (Noubissi et al. (2011)), the authors presented a     specification languages is section 5. In section 6,
system to perform DSU: while the Java Card virtual       we give our functional modelisation of Java bytecode
machine is executing the program, the bytecode is        and annotations. We propose a predicate calculus
updated.                                                 for update operations in section 7 and give the
                                                         notion of a correct update. This section ends with an
This large interest of Java bytecode transformation      example to show how the logic works. We discuss
and its use in many critical applications raise the      related work in section 8 and conclude in section 9.
question of its correctness. In fact, a transformation
may introduce an error which may alter the
bytecode leading the system to an unexpected             2. OVERVIEW OF EMBEDDSU
state. Besides, in some cases, the update is
                                                         EmbedDSU (Noubissi (2011), Noubissi et al. (2011),
critical (e.g. EmbedDSU) in such a way that an
                                                         Noubissi et al. (2010)), is a software-based DSU
attacker can take advantage of an incorrect update.
                                                         technique for Java-based smart cards which relies
In these applications where security issues are
                                                         on the Java virtual machine. It is based on
involved the update must pass some certification
                                                         the modification of an embedded virtual machine.
procedure for example Common Criteria (Common
                                                         EmbedDSU is divided in two parts: off-card and on-
Criteria (2015)). For a certain certification level
                                                         card:
one has to provide a formal proof of the security
mechanism implemented. A formal way to specify           (i) In off-card, a module called DIFF generator
transformations and verify their correctness is then           determines the syntactic changes between
necessary.                                                     versions of classes in order to apply the update
                                                               only to the parts of the application that are
Formal methods offer rigourous means in specifying
                                                               really affected by the update. The changes are
software properties and establishing the correctness
                                                               expressed using a Domain Specific Language
of programs regarding their formal specifications.
                                                               (DSL). Then, the DIFF file result is transfered
In this work, we present an approach for formal
                                                               to the card and used to perform the update.
verification of bytecode update. We focus on Java
bytecode and the system presented in (Noubissi et        (ii) The on-card part is divided into two layers:
al. (2011)) called embedDSU: a system developed                1) Application Layer: The binary DIFF file
to implement DSU functionalities in Java Card                  is uploaded into the card. After a signature
applications. It is based on two parts: off-card in            check with the wrapper, the binary DIFF is
which a module called DIFF generator computes                  interpreted and the resulting instructions are
the syntactic changes between the old and the new              transferred to the patcher in order to perform
version of the application and generates a DIFF file           the update. The patcher initializes data
(called also a patch). This patch is then sent on              structures for update. These data structures
the card to perform the update by other modules                are read by the updater module to determine
implemented by extending the Java Card virtual                 what to update and how to update, by the
machine.                                                       safeUpdatePoint detector module to determine
                                                               when to apply the update and by the rollbacker
In this work, we propose to formally verify that               to determine how to return to the previous
the obtained bytecode is semantically equivalent to            version in case of update failure. These
the one written by the programmer and used to                  points require the introspection of the virtual
perform the DIFF file. Our approach is based on                machine. 2) System Layer: the modified virtual
                                                                Figure 2: An example of a patch (DIFF file)


         Figure 1: Architecture of EmbedDSU              update and where it occurs in the bytecode. An
                                                         example is shown figure 2: the patch indicates that
                                                         the instruction iadd in the method compute sum is
     machine supports the followings features: (1)
                                                         deleted and the instruction isub is added at the same
     Introspection module which provides search
                                                         place provided by the program counter.
     functions to go through VM data structures
     like the references tables, the threads table,
     the class table, the static object table,           3. LANGUAGE AND SEMANTICS
     the heap and stack frames for retrieving
     information necessary to other modules;             3.1. The language
     (2) updater module which modifies object
                                                         For the definition of the semantics, we extend the
     instances, method bodies, class metadata,
                                                         formalism used by Freund and Mitchell (Freund and
     references, affected registers in the stack
                                                         Mitchell (1999)). The authors define a type system
     thread and affected VM data structures; (3)
                                                         for a small subset of Java bytecode. We define a
     SafeUpdatePoint detector module permits to
                                                         subset and propose to extend it with instructions
     detect safe point in which we can apply the
                                                         to indicate updates called update instructions
     update by preserving coherence of the system.
                                                         (Upd instr ) for instruction addition, deletion and
The system EmbedDSU is suitable for smard cards          modification. In this definition, x is a local variable;
especially in term of resource limitations. It was       L is an instruction address; A is a class name; f is a
established that sending a DIFF file is less ressource   field name; l is a method name and pc the program
consuming than sendig the whole new version to the       counter.
card and perform updates and that the resources
                                                         Instruction ::= |pop |if L |store x |load x |new A
implied by the update modules are acceptable in
                                                         |binop |neg |const a |invokevirtual A l t |goto L
term of memory occupation (Noubissi (2011)). The
                                                         |getf ield A f t |putf ield A f t |return
system EmbedDSU updates three principal parts:

(i) The bytecode: the process updates first the          U pd Instr ::= Add Inst Instruction pc
      bytecode of the updated class and the meta         |Dlt Inst Instruction pc
      data associated with it e.g., constant pool,       |M od Inst Instruction instruction pc
      fields table, methods table...
                                                         In this language, the instruction pop extracts the top
(ii) The heap: The process updates the instances         of the stack and const a pushes a constant a on
      of the updated class in the heap, obtains new      the top of the stack. The instruction load x pushes
      references for modified objects and updates        the value in the variable x on the top of the stack
      instances using these references.                  whereas the instruction store x pops the top of the
                                                         stack and stores it in the variable x. The instruction
(iii) The frames: The process updates in each frame      if L jumps to L if the top of the stack is not zero else
       in the thread stack the references of updated     it performs the following instruction. Goto L jumps to
       objects to point to new instances.                L. The instruction N ew A allocates a new object of
                                                         type A and pushes it on the top of the stack. The
This paper addresses the first part: bytecode update     instructions manipulating fields are : getf ield A f t
at the method level. The types of updates that           and putf ield A f t. Getfield reads the field f , which
may occur are: adding, modifying or suppressing          has the type t of the object of class A whose
bytecode instructions, changing the signatures of a      reference is on the top of the stack and pushes its
method or modifying local variables. These updates       value on the top of the stack and putfield modifies
are contained in the DIFF file which indicates the       the field f with the value popped form the stack.
                                             ••


The instruction invokevirtual invokes the method l        the semantics to establish that an updated program
of signature t and the class A. The instruction Binop     is well typed. It is also used in further section to
is used to gather arithmetic binary operations: add,      derive specifications for program transformations. In
mult and sub. The instruction neg negates the top of      the rules shown in tables 2 and 3, F is a mapping
the stack and return is for method return.                from a program point to a mapping from a frame
                                                          variable to a type. S is a mapping from a program
Update instructions are respectively: adding an           point to an ordered sequence of types, i denotes
instruction, deleting instruction and modifying an        a program point or an address of code. The map
instruction. We indicate the place of the update          Fi gives a type of local variables at program point
operation with pc.                                        i. The string Si gives the types of entries in the
                                                          operand stack at program point i. These F and S
3.2. Operational semantics for bytecode                   are useful to our semantics since they contain typing
instructions                                              information about valid local variables and entries
                                                          in the operand stack respectively. SD represents
We model the interpretation of the instructions
                                                          the stack depth and M (mapping) is a function that
of the bytecode instructions using the standard
                                                          associates a number to each line. Dom is the set
framework for operational semantics (Freund and
                                                          of addresses used by the method. A configuration
Mitchell (1999), Bannwart and Müller (2005)). Each
                                                          at line i is represented by < (F, S, SD, M ), i >. The
instruction is characterised by the transformation of
                                                          judgement that expresses that a bytecode BC is well
a configuration. A configuration < M, s, h, f, pc >
                                                          typed by F , S, SD and M is:
representing a step execution consists of an operand
stack s, a heap h, a local variables map f , a             F1 = F⊤ , SD1 = 0
program counter pc and the body M . Operational            S1 = ε, M 1 = M ap(BC)
semantics is defined by a transition relation over         ∀i ∈ DOM (BC), F, S, SD, M, i ⊢ BC
configurations. A transition < M, s, h, f, pc >→<                       F,S,M,SD⊢BC
M, s2, h2, f 2, pc2 > takes the state from the
configuration < M, s, h, f, pc > to the configuration     The first two lines of the judgement represent the
< M, s2, h2, f 2, pc2 >.                                  initial configuration: all variables are mapped to the
                                                          value top (default initial value), stack depth is zero,
The rules for the instructions of our language are        the sequence of types is initially empty (ε) and M 1
represented in table 1. The instruction new A creates     is the mapping of the initial bytecode. The last line
a new object of class A, thereby modifying the            expresses that each instruction (update instruction)
current heap. A reference to the new object is            in the bytecode is well typed. This is ensured by
pushed onto the stack. store x pops a value from          the rules given in tables 2 and 3. For illustration,
the evaluation stack and assigns it to a variable,f is    the insertion of the instruction new A at line i +
modified accordingly. load x put the value of x on the    1 allows us to obtain a new configuration if the
top of the stack. The binop operation which pops two      stack depth is incremented, local variables are not
values from the stack, performs the binary operation,     affected and in the stack, the type A is inserted.
and pushes the result. if l has two rules; wether it      In the instruction invokevirtual the function dom
jumps to the indicated line or performs the following     represents the domain of the invoked function (types
instruction according to the value of the top of stack.   of its arguments) and the function card represents
The instruction putf ield updates the heap with the       the number of elements in the domain. The rule
new value of the field of the object which is on the      expresses that these arguments are popped from the
top of the stack. The new value is popped from the        stack of type and then the result is pushed. For the
second element of the stack. invokevirtual invokes        insertion of an instruction representing an arithmetic
the method l on an object reference and parameters        binary operation Binop, we show the rule of the
on the stack and replaces these values by the return      instruction add: this operation pops two elements
value v of the invoked method after its execution.        (integers) from the stack and then pushes the result.
                                                          mult and sub have analogous explanations by writing
3.3. Formal semantics for update instructions             the right operation. In the rules, the mapping M 2 is
                                                          the result of operations on M 1. The operations which
We propose a static semantics to express the effects      represent manipulations on bytecode are: range and
of update instructions on a configuration of the          shift. The operation range extracts from a mapping
bytecode. This semantics was introduced in our            M 1 a part M 2 included between line n and line m.
initial paper (Lounas et al. (2012)). The purpose         The second operation shifts a part from a mapping
of the semantics is to express formally the effects       between n and m for p positions which is determined
and the conditions of update instructions and thus        by the number of added instructions.
prevent type errors in the updated bytecode. In this
paper, we give more rules and show how to use
                                             ••


We define the operations look f or jumps and
update jumps to take into account jumps in bytecode
transformation: look f or jumps returns from a
mapping a list of jumps instructions represented by
their line number and the operation update jumps
updates jump instructions:
Look f or jumps : mapping → int list
U pdate jumps : mapping ∗ int list ∗ int → mapping

These operations updates jumps within the bytecode
if necessary. When we add for instance an
instruction at pc, the instructions after this position
                                                                     Figure 3: Approach for verification
are shifted and their numbers change. It is then
necessary to update goto and if instructions
accordingly. These modifications keep the structure       semantically equivalent. This equivalence ensures
of the bytecode coherent. In the rules for instructions   that the system indeed implemented the desired
suppression (table 3), Ef f ect ST K, Ef f ect F and      transformation. This problem can be expressed
Ef f ects SD are used to express the effects of           equationally by:
an instruction of the stack and the local variables
and stack depth. They are used to readjust these          ∀P 1, P 2, P 2′ , ∆ =  DIF F (P 1, P 2), P 2′          =
elements to the instruction at (i + 1) in the             App P AT CH(P 1, ∆) ⇒ P 2 ≡ P 2′
new bytecode after the suppression. The notation
(M 2)F (Respectively, (M 2)S) is used to express F        This raises two major issues: 1- how to model
(Respectively, S) in the mapping M 2. We notice that      the application of the DIFF file on an existing
in this formalisation, a modification is considered as    program? and 2- how to express the equivalence
a suppression followed by an insertion.                   which guarantees the correctness of the update?
                                                          We present the overview of our approach for
                                                          transformation verification. Figure 3 represents an
4. APPROACH FOR FORMAL VERIFICATION                       overview of our approach which is split in three parts:
The mechanism of EmbedDSU implies the modifica-           (i) The transformation block: in this stage, we obtain
tion of the bytecode of a running application on-card           from a first version of a bytecode program
after the conventional verification during the process          BC V 1 and a second version BC V 2 (Version
of its life cycle. In this process, bytecode passes             one transformed), a DIFF file. This DIFF file
verification process based especially on type veri-             will be applied to the on-card first version.
fication. The applications of update operations on-             We obtain a new version on-card. The goal
card is performed with insertion and suppression of             of our approach is to establish that the on-
instructions according to the DIFF file. Consequently,          card new version and BC V 2 are semantically
we obtain on-card, after the update process, a new              equivalent. At this level, the specifications of
bytecode that was not submitted to the conventional             both BC V 1 and BC V 2 are provided by
verification process. Our framework allows to:                  the programmer using existing specification
                                                                languages.
(i) Ensure the validity of update operations of the
      DIFF file according to the formal specification     (ii) The functional block: we define a functional
      of the Java Card virtual machine specification.           model for representing and manipulating
(ii) Guarantee that the application of the update               the Java Card bytecode. We implement an
      leads to a bytecode with the specification                automatic translator called functional reader
      that is conform to the intended specification             which takes a program written in bytecode
      (provided by the programmer).                             and produces a functional representation of it.
                                                                The application of the DIFF file is represented
The first point is ensured by the formalisation                 at this level as annotations of the functional
of the semantics of update operations. In the                   representation with expressions indicating the
second point, we aim to establish that given an                 place of the update operation and its nature
initial program P 1, its new version P 2 and a                  (addition of instructions, deletion . . . )
DIFF file ∆ containing the specification of the
                                                          (iii) The verification block: our goal is to verify
transformation derived from the differences between
                                                                 that the bytecode obtained by transformation
P 1 and P 2, the application of the DIFF file on-
                                                                 is equivalent to the one written by the program-
card on P 1 (noted App PATCH) leads to P 2′ .
                                                                 mer i.e., it satisfies the same specification. The
The two programs P 2 and P 2′ are verified to be
                                               ••



                                         Table 1: Rules for operational semantics


           M [pc]=pop                    M [pc]=new A,h′ =h[create(A,ref )]                    M [pc]=load x
                    

            M [pc]=store x                             M [pc]=if l                            M [pc]=if l,v̸=0
                     

         M [pc]=const a                   M [pc]=getf ield a f t,v=h[o.f ]                      M [pc]=neg
                

           M [pc]=binop,op∈{+,−,∗}                     M [pc]=putf ield A f t,h′ =h[o.f ←v]             M [pc]=goto l
              

                M [pc]=invokevirtual A l t ,
                      




                            Table 2: Rules for update operations (insertion of instructions)


Add inst goto L(i + 1)                  Add inst store x(i + 1)                       Add inst add(i + 1)
SDi+1 = SDi P C M AX + +                SDi+1 = SDi − 1 P C M AX + +                  SDi+1 = SDi − 1
Si+1 = Si Fi+1 = Fi                      Si = t.S0 Fi+1 = Fi [x ← t]                  Si = int.int.S0 ⇒
M2 =                                    Si+1 = S0                                     Si+1 = int.S0
Add inst(M 1, goto L, i + 1)            M 2 = Add inst(M 1, store x, i + 1)           M 2 = Add inst(M 1, add, i + 1)
i + 1, L ∈ DOM (BC)                     i + 1 ∈ DOM (BC) x ∈ V AR(BC)                 i + 1 ∈ DOM (BC) Fi+1 = Fi
      F,S,M 2,SD,i+1⊢BC                             F,S,M 2,SD,i+1⊢BC                           F,S,M 2,SD,i+1⊢BC


                                                                                          Add inst new A(i + 1)
Add inst pop (i + 1)                      Add inst putf ield(A, f, t)(i + 1)              SDi+1 = SDi + 1
SDi+1 = SDi − 1 Fi+1 = Fi                 SDi+1 = SDi − 2 Fi+1 = Fi                       Si+1 = A.Si Fi+1 = Fi
Si = t.S0 → Si+1 = S0                     Si = t.A.S0 ⇒ Si+1 = S0                         M2 =
M 2 = Add inst(M 1, pop, i + 1)           M2 =                                            Add inst(M 1, new A, i + 1)
P C M AX + +                              Add inst(M 1, putf ield(A, f, t), i + 1)        P C M AX + +
i + 1 ∈ DOM (BC)                          P C M AX + 3 i + 1 ∈ DOM (BC)                   i + 1 ∈ DOM (BC)
       F,S,M 2,SD,i+1⊢BC                              F,S,M 2,SD,i+1⊢BC                           F,S,M 2,SD,i+1⊢BC


                                                 Add inst load x(i + 1)                         Add inst if L(i + 1)
Add inst getf ield(A, f, t)(i + 1)               SDi+1 = SDi + 1                                SDi+1 = SDi
SDi+1 = SDi                                      P C M AX + +                                   P C M AX + +
Si = A.S0 ⇒ Si+1 = t.S0                          Si+1 = Fi [x].Si Fi+1 = Fi                     Si+1 = Si Fi+1 = Fi
M2 =                                             M2 =                                           M2 =
Add inst(M 1, getf ield(A, f, t), i + 1)         Add inst(M 1, load x, i + 1)                   Add inst(M 1, if L, i + 1)
P C M AX + 3 Fi+1 = Fi                           i + 1 ∈ DOM (BC) x ∈ V AR(BC)                  i + 1, L ∈ DOM (BC)
          F,S,M 2,SD,i+1⊢BC                                 F,S,M 2,SD,i+1⊢BC                       F,S,M 2,SD,i+1⊢BC


Add inst invokevirtuel(A, l, t)(i + 1)                 Add inst const a(i + 1)                 Add inst neg (i + 1)
SDi+1 = SDi − (card(dom(t)) + 1)                       SDi+1 = SDi + 1                         SDi+1 = SDi Fi+1 = Fi
Si+1 = tn1 .tn2 . . . tnn .S0 → Si+1 = S0              P C M AX + +                            Si = int.S0 = Si+1
M2 =                                                   Si+1 = int.Si Fi+1 = Fi                 M2 =
Add inst(M 1, invokevirtuel(A, l, t), i + 1)           M2 =                                    Add inst(M 1, negi + 1)
i + 1 ∈ DOM (BC) Fi+1 = Fi                             Add inst(M 1, const a, i + 1)           P C M AX + +
P C M AX + 3                                           i + 1 ∈ DOM (BC)                        i + 1 ∈ DOM (BC)
             F,S,M 2,SD,i+1⊢BC                                F,S,M 2,SD,i+1⊢BC                   F,S,M 2,SD,i+1⊢BC
                                     ••

                   Table 3: Rules for update operations (suppression of instructions)




Dlt inst goto L (i + 1)                             Dlt inst (store x (i + 1))
SDi = a →                                           SDi = a → SDi+1 = Ef f ects SD(a, M 2[i + 1])
SDi+1 = Ef f ects SD(a, M 2[i + 1])                 M 2 = Dlt inst(M 1, store x, i + 1)
M 2 = Dlt inst(M 1, goto L, i + 1)                  Si = t.S0 , Fi [x] = t →
(M 2)Si+1 = Ef f ects ST K(M 2[i + 1], Si )         (M 2)Si+1 Ef f ects ST K(M 2[i + 1], t.S0 )
(M 2)Fi+1 = Ef f ects F (M 2[i + 1], Fi )           (M 2)Fi+1 = Ef f ects F (M 2[i + 1], Fi )
i + 1, L ∈ DOM (BC) P C M AX − −                    i + 1 ∈ DOM (BC) P C M AX − −
             F,S,M 2,SD,i+1⊢BC                                       F,S,M 2,SD,i+1⊢BC


Dlt inst (add (i + 1))
M 2 = Dlt inst(M 1, add, i + 1)                     Dlt inst (pop (i + 1))
SDi = a →                                           SDi = a → SDi+1 = Ef f ects SD(a, M 2[i + 1])
SDi+1 = Ef f ects SD(a, M 2[i + 1])                 M 2 = Dlt inst(M 1, pop, i + 1)
Si = int.int.S0 →                                   Si = t.S0 →
(M 2)Si+1 = Ef f ects ST K(M 2[i + 1], Si )         (M 2)Si+1 = Ef f ects ST K(M 2[i + 1], t.S0 )
(M 2)Fi+1 = Ef f ects F (M 2[i + 1], Fi )           (M 2)Fi+1 = Ef f ects F (M 2[i + 1], Fi )
i + 1 ∈ DOM (BC) P C M AX − −                       i + 1 ∈ DOM (BC) P C M AX − −
             F,S,M 2,SD,i+1⊢BC                                       F,S,M 2,SD,i+1⊢BC


Dlt inst (putf ield(A, f, t) (i + 1))                 Dlt inst (getf ield(A, f, t) (i + 1))
SDi = a →                                             SDi = a →
SDi+1 = Ef f ects SD(a, M 2[i + 1])                   SDi+1 = Ef f ects SD(a, M 2[i + 1])
M 2 = Dlt inst(M 1, putif ield(A, f, t), i + 1)       M 2 = Dlt inst(M 1, getif ield(A, f, t), i + 1)
Si = A.t.S0 →                                         Si = A.S0 →
(M 2)Si+1 Ef f ects ST K(M 2[i + 1], Si )             (M 2)Si+1 Ef f ects ST K(M 2[i + 1], A.S0 )
(M 2)Fi+1 = Ef f ects F (M 2[i + 1], Fi )             (M 2)Fi+1 = Ef f ects F (M 2[i + 1], Fi )
i + 1 ∈ DOM (BC) P C M AX − −                         i + 1 ∈ DOM (BC) P C M AX − −
              F,S,M 2,SD,i+1⊢BC                                      F,S,M 2,SD,i+1⊢BC


Dlt inst new A (i + 1)                              Dlt inst if L (i + 1)
SDi = a →                                           SDi = a → SDi+1 = Ef f ects SD(a, M 2[i + 1])
SDi+1 = Ef f ects SD(a, M 2[i + 1])                 M 2 = Dlt inst(M 1, if L, i + 1)
M 2 = Dlt inst(M 1, new A, i + 1)                   Si = int.S0 →
(M 2)Si+1 = Ef f ects ST K(M 2[i + 1], Si )         (M 2)Si+1 = Ef f ects ST K(M 2[i + 1], Si )
(M 2)Fi+1 = Ef f ects F (M 2[i + 1], Fi )           (M 2)Fi+1 = Ef f ects F (M 2[i + 1], Fi )
i + 1 ∈ DOM (BC) P C M AX − −                       i + 1, L ∈ DOM (BC) P C M AX − −
             F,S,M 2,SD,i+1⊢BC                                       F,S,M 2,SD,i+1⊢BC


Dlt inst (neg (i + 1))
SDi = a →                                          Dlt inst (load x (i + 1))
SDi+1 = Ef f ects SD(a, M 2[i + 1])                SDi = a → SDi+1 = Ef f ects SD(a, M 2[i + 1])
M 2 = Dlt inst(M 1, neg, i + 1)                    M 2 = Dlt inst(M 1, load x, i + 1)
Si = int.S0 →                                      (M 1)Si+1 = t.S0 →
(M 2)Si+1 = Ef f ects ST K(M 2[i + 1], Si )        (M 2)Si+1 Ef f ects ST K(M 2[i + 1], S0 )
(M 2)Fi+1 = Ef f ects F (M 2[i + 1], Fi )          (M 2)Fi+1 = Ef f ects F (M 2[i + 1], Fi )
i + 1 ∈ DOM (BC) P C M AX − −                      i + 1 ∈ DOM (BC) P C M AX − −
             F,S,M 2,SD,i+1⊢BC                                      F,S,M 2,SD,i+1⊢BC


Dlt inst (const a (i + 1))
SDi = a →                                          Dlt inst (invokevirtuel(A, l, t) (i + 1))
SDi+1 = Ef f ects SD(a, M 2[i + 1])                SDi = a → SDi+1 = Ef f ects SD(a, M 2[i + 1])
M 2 = Dlt inst(M 1, const a, i + 1)                M 2 = Dlt inst(M 1, invokevirtuel(A, l, t), i + 1)
Si = S0 →                                          Si = tn1 .tn2 . . . tnn .S0 →
(M 2)Si+1 = Ef f ects ST K(M 2[i + 1], Si )        (M 2)Si+1 Ef f ects ST K(M 2[i + 1], Si )
(M 2)Fi+1 = Ef f ects F (M 2[i + 1], Fi )          (M 2)Fi+1 = Ef f ects F (M 2[i + 1], Fi )
i + 1 ∈ DOM (BC) P C M AX − −                      i + 1 ∈ DOM (BC) P C M AX − −
             F,S,M 2,SD,i+1⊢BC                                      F,S,M 2,SD,i+1⊢BC
                                            ••


     specification of the obtained bytecode in its
     functional representation with annotations is
     performed by a weakest precondition calculus
     that we define specially to deal with update
     operations. A verification condition generator
     gives then statements to be verified to estab-
     lish that the obtained specification matches
     the specification given by the programmer at
     the level one. A proof assistant is used to          Figure 4: Bytecode annotation with update instructions
     discharge verification conditions.

                                                         obtained by applying a compiler JML2BML and will
5. JML AND BML SPECIFICATIONS
                                                         be used by the next stages of the approach to
The starting point is a new version BC V 2 of            perform verification condition generation and ensure
un existing program BC V 1. First the programmer         the transformation correctness.
writes the new version with its specification in terms
of pre/post conditions. The specification language       6. ANNOTATION AND FUNCTIONAL
used is JML (Java Modeling Language).                    REPRESENTATION OF BYTECODE
JML (Burdy et al. (2005)) is a specification language    The DIFF file containing the update instructions
for Java/Java Card programs. It allows assertions        is calculated at bytecode level and then sent to
to be included in the source code, specifying for        perform the update on-card. In order to ensure that
example pre- and postconditions and invariants. JML      we send the right one, we model its application on
annotations are a special kind of Java comments:         an initial version of bytecode P1 as annotations.
they are preceded by / / @, or written between /*        The operation of annotating a bytecode with
@ and @* /.                                              expressions indicating where an update instruction
                                                         occurs and what is the operation involved can be
A simple method specifications is of the form:
                                                         defined recursively as an annotation function which
/*@ normal_behavior                                      transforms a program to an annotated program.
requires :  ;                              Annot(ε, P ) ≡ P
ensures :  ;                              Annot([U pdi |∆], P )     ≡       let    P′       =
@*/                                                      Add Annot Line(U pdi , P ) in Annot(∆, P ′ )

This specification means that if the precondition        The annotation of a program with an empty DIFF
(requires) holds at the beginning of a method            file (ε) is the program itself otherwise, the function
invocation, then the method terminates normally          iterates over the update operations (U pdi ) in the
and the postcondition (ensures) will hold at the         patch and adds a corresponding annotated line
end of the method. Constructs are defined to write       (Add Annot Line(U pdi , P )) to the program. Figure
assertion such as: \old, to denotes the old value of a   4 shows an annotated program obtained by the
variable,\result to denote the result of a method and    application of a DIFF file on an initial byte
the quantifiers, \f orall and \exists.                   code. The annotations are represented as special
                                                         commentaries. For example, Del 4 : deletes the
The DIFF file in the system EmbedDSU is created          instruction at program counter (pc) 4 and add isub
from the program’s bytecode. To ensure the               4, adds the instruction isub at pc 4.
correctness of the transformation, the verification
of the specification will be done at bytecode level.     In our framework, we use a functional representation
The language BML (Burdy et al. (2007)), allows           for both bytecode programs and annotation function.
to express specifications of bytecode programs. Its      Figure 5 shows a fragment of the formalisation
formalism is based on JML and the structures of          written in OCaml. We start by defining the data
specifications in both languages are very similar.       manipulated by the program (integers, objects and
                                                         variables, then, we formalise the instructions of the
At the transformation block, specifications for          sub language. The definition of an instruction is
both first version and second version are written        given by the name of a construct (representing the
in JML. Starting from a specified source code            name of the instruction) followed by its arguments.
{Pjml }codesource {Qjml }, with Pjml and Qjml rep-       For example, for the instruction new, we have
resenting respectively precondition and postcondi-       the construct New taking an Object as argument
tion of codesource , we obtain a specified bytecode      and the instruction putfield is represented by the
program {Pbml }codeBC {Qbml }. This information is       construct Putfield followed by a triple representing
                                                              the machine state where Heap represents the
                                                              contents of the heap, Frame represents the ex-
                                                              ecution state of the current Method and, Stack-
                                                              Frame is a list of frames corresponding to the
                                                              call stack. A frame contains the following ele-
                                                              ments : the stack of operands OperandStack and
                                                              the values of the local variables LocalV ar at the
                                                              program point P C of the method M ethod ( <
                                                              H, M ethod, P C, OperandStack, LocalV ar > ). The
                                                              definition of the update interpretation is based on the
                                                              notion of step.

                                                              Definition 1. Step The semantics of an instruction
                                                              (update instruction) is specified as a function step:
                                                              Bytecode P rog ∗ State ∗ Specif ication− > State ∗
                                                              StepN ame ∗ Specif ication that, given a bytecode
                                                              P, a state S and a specification SP, computes the
                                                              next state S’, the name of the next step and a new
                                                              specification.

Figure 5: An extract of functional modelisation of bytecode   Definition 2. Java bytecode update interpreter
                                                              We define now an update interpreter (U pd int) which
                                                              iterates over steps, take as parameters an annotated
the arguments: the class (Object) and the names of            program in its functional representation, an initial
the type of the field and its name as strings.                state and an initial specification and relies on
                                                              predicate calculus and update interpretation function
A bytecode line is defined as a number (representing          to produce a new state and a new specification. The
the program counter) with an instruction. The                 interpreter is defined as U pd int(BC, S) = (S ′ , Sp′ )
bytecode is represented as a list of bytecode                 with S = initial(BC, Sp) the function for defining an
lines. An annotated line is represented by the                initial state for the execution of the bytecode BC with
product of a bytecode line and a string representing          the initial specification Sp. The Code BC is given
the annotation. An annotated bytecode is a list               with its parameters and an initial heap. The result of
of annotated bytecode lines. The result of this               the interpreter is a state S ′ and a new specification
modelisation is used to derive specifications of              Sp′ .
updated programs.
                                                              Definition 3. Verified updated bytecode
7. VERIFICATION                                                  • Let P 1 and P 2 be the first and the new version
                                                                   of a program and P a patch,
Our approach for verification is based on the
fact that the transformation of a bytecode (of                   • let P 2′ = annot(P 1, P ) be the program
its semantics) implies the transformation of its                   obtained by annotation of P1 with P,
specification. In Hoare Logic (Hoare (1969)), a
program P 1 and its specification is represented by              • let f (P 2′ ) the functional representations of P 2′ ,
a triple {pre1}P 1{post1} where pre1 (post1) is the              • let spec(P 1) = (pre1, post1) the specification
precondition (postcondition) of the program P 1. A                 of P 1 and spec(P 2) = (pre2, post2) the
new version of this triple written off-card by the                 specification of P2,
programmer is {pre2}P 2{post2} (a target triple). The
DIFF file is performed with P1 and P2 and then sent           We say that P 2′ is a successfully verified update of
to the card to perform update operations, meaning,            P 1 if and only if: verif ication(spec(P 2), spec(P 2′ ))
obtaining a new bytecode and a new spacification.             succeeds where spec(P 2′ ) is obtained by predicate
Our goal is to establish that the target triple and the       transformation on f (P 2′ ) starting from post2.
obtained triple match.
                                                              7.2. Weakest precondition calculus
7.1. Interpretation of the update
                                                              In this section, we define a bytecode update
In order to formally define our update interpreter,           logic in terms of a weakest precondition calculus.
we need to define some notions. In this in-                   The proposed weakest precondition (WP) considers
terpretation, a state is modeled by a 3-tuple:<               that each (update) instruction has a precondition.
Heap, F rame, Stack − F rame > which represents               An instruction with its precondition is called an
                                               ••

                      Table 4: Defining rules for weakest precondition calculus for update operations

         wp( Add instr(pop,i)) = (shif t exp2 (@Ei ))
         wp( Add instr(store x,i)) = shif t exp2 (@Ei )(S(0)/x)
         wp(Add instr(if L,i)) = ((S(0) = 0) ⇒ shif t exp2 (EL )) ∧ ((S(0) ̸= 0) ⇒ shif t exp2 (@Ei ))
         wp(Add instr(load x,i)) = unshif t exp(shif t exp(@Ei ))(x/S(0))
         wp(Add instr(const a,i)) = unshif t exp(shif t exp(@Ei ))(a/S(0))
         wp(Add instr (new A,i)) = unshif t exp(shif t exp(@Ei [create(H, A)/S(0), A :: H/H])
         wp(Add instr(add,i) = (shif t exp2 (@Ei ))[(s(1) + S(0))/S(1)]
         wp(Add instr(neg,i) = (unshif t exp(@Ei ))[−S(0)/S(0)]
         wp(Add instr (getfield a f t,i) ) = shif t exp(@Ei [(val(S(0), (a, f )))/S(0)]) ∧ S(0) ̸= null
         wp(Add instr(putfield a f t,i)) = (shif t exp3 (@Ei ))[H((S(0), (a, f )) := S(1))/H] ∧ S(0) ̸= null
         wp(goto l1) = shif t exp(El1 )


instruction specification and is noted as: Ei : Ii               becomes the postcondition of the inserted instruction
where Ii is the instruction and the expression Ei                and thus the calculated precondition starts from
its specification. This notation expresses that the              this old postcondition (@Ei ). The function shif t exp
precondition Ei holds when the program pointer is                is used twice (shif t exp2 ) to express also the
at the program counter i. Table 4 shows the calculus             impact due to the insertion of the instruction on the
of the WP rules for the update operations (inserting             specifications of the following instructions.
instructions).
                                                                 The instructions new, putf ield and getf ield are heap
Functions and notations used. The functions                      manipulating instructions. The function create used
shif t exp and unshif t exp are used to express:                 in the instruction new A returns a new object of
the effect of pushing (popping) elements to (from)               type A in the heap H. This obtained heap (A :: H)
the stack S and the effect of shifting an expression             replaces the old heap. The function val used in the
regarding to the stack elements due to the insertion             definition of getfield to get the value of the field f of
of instructions. They are defined as follows:                    the class a from the address (top of the stack). This
                                                                 value is then pushed on the stack. In putf ield, the
shif t exp(Exp) = Exp[s(i + 1)/s(i) f orall i ∈ N ]              value of the field designated by the top of the stack
unshif t exp = shif t exp−1                                      is updated with the value at the second elements of
                                                                 the stack. The insertion of this instruction which pops
The elements of the stack are represented by                     two values implies three applications of shif t exp.
positive integers, the top stack is 0. The symbol @
is used to express the old specification associated              In order to establish semantical equivalence of a
to a position i: when we add an instruction at                   code written by the programmer and a program
position i, the program and the specification are                obtained by applying a DIFF file, we check the
shifted from i and then a new instruction is inserted.           equivalence of the weakest precondition of an
Its precondition is calculated with the specification            annotated program obtained by WP calculus and a
of the instruction that was at position i before the             precondition written by the programmer before DIFF
update.                                                          file is performed.

In the rules, for the instructions store x, load x,              7.3. Example
and pop, a precondition is obtained, as in Hoare’s
assignment (Hoare (1969)) by substituting the right-             In order to illustrate how the logic works, we take
hand side by the left-hand side in the postcondition.            the example of the function abs that returns the
The precondition of an instruction store x under a               absolute value of an integer taken as argument.
postcondition Ei+1 (the precondition of the following            This function is then transformed in order to get
instruction) is given by: shif t exp(Ei+1 )(S(0)/x)              the double of the result in the initial calculus: for
meaning that if the expression E holds after the                 an integer given as argument, the new function
execution of store x then it also holds for the top of           returns the abstract value multiplied by two (modified
the stack before storing it in x. The function shif t exp        abs). The specifications of the two functions are
is used to express that before the execution of the              respectively:
instruction, the top of the stack corresponding to the
instruction at i + 1 was at index 1.                             {p = P } abs {(P ≥ 0 → result = P ) ∧ (P < 0 →
                                                                 result = −P )}
Inserting an instruction, e.g. store x at line i means
that the precondition of the old instruction at i                {p = P } modif ied abs {(P ≥ 0 → result = 2 ∗ P ) ∧
                                                                 (P < 0 → result = −2 ∗ P )}
                                             ••


In the specification, P denotes the logical value at      The authors present a Hoare-style logic combined
the entry and result is the result of the function.       with instruction specification in term of precondition
Figure 6 shows the bytecode of the first version          for sequential bytecode. We adopted such instruction
(a) and the second version (b) of the described           specification in our logic for weakest precondition for
function. The part (c) of the figure shows the DIFF       update operation.
file generated from the two versions. The last part of
the figure (d) shows the bytecode of the function abs     In some studies, manipulating and analysing byte-
annotated with update instructions. We notice that        code requires its modelisation in flexible representa-
in this bytecode local variables are represented by       tions suitable to the manipulation required. In (Puder
integers: in load 1 for example, the number 1 means       and Lee (2009)), bytecode is represented by XML
the local variable 1. The same notation is applied to     trees in order to use the technologies supporting
other local variables.                                    XML to ease the injection and extraction of bytecode.
                                                          In (Albert and al. (2007)), bytecode is represented
In figure 7, The WP calculus is performed on              by clauses written in Prolog to perform verification of
the bytecode (without annotation) starting from the       bytecode programs. Generally, functional modelisa-
postcondition of the new version. The WP calculus         tion is used when the goal is to consider programs
is applied on the annotated bytecode as shown on          as mathematical models whose meaning is inde-
figure 8. The specification for the update instructions   pendent of runtime states. Therefore, it is possible
are in bold. This example shows that we obtain            to apply equational rewriting and reasoning to them
the same precondition {P = v0} which means                (Guodong (2010)) and use several proof systems
that at the beginning of the calculus the logical         that are built on or uses functional languages in
value P is in the first local variable of the function.   specifications.
This result expresses the equivalence of the two
bytecodes according to our definition of verified
updated program.                                          9. CONCLUSION

                                                          In this paper, we proposed an approach for
8. RELATED WORK                                           formalisation and verification of java bytecode
                                                          updated programs. Our approach relies on four
Several studies have been conducted in order              main concepts. We showed first how to use existing
to use formal semantics to prevent type errors            specification languages for Java and Java bytecode
in bytecode. Our work extends the formalism               programs to write specification and transform
presented in (Freund and Mitchell (1999)). This           them. Then, we defined a formal semantics which
work defined semantics and a type system to study         constitute a formal mean to establish the validity
object initialization in bytecode. The original idea      of update operations with regard to Java type
was developed in (Stata and Abadi (1999)) to              safety. We proposed a functional representation of
study bytecode subroutines. In (Freund and Mitchell       bytecode in order to model the application of update
(2003)), the authors extended the work (Freund            operations with the use of the notion of bytecode
and Mitchell (1999)) to bytecode subroutines, virtual     annotation. We presented a predicate transformation
method invocation and exceptions. On another              calculus based on weakest precondition for update
side, using predicate transformation to reason            operations to derive a specification for the annotated
about bytecode properties has been studied in             bytecode and showed how to establish the
(Grégoire,Sacchini and Sivan (2008)). The authors        correctness of the update.
presented a verification condition generator for
bytecode formalized in the Coq proof assistant and        The approach presented is implemented using
based on weakest precondition calculus. Another           the OCaml language. Our study started with
work using weakest precondition to generate               considering the system EmbedDSU but this is
verification conditions from an annotated bytecode        not restrictive, the framework proposed can be
is presented in (Burdy and Pavlova (2006), Burdy et       generalised to specification and verification of
al. (2007)).                                              updated programs written in languages that are
                                                          complied to bytecode. The use of the functional
Our work is close to ( Freund and Mitchell (1999))        language and representation eases its integration
in the sense of the use of static semantics to            with existing formal methods. Our immediate future
analyze bytecode. The specificity of our work is          work is to define WP calculus for instruction
the definition of semantics for updates. We use           suppression. We plan to define another predicate
predicate transformation to reason about bytecode         transformation calculus (strongest postcondition) for
properties using existing tools for specification and     update operation and the integration of our approach
proofs. Our bytecode logic for weakest precondtion        in an existing formal method supporting verification
calculus is inspired by (Bannwart and Müller (2005)).    condition generation for functional programs.
Figure 6: An example of an annotated bytecode (abs)




   Figure 7: WP calculus on the modified function




  Figure 8: WP calculus on an annotated bytecode
                                             ••


REFERENCES                                                Bannwart, F and Müller, P, (2005) A Program Logic
                                                            for Bytecode. In Electron. Notes Theor. Comput.
Freund, S. N and Mitchell, J. C, (1999) A type              Sci.vol 141, Elsevier Science Publishers B. V.,
  system for object initialization in the Java bytecode     2005, pp 255–273.
  language. In ACM Trans. Program. Lang. Syst., vol
  21, pp.1196–1250.                                       Common Criteria,http://www.commmoncriteria.org
                                                          McGachey, P, Hosking,A. L and Moss, J.E.B,
Grégoire, B, Sacchini, J. L and Sivan, R, (2008)
                                                           (2009) Pervasive Load-Time Transformation for
  Combining a verification condition generator for
                                                           Transparently Distributed Java. In Electron. Notes
  a bytecode language with static analyses. In
                                                           Theor. Comput. Sci., vol 253, Elsevier Science
  Proceedings of the 3rd conference on Trustworthy
                                                           Publishers B. V., pp.47–64.
  global computing, Springer-Verlag, pp.23–40.
                                                          Puder, P and Lee, J, (2009) Towards an XML-
Binder, W and Hulaas, J, (2005) Java Bytecode               based Bytecode Level Transformation Framework.
  Transformations for Efficient, Portable CPU Ac-           In Electron. Notes Theor. Comput. Sci.,vol 253,
  counting. In Electron. Notes Theor. Comput. Sci.,         Elsevier Science Publishers B. V., pp.97–111.
  Elsevier Science Publishers B. V. vol 141, pp.53–
  73.                                                     Boshernitsan, M and Graham,S. L, (2004) iXj: Inter-
                                                            active Source-to-source Transformations for Java.
Noubissi,A.C, Iguchi-Cartigny, J and Lanet,J. L,            In Companion to the 19th Annual ACM SIGPLAN
  (2011) Hot updates for Java based smart cards.            Conference on Object-oriented Programming Sys-
  In ICDE Workshops, pp.168-173.                            tems, Languages, and Applications, pp.212–213.
Burdy, L and Pavlova,M, (2006) Java bytecode              Guodong, L, (2010) Formal verification of programs
  specification and verification In SAC 2006,              and their transformations. PhD thesis, University
  pp.1835-1839.                                            of Utah, USA.
Burdy,L, Huisman, M and Pavlova,M, (2007)                 Lounas,R, Mezghiche, M and Lanet,J. L, (2012) To-
  Preliminary Design of BML: A Behavioral Interface         wards a General Framework for Formal Reasoning
  Specification Language for Java Bytecode In               about Java Bytecode Transformation In Proceed-
  FASE 2007, pp.215-229.                                    ings Fourth International Symposium on Symbolic
                                                            Computation in Software Science, pp.63–73.
Freund, S. N and Mitchell, J. C,(2003) A Type System
  for the Java Bytecode Language and Verifier. In J.      Noubissi,A. C, (2011) Mise á jour dynamique et
  Autom. Reasoning, vol 30, pp.271-321.                    sécurisée de composants systéme dans une carte
                                                           á puce. PhD thesis, University of Limoges, France,
Hoare,C. A. R, (1969) An Axiomatic Basis for               2011.
  Computer Programming. In Commun. ACM,
  vol 12, pp.576-580.                                     Albert, E, Gomez-Zamalloa, M, Hubert, L and
                                                            Puebla,G, (2007) Verification of Java Bytecode
Stata, R and Abadi, M, (1999) A Type System                 Using Analysis and Transformation of Logic Pro-
  for Java Bytecode Subroutine In ACM Trans.                grams . In Practical Aspects of Declarative Lan-
  Program. Lang. Syst., vol21, pp.90-137.                   guages,2007, Springer Berlin Heidelberg,pp.124-
                                                            139.
Dahm,M, (1999) Byte Code Engineering. InJava-
  Informations-Tage, pp.267-277.                          Neamtiu,I, Hicks,M, Stoyle, G and Oriol, M, (2006)
                                                           Practical Dynamic Software Updating for C.In
Sakamoto, T, Sekiguchi, T and Yonezawa, A, (2000)          ACM SIGPLAN Conference on Programming
  Bytecode Transformation for Portable Thread              Language Design and Implementation, pages
  Migration in Java. In ASA/MA, 2000, pp.16-28.            7283, 2006.
Bachrach, J and Playford, K, (2001) The Java              Gupta, D, Jalote P and Barua, G. A formal
  Syntactic Extender. In OOPSLA 2001, pp.31-42.            framework for online software version change.
                                                           Software Engineering, IEEE Transactions on, 22
Noubissi,A. C, Iguchi-Cartigny, J and Lanet, J.
                                                           (2):120131, 1996.
  L, (2010) Incremental Dynamic Update for
  Java-Based Smart Cards. In Fifth International          Orso,A, Rao, A and Harrold,M. J. A technique
  Conference on Systems, pp.110-113.                        for dynamic updating of Java Software. In ICSM,
                                                            2002.
Burdy,L, Cheon,Y, Cok, D. R, Ernst, M. D, Kiniry,J.
  R., Leavens,G. T, Leino, K. R. M, and Poll, E. An       Hlopko, M, Kurs,J, and Vrany, J. Towards a Runtime
  Overview of JML Tools and Applications . In Int. J.       Code Update in Java an exploration using
  Softw. Tools Technol. Transf., vol 7, pp. 212–232.        STX:LIBJAVA. In proceeding of Dateso 2013.