User Manual
Contents
1. General Environment Java Card SDK JC_ HOME Show Method s Names C java_card_kit 2 2 Java Home JAVA HOME C Program Files Javalre6 _ Verbose debug EEPROM image 1 2 Figure 19 Preference dialogs General tab 1 Environment tab 2 3 2 The component browser The CAP file and the Export files are represented in an expandable tree struc ture that allows the user to select nodes and view leaf values After a CAP file has been loaded the root of the tree automatically takes the name of the loaded CAP file An example is shown in Figure 20 Component airfrance cap is expanded into the following subcomponents header_component directory_component applet_component import_component constant_pool_component class_component method_component static_field_component reference_location_component export_component and descriptor_component The header_component is split into various subcomponents Among them the subcomponent this_package contains the AID of the Cap file 16 File Edit Tools Help CEJ airfrance Of airfrance cap GJ header_component D tag 1 size 19 D minor_version 1 D major_version 2 lie flags 6 ACC_APPLET ACC_EXPORT J this_package D minor_version 0 major_version 1 AID_length 9 D AID A0 0 0 0 62 3 1 D 1 com gemplus pacap airfrance CI directory_component C applet_component C import_component C constant_pool_component c class_component2. c 2002 2011 Department of Information Engineering University of Pisa Ita APPLET LOADED EXPORT FILES LOADED Figure 5 Ready to analyze a CAP file 2 3 Setting the parameters for the analysis The verification process starts by clicking on the Analyze button The setting of parameters for the analysis follows three main steps Step 1 Configuring packages names 1 The JCSI Analysis Wizard window is prompted Figure 6 to allow the user to set the number of packages that are already installed on card The CAP files for these packages are not required 2 Through the Package Names Editor window Figure 7 the user can choose the names for the packages These names are used as security levels po Pn by default At the end of this step the user clicks on the Next button Step 2 Configuring the Ambient file 1 The Analysis Setup Loader window is prompted Figure 8 to al low the user to choose whether to use the default Ambient file Use Default Ambient File option or to load the Ambient file from a previously saved configuration Load Custom Ambient File op tion In the latter case a browser window is opened to select the file 2 The Ambient File Editor window is prompted Figure 9 to allow the user to view and customize the selected Ambient file The Am bient file is organized in four sections Imported Methods Internal Methods Exported Methods and Heap Section For methods the window shows
3. C method_component cJ static_field_component C reference _location_component C export_component o c descriptor_component c pacapinterfaces exp c rentacar exp modified l Figure 20 The component browser 3 3 The description window The description window displays general multi line information on the se lected CAP file The following procedure displays the bytecode representation of a method Referring to Figure 20 with a double click expand the node method component then go to the Method_info node and expand it For each method a node will be shown to represent the root of a subtree containing the method s information To show the complete bytecode of the method expand the bytecode attribute of the method i e the node labeled with the first bytecode instruction As an example Figure 21 shows the bytecode of method method_254 whose length is 38 Instruction are numbered following the program counter value For Invoke instructions the token is also displayed References 1 Chen Z 2000 Java Card Technology for Smart Cards Architecture and Programmer s Guide Addison Wesley Longman Publishing Co Inc 2000 2 Java Card Platform Specification Sun Microsystem http java sun com products javacard 17 File Edit Tools Help CJ airfrance airfrance cap C header_component directory_component C applet_component J import_component C constant_pool_comp
4. the method s name together with information on the package that implements the method _name and the package that imports the method Aname 3 The user can either select a method from a Method section or an object from the Heap Section e The View Selected button shows the signature of the selected method or the security level of the selected object For methods the security levels of arguments return value calling environ ment are shown The security policy is also shown within angled brackets Figure 10 e g airfrance e The Edit Selected button allows the user to modify the secu rity levels and the security policy of methods Figure 11 or the security levels of objects Figure 12 At the end of this step the user clicks on the Next button Step 3 Confirming Analysis Setup The Analysis Setup window is prompted Figure 13 showing the Am bient file The user can set the following Save Ambient file To save the Ambient file for future utilization Fig ure 14 File View Tools Help Open Analyze x Details es D Ep fe f Package mes 7 aom D gd g New name for p0 tund Applet under analysis default p0 airfrance purse Packages already installed on card Packages already installed on card po p1 Number of packages a Progress Status Step 1 Configure Package Names lt lt Back Figure 7 Choosing the names for packages already i
5. DU V _airfrance airfrance airfrance airfrance airfrance lt Imported methods gt airfrance internal_class_15 lt init B S B V _purse airfrance airfrance airfrance airfrance airfrance airfrance lt airfrance airfrance internal_class_15 lt init B S B V _rentacar airfrance airfrance airfrance airfrance airfrance airfrance lt airfra javacard framework Applet lt init V _airfrance airfrance airfrance airfrance lt airfrance gt javacard framework Applet register V _airfrance airfrance airfrance airfrance lt airfrance gt javacard framework APDU getBuffer B _ airfrance airfrance airfrance airfrance airfrance lt airfrance gt javacard framework Applet selectingApplet Z _airfrance airfrance airfrance airfrance airfrance lt airfrance gt Analysis Complete Enable Log Disable Log Figure 16 Analysis completion 13 2 5 Viewing the details of the analysis Click on the Details button of the Java Card Information Flow Verifier 1 2 main window The Analysis Details window will pop up showing the results of the analysis Figure 17 In this window View Log Click this button to view the Log file For each method the window shows Verified if the method satisfies the security policy Failed if the method violates the security policy Report Click this button to view detailed information about the method signature reason of the failure byte
6. Java Card Secure Information flow tool JCSI Version 1 2 April 2012 User Manual Marco Avvenuti Cinzia Bernardeschi Nicoletta De Francesco Paolo Masci Department of Information Engineering University of Pisa Italy Contents 1 Introduction 2 JCSI 2 GUF CSCI GION 2 dsc My ee es ee Sarde a Ee Ree ee a E A 2 2 Loading the CAP file and the Export files 2 3 Setting the parameters for the analysis 2 4 Performing the analysis esse NN M Gee ee OR Ka 2 5 Viewing the details of the analysis 3 The DeCAP tool uli NICE D a RS Pin na Dr tie ne 3 2 The component browser 4224 55 964 644 4 25 3 3 The description window 1 Introduction A Java Card applet is a smart card application written in the Java programming language according to a set of conventions ISO 7816 that regulate programs running in small footprint devices Java Card applets are compiled by the standard Java compiler 1 An off card component the Converter takes the compiler s output and performs checking optimization name resolution and linking A compact representation of the applet code is saved in the CAP Converted APplet file CAP files are the loading units in Java Card They include the necessary information to install and execute applets in the Java Card Runtime Environ ment JCRE 2 CAP files are very similar to class files Nevertheless while a large number of tools to anal
7. code Analysis Details x View Log method_38 V _airfrance rentacar The method is safe Method name method_554 Ljavacard framework AID B Ljavacard framework Shareable _airfrance purse Analysis result Fails at 1 program point return level is airfrance purse rentacar max airfrance purse Method body 0 aload_1 1 getstatic_a 21 4 sconst_0 5 getstatic_a 21 8 arraylength 9 s2b 10 invokevirtual 22 13 ifeq 22 Af sleoad oO T Figure 17 Details of the analysis 14 3 The DeCAP tool DeCAP is a CAP file disassembler and visualizer tool The tool simplifies byte code inspection and analysis by resolving information coded in tokens and show ing it in a mnemonic format The graphical user interface of the tool reports all the information stored in binary CAP and export files DeCAP Tool File Edit Tools Help 1 a france AP C Users cinzia Documents JAVACARDIFINALE PACAP PACAP examplelairfrance cap successfully loaded c airfrance cap Export file s are required 2 3 4 modified Please load required Export File s Figure 18 The DeCAP tool window The DeCAP window Figure 18 is made of a menu 1 a CAP component browser 2 a description window 3 and a status bar 4 The CAP compo nent browser is an expandable tree which simplifies the view of the CAP file components The descr
8. eable _airfrance rentacar airfrance rentacar air method_34 Z _airfrance purse airfrance purse airfrance purse airfrance purse lt airfrance purse gt method_34 Z _airfrance rentacar airfrance rentacar airfrance rentacar airfrance rentacar lt airfrance rentacar gt method_41 Ljavacard framework APDU V _airfrance purse airfrance purse airfrance purse airfrance purse lt 2 method U iavacarditramework APIDU AUTAN ntaca alrfran ntacar airfran antaca auiran r Progress Status Step 1 Configure Package Names a amp 5 t Step 2 Configure Ambient File A PACAP e i Step 3 Confirm Analysis Setup Nome file ambient_file_v1 Toe Figure 14 Saving the Ambient file Stop at first violation Stop at first violation Figure 15 Choosing the stop condition for the analysis 12 M Java Card Information Flow Verifier 1 1 File View Tools Help FAILED THE APPLET IS NOT SAFE Some METHODS VIOLATE S I F ENT DETAILS BUTTON TO VIEW DETAILS Fixpoint reached gt Ambient File lt Internal methods gt method_1 B S B V _airfrance airfrance airfrance airfrance airfrance airfrance method_15 B S B V _airfrance airfrance airfrance airfrance airfrance airfrance airfrance method_103 Ljavacard framework APDU V _ airfrance airfrance airfrance airfrance airfrance method_254 Ljavacard framework AP
9. ework Applet selectingApplet Z _airfrance airfrance javacard framework ISOException throwit S V _airfrance airfrance Figure 10 Selecting and viewing a method Stop at first violation With this option set the data flow analysis stops as soon as the security levels calculated by the abstract interpreter violate the security policy specified in the Ambient file Stop at fixpoint With this option set the data flow analysis stops at the fixpoint of the analysis the security levels of the Ambient file are left unchanged by a run of the abstract interpreter After having selected the stop condition click on the OK button to start the analysis When the stop condition occurs the result of the analysis are reported in the Java Card Information Flow Verifier 1 2 main window Figure 16 The Analysis Log window reports the Ambient file updated according to the abstract interpreter rules At the end of this phase the Ambient file reports the maximum security level for methods and heap section Internal Methods Exported Methods airfrance internal_class_15 lt init B 5 8 V _ purse airfrance airfrance internal_class_15 lt init B 5 8 V _rentacar airfrance avacard framework Applet lt init V _airfrance airfrance ard framework Applet register V _airfrance airfrance ard framework APDU getBuffer B _airfrance airfranc ard framework Applet selectingApplet Z _airfrance airfrance ce airfrance acardii
10. ffer B _airfrance airfrance javacard framework Applet selectingApplet Z _airfrance airfrance javacard framework ISOException throwlt S V _airfrance airfrance airfrance internal_class_103 internal_method_103 Ljavacard framework APDU r Progress Status Step 1 Configure Package Names Step 2 Configure Ambient File Figure 9 The Ambient file editor e Given two security levels a and b notation a b is used for a b e The security policy all levels are allowed can be expressed either by including the whole set of levels within the angled brackets or by omitting the policy from the Ambient file e The security level public is used to denote public information e The name of the method is shown as the method s number as it appears in the CAP file The symbolic name of the method can be retrieved by using the DeCAP tool 2 4 Performing the analysis At the beginning of the analysis the JCSI Analysis Wizard window allows the user to choose the stop condition Figure 15 Imported Methods Internal Methods Exported Methods Heap Section airfrance internal_class_15 lt init gt B S B V __ purse airfrance airfrance internal_class_15 lt init gt B S B V _rentacar airfrance javacard framework Applet lt init gt V _airfrance airfrance javacard framework Applet register V _airfrance airfrance rk APDU ae ffer airfrance airfr javacard fram
11. files have been successfully loaded the main GUI is shown telling the user that the analysis of the informa tion flow can start Figure 5 File View Tools Help SECURE 7 INFORMATION FLOW for Java Cards Copright c 2002 2011 Department of Information Engineering University of Pisa Italy Figure 1 The JCSI tool main window 5 Open Files CAP File Automatically Load JCR Nome file airfrance cap mwone ava Cara apmettea Sd Aaoi Annuna Figure 2 Loading a CAP file CAP File C Users cinzia Documents JAVACARD PACAP example PACAP exampleiairfrance cap Export Files C Users cinzia Documents JAVACARD PACAP example PACAP examplelexports pacapin Automaticslly Load JCRE API Export Files 5 Add Applet Export Files coca ewe a E C airfrance exp D purse exp LC crypto exp rentacar exp framework exp rmi exp C io exp D security exp C tang exp Li service exp D openpiatform exp utils exp pacapinterfaces exp Nome file rentacar exp Tipofiie ExportFileexp y Figure 3 Loading Export files arning the following additional exports are need for the analysis xport AID com gemplus pacap pacapinterfaces xport AID com gemplus pacap renta Figure 4 Missing Export files window APPLET LOADED READY TO ANALYZE Copyrignt
12. iption window shows a text description of the highlighted component The status bar guides the user during the CAP file inspection 3 1 Menu Functions are grouped into four categories File Load CAP File To load a CAP file and begin a new working session In the description window a message signals the correct loading of the CAP file and requests the user to load the Export files The root of the CAP component browser tree has the same name as the loaded CAP file Add Export File To load an Export file Note that the Export files associated to the chosen CAP file are loaded automatically if they are stored in the same directory and if the JC HOME setting see Edit Preferences refers to a correctly installed version of Java Card SDK Exit To exit from DeCAP 15 Edit Preferences To set program options In the General tab Figure 19 1 the Show Method s Name checkbox enables the name lookup within the Export files of methods invoked when displaying byte code informations The Verbose debug option enables debug mes sages relative to this tool development The Environment tab Fig ure 19 2 lets the user choose a Java Card SDK a Java Runtime Environment and the filename of the cref EEPROM image file Tools System log To show the application log Cap file analysis A set of functions to gather information on CAP file structure Help Program version and license information and this help document
13. nstalled on card Log Ambient File Changes If this option is selected a text file is cre ated that logs all changes occurring to the ambient file during the analysis By default the text file is stored in the same folder of the CAP file and its name is given by the name of the CAP file under analysis followed by a timestamp Log Abstract Interpreter States If this option is selected a text file is created that logs a complete trace of the analysis performed by the tool As for option Log Ambient File Changes by default such text file is stored in the same folder of the CAP file and its name is given by the name of the CAP file under analysis followed by a timestamp At the end of this step the user clicks on the Next button The analysis starts as described in the next section In the tool the following conventions are used File View Tools Help oi nt tup Loade L al ina Use Default Ambient File Copyright c 2002 2011 Department of Information APPLET UNDER ANALYSIS Users cinzia Documents VAR Imported Methods V Internal Methods Exported Methods Heap Section airfrance internal_class_15 lt init gt B S B V _purse airfrance airfrance internal_class_15 lt init gt B S B V _rentacar airfrance javacard framework Applet lt init gt V _airfrance airfrance javacard framework Applet register V _airfrance airfrance javacard framework APDU getBu
14. onent J class_component 9 J method_component tag 7 size 610 handler_count 0 Exception_Handler_Infol 0 EJ Method _Infol 12 C method_1 B S B V C method_15 B S B V C method_34 Z method_38 V C method_41 Lexternal_method V EI method_103 Lexternal_method V Cf method_254 Lexternal_method V C flags 0 max_stack 3 B nargs 2 EJ args amp return value max_locals 2 bytecode length 38 J method_294 V c method_473 S C method_503 B S V gt CI method_554 Lexternal_method B Lexte c method_607 V interface_methods c static_field_component gt CJ reference_location_component gt c export_component oyte code aload_1 invokevirtual 6 astore_2 aload_1 invokevirtual 16 sstore_3 aload_1 sconst_4 invokevirtual 17 aload_2 sconst_0 getfield_s this 0 invokestatic 18 pop aload_2 sconst_2 getfield_s this 1 invokestatic 18 pop aload_1 gt sconst_0 sconst_4 invokevirtual 19 return cJ descriptor_component a A T modified Figure 21 The bytecode representation in the description window 18
15. ramework APDUIV purse airfrance ainfrance internal_class_15 lt init B S B V _ purse airfrance Figure 11 Changing the security policy of a method 10 Heap Section Progress Status Step 1 Configure Package Names New level for constant_pool 1 i default airfrance Step 2 Configure Ambient File D Annuna Figure 12 Changing the security level of an object Ambient File lt Internal methods gt method_1 B S B V _airfrance airfrance airfrance airfrance airfrance airfrance method_15 B S B V _airfrance airfrance airfrance airfrance airfrance airfrance airfrance method_103 Ljavacard framework APDU V _airfrance airfrance airfrance airfrance airfrance method_254 Ljavacard framework APDU V _airfrance airfrance airfrance airfrance airfrance Step 1 Configure Package Names Step 2 Configure Ambient File Step 3 Confirm Analysis Setup Figure 13 Confirming the Analysis Setup 11 Analysis Setup lt Exported methods gt method_38 V _airfrance purse a rfrance purse airfrance purse lt airfrance purse gt method_38 V _airfrance rentacar airfrance rentacar airfrance rentacar lt airfrance rentacar gt method_554 Ljavacard framework AID B Ljavacard framework Shareable _airfrance purse airfrance purse airfrance method_554 Ljavacard framework AID B Ljavacardiframework Shar
16. yze class files is available the software community still lacks of similar tools for CAP files The JCSI tool performs a static analysis of CAP files in order to study the information flow generated by the code Included in JCSI the DeCAP tool enables the analysis by converting a CAP file into a structure conforming to the Java Card Virtual Machine Language JCVML specification 2 JCSI 2 1 GUI description The JCSI s graphical user interface Figure 1 includes a status window 1 three function buttons 2 3 4 one tool button 5 and one help button 6 The analysis of a CAP file is carried out through the following steps 1 Load the CAP file and the necessary Export files Subsection 2 2 2 Set the parameters for the analysis Subsection 2 3 3 Perform the analysis Subsection 2 4 4 View the log file Subsection 2 5 2 2 Loading the CAP file and the Export files To load a CAP file and the needed Export files click on the Open button A new window Open Files will pop up showing the following buttons Open a file browser window is opened to choose the desired CAP Figure 2 Add Remove a file browser window is opened to add remove the Export files of the package Figure 3 To automatically load JCRE API Export Files select Automatically Load JCRE API Export Files Ok to confirm the chosen files Missing Export files if any are listed as in Figure 4 When the CAP file and all the necessary Export
Download Pdf Manuals
Related Search