The traditional approach for establishing the correctness of group communication protocols is through rigorous arguments. While this is a valid approach, the likelihood of subtle errors in the design and implementation of such complex distributed protocols is not negligible. The use of formal verification methods has been widely advocated to instill confidence in the correctness of protocols. In this paper, we describe how we used the SPIN model checker to formally verify a group membership protocol that is part of an intrusion-tolerant group communication system. We describe how we successfully tackled the state-space explosion problem by determining the right abstraction level for formally specifying the protocol. The verification exercise not only formally showed that the protocol satisfies its correctness claims, but also provided information that will help us make the protocol more efficient without violating correctness.

An Anomaly detection sensor, to detect an abnormal use of system resources or an abnormal behavior of authorized users, uses various measures and decides on the basis of threshold value. However, it has high false alarm rate, and it make it hard to merchandise. Also, it is not easy to have a threshold which is suitable for installation environment. In this paper, we propose a method to automatic generation of proper threshold of each sensor, and the threshold is applied for an integrated decision. Also, we propose a computing method for a correlation of heterogeneous detection sensors. As we use the correlation to integrate and decide the opinions of each sensor, false positive can be greatly reduced.

In the Internet, flow analysis and network monitoring have been studied by various methods. Some methods try to make TCP (Transport Control Protocol) traces more readable by showing them graphically. Others such as MRTG, NetScope, and NetFlow read the traffic counters of the routers and record the data for traffic engineering. Even if all of the above methods are useful, they are made only to perform a single task. This paper describes an improved TCP Protocol Machine, a multipurpose tool that can be used for flow analysis, intrusion detection and link congestion monitoring. It is developed based on a finite state machine (automaton). The machine separates the flows into two main groups. If a flow can be mapped to a set of input symbols of the automaton, it is valid, otherwise it is invalid. It can be observed that intruders' attacks are easily detected by the use of the protocol machine. Also link congestion can be monitored, by measuring the percentage of valid flows to the total number of flows. We demonstrate the capability of this tool through measurement and working examples.

The number of computer break-ins from the outside of an organization has increased with the rapid growth of the Internet. Since many intruders from the outside of an organization employ stepping stones, it is difficult to trace back where the real origin of the attack is. Some research projects have proposed tracing methods for DoS attacks and detecting method of stepping stones. It is still difficult to locate the origin of an attack that uses stepping stones. We have developed IDA (Intrusion Detection Agent system), which has an intrusion tracing mechanism in a LAN environment. In this paper, we improve the tracing mechanism so that it can trace back stepping stones attack in the Internet. In our method, the information about tracing stepping stone is collected from hosts in a LAN effectively, and the information is made available at the public information server. A pursuer of stepping stone attack can trace back the intrusion based on the information available at the public information server on an intrusion route.

Many methods have been proposed to detect intrusions; for example, the pattern matching method on known intrusion patterns and the statistical approach to detecting deviation from normal activities. We investigated a new method for detecting intrusions based on the number of system calls during a user's network activity on a host machine. This method attempts to separate intrusions from normal activities by using discriminant analysis, a kind of multivariate analysis. We can detect intrusions by analyzing only 11 system calls occurring on a host machine by discriminant analysis with the Mahalanobis' distance, and can also tell whether an unknown sample is an intrusion. Our approach is a lightweight intrusion detection method, given that it requires only 11 system calls for analysis. Moreover, our approach does not require user profiles or a user activity database in order to detect intrusions. This paper explains our new method for the separation of intrusions and normal behavior by discriminant analysis, and describes the classification method by which to identify an unknown behavior.

The problem of finding the location of the center and the problem of finding the median in a graph are important and basic among many network location problems. In connection with these two problems, the following two theorems are well-known. One is proved by Jordan and Sylvester, and it shows that the center of every tree consists of either one vertex or two adjacent vertices. The other is proved by Jordan and it shows that the centroid (median) of every tree consists of either one vertex or two adjacent vertices. These theorems have been generalized by many researchers so far. Harary and Norman proved that the center of every connected graph G lies in a single block of G. Truszczynski proved that the median of every connected graph G lies in a single block of G. Slater defined k-centrum, which can express both center and median, and proved that the k-centrum of every tree consists of either one vertex or two adjacent vertices. This paper discusses generalization of these theorems. We define the -blocks of a graph G as a generalization of the blocks of G, where is a subset of the vertex set of G; and define the -centroid of G as a generalization of the centroid of G. First, we prove that the -centroid of G is included in an -block of G. This is a generalization of the above theorems concerning centroid, by Jordan and Truszczynski. Secondly, we define the -centrum of G as a generalization of the k-centrum of G and prove some theorems concerning the location of -centrum. Using one of theorems proved here, we can easily obtain the theorem showing that the k-centrum of every connected graph G lies in a single block of G. This theorem is a generalization of the above theorem by Slater.

