*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h30                     *
*                             Salle R, etage -1                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

*** Vendredi 2 mars 2001 **** 14h00 *********************************

Relache

*** Vendredi 9 mars 2001 **** 14h00 *********************************

Prenom NOM (Institution)

Titre non parvenu

Re'sume' : non parvenu

*** Vendredi 16 mars 2001 **** 14h00 ********************************

Prenom NOM (Institution)

Titre non parvenu

Re'sume' : non parvenu

*** Vendredi 23 mars 2001 **** 14h00 ********************************

Andrei SABELFELD (Chalmers University of Technology)

The Impact of Synchronisation on Secure Information Flow in Concurrent Programs

Re'sume' : This talk focuses on the problem of determining whether a given
shared-memory multi-threaded program has secure information flow.  The
program runs on a partition of data on high (private) and low (public)
security data. The program is not trusted (possibly received over the
Internet). The program's low output is publicly available (e.g., sent
over the Internet) as well as, possibly, timing information about the
program's execution (e.g., times when the program makes Internet
accesses are observable).

The issue of secure information flow has become especially important
with the growing popularity of mobile code and networked information
systems.  For distributed programming, the use of multi-threaded
programming languages has become extremely popular.  However, in the
setting of an imperative shared-memory multi-threaded language, very
little has been done in treating secure programming with
synchronisation.  Because synchronisation is fundamental to concurrent
programs, it is highly desirable to have a robust security
specification and tools that aid in the design of secure programs with
synchronisation.  To fill this gap, this talk presents a compositional
bisimulation-based confidentiality specification for multi-threaded
programs with synchronisation and proposes a type-system-based
analysis improving on previous approaches to reject insecure programs.


*** Vendredi 30 mars 2001 **** 14h00 ********************************

Relache (reunion DAEDALUS)

*********************************************************************
Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************