Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

dezaghilpant06 (In proceedings)
Author(s) Mariangiola Dezani-Ciancaglini, Silvia Ghilezan and Jovanka Pantovic
Title« Security Types for Dynamic Web Data »
InTGC'06
SeriesLNCS
Editor(s) Roberto Bruni, Ugo Montanari and Donald Sannella
Volume4661
Page(s)263--280
Year2007
PublisherSpringer
URLhttp://www.di.unito.it/~dezani/papers/main-xdp.pdf
Abstract
We describe a type system for the X calculus. An X-network is a network of locations, where each location consists of both a data tree (which contains scripts and pointers to nodes in trees at different locations) and a process, for modelling process interaction, process migration and interaction between processes and data. Our type system is based on types for locations, trees and processes, expressing security levels. The type system enjoys type preservation under reduction (subject reduction). In consequence of subject reduction we prove the following security properties. In a well-typed X-network, data in a location are accessible only to processes in locations of equal or higher security level. Moreover, processes originating in a location can only go to locations of equal or less security level, with the exception of movements which are returns to the ``initial'' location.

BibTeX code

@inproceedings{dezaghilpant06,
  volume = {4661},
  author = {Mariangiola Dezani-Ciancaglini and Silvia Ghilezan and Jovanka
            Pantovic},
  series = {LNCS},
  booktitle = {TGC'06},
  editor = {Roberto Bruni and Ugo Montanari and Donald Sannella},
  url = {http://www.di.unito.it/~dezani/papers/main-xdp.pdf},
  title = {{Security Types for Dynamic Web Data}},
  abstract = {We describe a type system for the X$d\pi$ calculus. An
              X$d\pi$-network is a network of locations, where each location
              consists of both a data tree (which contains scripts and pointers
              to nodes in trees at different locations) and a process, for
              modelling process interaction, process migration and interaction
              between processes and data. Our type system is based on types for
              locations, trees and processes, expressing security levels. The
              type system enjoys type preservation under reduction (subject
              reduction). In consequence of subject reduction we prove the
              following security properties. In a well-typed X$d\pi$-network,
              data in a location are accessible only to processes in locations
              of equal or higher security level. Moreover, processes originating
              in a location can only go to locations of equal or less security
              level, with the exception of movements which are returns to the
              ``initial'' location.},
  publisher = {Springer},
  year = {2007},
  pages = {263--280},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)

Valid HTML 4.01!