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.
During their life cycle, programs need to be
updated in order to alter their semantics, perform
optimizations or add features. Several techniques
were presented for this purpose in literature, for
example, (
In some cases, the transformation occurs at runtime.
The update is then said to be dynamic (Dynamic
Software Update: DSU). In (
This large interest of Java bytecode transformation and its use in many critical applications raise the question of its correctness. In fact, a transformation may introduce an error which may alter the bytecode leading the system to an unexpected state. Besides, in some cases, the update is critical (e.g. EmbedDSU) in such a way that an attacker can take advantage of an incorrect update. In these applications where security issues are involved the update must pass some certification procedure for example Common Criteria (Common Criteria (2015)). For a certain certification level one has to provide a formal proof of the security mechanism implemented. A formal way to specify transformations and verify their correctness is then necessary.
Formal methods offer rigourous means in specifying
software properties and establishing the correctness
of programs regarding their formal specifications.
In this work, we present an approach for formal
verification of bytecode update. We focus on Java
bytecode and the system presented in (
In this work, we propose to formally verify that the obtained bytecode is semantically equivalent to the one written by the programmer and used to perform the DIFF file. Our approach is based on the following contributions: the definition of a new weakest precondition calculus as the base of the verification process, a formal interpretation of the semantics of the update operations, a functional representation of bytecode programs and bytecode annotation. The choice of functional representation is motivated by our interest in capturing the behavior of the initial bytecode and the updated version and the mature existing tools for formal reasoning about functional programming languages.
This paper is organized as follows: in section 2 we give an overview of embedDSU. Section 3 introduces the language and the formal semantics of the updates. In section 4, we present an overview of our approach in its steps. We present the specification languages is section 5. In section 6, we give our functional modelisation of Java bytecode and annotations. We propose a predicate calculus for update operations in section 7 and give the notion of a correct update. This section ends with an example to show how the logic works. We discuss related work in section 8 and conclude in section 9.
EmbedDSU (
This paper addresses the first part: bytecode update at the method level. The types of updates that may occur are: adding, modifying or suppressing bytecode instructions, changing the signatures of a method or modifying local variables. These updates are contained in the DIFF file which indicates the 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 deleted and the instruction isub is added at the same place provided by the program counter.
For the definition of the semantics, we extend the
formalism used by Freund and Mitchell (
Instruction ::= jpop jif L jstore x jload x jnew A jbinop jneg jconst a jinvokevirtual A l t jgoto L jgetf ield A f t jputf ield A f t jreturn U pd Instr ::= Add Inst Instruction pc jDlt Inst Instruction pc jM od Inst Instruction instruction pc In this language, the instruction pop extracts the top of the stack and const a pushes a constant a on the top of the stack. The instruction load x pushes the value in the variable x on the top of the stack whereas the instruction store x pops the top of the stack and stores it in the variable x. The instruction if L jumps to L if the top of the stack is not zero else it performs the following instruction. Goto L jumps to L. The instruction N ew A allocates a new object of type A and pushes it on the top of the stack. The instructions manipulating fields are : getf ield A f t and putf ield A f t. Getfield reads the field f , which has the type t of the object of class A whose reference is on the top of the stack and pushes its value on the top of the stack and putfield modifies the field f with the value popped form the stack. The instruction invokevirtual invokes the method l of signature t and the class A. The instruction Binop is used to gather arithmetic binary operations: add, mult and sub. The instruction neg negates the top of the stack and return is for method return.
Update instructions are respectively: adding an instruction, deleting instruction and modifying an instruction. We indicate the place of the update operation with pc.
We model the interpretation of the instructions
of the bytecode instructions using the standard
framework for operational semantics (
The rules for the instructions of our language are represented in table 1. The instruction new A creates a new object of class A, thereby modifying the current heap. A reference to the new object is pushed onto the stack. store x pops a value from the evaluation stack and assigns it to a variable,f is modified accordingly. load x put the value of x on the top of the stack. The binop operation which pops two values from the stack, performs the binary operation, and pushes the result. if l has two rules; wether it jumps to the indicated line or performs the following instruction according to the value of the top of stack. The instruction putfield updates the heap with the new value of the field of the object which is on the top of the stack. The new value is popped from the second element of the stack. invokevirtual invokes the method l on an object reference and parameters on the stack and replaces these values by the return value v of the invoked method after its execution.
We propose a static semantics to express the effects
of update instructions on a configuration of the
bytecode. This semantics was introduced in our
initial paper (
F1 = F⊤; SD1 = 0 S1 = "; M1 = Map(BC) 8i 2 DOM(BC); F; S; SD; M; i ⊢ BC
F;S;M;SD⊢BC The first two lines of the judgement represent the initial configuration: all variables are mapped to the value top (default initial value), stack depth is zero, the sequence of types is initially empty (") and M1 is the mapping of the initial bytecode. The last line expresses that each instruction (update instruction) in the bytecode is well typed. This is ensured by the rules given in tables 2 and 3. For illustration, the insertion of the instruction new A at line i + 1 allows us to obtain a new configuration if the stack depth is incremented, local variables are not affected and in the stack, the type A is inserted. In the instruction invokevirtual the function dom represents the domain of the invoked function (types of its arguments) and the function card represents the number of elements in the domain. The rule expresses that these arguments are popped from the stack of type and then the result is pushed. For the insertion of an instruction representing an arithmetic binary operation Binop, we show the rule of the instruction add: this operation pops two elements (integers) from the stack and then pushes the result. mult and sub have analogous explanations by writing the right operation. In the rules, the mapping M2 is the result of operations on M1. The operations which represent manipulations on bytecode are: range and shift. The operation range extracts from a mapping M1 a part M2 included between line n and line m. The second operation shifts a part from a mapping between n and m for p positions which is determined by the number of added instructions.
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 are shifted and their numbers change. It is then necessary to update goto and if instructions accordingly. These modifications keep the structure of the bytecode coherent. In the rules for instructions suppression (table 3), Ef f ect ST K, Ef f ect F and Ef f ects SD are used to express the effects of an instruction of the stack and the local variables and stack depth. They are used to readjust these elements to the instruction at (i + 1) in the new bytecode after the suppression. The notation (M 2)F (Respectively, (M 2)S) is used to express F (Respectively, S) in the mapping M 2. We notice that in this formalisation, a modification is considered as a suppression followed by an insertion.
The mechanism of EmbedDSU implies the modification of the bytecode of a running application on-card after the conventional verification during the process of its life cycle. In this process, bytecode passes verification process based especially on type verification. The applications of update operations oncard is performed with insertion and suppression of instructions according to the DIFF file. Consequently, we obtain on-card, after the update process, a new bytecode that was not submitted to the conventional verification process. Our framework allows to: (i) Ensure the validity of update operations of the DIFF file according to the formal specification of the Java Card virtual machine specification. (ii) Guarantee that the application of the update leads to a bytecode with the specification that is conform to the intended specification (provided by the programmer).
The first point is ensured by the formalisation of the semantics of update operations. In the second point, we aim to establish that given an initial program P 1, its new version P 2 and a DIFF file ∆ containing the specification of the transformation derived from the differences between P 1 and P 2, the application of the DIFF file oncard on P 1 (noted App PATCH) leads to P 2′. The two programs P 2 and P 2′ are verified to be semantically equivalent. This equivalence ensures that the system indeed implemented the desired transformation. This problem can be expressed equationally by: 8P 1; P 2; P 2′; ∆ = DIF F (P 1; P 2); P 2′ App P AT CH(P 1; ∆) ) P 2 P 2′ = This raises two major issues: 1- how to model the application of the DIFF file on an existing program? and 2- how to express the equivalence which guarantees the correctness of the update? We present the overview of our approach for transformation verification. Figure 3 represents an overview of our approach which is split in three parts: (i) The transformation block: in this stage, we obtain from a first version of a bytecode program BC V 1 and a second version BC V 2 (Version one transformed), a DIFF file. This DIFF file will be applied to the on-card first version. We obtain a new version on-card. The goal of our approach is to establish that the oncard new version and BC V 2 are semantically equivalent. At this level, the specifications of both BC V 1 and BC V 2 are provided by the programmer using existing specification languages. (ii) The functional block: we define a functional model for representing and manipulating the Java Card bytecode. We implement an automatic translator called functional reader which takes a program written in bytecode and produces a functional representation of it. The application of the DIFF file is represented at this level as annotations of the functional representation with expressions indicating the place of the update operation and its nature (addition of instructions, deletion . . . ) (iii) The verification block: our goal is to verify that the bytecode obtained by transformation is equivalent to the one written by the programmer i.e., it satisfies the same specification. The 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 establish that the obtained specification matches the specification given by the programmer at the level one. A proof assistant is used to discharge verification conditions.
The starting point is a new version BC V 2 of un existing program BC V 1. First the programmer writes the new version with its specification in terms of pre/post conditions. The specification language used is JML (Java Modeling Language).
JML (Burdy et al. (2005)) is a specification language for Java/Java Card programs. It allows assertions to be included in the source code, specifying for example pre- and postconditions and invariants. JML annotations are a special kind of Java comments: they are preceded by / / @, or written between /* @ and @* /.
A simple method specifications is of the form: This specification means that if the precondition (requires) holds at the beginning of a method invocation, then the method terminates normally and the postcondition (ensures) will hold at the end of the method. Constructs are defined to write assertion such as: nold, to denotes the old value of a variable,nresult to denote the result of a method and the quantifiers, nforall and nexists.
The DIFF file in the system EmbedDSU is created
from the program’s bytecode. To ensure the
correctness of the transformation, the verification
of the specification will be done at bytecode level.
The language BML (
The DIFF file containing the update instructions is calculated at bytecode level and then sent to perform the update on-card. In order to ensure that we send the right one, we model its application on an initial version of bytecode P1 as annotations. The operation of annotating a bytecode with expressions indicating where an update instruction occurs and what is the operation involved can be defined recursively as an annotation function which transforms a program to an annotated program. Annot("; P ) P Annot([Updij∆]; P ) let P ′ = Add Annot Line(Updi; P ) in Annot(∆; P ′) The annotation of a program with an empty DIFF file (") is the program itself otherwise, the function iterates over the update operations (Updi) in the patch and adds a corresponding annotated line (Add Annot Line(Updi; P )) to the program. Figure 4 shows an annotated program obtained by the application of a DIFF file on an initial byte code. The annotations are represented as special commentaries. For example, Del 4 : deletes the instruction at program counter (pc) 4 and add isub 4, adds the instruction isub at pc 4.
In our framework, we use a functional representation for both bytecode programs and annotation function. Figure 5 shows a fragment of the formalisation written in OCaml. We start by defining the data manipulated by the program (integers, objects and variables, then, we formalise the instructions of the sub language. The definition of an instruction is given by the name of a construct (representing the name of the instruction) followed by its arguments. For example, for the instruction new, we have the construct New taking an Object as argument and the instruction putfield is represented by the construct Putfield followed by a triple representing the arguments: the class (Object ) and the names of the type of the field and its name as strings. A bytecode line is defined as a number (representing the program counter) with an instruction. The bytecode is represented as a list of bytecode lines. An annotated line is represented by the product of a bytecode line and a string representing the annotation. An annotated bytecode is a list of annotated bytecode lines. The result of this modelisation is used to derive specifications of updated programs.
Our approach for verification is based on the
fact that the transformation of a bytecode (of
its semantics) implies the transformation of its
specification. In Hoare Logic (
In order to formally define our update interpreter, we need to define some notions. In this interpretation, a state is modeled by a 3-tuple:< Heap; F rame; Stack F rame > which represents the machine state where Heap represents the contents of the heap, Frame represents the execution state of the current Method and, StackFrame is a list of frames corresponding to the call stack. A frame contains the following elements : 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.
Definition 2. Java bytecode update interpreter We define now an update interpreter (U pd int) which iterates over steps, take as parameters an annotated program in its functional representation, an initial state and an initial specification and relies on predicate calculus and update interpretation function to produce a new state and a new specification. The interpreter is defined as U pd int(BC; S) = (S′; Sp′) with S = initial(BC; Sp) the function for defining an initial state for the execution of the bytecode BC with the initial specification Sp. The Code BC is given with its parameters and an initial heap. The result of the interpreter is a state S′ and a new specification Sp′.
Definition 3. Verified updated bytecode
Let P 1 and P 2 be the first and the new version of a program and P a patch, let P 2′ = annot(P 1; P ) be the program obtained by annotation of P1 with P, let f (P 2′) the functional representations of P 2′, let spec(P 1) = (pre1; post1) the specification of P 1 and spec(P 2) = (pre2; post2) the specification of P2, We say that P 2′ is a successfully verified update of P 1 if and only if: verif ication(spec(P 2); spec(P 2′)) succeeds where spec(P 2′) is obtained by predicate transformation on f (P 2′) starting from post2.
In this section, we define a bytecode update logic in terms of a weakest precondition calculus.
The proposed weakest precondition (WP) considers that each (update) instruction has a precondition.
An instruction with its precondition is called an 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 where Ii is the instruction and the expression Ei its specification. This notation expresses that the precondition Ei holds when the program pointer is at the program counter i. Table 4 shows the calculus of the WP rules for the update operations (inserting instructions).
Functions and notations used. The functions shif t exp and unshif t exp are used to express: the effect of pushing (popping) elements to (from) the stack S and the effect of shifting an expression regarding to the stack elements due to the insertion of instructions. They are defined as follows: shif t exp(Exp) = Exp[s(i + 1)=s(i) f orall i 2 N ] unshif t exp = shif t exp 1 The elements of the stack are represented by positive integers, the top stack is 0. The symbol @ is used to express the old specification associated to a position i: when we add an instruction at position i, the program and the specification are shifted from i and then a new instruction is inserted.
Its precondition is calculated with the specification of the instruction that was at position i before the update.
In the rules, for the instructions store x, load x,
and pop, a precondition is obtained, as in Hoare’s
assignment (
The precondition of an instruction store x under a postcondition Ei+1 (the precondition of the following instruction) is given by: shif t exp(Ei+1)(S(0)=x) meaning that if the expression E holds after the execution of store x then it also holds for the top of the stack before storing it in x. The function shif t exp is used to express that before the execution of the instruction, the top of the stack corresponding to the instruction at i + 1 was at index 1.
Inserting an instruction, e.g. store x at line i means that the precondition of the old instruction at i becomes the postcondition of the inserted instruction and thus the calculated precondition starts from this old postcondition (@Ei). The function shif t exp is used twice (shif t exp2) to express also the impact due to the insertion of the instruction on the specifications of the following instructions.
The instructions new, putf ield and getf ield are heap manipulating instructions. The function create used in the instruction new A returns a new object of type A in the heap H. This obtained heap (A :: H) replaces the old heap. The function val used in the definition of getfield to get the value of the field f of the class a from the address (top of the stack). This value is then pushed on the stack. In putf ield, the value of the field designated by the top of the stack is updated with the value at the second elements of the stack. The insertion of this instruction which pops two values implies three applications of shif t exp.
In order to establish semantical equivalence of a code written by the programmer and a program obtained by applying a DIFF file, we check the equivalence of the weakest precondition of an annotated program obtained by WP calculus and a precondition written by the programmer before DIFF file is performed.
In order to illustrate how the logic works, we take the example of the function abs that returns the absolute value of an integer taken as argument. This function is then transformed in order to get the double of the result in the initial calculus: for an integer given as argument, the new function returns the abstract value multiplied by two (modified abs). The specifications of the two functions are respectively:
0 ! result = P ) ^ (P < 0 ! fp = P g abs f(P result = P )g fp = P g modif ied abs f(P (P < 0 ! result = 2 P )g 0 ! result = 2
P ) ^ In the specification, P denotes the logical value at the entry and result is the result of the function. Figure 6 shows the bytecode of the first version (a) and the second version (b) of the described function. The part (c) of the figure shows the DIFF file generated from the two versions. The last part of the figure (d) shows the bytecode of the function abs annotated with update instructions. We notice that in this bytecode local variables are represented by integers: in load 1 for example, the number 1 means the local variable 1. The same notation is applied to other local variables.
In figure 7, The WP calculus is performed on the bytecode (without annotation) starting from the postcondition of the new version. The WP calculus is applied on the annotated bytecode as shown on figure 8. The specification for the update instructions are in bold. This example shows that we obtain the same precondition fP = v0g which means that at the beginning of the calculus the logical value P is in the first local variable of the function. This result expresses the equivalence of the two bytecodes according to our definition of verified updated program.
Several studies have been conducted in order
to use formal semantics to prevent type errors
in bytecode. Our work extends the formalism
presented in (
Our work is close to (
In some studies, manipulating and analysing
bytecode requires its modelisation in flexible
representations suitable to the manipulation required. In (
In this paper, we proposed an approach for formalisation and verification of java bytecode updated programs. Our approach relies on four main concepts. We showed first how to use existing specification languages for Java and Java bytecode programs to write specification and transform them. Then, we defined a formal semantics which constitute a formal mean to establish the validity of update operations with regard to Java type safety. We proposed a functional representation of bytecode in order to model the application of update operations with the use of the notion of bytecode annotation. We presented a predicate transformation calculus based on weakest precondition for update operations to derive a specification for the annotated bytecode and showed how to establish the correctness of the update.
The approach presented is implemented using the OCaml language. Our study started with considering the system EmbedDSU but this is not restrictive, the framework proposed can be generalised to specification and verification of updated programs written in languages that are complied to bytecode. The use of the functional language and representation eases its integration with existing formal methods. Our immediate future work is to define WP calculus for instruction suppression. We plan to define another predicate transformation calculus (strongest postcondition) for update operation and the integration of our approach in an existing formal method supporting verification condition generation for functional programs.
Common Criteria,http://www.commmoncriteria.org