Detail publikace

A Formal Model for Network-wide Security Analysis

Originální název

A Formal Model for Network-wide Security Analysis

Anglický název

A Formal Model for Network-wide Security Analysis

Jazyk

en

Originální abstrakt

Network designers perform challenging tasks with so many configuration options that it is often hard or even impossible for a human to predict all potentially dangerous situations. In this paper, we introduce a formal method approach for verification of security constraints on networks with dynamic routing protocols in use. A unifying model based on packet-filters is employed for modelling of network behaviour. Over this graph model augmented with filtering rules over edges verification of  reachability properties can be made. In our approach we also consider topology changes caused by dynamic routing protocols.

Anglický abstrakt

Network designers perform challenging tasks with so many configuration options that it is often hard or even impossible for a human to predict all potentially dangerous situations. In this paper, we introduce a formal method approach for verification of security constraints on networks with dynamic routing protocols in use. A unifying model based on packet-filters is employed for modelling of network behaviour. Over this graph model augmented with filtering rules over edges verification of  reachability properties can be made. In our approach we also consider topology changes caused by dynamic routing protocols.

BibTex


@inproceedings{BUT27706,
  author="Petr {Matoušek} and Ondřej {Ryšavý} and Jaroslav {Ráb} and Miroslav {Švéda}",
  title="A Formal Model for Network-wide Security Analysis",
  annote="Network designers perform challenging tasks with so many configuration options
that it is often hard or even impossible for a human to predict all potentially
dangerous situations. In this paper, we introduce a formal method approach for
verification of security constraints on networks with dynamic routing protocols
in use. A unifying model based on packet-filters is employed for
modelling of network behaviour. Over this graph model augmented with filtering
rules over edges verification of  reachability properties can be made. In our
approach we also consider topology changes caused by dynamic routing protocols.",
  address="University of Ulster",
  booktitle="Proceeding of the 15 IEEE International Symposium and Workshop on the Engineering of Computer-based Systems",
  chapter="27706",
  edition="NEUVEDEN",
  howpublished="print",
  institution="University of Ulster",
  year="2008",
  month="march",
  pages="171--181",
  publisher="University of Ulster",
  type="conference paper"
}