Using Behavior Specifications

lora

Hypothesizing Program Properties. [1] describes a technique for automatically extracting likely program properties from execution traces. However, it relies on humans to specify regions within a trace where such property extraction will be attempted.  This contrasts with our technique, which is fully automated.  [24] has similar goals, but is fully automated.  The primary difference with our technique is that they focus on invariant properties, whereas our algorithm is focused on trace properties. Technically,  the two problems are quite different, requiring different techniques to be employed. For instance, algorithms for learning invariants can be speeded up by exploiting transitivity, i.e., if p holds and p ! q, then we need not explicitly verify q. Unfortunately, this is not true for trace properties.
Mobile Code Security. [27] presents an approach called model-carrying code (MCC) for mobile code security. The main components of MCC are: (a) a policy language for specifying security policies and a compiler for this language, (b) a language for specifying program behavior models and techniques for extracting them, and (c) a policy refinement component that is based on model-checking techniques.  The paper provides a short overview of each of these areas and reports on implementation experience with MCC.
The idea of learning relationships between system call arguments is borrowed from [27], as are the suggestions for using trie data structures for speeding up search operations involving strings. However, [27]  does not provide a detailed algorithm for learning relationships,  perhaps due to its focus on describing a large system. In contrast, this paper provides a careful treatment of the learning algorithm and discusses its runtime complexity, as well as implementation performance. Moreover, this is the first paper to provide a formal treatment of data flow properties on system call traces. By doing so, we been able to parameterize our learning algorithm with respect to relations of interest. Moreover, the approach presented  in this paper can be uniformly applied to most existing techniques for learning control-flow models,  whereas the [27] approach is limited to FSA.  Another important practical advance in this paper is that of developing models that capture dependence on program environment, including command-line argument, environment variables, and so on. Most importantly, the focus of this paper is on intrusion detection, demonstrating the ability of our technique to detect a wide range of attacks, and provide significantly enhanced precision over previous techniques.