VerifiCard @ Munich

Project Description Project Members Deliverables Publications Events Isabelle Formalizations Teaching

Project Description

The project VerifiCard is concerned with the formalization of aspects of JavaCard, a subset of the Java language deployed on smartcards.

VerifiCard @ Munich is part of the EU-sponsored project VerifiCard which involves partners from academia and industry. The focus of our group is on formalization and machine-aided analysis of

• the JavaCard source language, in particular its operational and axiomatic semantics (Tasks 2.1 and 2.2 of VerifiCard)
• the JavaCard bytecode language (operational semantics) and the bytecode verifier (Tasks 3.1 and 3.3 of VerifiCard)
• a compiler from the JavaCard source language into the bytecode (Task 3.4 of VerifiCard)

Project Members

• Gerwin Klein
• Tobias Nipkow
• Norbert Schirmer
• Martin Strecker (contact)
• Martin Wildmoser

Deliverables

(see list of all Verificard deliverables)

• 2.1: Operational semantics and type system (MicroJava and Bali)
• 2.2: Correctness proof for axiomatic semantics (Bali)
• 3.4: Compiler and its correctness proof

Publications

• Stefan Berghofer, Martin Strecker
  Extracting a formally verified, fully executable compiler from a proof assistant
  
• Gerwin Klein
  Verified Java Bytecode Verification
  
• Gerwin Klein, Tobias Nipkow
  Verified Bytecode Verifiers
  
• Gerwin Klein, Tobias Nipkow
  Verified Lightweight Bytecode Verification
  
• Gerwin Klein, Martin Strecker
  Verified Bytecode Verification and Type-Certifying Compilation
  
• Gerwin Klein, Martin Wildmoser
  Verified Bytecode Subroutines
  
• Farhad Mehta, Tobias Nipkow
  Proving Pointer Programs in Higher-Order Logic
  
• Tobias Nipkow
  Hoare Logics in Isabelle/HOL
  
• Tobias Nipkow
  Hoare Logics for Recursive Procedures and Unbounded Nondeterminism
  
• Tobias Nipkow
  Jinja: Towards a Comprehensive Formal Semantics for a Java-like Language (work in progress)
  
• David von Oheimb, Tobias Nipkow
  Hoare Logic for NanoJava: Auxiliary Variables, Side Effects and Virtual Methods revisited
  
• Norbert Schirmer
  Analysing the Java Package/Access Concepts in Isabelle/HOL
  
• Norbert Schirmer
  Java Definite Assignment in Isabelle/HOL
  
• Martin Strecker
  Formal Verification of a Java Compiler in Isabelle
  
• Martin Strecker
  Investigating Type-Certifying Compilation with Isabelle
  

Events

• Kick-Off Meeting, Nijmegen
• Annual Meeting 2002, Marseille
• VeriSafe Workshop, Nice
• Annual Meeting 2003, Munich

Isabelle Formalizations

• MicroJava is a reduced model of JavaCard, dedicated to the study of the interaction of the source language, byte code, the byte code verifier and the compiler. An overview is available as
  • PDF document / doublesided Postscript document
  • browsable Isabelle theories
• Bali is a comprehensive model of the JavaCard source language. An overview is available as
  • PDF document
  • browsable Isabelle theories

JavaCard source language

• Source language (MicroJava): Isabelle sources as gziped tar
• Source language (Bali): Isabelle sources as gziped tar

JavaCard bytecode language

• JVM (MicroJava): Isabelle sources as gziped tar
• Bytecode verifier (MicroJava): Isabelle sources as gziped tar

• PDF document
• Browsable Isabelle Theories
• Isabelle Sources

• PDF document
• Browsable Isabelle Theories
• Isabelle Sources

Compiler

• Conference paper: Investigating Type-Certifying Compilation with Isabelle
• Journal paper: Verified Bytecode Verification and Type-Certifying Compilation
• Isabelle sources as gziped tar

Teaching

• Seminar: Security (SS02 / WS02/03)
• Seminar: Proof of JavaCard security properties by approximate computation