Solange Coupet-Grimal and William Delobel
                                                                           April 2005  
   

                                       Laboratoire d'informatique fondamentale de Marseille

              
UMR 6166 - CNRS, Université de la Méditerranée, Université de Provence
       
                                                                     Coq Development
                                      
                                                                        related to the paper entitled

                               A uniform and certified approach for two static analyses
                                                               
      Post-proceedings of Types 2004, Filliatre and al Eds., Springer LNCS 3839, pp 116-138, 2006. Copyright : Springer-Verlag.
      Also   RR LIF 24-2005                               

                 Research partially supported by
ACI CRISS


Over the last decade, research on mobile code has been a hot topic and intensive
efforts have been made to reduce the risk of malicious (Java) applets performing
a security attack. For this, a crucial functionality of the Java Platform is the
bytecode verifier which performs a static type analysis on programs. This kind
of analysis ensures integrity properties of the execution environment such as
the absence of memory faults. Consequently, there has been considerable interest
in specifying formally the Java Virtual Machine and proving the correctness of
its bytecode verifier (see for instance  [3, 2, 7, 6, 8) .

More recently, these investigations have been extended to establishing an
additional property that contributes to guarantee the safety of  bytecode by
ensuring bounds on the computational resources needed by its execution. 
Within this context, a project has been undertaken [1] which focuses on  a rather
standard first-order functional programming language with inductive types,
pattern matching, and call-by-value,  to be executed on a simple stack machine.
The language comes with various bytecode static analyses: a standard type analysis,
an analysis on the algebraic shape of the  values in the stack, an analysis of the
size of these values, and an analysis that insures the termination. The last three
analyses, and in particular their combination, are instrumental in predicting  the
space and time required for the execution of a program.

Here are the formal specification of the virtual machine related to this language
and the certification in the Coq proof assistant of an extended bytecode verifier
which performs the first two phases of the analysis, that is the type and shape
verifications. Our contribution is threefold:

     - First, we design a verifier in a uniform way, so as  both verification processes
become special  cases of a general framework for data flow analysis based on the
well known algorithm due to Kildall [5].

    - Second, we propose a functional specification in Coq of Kildall's algorithm and
we prove its correctness. This is related to Klein and Nipkow's work  with the
system Isabelle/HOL [7, 6]. However our formalization differs from theirs by theheavy
use of Coq dependent types and the way of encoding a recursive function which is not
structurally recursive. With this approach, properties common to both analyses
are established once and for all. Note that this approach also suits size analysis,
although  this remains work to be done in future.

    - Third,  these generic properties are used,  for proving not only the correctness
of type verification which is now quite standard, (see [4, 7, 8]), but also, and
this is the novelty, that of  algebraic  shape verification.

See the paper for a detailed description. The structure of the Coq development is made
explicit in a readme file.

References.

[1] Roberto M. Amadio, Solange Coupet-Grimal, Silvano Dal-Zilio, and Line Jakubiec.
A Functional Scenario for Bytecode Verification of Space Bounds,
In CSL, pages 265--279, 2004.

[2] Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard~P. Serpette, and
  Simao  Melo de Sousa.
A Formal Executable Semantics of the JavaCard Platform
In  ESOP, pages 302--319, 2001.

[3] Gilles Barthe, Guillaume Dufay, Line Jakubiec, and Simao Melo de Sousa.
A formal correspondence between offensive and defensive JavaCard virtual machines.
In VMCAI, LNCS 2294, 2002.

[4] Allen Goldberg.
A specification of java loading and bytecode verification.
In ACM Conference on Computer and Communications Security,pages 49--58, 1998.

[5] Gary Arlen Kildall.
A unified approach to global program optimization.
In ACM Symposium on Principles of Programming Languages, pages 194--206, 1973.

[6] Gerwin Klein and Tobias Nipkow.
Verified bytecode verifiers.
Theoretical Computer Science, 298:583--626, 2003.

[7] Xavier Leroy
Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning 30(3-4):235-269, 2003.

[8] Tobias Nipkow.
Verified bytecode verifiers.
In FOSSACS 2001, LNCS 2030, pages 347--363, 2001.