author = {Wolfgang Schreiner},
title = {{Generating Network Monitors from Logic Specifications}},
language = {english},
abstract = { Current approaches to ensuring network security mainly rely on hardware or software-based firewalls that monitor the IP traffic and decide by a set of rules whether an IP packet is to be forwarded or not. These rules are based on simple criteria such as protocol type, IP address and port, and other attributes that can be extracted from the packet headers, possibly taking into account the set of currently open TCP connections. More sophisticated systems to intrusion detection and prevention apply deep packet inspection to consider also the transmitted content; furthermore, their decisions may be based on matching the traffic against predetermined signatures of known attacks or on applying statistical analysis to identify traffic anomalies by comparison with the characteristics of normal traffic. Still these mechanisms are quite crude; to detect certain attacks, in general more specific monitors have to be manually programmed. We report on a project that pursues another approach where safety properties of network traffic is specified in an abstract but expressive form by logic formulas. These specifications are automatically translated to programs that monitor the network for compliance with the specification; thus no low-level and error-prone manual coding of network monitors is required. The formalism is based on classical predicate logic where the network traffic is considered as an indexed sequence of messages; by quantification over indices it is possible to describe the desired network behavior. In order to transform the raw packet sequence to the appropriate level of abstraction, the specification language supports the definition of virtual streams by constructions analogous to classical set builder notation. This formalism is very general and allows to express various kinds of properties; the challenge is to devise a translation into efficient monitors that operate within limited time and space bounds, respectively to identify language subsets for which such a translation is possible. The project is pursued in a cooperation between an academic institution, an industrial software company, and a leading manufacturer of high-quality integrated security solutions.},
year = {2012},
month = {December 18},
note = {Invited talk at t FIT 2012, 10th International Conference on Frontiers of Information Technology, Islamabad, Pakistan},
institution = {COMSATS Institute of Information Technology},
conferencename = {t FIT 2012, 10th International Conference on Frontiers of Information Technology, Islamabad, Pakistan},
url = {http://fit.edu.pk/index.php?option=com_content&view=article&id=116}