@comment{{This file has been generated by bib2bib 1.93}}
@comment{{Command line: /usr/bin/bib2bib -oc selectedKeys -ob mySelectedPapers.bib -c author:'gurvan' --expand myPapers.bib}}
@inproceedings{LeGuernic2009aspcdp,
author = {Fournet, Cédric and Le Guernic, Gurvan and Rezk, Tamara},
title = {{A} {S}ecurity-{P}reserving {C}ompiler for
{D}istributed {P}rograms},
booktitle = {Proceedings of the ACM Conference on Computer and
Communications Security},
pages = {432--441},
year = 2009,
month = nov,
isbn = {978-1-60558-894-0},
location = {Chicago, Illinois, USA},
doi = {http://doi.acm.org/10.1145/1653662.1653715},
publisher = {ACM Press},
address = {New York, NY, USA},
abstract = {We enforce information flow policies in programs
that run at multiple locations, with diverse levels
of security. We build a compiler from a small
imperative language with locality and security
annotations down to distributed code linked to
concrete cryptographic libraries. Our compiler
splits source programs into local threads; inserts
checks on auxiliary variables to enforce the source
control flow; implements shared distributed
variables using instead a series of local replicas
with explicit updates; and finally selects
cryptographic mechanisms for securing the
communication of updates between locations. We
establish computational soundness for our compiler:
under standard assumptions on cryptographic
primitives, all confidentiality and integrity
properties of the source program also hold with its
distributed code, despite the presence of active
adversaries that control all communications and some
of the program locations. We also present
performance results for the code obtained by
compiling sample programs.}
}
@inproceedings{LeGuernic2008pdvoc,
crossref = {proc_work_VERIFY-08},
author = {Le Guernic, Gurvan},
title = {{P}recise {D}ynamic {V}erification of
{C}onfidentiality},
pages = {82--96},
url = {http://www.pubzone.org/pages/publications/showPublication.do?deleteform=true&search=venue&pos=1&publicationId=69514},
pdf = {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-372/paper09.pdf},
abstract = {Confidentiality is maybe the most popular security
property to be formally or informally
verified. Noninterference is a baseline security
policy to formalize confidentiality of secret
information manipulated by a program. Many static
analyses have been developed for the verification of
noninterference. In contrast to those static
analyses, this paper considers the run-time
verification of the respect of confidentiality by a
single execution of a program. It proposes a dynamic
noninterference analysis for sequential programs
based on a combination of dynamic and static
analyses. The static analysis is used to analyze
some unexecuted pieces of code in order to take into
account all types of flows. The static analysis is
sensitive to the current program state. This
sensitivity allows the overall dynamic analysis to
be more precise than previous work. The soundness of
the overall dynamic noninterference analysis with
regard to confidentiality breaches detection and
correction is proved.}
}
@techreport{LeGuernic2008pdvon,
author = {Le Guernic, Gurvan},
title = {{P}recise {D}ynamic {V}erification of
{N}oninterference},
institution = {INRIA-MSR},
year = 2008,
month = jul,
url = {http://hal.inria.fr/inria-00162609/fr/},
pdf = {http://hal.inria.fr/docs/00/30/06/33/PDF/contextSensitiveNIA.pdf},
abstract = {Confidentiality is maybe the most popular security
property to be formally or informally
verified. Noninterference is a baseline security
policy to formalize confidentiality of secret
information manipulated by a program. Many static
analyses have been developed for the verification of
noninterference. In contrast to those static
analyses, this paper considers the run-time
verification of the respect of confidentiality by a
single execution of a program. It proposes a dynamic
noninterference analysis for sequential programs
based on a combination of dynamic and static
analyses. The static analysis is used to analyze
some unexecuted pieces of code in order to take into
account all types of flows. The static analysis is
sensitive to the current program state. This
sensitivity allows the overall dynamic analysis to
be more precise than previous work. The soundness of
the overall dynamic noninterference analysis with
regard to confidentiality breaches detection and
correction is proved.}
}
@phdthesis{leguernic07thesis,
author = {Le Guernic, Gurvan},
title = {{C}onfidentiality {E}nforcement {U}sing {D}ynamic
{I}nformation {F}low {A}nalyses},
school = {Kansas State University},
year = 2007,
url = {http://tel.archives-ouvertes.fr/tel-00198621/fr/},
pdf = {http://tel.archives-ouvertes.fr/docs/00/19/86/21/PDF/thesis_report.pdf},
abstract = {With the intensification of communication in
information systems, interest in security has
increased. The notion of noninterference is
typically used as a baseline security policy to
formalize confidentiality of secret information
manipulated by a program. This notion, based on
ideas from classical information theory, has first
been introduced by Goguen and Meseguer (1982) as the
absence of strong dependency (Cohen, 1977).
``information is transmitted from a source to a
destination only when variety in the source can be
conveyed to the destination'' Cohen (1977) Building
on the notion proposed by Goguen and Meseguer, a
program is typically said to be noninterfering if
the values of its public outputs do not depend on
the values of its secret inputs. If that is not the
case then there exist illegal information flows that
allow an attacker, having knowledge about the source
code of the program, to deduce information about the
secret inputs from the public outputs of the
execution. In contrast to the vast majority of
previous work on noninterference which are based on
static analyses (especially type systems), this PhD
thesis report considers dynamic monitoring of
noninterference. A monitor enforcing noninterference
is more complex than standard execution monitors.
``the information carried by a particular message
depends on the set it comes from. The information
conveyed is not an intrinsic property of the
individual message.'' Ashby (1956). The work
presented in this report is based on the combination
of dynamic and static information flow analyses. The
practicality of such an approach is demonstrated by
the development of a monitor for concurrent programs
including synchronization commands. This report also
elaborates on the soundness with regard to
noninterference and precision of such approaches.}
}
@inproceedings{leguernic07ift,
author = {Le Guernic, Gurvan},
title = {{I}nformation {F}low {T}esting},
booktitle = {Proceedings of the Annual Asian Computing Science
Conference},
year = 2007,
series = {Lecture Notes in Computer Science},
volume = 4846,
pages = {33--47},
editor = {Cervesato, Iliano},
publisher = {Springer-Verlag},
organization = {Carnegie Mellon University Qatar Campus},
month = dec # { 9--11},
location = {Doha, Qatar},
url = {http://hal.inria.fr/inria-00198595/fr/},
pdf = {http://hal.inria.fr/docs/00/19/85/95/PDF/noninterferenceTesting.pdf},
abstract = {Noninterference, which is an information flow
property, is typically used as a baseline security
policy to formalize confidentiality of secret
information manipulated by a
program. Noninterference verification mechanisms are
usually based on static analyses and, to a lesser
extent, on dynamic analyses. In contrast to those
works, this paper proposes an information flow
testing mechanism. This mechanism is sound from the
point of view of noninterference. It is based on
standard testing techniques and on a combination of
dynamic and static analyses. Concretely, a semantics
integrating a dynamic information flow analysis is
proposed. This analysis makes use of static analyses
results. This special semantics is built such that,
once a path coverage property has been achieved on a
program, a sound conclusion regarding the
noninterfering behavior of the program can be
established.}
}
@techreport{LeGuernic2007dnaucssa,
author = {Le Guernic, Gurvan},
title = {{D}ynamic {N}oninterference {A}nalysis {U}sing
{C}ontext {S}ensitive {S}tatic {A}nalyses},
optinstitution = {{D}epartment of {C}omputing and {I}nformation
{S}ciences, {C}ollege of {E}ngineering, {K}ansas
{S}tate {U}niversity},
institution = {{K}ansas {S}tate {U}niversity},
year = 2007,
number = {2007-5},
address = {234 Nichols Hall, Manhattan, KS 66506, USA},
month = jul,
url = {http://www.cis.ksu.edu/~schmidt/techreport/2007.list.html},
pdf = {http://hal.inria.fr/docs/00/16/26/09/PDF/contextSensitiveNIA_report.pdf},
abstract = {This report proposes a dynamic noninterference
analysis for sequential programs. This analysis is
well-suited for the development of a monitor
enforcing the absence of information flows between
the secret inputs and the public outputs of a
program. This implies a sound detection of
information flows and a sound correction of
forbidden flows during the execution. The monitor
relies on a dynamic information flow analysis. For
unexecuted pieces of code, this dynamic analysis
uses any context sensitive static information flow
analysis which respects a given set of three
hypotheses. The soundness of the overall monitoring
mechanism with regard to noninterference enforcement
is proved, as well as its higher precision than the
automaton-based mechanism proposed in previous
work.}
}
@inproceedings{leguernic07flic,
crossref = {proc_work_RULE-07},
author = {Le Guernic, Gurvan and Perret, Julien},
title = {{FLIC}: {A}pplication to {C}aching of a {D}ynamic
{D}ependency {A}nalysis for a {3D} {O}riented {CRS}},
pages = {3--18},
url = {http://hal.inria.fr/inria-00159267/fr/},
pdf = {http://hal.inria.fr/docs/00/15/92/67/PDF/flic_pre-vRULE.pdf},
doi = {10.1016/j.entcs.2008.10.031},
abstract = {FL-systems are conditional rewriting systems. They
are used for programming (describing) and evaluating
(generating) huge 3D virtual environments, such as
cities and forests. This paper presents a formal
semantics and a dynamic dependency analysis for
FL-systems. This analysis allows the
characterization of a set of terms which are
joinable with the currently rewritten
term. Consequently, it is possible to speed up the
rewriting steps of the environments generation by
using a cache mechanism which is smarter than
standard ones. This work can be seen as a dynamic
completion of a set of rewriting rules. This
completion increases the number of terms which are
rewritten in normal form by the application of a
single rewriting rule.}
}
@inproceedings{LeGuernic2007acmocp,
crossref = {proc_sym_CSF-07},
author = {Le Guernic, Gurvan},
title = {{A}utomaton-based {C}onfidentiality {M}onitoring of
{C}oncurrent {P}rograms},
pages = {218--232},
url = {http://hal.inria.fr/inria-00161019/fr/},
pdf = {http://hal.inria.fr/docs/00/16/10/19/PDF/abnim_concurrent.pdf},
abstract = {Noninterference is typically used as a baseline
security policy to formalize confidentiality of
secret i nformation manipulated by a program. In
contrast to static checking of noninterference, this
paper consid ers dynamic, au\-to\-maton-based,
monitoring of information flow for a single
execution of a concurrent p rogram. The monitoring
mechanism is based on a combination of dynamic and
static analyses. During program execution,
abstractions of program events are sent to the
automaton, which uses the abstractions to track
information flows and to control the execution by
forbidding or editing dangerous actions. All
monitore d executions are proved to be
noninterfering (soundness) and executions of
programs that are well-typed i n a security type
system similar to the one of Smith and Volpano are
proved to be unaltered by the monitor (partial
transparency).}
}
@techreport{LeGuernic2007anmocp,
author = {Le Guernic, Gurvan},
title = {{A}utomaton-based {N}on-interference {M}onitoring of
{C}oncurrent {P}rograms},
optinstitution = {{D}epartment of {C}omputing and {I}nformation
{S}ciences, {C}ollege of {E}ngineering, {K}ansas
{S}tate {U}niversity},
institution = {{K}ansas {S}tate {U}niversity},
year = 2007,
number = {2007-1},
address = {234 Nichols Hall, Manhattan, KS 66506, USA},
optaddress = {Manhattan, KS, USA},
month = feb,
url = {http://www.cis.ksu.edu/~schmidt/techreport/2007.list.html},
abstract = {Earlier work [LGBJS06] presents an automaton-based
non-interference monitoring mechanism for sequential
programs. This technical report extends this work to
a concurrent setting. Monitored programs are
constituted of a set of threads running in
parallel. Those threads run programs equivalent to
those of [LGBJS06] except for the inclusion of a
synchronization command. The monitoring mechanism is
still based on a security automaton and on a
combination of dynamic and static analyses. As in
[LGBJS06], the monitoring semantics sends
abstractions of program events to the automaton,
which uses the abstractions to track information
flows and to control the execution by forbidding or
editing dangerous actions. All monitored executions
are proved to be non-interfering (soundness).}
}
@inproceedings{LeGuernic2006acm,
crossref = {proc_conf_ASIAN-06},
author = {Le Guernic, Gurvan and Banerjee, Anindya and Jensen, Thomas
and Schmidt, David},
title = {{A}utomata-based {C}onfidentiality {M}onitoring},
pages = {75--89},
url = {http://hal.inria.fr/inria-00130210/fr/},
pdf = {http://hal.inria.fr/docs/00/13/02/10/PDF/automatonBasedNiMonitoring.pdf},
abstract = {Non-interference is typically used as a baseline
security policy to formalize confidentiality of
secret information manipulated by a program. In
contrast to static checking of non-interference,
this paper considers dynamic, automaton-based,
monitoring of information flow for a single
execution of a sequential program. The mechanism is
based on a combination of dynamic and static
analyses. During program execution, abstractions of
program events are sent to the automaton, which uses
the abstractions to track information flows and to
control the execution by forbidding or editing
dangerous actions. The mechanism proposed is proved
to be sound, to preserve executions of well-typed
programs (in the security type system of Volpano,
Smith and Irvine), and to preserve some safe
executions of ill-typed programs. }
}
@inproceedings{leguernic06jmbrowser,
author = {Bonnel, Nicolas and Le Guernic, Gurvan},
title = {{S}ystème de recherche de méthodes {J}ava basé sur leur
signature},
booktitle = {Proceedings of Majecstic 2006},
year = 2006,
month = nov,
pdf = {http://hal.inria.fr/docs/00/11/32/31/PDF/Bonnel_MajecSTIC06_web.pdf},
abstract = {L'objectif de cet article est de proposer une
démarche permettant de mettre en place un moteur de
recherche de méthodes au sein d'un langage de
programmation. Un tel outil s'avère particulièrement
utile aux développeurs. Des solutions ont déjà été
proposées mais elles sont pour la plupart basées sur
une recherche textuelle, c'est-à-dire uniquement
basées sur le contenu textuel de la description des
différentes méthodes. Nous proposons dans cet
article une nouvelle approche basée sur la signature
des méthodes. Le langage utilisé tout au long de cet
article est le langage Java.}
}
@techreport{LeGuernic2006abnim,
author = {Le Guernic, Gurvan and Banerjee, Anindya and Schmidt, David},
title = {{A}utomaton-based {N}on-interference {M}onitoring},
institution = {{D}epartment of {C}omputing and {I}nformation {S}ciences,
{C}ollege of {E}ngineering, {K}ansas {S}tate {U}niversity},
optinstitution = {{K}ansas {S}tate {U}niversity},
year = 2006,
number = {2006-1},
address = {234 Nichols Hall, Manhattan, KS 66506, USA},
optaddress = {Manhattan, KS, USA},
month = apr,
abstract = {This report presents a non-interference monitoring
mechanism for sequential programs. Non-interference
is a property of the information flows of a
program. It implies the respect of the
confidentiality of the secret information
manipulated. The approach taken uses an automaton
based monitor. During the execution, abstractions of
the events occurring are sent to the automaton. The
automaton uses those inputs to track the information
flows and to control the execution by forbidding or
editing dangerous actions. The mechanism proposed is
proved to be sound and more efficient than a type
system similar to the historical one developed by
Volpano, Smith and Irvine. },
url = {http://www.cis.ksu.edu/~schmidt/techreport/2006.list.html}
}
@inproceedings{leguernic05flic,
author = {Le Guernic, Gurvan and Perret, Julien},
title = {{FL}-system's {I}ntelligent {C}ache},
booktitle = {Proceedings of Majecstic 2005},
editor = {Vautier, Alexandre and Saget, Sylvie},
pages = {79--88},
year = 2005,
month = nov,
pdf = {http://hal.inria.fr/docs/00/04/36/98/PDF/43.pdf},
abstract = {Cet article présente une application de techniques
issues du génie logiciel à la modélisation
d'environnements virtuels. Ces derniers, dès lors
qu'ils sont complexes, constituent des masses de
données particulièrement volumineuses et, de ce
fait, difficiles à manipuler. De plus, les
descriptions exhaustives de ces environnements,
c'est-à-dire explicites, sont peu évolutives. Pour
résoudre ces problèmes, il existe des méthodes
basées sur des systèmes de réécriture permettant de
décrire de fac¸on générique les objets de
l'environnement. Chaque objet est ainsi décrit par
un axiome qui est réécrit lors de la génération de
l'environnement. Lors de cette phase, il est
fréquent de retrouver deux séquences de réécriture
aboutissant à un même objet. Il est alors possible
d'utiliser un mécanisme tel que le cache afin
d'améliorer les performances en profitant des
calculs déjà effectués. Cependant, se contenter de
mettre en correspondance les noms et paramètres des
axiomes n'est pas suffisant pour établir l'ensemble
des réécritures identiques. En effet, les
réécritures d'un même axiome avec des paramètres
effectifs différents peuvent aboutir au même
objet. Le système proposé dans cet article effectue
une analyse dynamique des réécritures afin
d'améliorer les performances du cache en d´etectant
de tels cas. La première partie de cet article
présente le système de réécriture, la seconde
l'analyse utilisée, et la dernière le mécanisme
proposé.}
}
@inproceedings{LeGuernic2005mif,
author = {Le Guernic, Gurvan and Jensen, Thomas},
title = {{M}onitoring {I}nformation {F}low},
crossref = {proc_work_FCS-05},
pages = {19--30},
pdf = {http://hal.inria.fr/docs/00/06/50/99/PDF/le-guernic05monitoringInformationFlow.pdf},
abstract = {We present an information flow monitoring mechanism
for sequential programs. The monitor executes a
program on standard data that are tagged with labels
indicating their security level. We formalize the
monitoring mechanism as a big-step operational
semantics that integrates a static information flow
analysis to gather information flow properties of
non-executed branches of the program. Using the
information flow monitoring mechanism, it is then
possible to partition the set of all executions in
two sets. The first one contains executions which
\emph{are safe} and the other one contains
executions which may be unsafe. Based on this
information, we show that, by resetting the value of
some output variables, it is possible to alter the
behavior of executions belonging to the second set
in order to ensure the confidentiality of secret
data.}
}
@misc{LeGuernic2003ras_misc,
author = {Le Guernic, Gurvan},
title = {{R}oles \& {S}ecurity},
crossref = {proc_sem_LBS-05},
note = {Dagstuhl Seminar 03411: Language-Based Security},
month = oct,
year = 2003
}
@proceedings{proc_work_VERIFY-08,
editor = {Beckert, Bernhard and Klein, Gerwin},
title = {VERIFY 2008: The 5th International Verification
Workshop},
booktitle = {Proceedings of the International Verification
Workshop},
year = 2008,
publisher = {CEUR-WS.org},
series = {CEUR Workshop Proceedings},
volume = 372,
month = aug # { 10--11},
location = {Sydney, Australia},
note = {In connection with IJCAR 2008}
}
@article{1461260,
author = {Le Guernic, Gurvan and Perret, Julien},
title = {FLIC: Application to Caching of a Dynamic Dependency Analysis for a 3D Oriented CRS},
journal = {Electron. Notes Theor. Comput. Sci.},
volume = {219},
year = {2008},
issn = {1571-0661},
pages = {3--18},
doi = {http://dx.doi.org/10.1016/j.entcs.2008.10.031},
publisher = {Elsevier Science Publishers B. V.},
address = {Amsterdam, The Netherlands, The Netherlands}
}
@proceedings{proc_work_RULE-07,
title = {RULE 2007: The Eighth International Workshop on
Rule-Based Programming},
year = 2007,
month = jun # { 29},
location = {Paris, France},
booktitle = {Proceedings of the International Workshop on
Rule-Based Programming},
series = {Electronic Notes in Theoretical Computer Science (ENTCS)},
volume = 219,
issn = {1571-0661},
doi = {http://dx.doi.org/10.1016/j.entcs.2008.10.031}
}
@proceedings{proc_sym_CSF-07,
booktitle = {Proceedings of the 20th IEEE Computer Security
Foundations Symposium (CSFS20)},
year = 2007,
month = jul # { 6--8},
location = {S. Servolo island, Venice, Italy},
publisher = {IEEE Computer Society},
isbn = {0-7695-2819-8},
issn = {1063-6900},
optaddress = {10662 Los Vacqueros Circle, P.O. Box 3014, Los
Alamitos, CA 90720-1314}
}
@proceedings{proc_conf_ASIAN-06,
title = {Annual Asian Computing Science Conference: Focusing
on Secure Software and Related Issues},
booktitle = {Proceedings of the Annual Asian Computing Science
Conference},
year = 2006,
series = {Lecture Notes in Computer Science},
volume = 4435,
publisher = {Springer-Verlag},
month = dec # { 6--8},
location = {Tokyo, Japan}
}
@proceedings{proc_work_FCS-05,
booktitle = {Proceedings of the Workshop on Foundations of Computer Security},
year = 2005,
editor = {Sabelfeld, Andrei},
month = jun,
publisher = {DePaul University},
note = {Affiliated with LICS'05}
}
@proceedings{proc_sem_LBS-05,
booktitle = {03411 Abstracts Collection -- Language-Based
Security},
year = 2005,
editor = {Banerjee, Anindya and Mantel, Heiko and Naumann, David A. and Sabelfeld, Andrei},
number = 03411,
series = {Dagstuhl Seminar Proceedings},
address = {Dagstuhl, Germany},
publisher = {Internationales Begegnungs- und Forschungszentrum
(IBFI), Schloss Dagstuhl, Germany},
url = {http://drops.dagstuhl.de/opus/volltexte/2005/173
[date of citation: 2005-01-01]},
note = {$<$http://drops.dagstuhl.de/opus/volltexte/2005/173$>$
[date of citation: 2005-01-01]},
abstract = {From October 5th to 10th 2003,the Dagstuhl Seminar 03411 ``Language Based security'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar are put together in this paper.},
annote = {Keywords: Access control , information flow ,
noninterference , downgrading}
}
This file was generated by bibtex2html 1.93.