Both at the EUP session on the last afternoon of the meeting, and indeed throughout the meeting after the individual talks, there was a lot of interesting discussion on the role that VerifiCard could and should play, and on the direction that future work should take.
Below we try to summarize the main points that came up in these discussions.
A more general recurring theme in the discussions was the role that academia in general should play in the field of smartcards, and the kind of things academia should be working on - either as part of the VerifiCard project or beyond - according to the industrial partners and the EUP members. E.g. Eduardo Gimenez (Trusted Logic) felt that two possible contributions from academia are program design methodologies and language design principles: academics are quite trained in the problem of designing programming languages, including clear syntax, semantics and associated calculi (like typing calculus, access control calculus, etc), much more than the people that usually fix standards.
One particular topic where this question arose was the formal description of the JavaCard Virtual Machine. Here the question was whether the VerifiCard partners should try to develop ever more detailed formalisations, with as ultimate goal a formalisation that could serve as an industry standard (notably in response to the feedback by Gemplus on the formalisation so far), or whether it would be more worthwhile to invest in the development of tools and languages that help reducing the cost and effort required to develop such formal models. Eduardo Gimenez (Trusted Logic) saw the huge cost and effort required for developing complete formal models as a major obstacle, and thought VerifiCard should focus their attention on better tool-support for this. The people from France Telecom supported this view. David Naccache (Gemplus) also remarked that there is a danger that academics spent all their energy in following and keeping up with developments in industry, whereas they should rather be leading the way with developing new ideas to be eventually picked up by industry, as is for instance the case in the field of cryptography. Olivier Ly (Schlumberger CP8) thought that a reference formal description of a Java Card platform is indeed necessary, but that such a description will eventually be provided anyhow, either by academia, or by some company, because e.g. Schlumberger has started a certification procedure and the French government authorities (French DCSSI) requires specifications to be public.
Clearly the work by the academic partners on the Gemplus case study has been very useful in demonstrating the current possibilities for applet verification. Both Thomas Arts (Ericsson) and Didier Begay (France Telecom) expressed their interest in JML as a specification language and in experimenting with automatic tools like ESC/Java as part of their development process. The work on the purse case study with ESC/Java and LOOP has already convinced researchers at Gemplus that it is worthwhile to take a closer look at these approaches.
Eduardo Gimenez (Trusted Logic) mentioned several subjects where he saw an important role for the academic partners in VerifiCard:
Pierre Cregut and Didier Begay (France Telecom) explained that the interest of France Telecom in VerifiCard has been evolving; whereas in the beginning there was just academic interest in the project, they now have new projects appearing that rely on the security of JavaCard and related technologies. Though it is difficult for them to say any more on these projects, they welcome closer cooperation with academics on these topics.
Regarding JavaCard Virtual Machine formalisation, Pierre Cregut thought this it is not the role of VerifiCard or academia of following a standard to provide a complete and detailed formal semantics, as this is too daunting a task for an institution with limited resources and limited research interest of following its evolution. Instead, Pierre thought the focus should be on tools that make the task of formalisation possible. Ultimately JavaCard users (like France Telecom) are the parties that will need a precise semantics to establish contractual relationships with the manufacturers -- i.e. what exactly can they expect of a JavaCard -- and they will then provide the pressure and the means to get a full-fledged formal semantics of the platform, if they feel that the necessary tools are available, because inter-operability is so important.
Pierre strongly supported the idea of having a single specification language like JML which could be used for a whole range of tools. Given that currently the cost of proving correctness of applications is high, Pierre also stressed the interest of -- and even the necessity for -- tools and languages that allow an incremental approach to verification. He thought the approach of using JML with ESC/Java and Loop was a perfect example of this. The only way to getting business units involved in applet verification is to provide some verification with a "press button" tool, with the ability to then provide better results on critical parts with real theorem proving.
Didier Begay mentioned that they were interested in applet verification, and could provide more case studies on a bilateral basis, subject to NDAs. However, he also remarked that academia should not get too obsessed with industrial cases studies, and shouldn't be afraid of keeping on doing more fundamental research.
Thomas Arts (Ericsson) found that having some case studies presented was very enlightening, as it gave a good impression of the state-of-the-art for the industrial participants. He particularly enjoyed the very pragmatic approach of the purse case study using ESC/Java, which, in spite of unsoundness and incompleteness, gives quick results. At Ericsson they would be trying out JML and ESC/Java in one new project in addition to current practice of using UML with Rational Rose.
Thomas would like to see more advice on getting a tool/method to work for one problem on all kinds of code, like using ESC/Java to detect array boundaries and null-pointer problems. Industry wants specific solutions for a problem with a high degree of automation. If automation is not feasible, there should be a cookbook to support people doing things by hand. So a detailed explanation of how one can use JML to specify a certain property and how that property can be proved for general code, with as much support by tactics to make it as automatic as possible.
Thomas found the variety of specification languages that were mentioned in the different talks at the workshop confusing. He stressed the importance of having a single specification language. The project should not show two different languages for specifying properties. He suggested to try to sell all specification languages under one name, with one syntax, and to present results with the same language, even if one uses a different language with the tools.
He also stressed the importance to trying to formalize standards within the project. He noted that the group of Gilles Barthe seems to have the possibility to push a standard way of formalizing virtual machines and thought they should use that.
Thomas thought there was somewhat too much focus on proving things with a theorem prover. Using formal methods does not necessarily mean "proving with a theorem prover"; just the fact that you prove something (even with pen and paper) should suffice. Thomas would like to see more
Regarding the meeting itself, Thomas thought there were interesting talks, but found it hard to see the relations between them. He missed a clear overview the whole VerifiCard project, which was only given on the last day at the beginning of the EUP session, and contexts of the individual talks. At the following JavaCard meetings talks should begin by pointing out their relation to the larger picture.
Jani Nikula (Setec Oy) said that Setec Oy are currently working on a JavaCard platform implementation for CC evaluation at level 4+ and on applets for the JavaCard platform. From the viewpoint of Setec Oy the work in VerifiCard has been quite academic (at least up to now), which is why they have just been silently observing. However, they will probably be more active now that the project is getting onto something more and more concrete (such as tools that they could use without too much effort). Jani also said that they could provide more case studies on a bilateral basis, subject to NDAs.
Like Thomas Arts, Marcus Oestreicher (IBM Zurich) also mentioned that he found the variety of specification languages discussed at the meeting somewhat confusing. He said work on API specifications made a lot of sense, as something that is very visible to the application programmers. Marcus also drew attention to the typically wide gap between protocol specifications and implementations as an area for interesting and useful work. Finally, Marcus gave a pointer to an (open source) implementation of a smart card application that might be an interesting case study.