mySelectedPapers.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -oc selectedKeys -ob mySelectedPapers.bib -c author:'gurvan' --expand myPapers.bib}}
@inproceedings{LeGuernic2012encover,
  author = {Balliu, Musard and Dam, Mads and Le Guernic, Gurvan},
  title = {{ENCOVER}: {S}ymbolic {E}xploration for
                  {I}nformation {F}low {S}ecurity},
  crossref = {proc_conf_CSF-12},
  abstract = {We address the problem of program verification for
                  information flow policies by means of symbolic
                  execution and model checking. Noninterference-like
                  security policies are formalized using epistemic
                  logic. We show how the policies can be accurately
                  verified using a combination of concolic testing and
                  SMT solving. As we demonstrate, many scenarios
                  considered tricky in the literature can be solved
                  precisely using the proposed approach. This is
                  confirmed by experiments performed with ENCOVER, a
                  tool based on Java Pathfinder which we have
                  developed for concolic information flow testing.}
}
@inproceedings{LeGuernic2011etl4ifs,
  author = {Balliu, Musard and Dam, Mads and Le Guernic, Gurvan},
  title = {{E}pistemic {T}emporal {L}ogic for {I}nformation
                  {F}low {S}ecurity},
  crossref = {proc_work_PLAS-11},
  pages = {Article No~6},
  doi = {http://dx.doi.org/10.1145/2166956.2166962},
  pdf = {http://www.csc.kth.se/tcs/publications/2011/plas11.pdf},
  html = {http://dl.acm.org/citation.cfm?id=2166962&CFID=94320345&CFTOKEN=14057310},
  abstract = {Temporal epistemic logic is a well-established
                  framework for expressing agents knowledge and how it
                  evolves over time. Within language-based security
                  these are central issues, for instance in the
                  context of declassification. We propose to bring
                  these two areas together. The paper presents a
                  computational model and an epistemic temporal logic
                  used to reason about knowledge acquired by observing
                  program outputs. This approach is shown to elegantly
                  capture standard notions of noninterference and
                  declassification in the literature as well as
                  information flow properties where sensitive and
                  public data intermingle in delicate ways.}
}
@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},
  crossref = {proc_conf_CSF-09},
  pages = {432--441},
  doi = {http://doi.acm.org/10.1145/1653662.1653715},
  pdf = {http://www.msr-inria.inria.fr/projects/sec/cflow/papers/from-information-flow-policies-to-cryptographic-mechanisms_ccs09.pdf},
  html = {http://dl.acm.org/citation.cfm?id=1653715},
  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://ftp.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_conf_CSF-12,
  title = {25th IEEE Computer Security Foundations Symposium},
  year = 2012,
  month = jun,
  location = {Cambridge, USA},
  booktitle = {Proceedings of the IEEE Computer Security
                  Foundations Symposium},
  note = {To appear}
}
@proceedings{proc_work_PLAS-11,
  title = {PLAS '11: Proceedings of the ACM SIGPLAN 6th
                  Workshop on Programming Languages and Analysis for
                  Security},
  year = 2011,
  month = jun,
  location = {San Jose, USA},
  booktitle = {Proceedings of the ACM SIGPLAN Workshop on
                  Programming Languages and Analysis for Security},
  isbn = {978-1-4503-0830-4},
  html = {http://dl.acm.org/citation.cfm?id=2166956&picked=prox},
  editor = {Askarov, Aslan and Guttman, Joshua},
  publisher = {ACM Digital Library},
  address = {New York, NY, USA},
  note = {Co-located with FCRC 2011}
}
@proceedings{proc_conf_CSF-09,
  editor = {Al-Shaer, Ehab and Jha, Somesh and Keromytis,
                  Angelos D.},
  title = {Proceedings of the 2009 ACM Conference on Computer
                  and Communications Security, CCS 2009, Chicago,
                  Illinois, USA, November 9-13, 2009},
  location = {Chicago, Illinois, USA},
  year = 2009,
  month = nov,
  booktitle = {Proceedings of the ACM Conference on Computer and
                  Communications Security},
  publisher = {ACM Press},
  address = {New York, NY, USA},
  isbn = {978-1-60558-894-0}
}
@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},
  url = {http://ftp.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-372/}
}
@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.94.