CN100462890C - Control method of smart card security environment - Google Patents

Abstract

The invention discloses a method for controlling the security environment of a smart card. An application program downloaded to a smart card is compiled and converted to generate a byte code sequence of a Java card virtual machine instruction set, and the byte code sequence is generated by the Java card virtual machine. Operation; The Java card virtual machine has a virtual machine in the card and a virtual machine outside the card, and the virtual machine outside the card realizes converting the compiled file to generate a CAP file; the virtual machine in the card realizes executing the bytes in the CAP file code sequence; in the control of the security environment in the card, at first the byte code sequence output by the converter of the virtual machine outside the card is subjected to type demarcation to obtain the first check type and the second check type; then use check The rule performs security verification on the verification type. The smart card security environment control method of the present invention, on the basis of Java card internal and external virtual machine structure, designs and realizes the elliptic curve digital signature and the generation method of the code certificate outside the card and the security verification of the byte code sequence on the card. test.

Description

The control method of smart card safety environment

Technical field

The present invention relates to a kind of method that smart card safety environment is controlled, specifically, be meant a kind of control method of security context management system of Java smart card.

Background technology

Along with the widespread use of Java smart card, for the also progressively expansion of research of Java smart card techniques.How providing a secured computing environment by the Java smart card, this comprises many-sided problems such as safety assurance of code safety verification, downloading process.

The Java smart card techniques is the transplanting of Java Virtual Machine technology to the limited resources equipment platform.The Applet of Java smart card generates the bytecode program of virtual machine instructions collection through compiling and conversion back.These bytecodes are gone up virtual machine by card again and are moved.The early stage running technology of Java Virtual Machine mainly is to explain execution mechanism, and being about to bytecode is that corresponding local run time version moves by interpretive program translation, and it is suitable for using in the resource less equipment.Then, in order to improve the execution speed of bytecode, local code execution, on-the-flier compiler and running technologies such as jit compiling execution, HotSpot technology and the execution of direct specialized hardware structure have been proposed to be compiled as again in succession.Improved speed significantly though be compiled as the method for local code, influenced the security mechanism and the portability of Java language to a certain extent, this in the application of IC cards that high security requires obviously and be not suitable for.On-the-flier compiler, jit compiling technology and HotSpot technology are when operation bytecode to be compiled as local code, the storage resources when this needs a large amount of operations, and this is not feasible in the smart card that has only 2K left and right sides RAM usually yet.

For a secured computing environment is provided by the Java smart card, must solve the application firewall mechanism in code safety verification, the running environment, many-sided problems such as safety assurance of downloading process.Applet in the Java smart card generates the byte code instruction that Java smart card virtual machine can be discerned through compiling and conversion back, then downloads on the smart card by read write line again.Move in order to prevent that malice Applet from downloading on the Java card, must carry out the security verification the byte code instruction that generates.This mainly comprise prevent to occur in the Applet operational process stack overflow, illegal jump instruction and illegal type conversion as: integer is converted to conversion between object reference, incompatible object reference etc.This process must in conjunction with the characteristics of Java card virtual machine, adopt the outer method that generates verification in the code card book card of card to carry out on the basis to the description of Java card instruction type system form.

Summary of the invention

The management method that the purpose of this invention is to provide a kind of smart card safety environment, this management method is in order to provide the computing environment of a safety to the smart card platform under the limited computational resource environment, in the Java card card, outside the card on the basis of virtual machine structure, design and Implement the method for digital signature of elliptic curve, blocked the method for formation of outer code certificate (CodeCertificate) and the safety check method that card is gone up bytecode.

The control method of a kind of smart card safety environment of the present invention, described smart card includes the smart card hardware system and relevant nation method collection, Java card virtual machine, Java card running environment, Java card class libraries and the Java card application management assembly of hardware system formed, be downloaded to the application program process compiling in the smart card and change the byte code sequence that the back generates Java card virtual machine instructions collection, described byte code sequence moves by the Java card virtual machine; Described Java card virtual machine has virtual machine and the outer virtual machine of card in the card, blocks outer virtual machine and realizes the file after the compiling is changed, and generates the CAP file; Virtual machine realizes carrying out the described byte code sequence in the CAP file in the card; In card, at first will carry out type by the described byte code sequence that the converter of virtual machine outside the card is exported in the control of security context and demarcate, obtain the first verification type and the second verification type; Adopt the verification rule that described verification type is carried out safety check then.

The control method of described smart card safety environment, its type are demarcated and are comprised the first verification type and the second verification type.Verification rule with respect to the verification type has first verification rule and the second verification rule.

