Résumé de rapport du LIF

Téléchargement / Download : pdf 256k , ps.gz 208k , bibtex

Abstract

We define a method to statically bound the size of values computed during the execution of a program as a function of the size of its parameters. More precisely, we consider bytecode programs that should be executed on a simple stack machine with support for algebraic data types, pattern-matching and tail-recursion. Our size verification method is expressed as a static analysis, performed at the level of the bytecode, that relies on machine-checkable certificates. We follow here the usual assumption that code and certificates may be forged and should be checked before execution.

Our approach extends a system of static analyses based on the notion of quasi-interpretations that has already been used to enforce resource bounds on first-order functional programs. This paper makes two additional contributions. First, we are able to check optimized programs, containing instructions for unconditional jumps and tail-recursive calls, and remove restrictions on the structure of the bytecode that was imposed in previous works. Second, we propose a direct algorithm that depends only on solving a set of arithmetical constraints.

Keywords

Resource Control, Quasi-Interpretation, Program Analysis.

Résumé

Nous présentons une méthode permettant de borner statiquement la taille des valeurs générées durant l'exécution d'un programme, la borne obtenue étant exprimée comme une fonction de la taille des paramètres initiaux. Plus précisément, nous considérons des programmes écrits dans une forme pré-compilé, aussi appelé bytecode, qui doivent s'exécuter sur une machine à pile très simple, offrant un support pour les types de données inductifs, le filtrage et la récursion terminale. Cette méthode de vérification de taille est présentée comme une analyse statique, menée au niveau du bytecode, qui repose sur des certificats pouvant être validés automatiquement. Nous nous plaçons ici dans l'hypothèse courante que le code et les certificats peuvent avoir été compromis et qu'ils doivent donc être vérifié avant l'exécution.

Notre approche étend un système d'analyses statiques basé sur la notion de quasi-interpretations qui ont été utilisés afin d'assurer des bornes sur l'utilisation des ressources dans le cadre de programmes fonctionnels du premier ordre. Ce travail apporte deux nouvelles contributions. D'abord, nous sommes capable de vérifier des programmes optimisés, contenant des instructions de saut inconditionnel, sans imposer les restrictions sur la structure des programmes qui étaient nécessaires dans nos travaux précédents. Ensuite nous proposons une méthode directe qui repose uniquement sur la résolution d'un systèmes de contraintes arithmétique à variable rationnelles.

Mots clés

Contrôle de ressource, quasi-interpretation, analyse statique.

Bibtex

@TECHREPORT{26-2005,
    AUTHOR	= {Silvano Dal Zilio and Régis Gascon},
    TITLE	= {{Resource Bound Certification for a Tail-Recursive Virtual Machine}},
    INSTITUTION	= {{LIF}},
    ADDRESS	= {Marseille, France},
    TYPE	= {Research report},
    NUMBER	= {26-2005},
    MONTH	= {June},
    YEAR	= {2005},
    NOTE	= {http://pageperso.lif.univ-mrs.fr/~edouard.thiel/RESP/Rapports/26-2005.html},
}