Specifying and Analyzing Security Automata

Relatore
David Basin - Department of Computer Science, ETH Zurich

Data e ora
lunedì 17 settembre 2007 alle ore 16.00

Luogo
Ca' Vignal 3 - Piramide, Piano 0, Sala Verde

Referente

Referente esterno

Data pubblicazione
12 settembre 2007

Dipartimento
 

Riassunto

Security automata are a variant of Buechi automata used to
specify security policies that can be enforced by monitoring system
execution.  We propose using CSP-OZ for specifying security automata,
formalizing their combination with target systems, and analyzing the
security of the resulting system specifications.  CSP-OZ is a rich
specification language that combines Communicating Sequential Processes
(CSP) and Object-Z (OZ).  Our thesis is that this language is very well
suited for specifying and reasoning about complex security automata and
their combination with large-scale systems. This includes the ability to
specify concisely complex operations and complex control, support for
structured specifications, refinement, and transformational design, as
well as automated, tool supported analysis.  We present two case
studies, which provide support for this thesis.

ornamento
Inizio pagina