Generating Network Monitors from Logic Specifications

Description

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.

Period	18 Dec 2012
Event title	FIT 2012, 10th International conference on Frontiers of Information Technology
Event type	Conference
Location	PakistanShow on map