Action Concertée Incitative

SÉCURITÉ INFORMATIQUE

Projet CRISS
Contrôle de Ressources et d'Interférence dans les Systèmes Synchrones

Coordinateur : Roberto Amadio (Université Paris 7)


Descriptif synthéthique du projet

Sites Participants :

INRIA, Sophia (resp. Gérard Boudol).
LIF, Marseille (resp. Solange Coupet).
LIPN, Villetaneuse (resp. Patrick Baillot).
LORIA, Nancy (resp. Jean-Yves Marion).
PPS, Paris (resp. Roberto Amadio).


Table des matières :

Réunions,
Exposés et Rapports de syntèse,
Publications,
Logiciel Expérimental.
















Réunion de coordination à Marseille, le 7 Septembre 2003.

Première réunion à l'INRIA Sophia, le Vendredi 23 Janvier 2004.

J.Y. Moyen, Termination and resource analysis of assembly programs by Petri Nets.
P. Baillot. Soft lambda-calculus: a language for polynomial time computation.
G. Boudol. ULM, a core programming model for global computing.
S. Dal Zilio. A functional scenario for bytecode verification of resource bounds.
F. Dabrowski. Resource control for cooperative synchronous threads: preliminary ideas.
A. Matos. Typing non-interference for a reactive language.

Deuxième réunion au LORIA Nancy, le Mercredi 23 Juin 2004.

P. Baillot. Light types for polynomial time computation in lambda-calculus (voir papier LICS04)
W. Delobel. Algorithme de Kildall en Coq et applications (memoire DEA Marseille, 2004)
S. Coupet. Un survol du logiciel developpe (travail TER Marseille, 2004)
R. Pechoux et N. Remond. Synthèse et vérification de qi (memoire DEA Nancy et stage Mines-Nancy 2004)
R. Gascon. Synthèse et vérification de quasi-interpretations (memoire DEA Marseille, 2004)
S. Dal Zilio. Controle de ressources pour systemes cooperatifs synchrones (voir papier CONCUR04).
S. Epardaud. Implantation d'UML (memoire DEA Nice, 2004).
F. Dabrowski. Terminaison des instants en ULM (1er ordre) et
langage fonctionnel (1er ordre) avec effets de bord et bornes polynomiales (travail en cours).
Discussion, problèmes ouverts et directions.
Réunion de l'ACI GEOCAL Complexité Implicite et Logique, à Villetaneuse.
Dates : 6 et 7 septembre 2004.
Organisateur : Patrick Baillot (LIPN, Villetaneuse).
Troisième réunion: Marseille, 17-18 Janvier 2005.