Advantage of the present invention: (one) has accelerated the speed of type checking, because avoided the type inference of intersection of instruction branch and iterate repeatedly.(2) reduced requirement to storage resources.Because the code certificate is a read message, can be stored among the bigger EEPROM of card inner capacities, after finishing, verification can delete.Thereby avoided in RAM, storing the pilot process that a large amount of need carry out the type inference of read-write operation.(3) owing to increased check part in the card,, avoided the outer verification of card to adopt encrypted signature mechanism existing one-point safety failure problem (signature key leakage) so improved the security of system.

Description of drawings

Fig. 1 is the inner structure synoptic diagram of Java smart card.

Fig. 2 is the structured flowchart of Java smart card virtual machine.

Fig. 3 is based on the bytecode safety check structure of proof-carrying mechanism.

Fig. 4 is the process flow diagram of bytecode safety check.

Fig. 5 is a Java Card type paritially ordered set Haas structural drawing.

Embodiment

The present invention is described in further detail below in conjunction with accompanying drawing.

Applet in the Java smart card (application program) generates the byte code instruction that Java smart card virtual machine can be discerned through compiling and conversion back, then downloads on the smart card by read write line again.Move in order to prevent that malice Applet from downloading on the Java card, must carry out the security verification the byte code instruction that generates.

The control method of a kind of smart card safety environment of the present invention, described smart card includes the smart card hardware system and relevant nation method collection, Java card virtual machine, Java card running environment, Java card class libraries and the Java card application management assembly of hardware system formed, be downloaded to the application program process compiling in the smart card and change the byte code sequence that the back generates Java card virtual machine instructions collection, described byte code sequence moves by the Java card virtual machine; Described Java card virtual machine has virtual machine and the outer virtual machine of card in the card, blocks outer virtual machine and realizes the file after the compiling is changed, and generates the CAP file; Virtual machine realizes carrying out the described byte code sequence in the CAP file in the card; In card, at first will carry out type by the described byte code sequence that the converter of virtual machine outside the card is exported in the control of security context and demarcate, obtain the first verification type and the second verification type; Adopt the verification rule that described verification type is carried out safety check then.Obtain the first verification type and the second verification type according to the type of byte code sequence is demarcated, first verification rule and the second verification rule are arranged for the verification rule of verification type.

The first verification type among the present invention is for realizing the structuring verification of the download component in the described CAP file; The second verification type is for realizing the type checking of the byte code sequence that the outer virtual machine of described card is exported.The first verification rule, download component in the described first verification type is carried out digital signature of elliptic curve, contain the digital signature information based on elliptic curve mechanism in the download component behind the described signature, the structuring checker in the intelligent card will be verified described digital signature information; The second verification rule is to the byte code sequence safe checking method of the employing of the byte code sequence in the described second verification type based on proof-carrying mechanism.

In the present invention, the bytecode safety check on the Java card can be divided into two processes: first process is the structuring checking procedure of download component, i.e. the first verification type.Second type checking process that process is a bytecode, the i.e. second verification type.

For the first verification type procedure, mainly be integrality and the consistance that is used for the verification download component.In order to guarantee the safety of downloading process, taked assembly is carried out the method for digital signature of elliptic curve among the present invention, in download component, contain digital signature information based on elliptic curve mechanism, the structuring checker can be verified this signing messages on the card, to prevent distorting assembly in the downloading process.In addition, the first verification type also comprises for each length component, form, component and defines conforming inspection, to guarantee the correctness of modular construction.

Because limited computational resource (2K RAM) in the smart card, therefore on present hardware platform, can't finish whole bytecode safety check processes, especially the type inference on the type partial ordering set calculates, therefore we in conjunction with in the Java intelligent card, the design feature of the outer virtual machine of card, taked the bytecode safety check algorithm based on proof-carrying mechanism of being used widely on the embedded device.Promptly outside card, generate the code certificate (Certificate) that is used to verification use in the card, download to virtual machine in the card together with bytecode as customizable component.The bytecode type checking device of virtual machine uses certificate to carry out the verification of second type as supplementary in the card, to accelerate the verification speed of virtual machine in the whole card.

