Specifying and Analyzing Security Automata

David Basin - Department of Computer Science, ETH Zurich
Data e ora
lunedì 17 settembre 2007 alle ore 16.00
Ca' Vignal - Piramide, Piano 0, Sala Verde
Referente esterno
Data pubblicazione
12 settembre 2007


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.

© 2002 - 2021  Universit√† degli studi di Verona
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234