Verification of Java card programs [Elektronische Ressource] / von Kurt Stenzel

Sujets

• Informatik

Informations

• Publié par: universitat_augsburg
• Publié le: 01 janvier 2005
• Nombre de lectures: 39
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Veri cation of Java Card Programs
Dissertation
zur Erlangung des Doktorgrades Dr. rer. nat.
der Fakult at fur Angewandte Informatik
der Universit at Augsburg
im Jahr 2005 von
Kurt Stenzel2
Amtierender Dekan: Prof. Dr. Wolfgang Reif
Gutachter: Prof. Dr. Wolfgang Reif
Prof. Dr. Bernhard Bauer
Tag der Prufung: 30. Mai 2005
Prufer: Prof. Dr. Bernhard Bauer
Prof. Dr. M oller
Prof. Dr. Wolfgang Reif
Prof. Dr. Theo Ungerer3
Summary
Smart cards are used in security critical applications where money or private data is
involved. Examples are the German Geldkarte or new passports with biometrical data.
Design or programming errors can have severe consequences. Formal methods are the
best means to avoid errors. Java Card is a restricted version of Java to program smart
cards. This work presents a logical calculus to formally prove the correctness and
security of Java Card programs. The is implemented in the KIV system, and
ready for use. First, an operational big-step semantics for sequential Java is presented
based on algebraic speci cations. All Java language constructs are modeled. Then,
a sequent calculus for dynamic logic for Java Card is developed, and the correctness
of the calculus is formally proved. The calculus is designed to support libraries, the
reuse of proofs, and program modi cations. This entails two di eren t notions of type
soundness, the standard one, and a weaker version. Furthermore, the calculus is not
restricted to Java Card, but can be used for arbitrary sequential Java program. The
work ends with some intricate examples. All properties and theorems are formally
proved with the KIV system. The resulting veri cation system is able to cope with
real-life e-commerce applications.4
Acknowledgments
I wish to thank my supervisor Wolfgang Reif for his support, patience, trust, and guidance {
without him this work would not exist.
I wish to thank the members of the KIV group, especially Gerhard Schellhorn, Michael Balser,
and Christoph Duelli for the years they have spent for improving the KIV system {
without them this work would not have been possible.
I wish to thank all my colleagues, particularly Dominik Haneberg and Holger Grandy, for many
discussions and demands (yes!) {
without them this work would be less than it is.Contents
1 Introduction 7
2 Java Programs 13
2.1 Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.2 Statements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3 Java Type Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.4 Assumptions about the Compiler . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3 Semantics 23
3.1 The Evaluation Environment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3.2 Semantics of Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3.3tics of Statements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.4 Proof Technique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
4 The Calculus 63
4.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
4.2 Semantics of Formulas and Sequents . . . . . . . . . . . . . . . . . . . . . . . . . . 69
4.3 Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
4.4 Statements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
4.5 Generic Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
4.6 Additional Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
4.7 Predicate Logic Proof Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
4.8 Soundness of the Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
5 Type Safety 109
5.1 Primitive Type Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
5.2 De nition of Primitive Type Correctness . . . . . . . . . . . . . . . . . . . . . . . . 113
5.3 Properties ofe Type Correct Programs . . . . . . . . . . . . . . . . . . . . 117
5.4 Full Type Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118
6 Libraries and Modi cations 127
6.1 Java Libraries in KIV . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127
6.2 Extending Type Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129
6.3 Context dependency of Proof Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 130
6.4 Axioms for the Class Hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131
6.5 Detailed Analysis of Dependencies . . . . . . . . . . . . . . . . . . . . . . . . . . . 133
6.6 Theorems in Libraries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135
6.7 Libraries and Compatibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135
6.8 Context Modi cations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
56 CONTENTS
7 Four Examples 139
7.1 A CopyCard . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139
7.2 The Java Card API . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144
7.3 Decimal Numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 150
7.4 Linked Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 156
7.5 An example proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161
8 Conclusion 165
Bibliography 167
Index 175Chapter 1
Introduction
Overview
When Java appeared in the mid-nineties it rapidly became an object of big interest in the research
community. The main reason is that Java joins a number of interesting concepts. It is object
oriented, contains threads, uses a virtual machine to run byte code, has a byte code veri er, has
a sandbox concept to run untrusted code, etc. (Other reasons are: it is backed by a well-known
company; large libraries, compiler, and virtual machine are freely available on di eren t platforms.)
Furthermore, the language has been designed from scratch, is rather small, and is intended to be
programmer-friendly; i.e tries to prevent the programmer from making errors. This makes Java
a worthwhile target for a formal treatment, but also poses a challenge to the maturity of formal
methods (and their supporting tools) since it is no toy language. For program veri cation, however,
another target is needed: programs that are worth proving correct, and that are not too big. As
it turns out, smart cards programmed in Java Card are an almost perfect target. This thesis is
concerned with the veri cation of sequential Java programs with a focus on Java Card. All work
has been done with KIV (described below).
Smart Cards and Java Card
Smart Cards are credit card sized plastic cards with an embedded chip that contains a micro-
processor together with memory, i.e. a full { though small { computer. Without the enclosing card
the chip can be found, for example, in mobile phones as the Subscriber Identity Module (SIM).
Smart card applications often involve money or sensitive data; their importance is increasing.
Some examples:
The German Geldkarte is based on smart cards.
Several credit card companies have begun to issue smart cards to reduce fraud.
Next year, passports will contain embedded chips with biometric data to identify terrorists.
Also next year, the German health care card will be issued, a smart card.
These applications are highly security critical; millions of cards have been and will be issued.
Breaking the security of these cards { possibly due to a programming error { in a systematic manner
would be devastating. On a smaller scale, smart cards are used in universities (as student cards
and to pay for lunch), in larger companies for employees, in public transport, or in tness studios
for access and payment. Embedded chips are used in mobile phones, for pay-TV applications, in
car keys to avoid theft. Since security is the most important aspect in these they
are are a worthwhile target for program veri cation (among others; security of the protocols, the
cryptographic methods, and physical security is equally important).
78 CHAPTER 1. INTRODUCTION
Java Card [Jav00] [Che00] is a reduced version of Java designed for smart cards. Smart cards
are full computers, but have very limited resources, e.g. 64 KByte EEPROM for code and data,
4 KByte RAM, and a 8-bit processor running with 5 MHz. This means that a fully- edged Java
virtual machine does not t on a smart card. Therefore, in Java Card all resource consuming
features have been discarded: threads, garbage collection, streams, oating point arithmetic,
characters and strings, and integers. Essentially, Java Card is sequential Java with fewer primitive
data types (only boolean, byte, and short remain) and a much smaller (and di eren t) API. A
normal Java compiler is used to convert the source code into byte code, but then a converter must
be used that converts the byte code to a more condensed form that can be loaded onto a smart
card. The converter al