BACK TO INDEX

Publications of year 2001

Books and proceedings

  1. Isabelle Attali and Thomas Jensen, editors. Smart Card Programming and Security (e-Smart 2001), September 2001. Springer LNCS vol. 2140. 
    @Proceedings{Attali:01:EsmartProceedings,
publisher = {Springer LNCS vol.~2140},
editor = {Isabelle Attali and Thomas Jensen},
year = {2001},
author = {Isabelle Attali and Thomas Jensen},
Title = {Smart Card Programming and Security (e-Smart 2001)},
month = sep,

}


Thesis

  1. Marc Éluard. Analyse de sécurité pour la certification d'applications Java Card. PhD thesis, Université de Rennes 1, December 2001. Note: N. d'ordre : 2614. 
    @phdthesis{Eluard:01:PhD,
year = {2001},
school = {Université de Rennes~1},
note = {N. d'ordre~: 2614},
title = {Analyse de sécurité pour la certification d'applications Java Card},
author = {Marc Éluard},
month = dec 
}


Articles in journal or book chapters

  1. F. Besson, T. Jensen, D. Le Métayer, and T. Thorn. Model ckecking security properties of control flow graphs. Journal of Computer Security, 9:217-250, 2001. [WWW]
    A fundamental problem in software-based security is whether local security checks inserted into the code are sufficient to implement a global security property. This article introduces a formalism based on a linear-time temporal logic for specifying global security properties pertaining to the control flow of the program, and illustrates its expressive power with a number of existing properties. We define a minimalistic, security-dedicated program model that only contains procedure call and run-time security checks and propose an automatic method for verifying that an implementation using local security checks satisfies a global security property. We then show how to instantiate the framework to the security architecture of Java 2 based on stack inspection and privileged method calls.

    @Article{Besson:01:ModelChecking,
author = "F. Besson and T. Jensen and D. Le~Métayer and T. Thorn",
title = "Model ckecking security properties of control flow graphs",
journal = "Journal of Computer Security",
year = "2001",
volume = "9",
pages = "217--250",
url = {http://www.irisa.fr/lande/fbesson/fbesson.html},
abstract = {A fundamental problem in software-based security is whether local security checks inserted into the code are sufficient to implement a global security property. This article introduces a formalism based on a linear-time temporal logic for specifying global security properties pertaining to the control flow of the program, and illustrates its expressive power with a number of existing properties. We define a minimalistic, security-dedicated program model that only contains procedure call and run-time security checks and propose an automatic method for verifying that an implementation using local security checks satisfies a global security property. We then show how to instantiate the framework to the security architecture of Java 2 based on stack inspection and privileged method calls.},

}


Conference articles

  1. T. Genet and Valérie Viet Triem Tong. Reachability Analysis of Term Rewriting Systems with Timbuk. In 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, volume 2250 of Lectures Notes in Artificial Intelligence, pages 691-702, 2001. Springer Verlag. [WWW] Keyword(s): Timbuk, Term Rewriting, Reachability, Tree Automata, Descendants, Verification.
    We present Timbuk -- a tree automata library -- which implements usual operations on tree automata as well as a completion algorithm used to compute an over-approximation of the set of descendants R*(E) for a regular set E and a term rewriting system R, possibly non linear and non terminating. On several examples of term rewriting systems representing programs and systems to verify, we show how to use Timbuk to construct their approximations and then prove unreachability properties of these systems.

    @INPROCEEDINGS{GenetVTTong-LPAR01,
AUTHOR = {Genet, T. and Viet Triem Tong, Valérie},
TITLE = {{R}eachability {A}nalysis of {T}erm {R}ewriting {S}ystems with {Timbuk}},
BOOKTITLE = {8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
PUBLISHER = {Springer Verlag},
SERIES = {Lectures Notes in Artificial Intelligence},
YEAR = {2001},
PAGES = {691--702},
VOLUME = 2250,
ABSTRACT = {We present Timbuk -- a tree automata library -- which implements usual operations on tree automata as well as a completion algorithm used to compute an over-approximation of the set of descendants R*(E) for a regular set E and a term rewriting system R, possibly non linear and non terminating. On several examples of term rewriting systems representing programs and systems to verify, we show how to use Timbuk to construct their approximations and then prove unreachability properties of these systems.},
KEYWORDS = {Timbuk, Term Rewriting, Reachability, Tree Automata, Descendants, Verification},
URL = {ftp://ftp.irisa.fr/local/lande/tg-vvtt-lpar01.ps.gz} 
}


  2. T. Jensen and F. Spoto. Class analysis of object-oriented programs through abstract interpretation. In F. Honsell and M. Miculan, editors, Proc. of Foundations of Software Science and Computation Structures (FoSSaCS'01), pages 261-275, 2001. Springer LNCS vol .2030. 
    @InProceedings{Jensen:01:ClassAnalysis,
author = {T. Jensen and F. Spoto},
title = {Class analysis of object-oriented programs through abstract interpretation},
booktitle = {Proc.~of Foundations of Software Science and Computation Structures (FoSSaCS'01)},
year = {2001},
editor = {F.~Honsell and M.~Miculan},
pages = {261--275},
publisher = {Springer LNCS vol~.2030} 
}


  3. David Pichardie and Yves Bertot. Formalizing Convex Hulls Algorithms. In Proc. of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01), number 2152 of Lecture Notes in Computer Science, pages 346-361, 2001. Springer-Verlag. 
    @InProceedings{BePi01Convexhull,
author = "David Pichardie and Yves Bertot",
title = {{Formalizing Convex Hulls Algorithms}},
booktitle = "Proc.\ of 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01)",
year = "2001",
pages = "346--361",
number = "2152",
series = "Lecture Notes in Computer Science",
publisher = "{Springer-Verlag}",

}


  4. Igor Siveroni, Thomas Jensen, and Marc Éluard. A Formal Specification of the Java Card Applet Firewall. In Hanne Riis Nielson, editor, Nordic Workshop on Secure IT-Systems, November 2001. 
    @inproceedings{Siveroni:01:Nordsec,
title = {A Formal Specification of the Java Card Applet Firewall},
month = nov,
booktitle = {Nordic Workshop on Secure IT-Systems},
year = {2001},
editor = {Hanne Riis Nielson},
author = {Igor Siveroni and Thomas Jensen and Marc Éluard} 
}


  5. Marc Éluard, Thomas Jensen, and Ewen Denney. An Operational Semantics of the Java Card Firewall. In Isabelle Attali and Thomas Jensen, editors, Smart Card Programming and Security (e-Smart 2001, volume Springer LNCS vol. 2140, September 2001. 
    @inproceedings{Eluard:01:Esmart,
volume = {Springer LNCS vol.~2140},
editor = {Isabelle Attali and Thomas Jensen},
year = {2001},
author = {Marc Éluard and Thomas Jensen and Ewen Denney},
booktitle = {Smart Card Programming and Security (e-Smart 2001},
title = {An Operational Semantics of the Java Card Firewall},
month = sep,

}


Internal reports

  1. Thomas Genet and Valérie Viet Triem Tong. Reachability Analysis of Term Rewriting Systems with Timbuk (extended version). Technical Report RR-4266, INRIA, 2001. [WWW]
    We present Timbuk -- a tree automata library -- which implements usual operations on tree automata as well as a completion algorithm used to compute an over-approximation of the set of descendants R*(E) for a regular set E and a term rewriting system R, possibly non linear and non terminating. On several examples of term rewriting systems representing programs and systems to verify, we show how to use Timbuk to construct their approximations and then prove unreachability properties of these systems.

    @TECHREPORT{GenetVTTong-RR01,
AUTHOR = "Genet, Thomas and Viet Triem Tong, Valérie ",
TITLE = "{R}eachability {A}nalysis of {T}erm {R}ewriting {S}ystems with {Timbuk} (extended version)",
INSTITUTION = {INRIA},
TYPE = {Technical Report},
NUMBER = {RR-4266},
YEAR = 2001,
URL = {ftp://ftp.irisa.fr/local/lande/tg-vvtt-inria01.ps.gz},
ABSTRACT = {We present Timbuk -- a tree automata library -- which implements usual operations on tree automata as well as a completion algorithm used to compute an over-approximation of the set of descendants R*(E) for a regular set E and a term rewriting system R, possibly non linear and non terminating. On several examples of term rewriting systems representing programs and systems to verify, we show how to use Timbuk to construct their approximations and then prove unreachability properties of these systems.} 
}



BACK TO INDEX

This document was translated from BibTEX by bibtex2html