1\chapter{Preface} 2 3\section{Introduction} 4\label{sec:introduction} 5 6This document contains the automatically generated listings of the 7Isabelle sources for \mJava. \mJava{} is a reduced model of JavaCard, 8dedicated to the study of the interaction of the source language, byte 9code, the byte code verifier and the compiler. In order to make the 10Isabelle sources more accessible, this introduction provides a brief 11survey of the main concepts of \mJava. 12 13The \mJava{} \textbf{source language} (see \charef{cha:j}) 14only comprises a part of the original JavaCard language. It models 15features such as: 16\begin{itemize} 17\item The basic ``primitive types'' of Java 18\item Object orientation, in particular classes, and relevant 19 relations on classes (subclass, widening) 20 21\item Methods and method signatures 22\item Inheritance and overriding of methods, dynamic binding 23 24\item Representatives of ``relevant'' expressions and statements 25\item Generation and propagation of system exceptions 26\end{itemize} 27 28However, the following features are missing in \mJava{} wrt.{} JavaCard: 29\begin{itemize} 30\item Some primitive types (\texttt{byte, short}) 31\item Interfaces and related concepts, arrays 32\item Most numeric operations, syntactic variants of statements 33 (\texttt{do}-loop, \texttt{for}-loop) 34\item Complex block structure, method bodies with multiple returns 35\item Abrupt termination (\texttt{break, continue}) 36\item Class and method modifiers (such as \texttt{static} and 37 \texttt{public/private} access modifiers) 38\item User-defined exception classes and an explicit 39 \texttt{throw}-statement. Exceptions cannot be caught. 40\item A ``definite assignment'' check 41\end{itemize} 42In addition, features are missing that are not part of the JavaCard 43language, such as multithreading and garbage collection. No attempt 44has been made to model peculiarities of JavaCard such as the applet 45firewall or the transaction mechanism. 46 47For a more complete Isabelle model of JavaCard, the reader should 48consult the Bali formalization 49(\url{https://isabelle.in.tum.de/verificard/Bali/document.pdf}), which 50models most of the source language features of JavaCard, however without 51describing the bytecode level. 52 53The central topics of the source language formalization are: 54\begin{itemize} 55\item Description of the structure of the ``runtime environment'', in 56 particular structure of classes and the program state 57\item Definition of syntax, typing rules and operational semantics of 58 statements and expressions 59\item Definition of ``conformity'' (characterizing type safety) and a 60 type safety proof 61\end{itemize} 62 63 64The \mJava{} \textbf{virtual machine} (see \charef{cha:jvm}) 65corresponds rather directly to the source level, in the sense that the 66same data types are supported and bytecode instructions required for 67emulating the source level operations are provided. Again, only one 68representative of different variants of instructions has been 69selected; for example, there is only one comparison operator. The 70formalization of the bytecode level is purely descriptive (``no 71theorems'') and rather brief as compared to the source level; all 72questions related to type systems for and type correctness of bytecode 73are dealt with in chapter on bytecode verification. 74 75The problem of \textbf{bytecode verification} (see \charef{cha:bv}) is 76dealt with in several stages: 77\begin{itemize} 78\item First, the notion of ``method type'' is introduced, which 79 corresponds to the notion of ``type'' on the source level. 80\item Well-typedness of instructions wrt. a method type is defined 81 (see \secref{sec:BVSpec}). Roughly speaking, determining 82 well-typedness is \emph{type checking}. 83\item It is shown that bytecode that is well-typed in this sense can 84 be safely executed -- a type soundness proof on the bytecode level 85 (\secref{sec:BVSpecTypeSafe}). 86\item Given raw bytecode, one of the purposes of bytecode verification 87 is to determine a method type that is well-typed according to the 88 above definition. Roughly speaking, this is \emph{type inference}. 89 The Isabelle formalization presents bytecode verification as an 90 instance of an abstract dataflow algorithm (Kildall's algorithm, see 91 \secrefs{sec:Kildall} to \ref{sec:JVM}). 92%\item For \emph{lightweight bytecode verification}, type checking of 93% bytecode can be reduced to method types with small size. 94\end{itemize} 95 96Bytecode verification in \mJava{} so far takes into account: 97\begin{itemize} 98\item Operations and branching instructions 99\item Exceptions 100\end{itemize} 101Initialization during object creation is not accounted for in the 102present document 103(see the formalization in 104\url{https://isabelle.in.tum.de/verificard/obj-init/document.pdf}), 105neither is the \texttt{jsr} instruction. 106 107 108%%% Local Variables: 109%%% mode: latex 110%%% TeX-master: "root" 111%%% End: 112