R. Amadio, Présentation du projet à mi-parcours.
S. Epardaud, Mise en oeuvre d'ULM en Scheme (rapport d'avancement).
F. Boussinot, Programmation reactive des automates cellulaires (exposé invité projet ALIDECS).
L. Mandel, ML reactif (exposé invité projet ALIDECS).
W. Delobel, Certification d'une architecture logicielle pour le contrôle de ressources (rapport d'avancement).
F. Blanqui, Certification de preuves de terminaison dans Coq, (exposé invité projet ModuLogic).
S. Coupet-Grimal, Une preuve effective de la bonne fondaison de MPO (rapport d'avancement).
G. Boudol, Non interférence et declassification (rapport d'avancement).
G. Bonfante, De nouvelles caractérisations en espace à l'aide des quasi-interprétations (survol + papier RTA 2005).
P. Baillot, Algorithmes d'inference de types dans EAL et DLAL (voir papier TLCA 2005).
R. Pechoux, Sup-interprétations (rapport d'avancement).
Discussion, problèmes ouverts et directions.
Quatrième réunion: Paris, Lundi 13 et Mardi 14 Juin 2005.

Jean-Pierre Jouannaud (LIX). Ordres d'ordre supérieur. (exposé invité)
Ugo Dal Lago (Bologna).The Geometry of Linear Ramified Recursion. (exposé invité)
Julien Verlaguet et Emmanuel Chailloux (PPS). HirondML: Fair threads Migrations for Objective Caml (exposé invité)
Roberto Amadio. The Synchronous Language, revisited.
Vincent Atassi. Sur l'inférence de type en Logique linéaire élémentaire et son implémentation.
Gérard Boudol. Sur le typage du flux d'information.
Roberto Amadio. Feasible reactivity for synchronous cooperative threads.
Paulin Jacobé de Naurois. Implicit Complexity over an Arbitrary Structure: Sequential and Parallel Polynomial Time.
Romain Péchoux. Synthesis of Quasi-Interpretations.
18th Computer Security Foundations Workshop, 20-22 Juin 2005.
Cinquième réunion: Marseille, Lundi 27 Fevrier 2006.

Roberto Amadio : Sémantique du modèle synchrone Criss
Romain Pechoux : On the modularity of quasi-interpretations
Jean-Yves Moyen : Graphes de Contrôle de Ressources
Patrick Baillot : Un algorithme polynomial pour l'inférence de type dans DLAL
Vincent Atassi : Implementation d'un algorithme de typage pour EAL et extension aux coercions
Guillaume Bonfante: Présentation de système. Une relecture de Jones. logspace, ptime.
William Delobel : Une axiomatisation constructive de RPO.

Sixième et dernière réunion à Paris, le Jeudi 14 Septembre 2006 (10h-17h).

R. Péchoux. Bilan des Sup-interpretations.
G. Bonfante. Crocus logiciel expérimental pour trouver des quasi-interprétations.
P. Baillot. Complexité, ordre supérieur et logique linéaire.
U. Dal Lago. On blind abstractions, quasi-interpretations and implicit computational complexity.
G. Boudol. Bilan du modèle CRISS.
R. Amadio. Pi-calcul synchrone.
I. Castellani. Bilan sur la non-interférence.
F. Dabrowski. Réactivité efficace pour le pi-calcul synchrone.

















Exposés et rapports de synthèse en rélation avec le projet

Projet soumis en 2003.

Journées ACISI 2003, Rennes (présentation du projet, S. Dal Zilio).

Workshop SATYFT 2004, Orleans (exposé invité sur la partie contrôle de ressources, R. Amadio).

Journées ACISI 2004, Toulouse (rapport d'avancement, R. Amadio).

Resource Analysis by Quasi-Interpretations, Sixth International Workshop on Logic and Computational Complexity, Juillet 2004, Turku, Finlande (J.-Y. Marion).

Rapport de mi-parcours, Avril 2005 (R. Amadio).

Cours sur la non-interférence, Spring School on Security, CIRM Marseille, 2005 (G. Boudol)

Data tiering as a complexity tool which jumps from discrete to real computation, International Workshop "Computations on the continuum", Juin 2005, Lisbonne (J.-Y. Marion).

Exposé sur le flot d'information et la déclassification aux journées PARISTIC, Bordeaux, Novembre 2005 (G. Boudol).

Complexity and Logic: Lectures from the Geocal'06 Winter School (P. Baillot et J.-Y. Marion).

Rapport final du projet (Septembre 2006).


























Publications (par ordre chronologique)

J.Y. Moyen ICAR System (Implicit complexity analysis). (NB This was developed before the project started) See here.

P. Baillot, V. Mogbil. Soft lambda-calculus: a language for polynomial time computation. In Proc. of FOSSACS 2004, Springer-Verlag. See here.

J.Y. Moyen Analyse de la complexité et transformation de programmes. PhD Thesis. See here.

G. Boudol ULM, a core programming model for global computing. In Proc of ESOP04, Springer-Verlag. See here.

R.M. Amadio. Synthesis of max-plus quasi-interpretations. Research Report LIF 18-2004, January 2004. See here. Revised version in Fundamenta Informaticae 65(1-2):29--60, 2005.

R.M. Amadio, S. Coupet-Grimal, S. Dal Zilio, L. Jakubiec. A functional scenario for bytecode verification of resource bounds. Research Report LIF 17-2004, January 2004. Extended abstract in Proc. CSL 2004, Springer LNCS. See here.

G. Boudol, I. Castellani, A. Matos. Typing non-interference for reactive programs. February 2004. Extended abstract in Foundations of Computer Security 2004 Workshop. Full version accepted for publication in the Journal of Logic and Algebraic Programming See here.

P.Baillot, K.Terui Light types for polynomial time computation in lambda-calculus. In proceedings of LICS 2004, April 2004. See here.

R.M. Amadio, S. Dal Zilio. Resource Control for Synchronous Cooperative Threads Research Report LIF 22-2004, May 2004. Extended abstract in Proc. CONCUR 2004, Springer LNCS. See here.

P.Baillot, K. Terui. A feasible algorithm for typing in Elementary Affine Logic. In the Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA'05), LNCS, Springer. Preliminary version available as arXiv preprint cs.LO/0412028. See here.

Guillaume Bonfante, Jean-Yves Marion and Jean-Yves Moyen Quasi-interpretations and small space bounds. In Proc. Rewriting techniques and applications (RTA 2005), LNCS, Springer. See here.

S. Epardaud. Mobile Reactive Programming in ULM. Scheme Workshop 2004, In Proceedings of the Fifth ACM SIGPLAN Workshop on Scheme and Functional Programming. See here.

G. Boudol, A. Matos. On declassification and the non-disclosure policy. In Proc IEEE Computer Security Foundations Workshop 2005. See here.

S. Coupet-Grimal, W. Delobel. A uniform and certified approach for two static analyses. To appear in Post Proceedings TYPES 2004, Filliatre et al (eds.), Springer LNCS. Also RR-LIF 24-2005. See here.

R.M. Amadio, S. Dal Zilio. Resource Control for Synchronous Cooperative Threads. Theoretical Computer Science, 358:229-254, 2006. See here.

G. Boudol. On typing information flow. In Proc. International Colloquium on Theoretical Aspects of Computing. LNCS, Springer. October 2005. See here.

R. Amadio, G. Boudol, F. Boussinot, I. Castellani. Reactive concurrent programming revisited. Extended abstract presented at the workshop Algebraic Process Calculi: the first twenty five years and beyond, Bertinoro, August 2005. To appear in Electronic Notes in TCS. See here.

G. Boudol, I. Castellani, A. Matos. Typing non-interference for reactive programs. June 2005. RR-INRIA 5594. Submitted. See here.

S. Dal Zilio, R. Gascon. Resource bound certification for a tail recursive machine. RR-LIF 26-2005. July 2005. Extended abstract in Proc. Third Asian Symposium on Programming Languages and Systems (APLAS 2005), LNCS, Springer.* See here.

A. Almeida Matos. Non-disclosure for distributed mobile code. In the proceedings of the Conference on Foundations of Software Technology and Theoretical Computer Science, 2005. LNCS 3821,177 - 188. See here.

R. Amadio, F. Dabrowski. Feasible reactivity for synchronous cooperative threads. In Proc. Expressiveness in Concurrency Workshop, September 2005. Electronic Notes in TCS, volume 154, issue 3. See here.

Amadio R., Guttman J. and Herzog J.
Proceedings 18th IEEE Computer Security Foundations Workshop. ISBN 0-7695-2340-4. Aix-en-Provence, 2005.

R. Amadio. The SL synchronous language, revisited. Technical Report, Université Paris 7, Laboratoire PPS, November 2005. To appear in Journal of Logic and Algebraic Programming. See here.

S. Coupet-Grimal, W. Delobel. An Effective Proof of the Well-Foundedness of the Multiset Path Ordering. RR LIF 27-2005. To appear in AAECC Journal (Applicable Algebra in Engineering Communication and Computing). See here.

S. Coupet-Grimal, W. Delobel. Une preuve effective de la bonne fondation de l'ordre récursif multi-ensemble sur les chemins. Dans Journées Francophones des Langages Applicatifs, JFLA 2006. (Version en français de l'article ci-dessus). See here.

S. Coupet-Grimal, W. Delobel. A Constructive Axiomatization of the Recursive Path Ordering. RR LIF 28-2006. See here.

A. Almeida Matos. Typing secure information flow: declassification and mobility. Thèse. École des Mines (Sophia-Antipolis). January 2006. See here.

V. Atassi , P. Baillot, K. Terui. Verification of Ptime reducibility for system F terms via Dual Light Affine Logic. Preprint arXiv cs.LO/0603104 and HAL ccsd-00021834, 21pp., March 2006. Also in Proc. Computer Science Logic. See here.

P. Baillot, U. Dal Lago et J.-Y. Moyen. On Quasi-Interpretations, Blind Abstractions and Implicit Complexity. Preprint HAL ccsd-00023668. Presented at 8th International Workshop on Logic and Computational Complexity (LCC'06), August 2006 (Satellite of FLOC-LICS) See here.

G. Bonfante, J.-Y. Marion et R. Péchoux. A characterisation of alternating log time by first-order functional programs. In Proc. LPAR 2006. See here.

G. Bonfante, R. Kahle, J.-Y. Marion et I. Oitavem. Towards and implicit characterisation of NCk. In Proc. CSL 2006. See here.

R. Amadio. A synchronous pi-calculus Technical Report, Université Paris 7, Laboratoire PPS, June 2006. See here.

J.-Y. Marion et R. Péchoux. Resource Analysis by Sup-interpretation. In Proc. FLOPS 2006, Springer Lecture Notes in Comp. Sci. 3945, pages 163-176. See here.

G. Bonfante. Some programming languages for LOGSPACE and PTIME. In Proc. AMAST 2006, Springer LNCS. See here.

J.-Y. Marion et R. Péchoux. Quasi-friendly sup-interpretations. Presented at 8th International Workshop on Logic and Computational Complexity (LCC'06), August 2006 (Satellite of FLOC-LICS).

F. Dabrowski et F. Boussinot, Cooperative threads and preemptive computations. Presented at Workshop on Thread Verification, August 2006 (Satellite of FLOC-LICS).

O. Bournez, F. Cucker, P.J. de Naurois and J.Y. Marion. Implicit complexity over an arbitrary structure: Quantifier alternations. Information and Computation, 204(2):210-230, 2006.

O. Bournez, F. Cucker, P. Jacobé de Naurois and J.-Y. Marion. Implicit Complexity over an Arbitrary Structure: Sequential and Parallel Polynomial Time. Journal of Logic and Computation, 15(1):41-58, 2005.

















Logiciel expérimental (par ordre chronologique)

J.Y. Moyen ICAR System (Implicit complexity analysis). (NB This was developed before the project started) See here.

S. Epardaud. The embedding of the ULM model in a Scheme language, and a Compiler and Virtual Machine for this embedding. January 2005. See here.

LIF Marseille team. Implementation of shape analysis for the byte code of a first-order functional language. January 2005. See here.

S. Coupet-Grimal, W. Delobel. A generic development of Kildall algorithm in Coq and its specialisation to type and shape analysis of functional bytecode. June 2005. See here.

V. Atassi. A type inference program in OCAML for elementary linear logic. November 2005. See here.

S. Coupet-Grimal, W. Delobel. Two contributions concerning MPO and RPO to the Coq library on rewriting and termination (CoLoR). See here.

G. Bonfante. CROCUS un synthétiseur de quasi-interpretations. See here.