Table of Contents
Formal Specification and Verification Techniques in Computer Security
Talk Outline
Motivation
How to Defend Against Attacks
Vulnerabilities in Computer Systems
How to Defend Against Attacks
Enforcing Secure Behaviors
Intrusion Detection Approaches
Protected System Model
Our Approach
Specification Language
Specification Language -- Patterns
Example Specifications
Example Specifications
Research Issues -- Conflicts Among Rules
Research Issues -- Interfacing to Multiple Data Sources
Interfacing to Packet Data -- Records with Constraints
Type-safety for Packet Data
Interfacing to System Call Data
Research Issues -- Efficient Pattern Matching Algorithms
Efficient Pattern Matching
Compilation of Pattern-Matching
Research Issues -- Interception of System Calls
Key Benefits of Our Approach
Vulnerability Analysis
Vulnerabilities in Computer Systems
Multi-Component Vulnerability Example
Solution
Vulnerability Analysis -- Current Approach
Our Approach
Approach Overview
A Simple Model of a UNIX System
Model of Filesystem
Model of Mailer and Mail Notifier
Vulnerabilities with Comsat
Adding Symbolic Links ...
Adding lpr ...
Rule Generation with Model Checker
Research Issues
Benefits of Our Approach
Detection System Model
Intrusion Detection -- Our Approach
Specification Language Overview
Specification Language: Reactions
Example Isolation Specification
Protocol Layering
Putting It All Together
Effectiveness of Approach (Preliminary)
|