|
|
MODOCOP WORKSHOP
on
Smart Card Specification, Verification, and Testing
Thursday December 4, 2003
Amphitheatre of INRIA Rhône-Alpes
Montbonnot
|
|
|
The goal of the Modocop workshop is to bring together researchers working in the fields of specification, verification and symbolic testing of object-oriented concurrent programs, and in particular of smart card applications. The workshop is financed by INRIA in the context of the ARC (collaborative project) Modocop.
The program of this one-day workshop consists of three invited talks by specialists in the domain, plus several presentations by the Modocop participants. During coffee breaks and lunch there will be ample possibilities for informal discussions. Working language of the workshop will be English.
Registration is closed.
More information about transport, hotels, access to INRIA Rhône-Alpes etc.
8h30-9h00: Registration, coffee
9h00-10h00: Invited talk
"Smart cards and formal methods: an experience report"
Abstract. Smart cards seem to be the killer application for formal methods. There are three clearly identified needs for them: managing the complexity of the new open platforms, high level certification and reducing the cost of the testing process. High level certification is currently not a market requirement, but the cost of the testing process is an important issue, which is linked to the complexity of the new features of the Java Card virtual machine. We have demonstrated that it is technically feasible to use formal methods, unfortunately for a wide acceptance we also need to demonstrate that these methods are economically affordable. For this purpose, we have set up an evaluation process to compare two developments: a conventional and a formal development. We recorded several metrics in order to convince managers of the costs and benefits of this approach. Unfortunately, this has not lead to changes in the software development rules of Gemplus. We will present the metrics and draw conclusions about this experiment.
10h00-10h40: Fabrice Bouquet (University of Franche Comté, Besançon)
Abstract. In the ARC Modocop, we defined some case study to compare the several approaches of the ARC members. In this talk, we present one of them: Common Electronic Purse Specifications (CEPS). The CEPS is a standard for creating multi-currency smart-card electronic purse systems. In the case study, we found two complementary approaches: Formal verification and Testing. Formal verification is used to validate the model and their invariant properties. Testing is used to validate the CEPS behavior with functional test. In fact, we present the CEPS and the choice in the modeling of the system. The invariant properties defined on the system and the tests realized from model by each partner.
| Slides: |
 PPS |
10h40-11h10: Coffee break
11h10-12h10: Invited talk
"JML: some experiences and directions for future work"
Abstract. In the first part of this talk I will discuss a case study in the use of JML, namely the BART case study, which concerns a part of the control system for the Bay Area Rapid Transit (BART) train system. I will compare the use of JML to the use of OCL, the Object Constraint Language that is part of UML, which has also been used on this case study. In the second part of the talk I will discuss some of the (many!) open issues in JML. I'll try to include any issues that are relevant in the setting of distributed Java applications and which should be interesting for the ModoCop-ers.
| Slides: |
 |
12h10-12h50: Marieke Huisman (INRIA Sophia-Antipolis)
Abstract. This talk presents the use of a method - and its corresponding tool set - for compositional verification of applet interactions on a realistic industrial smart card case study. The case study, an electronic purse, is provided by smart card producer Gemplus, as a test case for formal methods for smart cards. The compositional verification method focuses on the possible interactions between different applets, co-existing on the same card, and provides a technique to detect illicit interactions between these applets. As the method is compositional, it supports the idea of post-issuance loading of applets. The correctness of a global system property can be established, using only local applet specifications. Later, when loading applets on a card, the implementations are matched against these local specifications, in order to guarantee the global property. We will briefly present the theoretical framework underlying our method, and then evaluate its practical usability by means of this industrial case study. In particular, we outline the tool set that we have assembled to support the whole verification process. This tool set combines existing model checkers with several newly developed tools, tailored to our method.
| Slides: |
|
12h50-14h00: Lunch
14h00-15h00: Invited talk
"Model Checking for Graph Transformation Systems, with Applications to Java"
Abstract. We propose graphs as a natural model for state snapshots of object-oriented programs, and graph transformations as the corresponding computation steps. This gives rise to operational models called graph transition systems, for which we propose a monadic second-order graph logic, with the capability to express dynamic allocation and de-allocation of entities, for the purpose of model checking.
As a proof-of-concept, we have worked this out in the context of Java: there are (partial) compilers to graph grammars from Java and Java bytecode, respectively, which faithfully model such aspects as class initialisation and dynamic method invocation. Furthermore, we show a tool for the automatic generation of graph transition systems from graph grammars.
| Slides: |
|
15h00-15h40: Eric Madelaine (INRIA Sophia-Antipolis)
Abstract. Distributed Java applications use remote method invocation as a communication means between distributed objects. The ProActive library provides high level primitives and strong semantic guaranties for programming Java applications with distributed, mobile, secured components. We present a method for building finite, parameterized models capturing the behavioral semantics of ProActive objects. Our models are symbolic labeled transition systems, whose labels represent (abstractions of) remote method calls. In contrast to the usual finite models, they encode naturally and finitely a large class of distributed object-oriented applications. Their finite instantiations can be used in classical model-checkers and equivalence-checkers for checking temporal logic properties in a compositional manner. We are building a software toolset for the analysis of ProActive applications using these methods.
| Slides: |
|
15h40-16h10: Coffee break
16h10-16h50: Thomas Jensen (IRISA)
Abstract. In this talk we will review techniques for verifying security properties of Java programs by a combination of static analysis and model checking. We will be addressing the problem of verifying the security of program fragments; in particular libraries protected by the use of Java's stack inspection mechanism.
| Slides: |
|
16h50-17h30: Wendelin Serwe (INRIA Rhône-Alpes)
Abstract. We propose a new approach to interprocedural analysis/verification, consisting in deriving an interprocedural analysis method by abstract interpretation of the standard operational semantics of programs. The advantages of this approach are twofold. From a methodological point of view, it provides a direct connection between the concrete semantics of the program and the effective analysis, which facilitates implementation and correction proofs. Moreover, this method subsumes/integrates two main, distincts methods for interprocedural analysis, namely the call-string and the functional approaches introduced by Sharir and Pnueli. This enables strictly more precise analysis and gives additional flexibility in the tradeoff between efficiency and precision of the analysis.
| Slides: |
|
Back to the VASY Home Page