A framework for the modeling and synthesis of security automata based on process algebras (Rapporti tecnici, manuali, carte geologiche e tematiche e prodotti multimediali)

Type
Label
  • A framework for the modeling and synthesis of security automata based on process algebras (Rapporti tecnici, manuali, carte geologiche e tematiche e prodotti multimediali) (literal)
Anno
  • 2007-01-01T00:00:00+01:00 (literal)
Alternative label
  • Martinelli F., Matteucci I. (2007)
    A framework for the modeling and synthesis of security automata based on process algebras
    (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori
  • Martinelli F., Matteucci I. (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#altreInformazioni
  • http://puma.isti.cnr.it//linkdoc.php?idauth=18&idcol=17&icode=2007-TR-004&authority=cnr.iit&collection=cnr.iit&langver=it (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#note
  • rapporti tecnici IIT 2007-TR-004 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#descrizioneSinteticaDelProdotto
  • In this paper we present our approach for the modeling and the synthesis of enforcement mechanismsthat are mechanism able to force security policies. In particular, starting from the definition of security automata introduced in the literature by Schneider, Ligatti et al., we define a set of process algebra operators, said controller operators, able to mimic the security automata's behavior. Hence we present semantics definitions of four different controller operators that act by monitoring possible un-trusted component of a given system. They guarantee that the whole system is secure, i.e. it works as prescribed by a given security policy. We also present our theory for automatically building a process that is a controller program for a chosen controller operator. By exploiting satisfiability results on temporal logic we have developed a tool that generates such processes. The tool implements the partial model checking technique and a satisfiability procedure for a modal ¹-calculus formula. We then present how it is possible to extend our approach in a timed setting and to deal with parameterized systems. (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#supporto
  • Altro (literal)
Titolo
  • A framework for the modeling and synthesis of security automata based on process algebras (literal)
Prodotto di
Autore CNR
Insieme di parole chiave

Incoming links:


Prodotto
Autore CNR di
Insieme di parole chiave di
data.CNR.it