Formal model and implementation of the Java Card dynamic security policy

  • 格式:pdf
  • 大小:159.48 KB
  • 文档页数:14

July1999Gemplus Research LabTechnical Report SM-99-09Formal Model and Implementation of the Java Card Dynamic Security PolicyS TEPHANIE MOTRE Gemplus Research LabAvenue du Pic de Bertagne,13881Gemenos cedex.Formal Model and Implementation of the Java Card DynamicSecurity PolicyStéphanie MotréGemplus Research LaboratoryAvenue du Pic de Bertagne13881Gémenos CEDEXStephanie.Motre@IntroductionSecurity is one of the most important features in smart card technology and particularly with open smart cards(e.g.,Java Card).Due to the limited resources of the card,the main part of the security procedures of Java Card Virtual Machine(VM)[Lyn96],is located off card. Thus,several on-card solutions may be used to provide security on Java Card technology based devices.Gemplus Java on card Security is based on three separate processes.The Loader and Linker verify the content of a Converted Applet(CAP)file downloaded into the device,while performing authentication(optional)and reference resolution.These first two procedures may only guarantee static security properties,as they do not foresee applets behaviour at runtime.As a consequence,the Java Card Runtime Environment(JCRE) [Sun99a]imposes additional runtime security requirements,which result of specific additional features on the Java Card VM.The additional runtime checks are done by the applet firewall.This program is in charge of controlling the segregation between applets and the correct access to objects.It prevents non-authorised access to the fields and methods of class instances.Due to the fact that the applet may share objects in some situations(data or services exchanges),the applet firewall enforces object access policy on card.It grants applets permission to access objects,arrays contents or length.Memory integrity preserving is the starting point for modelling the Firewall functional requirements:each object on card is protected by the Firewall,according to its type.The Firewall is the last Java card VM defence against malicious code.Its role is to make sure that the execution of the byte code does not prejudice memory integrity.The first part of the document presents the properties to be fulfilled by the Java card dynamic security.The second and third parts are dedicated to the Firewall formal model,and its refinement using the B-Method[Abr96].The fourth part sets out the implementation of the formal model,and the last exposes the lessons learnt from this research.1Dynamic Security Policy Specification1.1Java Card SecurityJava Card is an open platform that enforces strong security procedures because of its vulnerability.This device is not dedicated to a single application:other applications can be loaded and installed into the card.The Java card VM has a single execution thread,but manages different execution contexts.Actually,the access policy,enforced by the Firewall,is based on the applet isolation need.Each application loaded on a Java Card is associated to a unique execution context.Thus,each application on card is securely isolated from the others, by the Firewall.Dynamically,no tests are performed to verify the correctness of the code currently being executed.The Java compiler and bytecode verifier have checked the code off card to assert the good use of Java semantics,and runtime stack.The Java Card standard does not specify anyloading policy:the Loader(loading mechanism of the Java Card)must not verify the source of applications loaded.Thus,the standard defines a secure loading chain:compiler,verifier,and loader.Figure1presents the different security mechanisms of the Java Card.Figure1-Java Card securityThe Java Card allows application downloading during the deployment phase.The Loader description furnished by the standard appears not to be sufficient to guarantee card security:a malicious application would be easily introduced into the card.Thus,the Gemplus Java Card Loader has been developed according to the Visa Open Platform(VOP)standard. Applications can be compiled,verified,and then loaded on card after card distribution:the Loader,prior the application download authenticates a certificate delivered by the application provider.Sun standard and VOP standard restrict the dynamic security of the Java Card to the Firewall.The access policy respect is the only point that has never been verified before runtime.1.2The FirewallThe SUN's Java Card JCRE[Sun99a]document provides a set of requirements.The on-card linker,the loader,and the Java Card VM contribute to fulfil these requirements.The Firewall performs a set of additional verifications to insure that the JCRE requirements are indeed respected and that memory integrity is preserved.The essential task of the on card Firewall is to make the execution of a Java byte code secured by preventing objects from illegal access outside Java Card packages.Some on-card applications may manage confidential data(purse applications for example)that will not be accessible from other applications.The goal of the Firewall is not to enforce the Java Card bytecode semantic rules defined by Java Card bytecode specification,but instead to make sure that the access rules of the Java Card Runtime Environment specification2.1are fulfilled.1.3Context ManagementTo enforce runtime Security,the JCRE uses the Firewall to prevent objects from being accessed illegally by other applets without respecting access rules.The context notionenforces access requirements.Indeed,each CAP file loaded on card is associated to a runtime context:-each on-card application is represented by an applet package,-a Java Card package defines a single runtime context,-all applets of a same package are associated to the same runtime context,-an applet can access every object of the same context,-JCRE entry points objects,and global arrays are owned by the JCRE,and can be accessed by any object of any context.As a consequence applets are securely isolated from other contexts.However,a safety mechanism of communication based on shared interfaces enables applets to share objects with applets of other packages[Sun99c].Figure2-Activity area of the Firewall access policyThe package isolation preserved by the Firewall is not completely impervious:a mechanism of inter-package communication exists.Shareable Interface(SI)objects are specific objects which methods may be accessed from outside its context.They are class instances that extend SI class(figure2).References to objects inside a package are resolved at linking when the CAP File is loaded on the card.But referring to an object that is not in the package is impossible:references to Shared Objects(SO)must be delivered by the JCRE because reference construction is forbidden.Data flow checks performed by the bytecode verifier guarantee that no reference is illegally built at runtime.Thus,the only way an applet would get a reference to a SO is secure.Actually,the JCRE delivers a reference to a SO only with the agreement of the owner of the object.-GetAppletShareableInterfaceObject is a JCRE entry point method that returns a reference to a SO or a null or an exception.The requested SO is referred by its owner and its SI type.The JCRE does not decide to allow or not the required access.It asks the SO owner(an applet)throughout another function.-GetShareableInterfaceObject is an applet method used by the JCRE to get a reference ofa SO.The SI type and the AID(Applet Identifier Data)of the requester are passed to theapplet in order to decide whether it wants to share this object with the requester.This decision is implementers free.2Firewall Modelling2.1B-MethodThe B Method is a formal method for software.It is a model-oriented approach to software construction.This method is based on the set theory and the first order logic.The basicconcept is the abstract machine,which is used to encapsulate the data describing the state of the system.The INVARIANT clause of an abstract machine developed with the B-language contains the whole static properties of the model variables.A model is proved when the initialisation of the entire set of variables establishes the invariant,and when each operation preserves it.Adding specification details refines the abstract machine.Several steps can be used before reaching the implementation level where the specification is detailed enough to generate code.The refinements and the implementation have other invariant,which express relations between the states of the different refinements.The proof process is a mean to check the coherence among the mathematical model,the abstract machine and the refinements.This way,it is possible to prove that the implementation is correct according to its specification.The tool AtelierB generates the proof obligations(PO) of the specification according to the mathematical model.A theorem prover is provided to discharge automatically the proof obligations and an interactive theorem prover allows the user to intervene in the proof.In this study,we use the B event driven method,successfully used is a previous study [Lan98].The main idea is to specify the model in a one-step fashion.Then,the model is refined by stretching the time progressively.At each level,new operations appear to refine the behaviour of the previous level.2.2Firewall formal modelThe Firewall modelling aims to:-provide a formal description of the security policy(or object access policy),as defined in JCRE specification,-formally demonstrate that the Firewall verifications of bytecodes are sufficient to fulfil the Security policy and to insure the memory integrity of the card,-provide a reference implementation of the Firewall.The entire on card VM has been modelled[Mot99]because the Firewall is not isolated on card.The memory architecture has been modelled in a first abstract machine which underlines the relations between the objects,their properties,and manages the VM registers.This machine is very important because it is the base of the VM and the Firewall.It will be more precisely explained in the next part of the document.The Firewall and the Java stack are two components of the VM working directly with the objects.The Firewall needs to access object properties to perform its checks,and the Java stack may contain information from card objects(references,field value...).Figure3-Formal model of the dynamic security policy of the Java CardWe decide to separate the Firewall and the byte code interpreter to give prominence to the specific function of each VM part involved in the byte code execution.The abstract machine of the interpreter manages the Firewall and the Java stack,throughout their operations.The Java Card API[Sun99b]document provides a complete specification of the interpreter.The source of any code execution is a command thrown to the card by the card reader (CAD).The JCRE waits for a command (APDU command)from the CAD when no code is running.The select command runs the process method of an applet,and then starts the execution stage of the VM.Figure 3shows the architecture of the formal model built.2.3Memory abstract modelEvery entity of Java Card is represented by variables in the B-language:the JCRE registers,the applets,their objects,fields,methods,context,and relations according to the access rules.Some JCRE registers are concrete variables of the object machine:"static"registers.Actually,those registers can not change during code execution:-the default applet:a register that contains the AID of the applet that will be automatically selected,but not processed,after a card power up (reset),-the selected applet:AID of the applet which is currently selected in the card,and that will process the APDU commands send throughout the JCRE by the CAD.The machine contains also "dynamic sets"which represent tables of the VM able to change during card life.The set of installed applets is a set of applet type objects contained in a larger set:applets loaded.When a new applet is installed (APDU command),the installed applets set grows.Concretely,an AID is added in the JCRE table for installed applets.This variable is concrete.Objects on card are all installed and well-defined objects contained in the memory of the card.Arrays,interfaces,installed applets,and JCRE entry points objects are objects on card.This set is abstract because it is a way to point out objects actually installed in the card among the set of all possible objects.The INVARIANT clause groups together every property relative to each variable.As an example,let us consider the property of applets selection:"Only installed applets can be selected by the CAD".The variables SelectedApplet and InstalledApplets are concrete variables:they are specific tables or register of the JCRE.They are modelled as follows:Figure 4-Example of INVARIANT clause.The operations contained by this machine aim to modify the objects state on card:-load a new package (application)on the card,-install an applet after its card load (this is a VOP specification),-set a new default applet,-card reset procedure,-object creation,-applet selection procedure.Abstractly,we modelled the operations considering their potential issues,according to the parameters values and the objects state.The operations as a whole have been refined only once in order to integrate their specifications.A last step in the object model would be thefinaltransition toward a model with no set(set of applets,set of arrays...).This final refinement step has been studied but not realised.2.4Access functions abstract modelThe runtime mechanism is concentrated in three machines:the interpreter,the Java stack and the Firewall.These models have been designed in the same way:around their status.When an exception is thrown during code execution,the status of the concerned machine indicates that an error occurs.The interpreter machine most important operation is treat_bytcode,which executes the current code.It also contains operations for reset mechanism and method process (initialisation of the interpreter to the process method of the selected applet).The stack machine manages the program counter(pc),but the interpreter needs it to get the current bytecode to treat.We decided to abstractly isolate each machine of the model.That way we were able to express the behaviour of each machine,separately.Each abstract machine contains the variables it should modify.The behaviour of the machine is described abstractly but closely to reality.Thus,a variable,current_pc,has been included in the interpreter machine to simulate the modifications involved by bytecode interpretation to the pc register.The pc is not the only variable managed abstractly by the interpreter.Actually,some bytecode may change the current object invoking a method,and a context switch may occur when the method to be invoked is not in the current context and is not static.The interpreter only keeps its status in the implementation because the other variables are identified to variables managed by the stack.A bytecode may also throw an exception if its request is not valid.Some evident cases can be related:access denied by the Firewall to an object,not enough parameters on the stack,or not enough space left to put the result.As a consequence,the behaviour of the interpreter is connected to the firewall and the Java stack.Figure5describes the relations between these three machines.Figure5-Abstract behaviour of the bytecode interpreterEach operation of the Firewall corresponds to a specific object access.Objects to be accessed may be arrays,interface methods,object methods,or object properties.We decided to model each access type by a specific operation.The Firewall relies on current context information, and not on current object information.Actually,the Firewall isolates packages on card and applies its rules according to the accessed object type.The specification of an interface access (bytecode invoke_interface)establishes that:"access to a method of an interface is allowed if -the current object is an object of the JCRE,or-the interface is a shareable interface,or-the interface is in the current context."Thus the abstract model of an interface access is based on three abstract variables:access_JCRE_interface ,access_shareable_interface ,access_package_interface .Figure 6describes the interface access abstract model.Figure 6-Abstract model of the Firewall for interface access policyAbstractly,an access request is represented by a relation between a context and an object.All the relations will be specified in a future refinement .3Model refinementThe refinement process of the whole model considers different mechanisms.The refinement step adds information in the model.The abstract machine of objects has been refined this way.Some machines manipulate variables of other machines included in the first refinement step.Those machines are then able to specify their behaviour calling other machines operations.These two procedures are developed in the first subsection.The second subsection of the model refinement part presents the Java stack model using B event driven.The refinement of the Firewall machine is proposed in the last subsection,and provides an example for abstract variables disappearing.3.1Machines relations introductionOur model is based on the isolation of each abstract machine of the model.Each machine manages abstractly the variables able to be modified by one of its operation.The first refinement of each machine of the model aims to connect the whole model as described Figure3.The INCLUDE clause has been used to connect the machines because it allows operation access as well as variableaccess.Each variable that has been added in an abstract machine (e.g.,the pc in the interpreter machine)is identified to its source.Thus,the variables in the whole model are unique and the model is entirely linked.The refinement of the operations,which simulates the evolution of abstract variables,introduces the required operations invocation.As an example,consider the JCRE machine,which represents the APDU commands treatment.The JCRE specification imposes that:-an APDU command can only be received when no code is being executed,-select command is performed by the JCRE,which sends back a Status Word (SW)to inform the CAD of the command result;-non select commands are sent to the process method of the currently selected applet;if there is no currently selected applet,the JCRE sends an error SW to the CAD,The JCRE machine must abstractly manage variables meaning that the interpreter is processing code or not (Runtime variable),and the VM has a currently selected applet or not (SelectedApplet variable).The SelectedApplet variable is identified to the VM register contained in the object machine,and Runtime is compared with Processing which indicates the interpreter activity.Figure 7presents this machine connection by variable identification.Figure 7-Link between the machines of the abstract model throughout their variablesThe link between interpreter,Java stack and Firewall machines is re-enforced by their status variables.Actually,when the code execution provokes an error within the Firewall (access denied to an object)or the Java stack,the Interpreter must take it into account.Thus,the three-status machine has been linked in the Interpreter machine Invariant clause:The demonstration of the proof obligations generated proves the correctness of the variables behaviour.3.2B Event Driven integrationWhen the interpreter initialises the stack,or when a method is invoked,a frame is pushed on the Java stack.A frame is a stack structure that contains a buffer for method return procedure,a buffer of method local variables and parameters,and an operand stack.Each method is associated to a frame,and the maximum size of its different components is fixed.The issue of a push frame procedure depends on the stack state when it is performed.The expected parameters must be on the previous operand stack.There must be enough space left on the Java Stack to allocate the entire frame.The push frame operation has been separated into four operations dedicated to each possible state of the stack:-PushFrame1is called when the expected parameters are not on the operandstack,-PushFrame2is called when the parameters are on the operand stack,but the space left in the Java stack is not sufficient to allocate the frame,-PushFrame3is dedicated to the normal case:it is possible to push the frame of the method to be executed,and it is the first one,-PushFrame4is similar to PushFrame3apart from the fact that it is not the first frame to be pushed,The pre-conditions of these operations(PRE clause)are limited to operation parameter checks.Actually,the SELECT clause is used to determine the case corresponding to the stack state.The interpreter machine is the only machine of the model designed to access stack operations. This machine does not call directly operations of the stack machine:a stack"spooler"machine has been included in the formal model to choose the operation corresponding to the current stack state.The checks realised by the stack spooler could have been integrated to the interpreter machine,but it would have been heavy and the operations would have lost clarity. Such a machine appears to be very important when some machines of a formal model are developed using B event driven.Actually,an abstract machine must have the same number of operations as its refinements:an operation developed in traditional B can not be split in operations.3.3Firewall refinementThe refinement of the Firewall abstract machine reveals the relation between the Firewall and the memory throughout the Objects machine.The dynamic checks specification provides the concrete values of the abstract access variables.Thus,the access variables are clearly identified owing to Objects machine variables as it is presented in Figure8.Figure8–Refinement process for the interface access policyThe JCRE manages a table that associates its execution context to each object installed in memory.This relation has been modelled by the function GetObjectContext.It is used to represent the abstract relation access_package_interface.This access imposes the couple formed by the current context and the interface fetched to be correctly typed,and linked by the relation“the interface is owned by the current context”.This case is represented by (GetObjectContext-1∧ValidContexts∗Interfaces).The specification of the checks performed by the Firewall to verify interface accesses has been entirely considered to get the most concrete model.The specification of the security policy is the base of the invariant clause of the Firewall,and the API specification is the base of the operation clause of the interpreter.Thus,the byte code execution formal model completes theJava card requirements.4Formal model implementation4.1The Interpreter implementationThe interpreter has been implemented to design the behaviour of byte code treatment.It should have been built using the B event driven because of the number of different byte codes supported.We preferred to bring together the byte codes owing to their properties:some byte codes only modify the stack,others require an access to a field,an interface,or an array.The loop has not been integrated to the model.The loop is the driving force of the JCRE but is not necessary to model the dynamic security policy of the Java card.Moreover,loops generate numerous PO,which are not automatically proved.The interpreter implementation relies on stack and Firewall operations to determine the evolution of its status.The interpreter does not manipulate directly the stack to get a byte code parameter for example.The stack machine has been completed with operations modelling “get parameter from stack”actions,or a stack modifications after computation.The access object checks are performed by Firewall operations.The behaviour of the interpreter described in the figure 8has been respected in its implementation.Each byte code treatment does not exactly follow this scheme:some byte codes does not necessitate any object access or does not require any parameter from stack.Figure 9–Implementation of the getfield byte code treatmentThe getfield byte code is used to get a field value and to push it on the current operand stack.The reference of the field class is popped from the operand stack of the current frame,and its access from the current context must be verified by the Firewall.Each step of the scheme is present in the implemented treatment of the getfield byte code.The figure 9gives an example of this byte codeinterpretation.4.2The Firewall implementationThe Firewall implementation is the most important part of machine refinement.The variables used by the machine must be concrete and their behaviour throughout operation process must be close to reality.The Firewall implementation manages only one variable,which is its status.The objects concerned by the verification are passed as operation parameters,and their properties are accessed owing to Objects machine operations.The Firewall implementation requires the introduction of assessor functions in the Objects machine.Actually,an implementation can not access directly variables of another machine, and the checks performed by its operations necessitate object information,such as object type. Abstractly an access to an object within a package has been identified to the relation access_package_object,which value is:Access_package_object=ObjectContext-1∩Contexts×ObjectsOnCardThe following operations have been added to the abstract Objects machine: -bool←is_object_context(obj,ctx)which returns TRUE if the context of obj is ctx.-bool←is_valid_context(ctx)which returns TRUE if ctx is an efficient context on card.-bool←is_valid_object(obj)which returns TRUE if obj is an object installed in the card. Figure10gives an implementation of the interface access operation.Figure10–Interface access implementationThis tool does not perform any check regarding variables implementation.The BO-Checker permits to verify that every variable of a machine is correctly defined to be implemented. Variables declarations are checked in the Invariant clause of the machine,and in its operations.The implementation operations have been developed the most closely to the last refinement operations of the abstract machine.Thus,most proof obligations(PO)generated are easy to prove.For example,the interactive prover generates the following PO for the interface access operation:Those PO are proved using the false hypothesis rule,which means that a local hypothesis of the PO is false.The proof must be based on the other local hypothesis,and can be proved in few instructions.4.3The ResultsThe first model built for the dynamic security policy was resumed in a single machine.This model was complicated and too large.The number of variables and invariant properties included in the model has generated too much PO to be easily proved and refined.We decided to separate the model into different machines representing the different elements of the Java card VM.The number of PO generated by each machine is exposed in the following table:Type checkBO check Obvious POPO unproved%Contexts machines ok ok 1000100CAD-JCRE ok ok 900100Implementation ok ok 58210100Interpreterok ok 3550100Implementation ok ok 5762289061Firewall ok ok 11730100Refinement ok ok 213170100Implementation ok ok 206800100Stackok ok 14841191588StackSpooler ok ok 11730100refinementokok3431151687The stack has been developed in three times:the abstract model,which has been refined twice,gave the usable version of the stack.Actually,the stack size and stack status variables are important variables,which are introduced along refinement procedures.The machine used in the model is the last refinement of the stack.The PO generated by the interactive prover have been verified but not completely proved,because the stack is the not a crucial point in the dynamic security policy modelling.ConclusionThe interactive proof process can be very costly.It is important to reduce this phase of software development to be productive.Development process must be as short as possible to reduce the time between the specification and the product.Our model has been strongly redesigned in order to obtain the highest rate of automatically proved PO.Several points should be observed and particularly avoid:-use of sets defined in extension,-existential quantificators,-lambda expressions,-sequence data structures,It is of common sense to use simple machines and expression writing e.g.,use a function instead of relational application with restriction.B event driven is a power full theory.The major drawback is the gluing invariant that can be constituted of difficult expressions.The formal model of the dynamic security policy has been completely proved.It has to be included in a complete Interpreter model,to be closer to reality.。