At the Information-technology Promotion Agency (IPA), we have been developing a network intrusion detection system called IDA (Intrusion Detection Agent system). IDA system has two distinctive features that most conventional intrusion detection systems lack. First, it has a mechanism for tracing the origin of a break-in by means of mobile agents. Second, it has a new and efficient method of detecting intrusions: rather than continuously monitoring the user's activities, it watches for an event that meets the criteria of an MLSI (Mark Left by Suspected Intruders) and may relate to an intrusion. By this method, IDA described herein can reduce the processing overhead of systems and networks. At present, IDA can detect local attacks that are initiated against a machine to which the attacker already has access and he or she attempts to exceed his or her authority. This paper mainly describes how IDA detects local attacks and traces intrusions.

Internet communication is increasingly becoming an important element in daily life. Keeping this network safe from malicious elements is an urgent task for network management. To maintain the security level networks are generally, monitored for indications of usage with ill-intentions. Such indications are events which need to be collated, correlated and analyzed in real-time to be effective. However, on an average medium to large size network the number of such events are very large. This makes it practically impossible to analyze the information in real-time and provide the necessary security measures. In this paper, we propose a mechanism that keeps the number of events, to be analyzed, low thereby making it possible to provide ample security measures. We discuss a real-time Intrusion Detection System (IDS) for detecting network attacks. The system looks out for TCP ACK/RST packets, which are generally caused by network scans. The system can extract the tendency of network flows in real-time, based on the newly developed time-based clustering and Dynamic Access Tree creation techniques. The algorithm, implemented and deployed on a medium size backbone network using RMON (Remote MONitoring) technology, successfully detected 195 intrusion attempts during a one month period. The results of the pilot deployment are discussed. In this paper, the proposal, implementation and evaluation will be described.

Network applications such as FTP, WWW, Mirroring etc. are presently operated with little or no knowledge about the characteristics of the underlying network. These applications could operate more efficiently if the characteristics of the network are known and/or are made available to the concerned application. But network characteristics are hard to come by. The IP Performance Metrics working group (IETF-IPPM-WG) is working on developing a set of metrics that will characterize Internet data delivery services (networks). Some tools are being developed for measurements of these metrics. These generally involve active measurements or require modificationsin applications. Both techniques have their drawbacks. In this work, we show a new and more practical approach of estimating network characteristics. This involves gathering and analyzing the network's experience. The experience is in the form of traffic statistics, information distilled from management related activities and ubiquitously available logs (squid access logs, mail logs, ftp logs etc. ) of network applications. An analysis of this experience provides an estimate of the characteristics of the underlying network. To evaluate the concept we have developed and experimented with a system wherein the network characteristics are generated by analyzing the logs and traffic statistics. The network characteristics are made available to network clients and administrators by Network Performance Metric (NPM) servers. These servers are accessed using standard network management protocols. Results of the evaluation are presented and a framework for efficient operation of network operations, using the network characteristics is outlined.

This paper presents a network surveillance technique for detecting malicious activities. Based on the hypothesis that unusual conducts like system exploitation will trigger an abnormal network pattern, we try to detect this anomalous network traffic pattern as a sign of malicious, or at least suspicious activities. Capturing and analyzing of a network traffic pattern is implemented with a concept of port profiling, where measures representing various characteristics of connections are monitored and recorded for each port. Though the generation of the port profiles requires the minimum calculation and memory, they exhibit high stability and robustness. Each port profile retains the patterns of the corresponding connections precisely, even if the connections demonstrate multi-modal characteristics. By comparing the pattern exhibited by live traffic with the expected behavior recorded in the profile, intrusive activities like compromising backdoors or invoking trojan programs are successfully detected.

The authors propose a method of detecting intruders around power line towers using a new image processing technique. With current technology for outdoor imaging, a varitey of factors may lead to erroneous image processing, such as changes of background brightness, rustling of leaves, mist, rain, intrusion of small animals, etc. These problems were solved as follows. With this method, a change of image, which may indicate an intruder, is first detected using a histogram of the brightness difference between a reference image and an observed image. The detected differences are further analyzed to determine whether they represent a human intruder by evaluating a restraint based on the number, the area, the dimensions of the circumscribing rectangle and the center of gravity of the detected portion. Field testing confirmed the method's usefulness, with a successful intruder detection rate of 82%.