Lightweight verification of control flow policies on Java bytecode

This paper presents the enforcement of control flow policies for Java bytecode devoted to open and constrained devices. On-device enforcement of security policies mostly relies on run-time monitoring or inline checking code, which is not appropriate for strongly constrained devices such as mobile phones and smart-cards. We present a proof-carrying code approach with on-device lightweight verification of control flow policies statically at loading- time. Our approach is suitable for evolving, open and constrained Java-based systems as it is compositional, to avoid re-verification of already verified bytecode upon loading of new bytecode, and it is regressive, to cleanly support bytecode unloading.Ce rapport présente l'application de politiques de flot de contrôle sur du bytecode Java pour les petits systèmes ouverts. La plupart du temps, l'application de ce type de politiques de sécurité est réalisée par l'observation du système ou l'insertion de code pour assuré en assurer le respect, ce qui n'est pas approprié pour les petits systèmes fortement contraints tels que les téléphones mobiles ou les cartes à puce. Nous présentons une méthode basée sur le proof-carrying code pour faire appliquer ce type de politiques avec une vérification embarquée réalisée au chargement. Notre approche est bien adaptée aux petits systèmes ouverts évolutifs car elle est compositionnelle, pour éviter la revérification du code déjà chargé, et régressive, afin de traiter proprement le déchargement de code déjà installé et vérifié