Tool-assisted Specification and Verification of Java Card Programs
This page contains information about the project "Tool-assisted Specification and Verification of Java Card Programs", VerifiCard for short.
Project Website
The official project website is
http://www.verificard.org.
Members
Abstract
General Aims
The next generation of smart cards will be used for services where security is a key issue: authenticated access to computer networks, e-commerce, high value wire-less services etc. Reliability and trust are necessary for large scale adoption and success of smart cards. The application programs (applets) for these cards will be written in , a simplified version of Java, the popular programming language. Correct functioning of these applets must be guaranteed, and potentially malicious applets must be identified. Therefore, new validation techniques are needed, based on well-defined models for Java Card, using special tools (theorem proving and model checking) for mathematically proving correctness, going well beyond testing. Correctness will be established for crucial components of the Java Card platform (bytecode verifier, virtual machine, API) based on the open Java Card standard, and for individual applets (provided by the industrial partners in case studies).
Aims of AG Softech
Development of the Java Card Interface Specification Language JCISL
JCISL will be a declarative interface specification language based on pre- and postconditions (capturing also exceptions), invariants, and constructs for frame properties and encapsulation aspects. The semantics of the specification language will be given in terms of an axiomatic semantics of Java Card, which is also developed in this project. JCISL will be developed in cooperation with the University of Nijmegen and the Institut Nationale de Recherche en Informatique et en Automatique. In our group, we will start by investigating specification primitives for frame properties and invariants. Moreover, we plan to develop a specification technique for alias properties based on our Universe Type System.
Development of an Interface Specification of the Java Card API
The interface specification of the Java Card API from Sun will be based on the existing informal specification and the reference implementation. It will be given in the form of annotated Java Card files using the interface specification language JCISL.
The API specification will be used to prove properties of Java Card applets and to verify the reference implementation. Furthermore, it serves as a case study for JCISL. The development of the API specification is joint work with the University of Nijmegen.
In the first project phase, our group's particular focus is on providing abstract models for the API classes and on specifying alias properties of the API.
Development of an Interactive Tool for Applet Verification
We will extend our Jive system, which has been developed in the Lopex project, to Java Card. Jive supports program-centered verification and provides a graphical user interface tailored to the specific needs and intuition of software developers. To integrate the tool with other techniques and proof tools used in VerifiCard, an interface to semantics-based program proofs in PVS and Isabelle/HOL will be implemented with the help of the Technical University of Munich.
Researchers in AG Softech
Funding
The project is funded by the Information Society Technologies (IST) Programme of the European Union under contract number ST-2000-26328-VERIFICARD.
Completion Status
The project is completed.
