Intrusion detection via static analysis
Published 13 November 2002
David Wagner, Ralph A. Dean
Citations647
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
It is shown how static analysis may be used to automatically derive a model of application behavior and the result is a host-based intrusion detection system with three advantages: a high degree of automation, protection against a broad class of attacks based on corrupted code, and the elimination of false alarms.
Abstract
One of the primary challenges in intrusion detection is modelling typical application behavior so that we can recognize attacks by their atypical effects without raising too many false alarms. We show how static analysis may be used to automatically derive a model of application behavior. The result is a host-based intrusion detection system with three advantages: a high degree of automation, protection against a broad class of attacks based on corrupted code, and the elimination of false alarms. We report on our experience with a prototype implementation of this technique.
Keywords
Computer Science
Mathematics and Computers in SimulationIntroduction to automata theory, languages and computation
10,827 Citations1981
IEEE Transactions on Software EngineeringAn Intrusion-Detection Model
3,358 Citations1987Dorothy E. Denning
Proof-carrying code
1,807 Citations1997George C. Necula
It is shown in this paper how proof-carrying code might be used to develop safe assembly-language extensions of ML programs and the adequacy of concrete representations for the safety policy, the safety proofs, and the proof validation is proved.
Communications of the ACMA note on the confinement problem
1,419 Citations1973Butler Lampson
A set of examples attempts to stake out the boundaries of the problem by defining a program during its execution so that it cannot transmit information to any other program except its caller.
ACM Transactions on Information and System SecurityEnforceable security policies
1,266 Citations2000Fred B. Schneider
Precise interprocedural dataflow analysis via graph reachability
1,135 Citations1995Thomas Reps, Susan Horwitz +1 more
The paper shows how a large class of interprocedural dataflow-analysis problems can be solved precisely in polynomial time by transforming them into a special kind of graph-reachability problem.
Points-to analysis in almost linear time
1,074 Citations1996Bjarne Steensgaard
This is the asymptotically fastest non-trivial interprocedural points-to analysis algorithm yet described and is based on a non-standard type system for describing a universally valid storage shape graph for a program in linear space.
IEEE Transactions on Software EngineeringDynamically discovering likely program invariants to support program evolution
1,039 Citations2001Michael D. Ernst, Jake Cockrell +2 more
Information and ControlRecognition and parsing of context-free languages in time n3
947 Citations1967D. H. Younger
A recognition algorithm is exhibited whereby an arbitrary string over a given vocabulary can be tested for containment in a given context-free language and it is shown that it is completed in a number of steps proportional to the “cube” of the number of symbols in the tested string.
A sense of self for Unix processes
838 Citations2002Stephanie Forrest, Steven Hofmeyr +2 more
A method for anomaly detection is introduced in which "normal" is defined by short-range correlations in a process' system calls, and initial experiments suggest that the definition is stable during normal behaviour for standard UNIX programs.
Communications of the ACMAn efficient context-free parsing algorithm
817 Citations1970Jay Earley
A parsing algorithm which seems to be the most efficient general context-free algorithm known is described and appears to be superior to the top-down and bottom-up algorithms studied by Griffiths and Petrick.
Munich Personal RePEc Archive (Ludwig Maximilian University of Munich)Insertion, Evasion, and Denial of Service: Eluding Network Intrusion Detection
655 Citations1998Thomas H. Ptacek, Timothy N. Newsham
Three classes of attacks which exploit fundamentally problems with the reliability of passive protocol analysis are defined--insertion, evasion and denial of service attacks--and how to apply these three types of attacks to IP and TCP protocol analysis is described.
A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities.
612 Citations2000David Wagner, Jeffrey S. Foster +2 more
The design and prototype of a new technique for finding potential buffer overrun vulnerabilities in security-critical C code are implemented and used to find new remotely-exploitable vulnerabilities in a large, widely deployed software package.
ACM Transactions on Programming Languages and SystemsFrom system F to typed assembly language
587 Citations1999Greg Morrisett, David Walker +2 more
The compiler and typed assembly lanugage provide a fully automatic way to produce certified code, suitable for use in systems where unstrusted and potentially malicious code must be checked for safety before execution.
Context-sensitive interprocedural points-to analysis in the presence of function pointers
573 Citations1994Maryam Emami, Rakesh Ghiya +1 more
This paper reports on the design, implementation, and empirical results of a new method for dealing with the aliasing problem in C based on approximating the points-to relationships between accessible stack locations that allows the smooth integration for handling general function pointers in C.
The SLam calculus
410 Citations1998Nevin Heintze, Jon G. Riecke
It is proved that the type system prevents security violations and some examples of its power are given.
USENIX Security SymposiumA secure environment for untrusted helper applications confining the Wily Hacker
391 Citations1996Ian Goldberg, David Wagner +2 more
It is found that with the completion of two writing assignments within a four-week period, students demonstrated a significantly greater ability to analyze the evidence within the claims.
Buffer overflows: attacks and defenses for the vulnerability of the decade
372 Citations2002Crispin Cowan, F. Wagle +3 more
This work surveys the various types of buffer overflow vulnerabilities and attacks and surveys the various defensive measures that mitigate buffer overflow vulnerabilities, including the various defensive measures that mitigate buffer overflow vulnerabilities, including StackGuard method.
Execution monitoring of security-critical programs in distributed systems: a specification-based approach
326 Citations2002Calvin Ko, Manfred Ruschitzka +1 more
A formal framework for specifying the security-relevant behavior of programs is developed, on which a real-time intrusion detection system for a distributed system is based, and security specifications for 15 Unix setuid root programs are written.
The base-rate fallacy and its implications for the difficulty of intrusion detection
313 Citations1999Stefan Axelsson
This paper aims to demonstrate that, for a reasonable set of assumptions, the false alarm rate is the limiting factor for the performance of an intrusion detection system.
Lecture notes in computer scienceRegular Model Checking
287 Citations2000Ahmed Bouajjani, Bengt Jönsson +2 more
Regular model checking is presented, a framework for algorithmic verification of infinite-state systems with, e.g., queues, stacks, integers, or a parameterized linear topology, by computation of the transitive closure of a transition relation.
Fast and accurate flow-insensitive points-to analysis
249 Citations1997Marc Shapiro, Susan Horwitz
This paper addresses techniques for flow- and context-insensitive interprocedural analysis of stack-based storage, and defines two new algorithms that are significantly more accurate than Steensgaard's algorithm, and significantly faster than Andersen's algorithm on large programs.
ACM Transactions on Programming Languages and SystemsAn Improved Context-Free Recognizer
217 Citations1980Susan L. Graham, Michael A. Harrison +1 more
Surprisingly close connections between the Cocke-Kasami-Younger and Earley algorithms are established which reveal that the two algorithms are “almost” identical.
Automated detection of vulnerabilities in privileged programs by execution monitoring
209 Citations2002Calvin Ko, G. Fink +1 more
By tightly restricting the behavior of all privileged programs, exploitations of unknown vulnerabilities can be detected by monitoring their execution using audit trails, and a program policy specification language is described, which is based on simple predicate logic and regular expressions.
Buffer overflows: attacks and defenses for the vulnerability of the decade
199 Citations2004Crispin Cowan, Perry Wagle +3 more
This work surveys the various types of buffer overflow vulnerabilities and attacks and surveys the various defensive measures that mitigate buffer overflow vulnerabilities, including the various defensive measures that mitigate buffer overflow vulnerabilities, including StackGuard method.
An efficient augmented-context-free parsing algorithm
195 Citations1987Masaru Tomita
Data flow analysis is model checking of abstract interpretations
187 Citations1998David A. Schmidt
This expository paper simplifies and clarifies Steffen's depiction of data flow analysis (d.f.a.) as model checking: by employing abstract interpretation (a.i.) to generate program traces and by utilizing Kozen's modal mu-calculus to express trace properties, it is expressed in simplest possible terms that a d.
ORBi (University of Liège)A direct symbolic approach to model checking pushdown systems
178 Citations1997Alain Finkel, Bernard Willems +2 more
Lecture notes in computer scienceVerifying systems with infinite but regular state spaces
158 Citations1998Pierre Wolper, Bernard Boigelot
The goal of this paper is to show that a surprisingly common characteristic of the systems that can be analyzed with this approach is that their state space can be represented as a regular language.
Electronic Notes in Theoretical Computer ScienceA Direct Symbolic Approach to Model Checking Pushdown Systems (extended abstract)
148 Citations1997Alain Finkel, Bernard Willems +1 more
This paper gives a simple and direct algorithm for computing the always regular set of reachable states of a pushdown system and exploits this algorithm for obtaining model checking algorithms for linear-time temporal logic as well as for the logic CTL∗.
Temporal abstract interpretation
118 Citations2000Patrick Cousot, Radhia Cousot
The more classical set-based semantics is shown to be an abstract interpretation of the trace- based semantics which leads to the understanding of model-checking and its application to data-flow analysis as incomplete temporal abstract interpretations.
Enforcing trace properties by program transformation
94 Citations2000Thomas Colcombet, Pascal Fradet
An automatic method to enforce trace properties on programs that integrates static analyses in order to avoid useless transformations and never rejects programs but adds dynamic checks when necessary.
Logic induction of valid behavior specifications for intrusion detection
66 Citations2002Calvin Ko
An automated technique for constructing valid behavior specifications of programs (at the system call level) that are independent of system vulnerabilities and are highly effective in identifying intrusions is introduced.
Operating system enhancements to prevent the misuse of system calls
65 Citations2000Massimo Bernaschi, Emanuele Gabrielli +1 more
A working prototype has been implemented inside the kernel of the Linux operating system, the prototype is able to detect and block also over ow based attacks and provides simple interception of both system calls and their argument values.
Lecture notes in computer scienceA Resolution Principle for a Logic with Restricted Quantifiers
51 Citations1991Hans-Jürgen Bürckert
A logic with restricted quantifiers andEquational constraint theories are presented, showing the role that constraint theories play in the development of logic.
Lecture notes in computer scienceModel checking the full modal mu-calculus for infinite sequential processes
46 Citations1997Olaf Burkart, Bernhard Steffen
Enforceable security policies
45 Citations2004F.B. Schneider
A precise characterization is given for the class of security policies enforceable with mechanisms that work by monitoring system execution, and automata are introduced for specifying exactly that class ofSecurity policies.
Theoretical Computer ScienceModel checking the full modal mu-calculus for infinite sequential processes
36 Citations1999Olaf Burkart, Bernhard Steffen
A new exponential algorithm for model-checking infinite sequential processes, including context-free processes, pushdown processes, and regular graphs, that decides the full modal mu-calculus.
Lecture notes in computer scienceAutomatic Verification of Sequential Infinite-State Processes
12 Citations1997Olaf Burkart
This research presents a meta-analysis of model checking and equivalence checking for pushdown processes and shows clear trends in support of belief-based decision-making in the rapidly changing environment.