Remotely-launched software exploits are a common way for attackers to intrude into vulnerable computer systems. As detection techniques improve, remote exploitation techniques are also evolving. Recent techniques for evasion of exploit detection include polymorphism (code encryption) and meta-morphism (code obfuscation). This paper addresses the problem of detecting in network traffic polymorphic remote exploits that are encrypted, and that self-decrypt before launching the intrusion. Such exploits pose a great challenge to existing malware detection techniques, partly due to the non-obvious starting location of the exploit code in the network payload.We describe a new method for detecting self-decrypting exploit codes. This method scans network traffic for the presence of a decryption routine, which is characteristic of such exploits. The proposed method uses static analysis and emulated instruction execution techniques. This improves the accuracy of determining the starting location and instructions of the decryption routine, even if self-modifying code is used. The method outperforms approaches that have been previously proposed, both in terms of detection capabilities, and in detection accuracy.The proposed method has been implemented and tested on current polymorphic exploits, including ones generated by state-of-the-art polymorphic engines. All exploits have been detected (i.e., a 100% detection rate), including those for which the decryption routine is dynamically coded, or self-modifying. The false positive rate is close to 0%. Running time is approximately linear in the size of the network payload being analyzed.

Regulatory agencies, such as US FDA, and other third party reviewers of software have the task of comprehending apiece of software in the event of its failure. Program slicing is the preferred technique to analyze software failures. However, program slicing might yield extremely large slices and also demand that an user have intimate knowledge of the software (by specifying a slicing criterion). In this paper we propose solutions to ameliorate both of these problems. The main hypothesis of the paper is that error reports can be used to generate slicing criteria, thus allowing a third-party reviewer to use slicing without any knowledge of the system being analyzed. The first contribution of the paper is a study of how error reports can be formalized and how execution sequences (called error traces) that satisfy an error report can be identified, which can then be sliced. A primary feature of this work is that incomplete error reports could be dealt with. The second contribution of the paper is a scheme for using abstract interpretation in the generation of error traces and (potential) slicing criteria from error reports. These "abstract" error traces can be sliced, much like in dynamic/conditional slicing, with respect to the criteria generated, allowing for inputs to be used to reduce the size of slices. Furthermore, being abstract in nature, they are shorter than exact execution sequences and also allow for easier comprehension. We finally present a case study involving a medical device that illustrates how our approach can aid with program comprehension.

In this paper we explore a method for carrying out pre-market analysis of software designs and implementations, based on formal-methods techniques, to aid the process of reviewing software in medical devices. We discuss a methodology to validate medical device software with the help of formal methods based usage models, and test cases derived from such models. We present a case study involving the design and verification of a generic infusion pump usage model, detailing how the various stages of our approach can be carried out. Finally, we present experimental results and effort estimates to show that the proposed methodology is effective and feasible

Post-mortem analysis - the process of tracing software failure to source code - is an important means for maintenance engineers and regulatory reviewers for establishing the cause of an error. Historically, static slicing techniques have been used for aiding post-mortem fault analysis. However, the slices obtained in this manner can often be too large and may not give a clear understanding of the code when dealing with complex reactive systems. We propose using model abstraction in conjunction with slicing to ameliorate the problem of understanding large slices. Combining slicing with abstraction provides the analyst with an integrated cognition model, leading to a better understanding of the code, and consequently more efficient error analysis. We formalize this concept through the notion of abstraction-driven slicing, and use it to develop CAdS, an automated tool to aid postmortem error detection in C programs using abstraction-driven static slicing. We list our experiences with CAdS and illustrate how it can be used to reduce effort involved in the postmortem analysis process

We consider the problem of verifying correctness of finite state machines that communicate with each other over unbounded FIFO channels that are unreliable. Various problems regarding verification of FIFO channels that can lose messages have been considered by Finkel [10], and by Abdulla and Johnson [1, 2]. We consider, in this paper, other possible unreliable behaviors of communication channels, viz. (a) duplication and (b) insertion errors. Furthermore, we also consider various combinations of duplication, insertion and lossiness errors.Finite state machines that communicate over unbounded FIFO buffers is a model of computation that forms the backbone of ISO standard protocol specification languages Estelle and SDL. While an assumption of a perfect communication medium is reasonable at the higher levels of the OSI protocol stack, the lower levels have to deal with an unreliable communication medium; hence our motivation for the present work.The verification problems that are of interest are reachability, unboundedness, deadlock, and model-checking against CTL. All of these problems are undecidable for machines communicating over reliable unbounded FIFO channels. So, it is perhaps surprising that some of these problems become decidable when unreliable channels are modeled. The contributions of this paper are: (a) An investigation of solutions to these problems for machines with insertion errors, duplication errors, or a combination of duplication, insertion and lossiness errors, and (b) A comparison of the relative expressive power of the various errors.

Let ( F'l, Pz, . . . .Pm) be a network of n finite state machines, communicating with each other asynchronously using typed messages over unbounded FIFO channels, In this paper we present a data flow approach to analyzing these communicating machines for nonprogress properties (deadlock and unspecified reception).We set up flow equations to compute the set of pending messages in the queues at any given state of such a network, The central technical contribution of this paper is an algorithm to compute approximations to solutions for the ensuing equations We then show how these approximate solutions can be used to check that interactions between the processes are free of nonprogress errors.We conclude with a number of example protocols that our algorithm certifies to be free of nonprog-ess errors.Included in the examples is a specification of X25 call establishment/clear protocol,

The problem of testing two processes (specified as finite-state machines) communicating asynchronously with each other using send and receive commands over a set of message types is considered for two forms of nonprogress: deadlock and unspecified reception. Since the nonprogress problem is undecidable, a dataflow approach is used to obtain sufficient conditions under which the two processes are free of deadlock and unspecified reception. The approximation analysis is based on weakening the receive operation. Polynomial time algorithms are presented to perform the analysis. This problem arises in the context of dataflow analysis of the processes that communicate by message passing and in the context of showing correctness of protocol specifications. Diagrams are provided for some networks that can be certified to be free of unspecified receptions using the algorithms. The problem of testing for deadlock in more than two processes still remains open.>

Certain aspects of the behavior of concurrent systems are intrinsically probabilistic in nature, e.g., the behavior of imperfect communication media used in network protocols. We address the problem of expressing such behavior in an algebraic calculus for communicating systems. The introduction of probabilistic information in the calculus alleviates the problem of proving liveness, as proving liveness now amounts to proving that its probability is 1. A methodology for proving both safety and liveness is developed and used in proving the correctness of the Alternating Bit Protocol.