Warning: pg_query(): Query failed: ERROR: missing chunk number 0 for toast value 29512337 in pg_toast_2619 in /dati/webiit-old/includes/database.pgsql.inc on line 138 Warning: ERROR: missing chunk number 0 for toast value 29512337 in pg_toast_2619 query: SELECT data, created, headers, expire, serialized FROM cache_page WHERE cid = 'https://www-old.iit.cnr.it/node/1139' in /dati/webiit-old/includes/database.pgsql.inc on line 159 Warning: pg_query(): Query failed: ERROR: missing chunk number 0 for toast value 29512337 in pg_toast_2619 in /dati/webiit-old/includes/database.pgsql.inc on line 138 Warning: ERROR: missing chunk number 0 for toast value 29512337 in pg_toast_2619 query: SELECT data, created, headers, expire, serialized FROM cache_page WHERE cid = 'https://www-old.iit.cnr.it/node/1139' in /dati/webiit-old/includes/database.pgsql.inc on line 159 A framework for the modeling and synthesis of security automata based on process algebras | IIT - CNR - Istituto di Informatica e Telematica
IIT Home Page CNR Home Page

A framework for the modeling and synthesis of security automata based on process algebras

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.


2007

Autori: Martinelli F., Matteucci I.
Autori IIT:

Tipo: Rapporti tecnici, manuali, carte geologiche e tematiche e prodotti multimediali
Area di disciplina: Information Technology and Communication Systems
rapporti tecnici IIT 2007-TR-004
Attività: Metodi formali per la sicurezza di sistemi ICT