JCVM program P is defined as the set { m of method ₁, m ₂... m _n.M wherein _iFor the unique method corresponding to each method is quoted.We use H to represent heap among the JCVM, wherein are used to deposit instance object, so H can be expressed as the mapping that instance object refers to the instance object storage organization, promptly

Wherein the objref representative object is quoted, fieldToken representative object territory, context representative object context.Local variable area in the Java stack architexture is defined as

And definition

Equal L, except wherein k is mapped to val.We are defined as tabulation S={val with the operand stack in the Java stack architexture ₀, val ₁..., val _N-1, and represent value val is pressed among the stack S with S+val.It is wide that element in local variable and the operand stack is a word (width of short type).Use J represents the Java stack among the JCVM.The frame of storing among the J be expressed as set of properties (context, L, S, rpc), wherein context represents current execution context, L represents local variable area, S represents operand stack, rpc represents that current method carries out the return address after finishing.We with running status be expressed as R=(bc, pc, J, L, S, H).Wherein bc represents current abnormality processing state, and it only contains two value throw and notThrow, and expression has been dished out unusually and do not dished out unusual respectively.The execution of program P can be expressed as the conversion of a series of running status R.

In addition, definition is used for the type information of type inference system, and it is defined as follows:

Class type cls=... the class type

Interface type interface=... interface type

Be cited as void type Null=null reference

Reference type ref=cls|interface|Null

Fundamental type prim=byte|short|boolean

Byte arrays type byteArray=byte or Bolean number set type

Short array type shortArray=short array type

Bolean number set type booleanArray=Bolean number set type

Number of references set type refArray=number of references set type

Fundamental type array type primArray=byteArray|shortArray|booleanArray

Array type array=primArray|refArray

ReturnAddress type returnAddress=return address type

Unavailable type unusable

Simultaneously, Java smart card byte code instruction set of types close the relation that defined reflexive a, antisymmetry, transmission≤: for α, $\mathrm{\β}\∈\left\{\stackrel{\‾}{{\mathrm{cls}}_n}\right\}$ If, α≤β, then α has expanded (extends) β.If $\mathrm{\α}\∈\left\{\stackrel{\‾}{{\mathrm{array}}_n}\right\},$ β is object class, then α≤β.If β is unusable, then α≤β.Then under the definition of≤relation, JavaCard language form set has constituted a paritially ordered set, and its Hasse diagram structure as shown in Figure 5.Numeral among the figure under the type is the coding of respective type, and this coding rule is mainly used in the speed of quickening computing on the paritially ordered set.In the type inference system, and the least upper bound LUB that frequent need calculating is two types (α, β).Under this coding rule, the computing of least upper bound can be exchanged into respective type coding with (

) operation.

In order to represent the formalization standard of byte code instruction effectively, we have introduced the definition of some auxiliary types:

The interface type set $\mathrm{int\; ers}=\left\{\stackrel{\‾}{{\mathrm{int\; erface}}_n}\right\}(n>0)$

Void type void

Data type ty=ref|prim

Data type or void type trOrVoid=ty|void

The object type raw=unin of no initializtion (pc, cls) | init (pc, cls)

Quote or array type refOrArray=ref|array

Quote or no initializtion object type refOrRaw=ref|raw

Quote, array or no initializtion object type

refOrAyyayOrRaw＝ref|raw|array

Quote, no initializtion object, return address type

refOrRawOrAds＝ref|raw|returnAddress

Quote, array, no initializtion object, return address type

refOrArrayOrRawOrAds＝ref|raw|returnAddress

Available types usuable=ty|raw|returnAddress

Any type any=usuable|unusable

A main task of bytecode safety check algorithm infers (when compiling) exactly thereby the runtime data type in local variable area and the operand stack guarantees that instruction can not used wrong data type when operation.The formalized description that for this reason at first provides the type list LT of local variable area is

Wherein max_local is the number of local variable in the current method.And definition

Equal LT, except wherein k is mapped to any.In addition, to count the stack type table be ST=[usable to defining operation ₀, usable ₁..., usable _Top], if use max_stack represents the maximum length of operand stack in the current method, then index top＜max_local.In order to make up the type inference system, the Status Type when we will move is defined as that П=(Contour), wherein Contour is a set for LT, ST.And will concern≤definition expand in the Status Type set in when operation:

If

If following formula is set up $\stackrel{\‾}{{\mathrm{any}}_{\max \_\mathrm{local}-1}\≤{\mathrm{any}}_{\max \_\mathrm{local}-1}\′},$ LT≤LT ' then.

If $\mathrm{ST}=\left[\stackrel{\‾}{{\mathrm{usable}}_n}\right],$ $\mathrm{ST}\′=\left[\stackrel{\‾}{{\mathrm{usable}\′}_n}\right],$ If following formula is set up $\stackrel{\‾}{{\mathrm{usable}}_n\≤{{\mathrm{usable}}^{,}}_n},$ ST≤ST ' then.

If П=(ST, LT, Contour), П '=(ST ', LT ', Contour '), if following condition is set up ST≤ST ', LT≤LT ', $\mathrm{Contour}\⊆{\mathrm{Contour}}^{,},$ П≤П ' then.

П≤П ' means for all instructions that can be applicable to Status Type П ' and all is applicable to Status Type П.

For the type inference system, Status Type П when we use pc ⊥ П to be illustrated in the compiling that pc place, address has.Because the Status Type at place, pc address not only depends on instruction itself, but also depends on the instruction execution path that arrives the pc place, promptly can have a plurality of Status Types for a pc address, so we uses pc ⊥ _≤П represents a kind of Status Type wherein, and this expression pc place has the instruction that can be applicable to Status Type П ' all to be applicable to Status Type П.

Before introducing the bytecode safety check algorithm based on proof-carrying mechanism in the present invention, we at first introduce traditional bytecode checking algorithm.Usually, the type checking device adopts data-flow analysis (Data FlowAnalysis) method to carry out bytecode security verification in the card.The whole analytical process is that unit carries out with single method, is equivalent to an abstract interpretation device on the type aspect.The type information of method porch is provided by the entrained certificate of bytecode, and uses these information to come local variable area's type at initialization function entrance place.For every in method instruction, zone bit " Changed " is set, when a new method verification began, having only the zone bit of article one instruction was 1.Next enter the major cycle process of data-flow analysis:

Step 1: find a zone bit and be 1 byte code instruction, and to put zone bit be O.If there is no zone bit is 1 instruction, and then the method checking procedure successfully finishes, and withdraws from the major cycle process.

Step 2: the typing rule (defining in a last joint) according to present instruction executes instruction, if present instruction can not be satisfied typing rule, then failure is carried out in instruction, and the major cycle process is withdrawed from the failure of method checking procedure.

Step 3: determine the subsequent instructions of present instruction, can be following arbitrary instruction:

If a. present instruction is non-jump instruction, link order and the exceptional instructions of dishing out, then next bar for present instruction instructs.If exceeded the instruction address space of current method, then failure is carried out in instruction, and the major cycle process is withdrawed from the failure of method checking procedure.

If b. present instruction is jump instruction, then be the byte code instruction at jump instruction destination address place.

C. the pairing abnormality processing handle of present instruction.

Step 4: the type state after merging present instruction execution finishes is in subsequent instructions:

If the not accessed mistake of subsequent instructions is a. then carried out present instruction type state after finishing as the preceding continuous type state of subsequent instructions, the zone bit of the continuous instruction of postpone is 1.

If the accessed mistake of subsequent instructions b. then merges the preceding continuous type state of current type state and existing subsequent instructions, if type state changes, then the zone bit of the continuous instruction of postpone is 1.

C. the process of type information merging is the process of asking two type LUB, for operand stack, can not have the unusable type after the merging, and the operand stack that merges must have identical height.Otherwise the major cycle process is withdrawed from the failure of method checking procedure.

D. we consider separately for the subprocess that calls by jsr (Subroutine), and more detailed discussion is arranged hereinafter.

Step 5: jump to step 1.

Because calling of subprocess is relatively complicated, the problem that exists many execution routes to arrive simultaneously, and can exist in the problem of storing different types of data in the same local variable and can not carry out the type merging.Therefore, for the processing of descriptor process correctly, in the method for the Java card developing instrument that reference Sun provides, the present invention adopts and introduced Contour in the type inference system, and it is defined as follows:

pc⊥П[ST，LT，Contour]

When in subprocess, carrying out type inference, the type merging is not carried out in instruction with different Contour, promptly be independent of each other between the type information from the instruction of different execution routes, and can after subprocess finishes, correctly bring subsequent instructions the type information in different paths.

If above-mentioned major cycle process successfully finishes, represent that then the bytecode of current method has passed through the security verification, otherwise expression verification failure.If it is that safety is available that methods whole in the current bag, are then represented current bag all by verification, otherwise refusal is carried out the program in the current bag.

As seen, the 4th step wherein must be calculated according to the type inference that the rule among the 4.c is carried out on the type partial ordering set in above-mentioned major cycle checking procedure, and if the change of type information has taken place, must carry out 4.b and carry out iterating of a new round.This has all proposed higher requirement for storage resources and execution speed, therefore, for fear of this topic, based on the bytecode safety check algorithm of proof-carrying mechanism the cross type information at place, address of program branches is judged, if occurrence type is inferred process (asking the LUB of two type informations), then at first generate this information by blocking outer checking procedure, be stored in the code certificate (Certificate), and with certificate as customization assembly (Custom component), download on the smart card together with other assemblies.For conserve storage, only storage need be carried out type inference accordingly and the element information of change and the element information of method porch have taken place in certificate, and the data structure definition of certificate is as follows:

Wherein pc is the address that crosses (or method entry address) of program branches, and LT is used for storing the change type information (or local variable type information of method inlet) of local variable area, and ST is used for the change type information of store operands stack.Therefore, the 4th step in the checking procedure is rewritten as:

4.a: if the not accessed mistake of subsequent instructions and have the pc address of subsequent instructions in certificate is then carried out present instruction the type П after finishing _cWith the type П in the certificate _δCompare, if П _c≤ П _δ, then adopt П _δAs the type state after merging, the zone bit of the continuous instruction of postpone is 1.Otherwise the major cycle process is withdrawed from the verification failure.If the not accessed mistake of subsequent instructions and do not have the pc address of subsequent instructions in certificate is then carried out present instruction type state after finishing as the preceding continuous type state of subsequent instructions, the zone bit of the continuous instruction of postpone is 1.

4.b: if the accessed mistake of subsequent instructions is then carried out present instruction the type П after finishing _cType П with subsequent instructions pc place in the certificate _δCompare, if П _c≤ П _δ, jump to step 5.Otherwise the major cycle process is withdrawed from the verification failure.

4.c: this step cancellation.

4.d: this step is constant.

This algorithm has three following advantages:

(1) accelerated the speed of type checking, because avoided the type inference of intersection of instruction branch and iterate repeatedly.

(2) reduced requirement to storage resources.Because the code certificate is a read message, can be stored among the bigger EEPROM of card inner capacities, after finishing, verification can delete.Thereby avoided in RAM, storing the pilot process that a large amount of need carry out the type inference of read-write operation.

(3) owing to increased check part in the card,, avoided the outer verification of card to adopt encrypted signature mechanism existing one-point safety failure problem (signature key leakage) so improved the security of system.

Claims (4)

1. the control method of a smart card safety environment, described smart card includes smart card hardware system and the relevant nation method collection of hardware system, it is characterized in that: also include Java card virtual machine, Java card running environment, Java card class libraries and Java card application management assembly and form, be downloaded to the application program process compiling in the smart card and change the byte code sequence that the back generates Java card virtual machine instructions collection, described byte code sequence moves by the Java card virtual machine; Described Java card virtual machine has virtual machine and the outer virtual machine of card in the card, blocks outer virtual machine and realizes the file after the compiling is changed, and generates the CAP file; Virtual machine realizes carrying out the described byte code sequence in the CAP file in the card; In card, at first will carry out type by the described byte code sequence that the converter of virtual machine outside the card is exported in the control of security context and demarcate, obtain the first verification type and the second verification type; Adopt the verification rule that described verification type is carried out safety check then; Described verification rule has first verification rule and the second verification rule;

The first verification type is for realizing the structuring verification of the download component in the described CAP file;

The second verification type is for realizing the type checking of the byte code sequence that the outer virtual machine of described card is exported;

The first verification rule, download component in the described first verification type is carried out digital signature of elliptic curve, contain the digital signature information based on elliptic curve mechanism in the download component behind the described signature, the structuring checker in the intelligent card will be verified described digital signature information;

The second verification rule is to the byte code sequence safe checking method of the employing of the byte code sequence in the described second verification type based on proof-carrying mechanism.

2. the control method of smart card safety environment according to claim 1, it is characterized in that: in the second verification rule, be that the cross element information at address place of program branches is judged according to bytecode safe checking method based on proof-carrying mechanism to the described second verification type, the type inference of described smart card is blocked outer verification generate the outer check information of described card, and be stored in the code certificate; Described code certificate is formulated to the customization assembly, and described customization assembly and described download component are downloaded on the smart card in the lump.

3. the control method of smart card safety environment according to claim 2, it is characterized in that: the major cycle process based on data-flow analysis in the bytecode safe checking method of proof-carrying mechanism is:

Step 1: find a zone bit and be 1 byte code instruction, and to put zone bit be 0; If there is no zone bit is 1 instruction, and then the method checking procedure successfully finishes, and withdraws from the major cycle process;

Step 2: the typing rule according to present instruction executes instruction, if present instruction can not be satisfied typing rule, then failure is carried out in instruction, and the major cycle process is withdrawed from the failure of method checking procedure;

Step 3: the subsequent instructions of determining present instruction;

Step 4: the type state after merging present instruction execution finishes is in subsequent instructions;

Step 5: jump to step 1.

4. the control method of smart card safety environment according to claim 2 is characterized in that: the outer check information of the described card of storing in the described code certificate is to carry out the cross element information at place, address of element information after described type inference changes and described program branches.

Images