Table of Contents

Two Security Criteria for Executing Mobile Code (doctoral dissertation, 2003, in french)

Doctoral dissertation, Ecole nationale des ponts et chaussées, 2003, 301 pages (in french)

The dissertation deals with language-based security and tries to answer the following question: how to protect the host system that executes mobile programs, like applets? As mobile programs are potentially malicious, the host system must ensure that their execution is not dangerous for its resources. A solution is to execute mobile programs in a secured environment: the environment enables the information flows between mobile programs and local resources and the accesses from mobile programs to local resources, to be controlled. We give two security criteria for securely executing mobile code. The first one deals with information flows, ensures confidentiality, is based on the code of the local environment, is accurate and undecidable; the second one deals with access controls, ensures confinement, is based on the type of the local environment, is approximate and decidable.

 author =       "Hervé Grall",
 title =        "Deux critères de sécurité pour l'exécution de code mobile",
 year =         "2003",
 address =      "CERMICS (ENPC-INRIA)",
 school =       "\'Ecole nationale des ponts et chaussées",

download (pdf)

A Confinement Criterion for Securely Executing Mobile Code (JALC 2006)

Journal of Automata, Languages and Combinatorics 11 (2006) 1, 59-106

Mobile programs, like applets, are not only ubiquitous but also potentially malicious. We study the case where mobile programs are executed by a host system in a secured environment, in order to control the accesses from mobile programs to local resources. The article deals with the following question: how can we ensure that the local environment is secure? We answer by giving a confinement criterion: if the type of the local environment satisfies it, then no mobile program can directly access a local resource. The criterion, which is type-based and hence decidable, is valid for a functional language with references. By proving its validity, we solve a conjecture stated by Leroy and Rouaix at POPL ’98. Moreover, we show that the criterion cannot be weakened by giving counter-examples for all the environment types that do not satisfy the criterion, and that it is pertinent by detailing the example of a specific security architecture. The main contribution of the article is the proof method, based on a language annotation that keeps track of code origin and that enables the study of the interaction frontier between the local code and the mobile code. The generalization of the method is finally discussed.

 author =       "Hervé Grall",
 title =        "A Confinement Criterion for Securely Executing Mobile Code",
 journal =      "Journal of Automata, Languages and Combinatorics",
 volume =       "11",
 number =       "1",
 pages =        "59--106",
 year =         "2006",

download (pdf)

Coinductive Big-Step Operational Semantics (I&C 2008)

With Xavier Leroy, Information and Computation, Special issue on Structural Operational Semantics (SOS), 2009.

Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We formalize the connections between the coinductive big-step semantics and the standard small-step semantics, proving that both semantics are equivalent. We then study the use of coinductive big-step semantics in proofs of type soundness and proofs of semantic preservation for compilers. A methodological originality of this paper is that all results have been proved using the Coq proof assistant. We explain the proof-theoretic presentation of coinductive definitions and proofs offered by Coq, and show that it facilitates the discovery and the presentation of the results. (See the Coq development.)

 title = "Coinductive big-step operational semantics ",
 journal = "Information and Computation ",
 volume = "207",
 number = "2",
 pages = "284 - 304",
 year = "2009",
 note = "Special issue on Structural Operational Semantics (SOS) ",
 author = "Xavier Leroy and Hervé Grall",

download (pdf)

read online on journal's website (restricted access)

Proving Fixed Points (FICS 2010)

7th Workshop on Fixed Points in Computer Science, FICS 2010 - Brno, Czech Republic, August 21-22 2010 - A satellite workshop of MFCS & CSL 2010

We propose a method to characterize the fixed points described in Tarski’s theorem for complete lattices. The method is deductive: the least and greatest fixed points are "proved" in some inference system defined from deduction rules. We also apply the method to two other fixed point theorems, a generalization of Tarski’s theorem to chain-complete posets and Bourbaki-Witt’s theorem. Finally, we compare the method with the traditional iterative method resorting to ordinals and the original impredicative method used by Tarski.

 AUTHOR = {Hervé Grall },
 TITLE = {Proving Fixed Point},
 BOOKTITLE = {Proceedings of the 7th Workshop on Fixed Points in Computer Science (FICS 2010)}
 YEAR = 2010,

download (pdf)

The Substitution Principle in an Object-Oriented Framework for Web Services: From Failure to Success (iiWAS 2013)

With Diana Allam and Jean-Claude Royer, Information Integration and Web-based Applications & Services, 2013

Nowadays, services are more and more implemented by using object-oriented frameworks. In this context, two properties could be particularly required in the specification of these frameworks: (i) a loose coupling between the service layer and the object layer, allowing evolution of the service layer with a minimal impact on the object layer, (ii) an interoperability induced by the substitution principle associated to subtyping in the object layer, allowing to freely convert a value of a subtype into a supertype. However, experimenting with the popular cxf framework, we observed some undesirable coupling and interoperability issues, due to the failure of the substitution principle. Therefore we propose a new specification of the data binding used to translate data between the object and service layers. We show that if the cxf framework followed the specification, then the substitution principle would be recovered, with all its advantages.

  TITLE = {{The Substitution Principle in an Object-Oriented Framework for Web Services: From Failure to Success}},
  AUTHOR = {Allam, Diana and Grall, Herv{\'e} and Royer, Jean-Claude},
  BOOKTITLE = {{The 15th International Conference on Information Integration and Web-based Applications \& Services (iiWAS2013)}},
  YEAR = {2013},

download (pdf)

Last Updated 2015-04-17T08:45+0200. Comments or questions: Send a mail.