The proceedings contain 12 papers. The special focus in this conference is on java on smartcards, programming and security. The topics include: A dynamic logic for the formal verification of java card programs;a tool...
ISBN:
(纸本)9783540421672
The proceedings contain 12 papers. The special focus in this conference is on java on smartcards, programming and security. The topics include: A dynamic logic for the formal verification of java card programs;a tool for detecting java card illegal flow;automated multi-modal deduction on javacards for multi-application security;a programming and a modelling perspective on the evaluation of java card implementations;automatic test generation for java card applets and formal specification and verification of java card’s application identifier class.
In this paper, we define a program logic (an instance of Dynamic Logic) for formalising properties of java CARD programs, and we give a sequent calculus for formally verifying such properties. The purpose of this work...
详细信息
ISBN:
(纸本)354042167X
In this paper, we define a program logic (an instance of Dynamic Logic) for formalising properties of java CARD programs, and we give a sequent calculus for formally verifying such properties. The purpose of this work is to provide a framework for software verification that can be integrated into real-world software development processes.
Open-cards have introduced a new life cycle for smart card embedded applications. In the case of java Card, they have raised the problem of embedded object-oriented applet validation. In this article, we describe a me...
详细信息
ISBN:
(纸本)354042167X
Open-cards have introduced a new life cycle for smart card embedded applications. In the case of java Card, they have raised the problem of embedded object-oriented applet validation. In this article, we describe a methodology for java Card applet verification, and its application an a case study. This methodology is based on automatic test generation. We first take benefits of the java Card platform validation, focusing on application conformity testing. Then, using UML, we model the applet and its probable communication with other embedded elements. In the next step, the resulting model is used to automatically generate test suites, using UMLAUT and TGV tools. The full process is iterative and incremental, in order to conform to an object-oriented approach. Moreover, this incremental process allows integrating priorities on validation, by focusing first on main functions and properties.
This paper presents some practical issues of a joint project between Gemplus and ONERA. In this approach, a smart card issuer can verify that a new applet securely interacts with already loaded applets. A security pol...
详细信息
ISBN:
(纸本)354042167X
This paper presents some practical issues of a joint project between Gemplus and ONERA. In this approach, a smart card issuer can verify that a new applet securely interacts with already loaded applets. A security policy has been defined that associates levels to applet attributes and methods and defines authorized flows between levels. We propose a technique based on model checking to verify that actual information flows between applets are authorized. In this paper, we focus on the development of the prototype of the analyzer and we present the first results.
Conventional interface distributions rely on Interface Description Language (IDL) files. From these IDL files, stubs are automatically generated to allow code to link to the desired interfaces. In contrast, the java C...
详细信息
ISBN:
(纸本)354042167X
Conventional interface distributions rely on Interface Description Language (IDL) files. From these IDL files, stubs are automatically generated to allow code to link to the desired interfaces. In contrast, the java Card interface distributions require both export files (IDL) and class files (stubs). This leads to the possibility of mismatched versions of the export files and class files. Furthermore, the class files distributed are typically generated from the original java card sources, which allows access to private information contained in the class file. Modifying sources to strip private code is error prone. In order to address these problems, a mechanism is proposed by which the necessary java class files may be synthesized from the export files, eliminating the need to distribute class files. This mechanism could be extended to other java platforms as a general-purpose means for interface distribution.
In this paper we present the first implementation of highspeed filesystem encryption with a slow java card. Using new "Remotely Keyed Protocols" designed by Lucks and Weis we can use the highly tamper-resist...
详细信息
ISBN:
(纸本)354042167X
In this paper we present the first implementation of highspeed filesystem encryption with a slow java card. Using new "Remotely Keyed Protocols" designed by Lucks and Weis we can use the highly tamper-resistant java ring, and even restrict ourselves to a version of the ring without built-in encryption. We have implemented this protocols on the ring and give a first performance comparision.
This paper discusses a verification in PVS of the AID (Application Identifier) class from the javaCard API. The properties that are verified are formulated in the interface specification language JML. This language is...
详细信息
ISBN:
(纸本)354042167X
This paper discusses a verification in PVS of the AID (Application Identifier) class from the javaCard API. The properties that are verified are formulated in the interface specification language JML. This language is also used to express the properties that are assumed about the native methods from the Util class that are used in the AID class. These properties include invariants for classes and behaviour specifications for methods;the latter give pre- and post-conditions describing the functional behaviour, and also specify when exceptions may be thrown.
The java Card(TM)2.1.1 Runtime Environment (JCRE) Specification [1] describes a secure virtual machine environment for smartcards that facilitates the post-issuance loading and installation of applets, via an optiona...
详细信息
ISBN:
(纸本)354042167X
The java Card(TM)2.1.1 Runtime Environment (JCRE) Specification [1] describes a secure virtual machine environment for smartcards that facilitates the post-issuance loading and installation of applets, via an optional "Installer". The Open Platform (OP) Card Specification [2] provides a robust specification for that installer. It identifies the oncard security features necessary to safeguard the various actors that are involved in a smart card system, including card issuers, application providers as well as cardholders. Such is the nature of information security these days it is necessary to demonstrate the trustworthiness of the OP approach. The Common Criteria (ISO 15408:1999) [3] presents an obvious course of action. A "Protection Profile", termed OP3 [4] has therefore been produced in order to ensure the benefit of Common Criteria evaluation of the OP installer, and by virtue of specifying the security requirements of the underlying operating system and integrated circuitry, of java Card(TM) and the chipcard platform itself. Evaluation will demonstrate that the OP security requirements are correctly implemented and cannot be bypassed, deactivated, corrupted or otherwise circumvented - at least to a given level of confidence (an EAL in Common Criteria terms). This is an amazingly useful firststep. However, there are important off-card assets that the smart card does not protect. Common Criteria evaluation does nothing to mitigate the risks to those assets. A Common Criteria evaluation will make assumptions about the environment of the target of evaluation. Evaluation does nothing to validate those assumptions. The assumptions usually concern the compromise of security data held off-card. It therefore makes little sense to rely just on the CC evaluation of just the smart card in order to establish and maintain the security of the overall system. Other steps are necessary. The paper describes what is being done to progress the Common Criteria evaluation of OP and
java Card Technology has provided a huge step forward in programmingsmartcards: from assembler to using a high level Object Oriented language. However, the authors have found some differences between the current Jav...
详细信息
暂无评论