A Formal Executable Semantics of the JavaCard Platform

Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard Serpette and Simão Melo de Sousa

View Related Documents

Journal Article
Tool-Assisted Specification and Verification of Typed Low-Level Languages
Gilles Barthe, Pierre Courtieu, Guillaume Dufay and Simão Melo de Sousa
Journal of Automated Reasoning, 2005, Volume 35, Number 4, Pages 295-354
- Download PDF (503.3 KB)
Book Chapter
A Very Small Bytecode-Verifier Based on PCC Algorithm for Smart Card
Jeung-Bo Cho and Min-Soo Jung
Lecture Notes in Computer Science, 2003, Volume 2713, Web and Communication Technologies and Internet-Related Social Issues — HSI 2003, Page 168
- Download PDF (1,004.7 KB)
Journal Article
Developing a Trojan applets in a smart card
Julien Iguchi-Cartigny and Jean-Louis Lanet
Journal in Computer Virology, 2010, Volume 6, Number 4, Pages 343-351
- Download PDF (639.7 KB)
Journal Article
A Type System for the Java Bytecode Language and Verifier
Stephen N. Freund and John C. Mitchell
Journal of Automated Reasoning, 2003, Volume 30, Numbers 3-4, Pages 271-321
- Download PDF (292.9 KB)
- View HTML
Journal Article
Bytecode Verification by Model Checking
David Basin, Stefan Friedrich and Marek Gawkowski
Journal of Automated Reasoning, 2003, Volume 30, Numbers 3-4, Pages 399-444
- Download PDF (276.4 KB)
- View HTML
Book Chapter
Attacks on Java Card 3.0 Combining Fault and Logical Attacks
Guillaume Barbu, Hugues Thiebeauld and Vincent Guerin
Lecture Notes in Computer Science, 2010, Volume 6035, Smart Card Research and Advanced Application, Pages 148-163
- Download PDF (387.3 KB)
Book Chapter
Computing Stack Maps with Interfaces
Frédéric Besson, Thomas Jensen and Tiphaine Turpin
Lecture Notes in Computer Science, 2008, Volume 5142, ECOOP 2008 – Object-Oriented Programming, Pages 642-666
- Download PDF (625.1 KB)
Journal Article
A New Type System for JVM Lock Primitives
Futoshi Iwama and Naoki Kobayashi
New Generation Computing, 2007, Volume 26, Number 2, Pages 125-170
- Download PDF (735.7 KB)
Journal Article
Verified Bytecode Subroutines
G. Klein and M. Wildmoser
Journal of Automated Reasoning, 2003, Volume 30, Numbers 3-4, Pages 363-398
- Download PDF (258.4 KB)
- View HTML
Journal Article
Completeness of a Bytecode Verifier and a Certifying Java-to-JVM Compiler
Robert F. Stärk and Joachim Schmid
Journal of Automated Reasoning, 2003, Volume 30, Numbers 3-4, Pages 323-361
- Download PDF (236.1 KB)
- View HTML

Abstract

We present a formal executable specification of two crucial JavaCard platform components, namely the Java Card Virtual Machine (JCVM) and the ByteCode Verifier (BCV). Moreover, we relate both components by giving a proof of correctness of the ByteCode Verifier. Both formalisations and proofs have been machined-checked using the proof assistant Coq.

Fulltext Preview

Image of the first page of the fulltext document

Frequently asked questions General info on journals and books Send us your feedback Impressum Contact us

SpringerLink

A Formal Executable Semantics of the JavaCard Platform

View Related Documents

Abstract

Fulltext Preview