Computer Security and Cryptography Seminar:
October 2004 Events

I present work by Lap Chung Lam and Tzi-Cker Chiueh that appeared at RAID 2004. You have likely heard previous talks about my own work: using static binary analysis to build models of correct program execution. Here is an opportunity to learn about another approach to model construction. This will be an informal discussion; come ready to critique and brainstorm.

The paper describes the design, implementation, and evaluation of a "program semantics-aware intrusion detection system" called Paid, which automatically derives an application-specific system call behavior model from the application's source code and checks the application's run-time system call pattern against this model to thware any control hijacking attacks. The per-application behavior model is in the form of the sites and orderings of system calls made in the application, as well as its partial control flow.

This is a survey of protocol verification techniques that extend the well-known Dolev-Yao intruder model. We will mainly summarize work presented in two papers presented at the 2003 IEEE Symposium on Logic in Computer Science (LICS 2003):

• H. Comon and V. Shmatikov. Intruder deductions, constraint solving and insecurity decision in presence of exclusive or.
• Y. Chevalier and R. Kusters and M. Rusinowitch and M. Turuani. An NP decision procedure for protocol insecurity with XOR.

The presentation style will be informal. Brainstorming is welcome, and encouraged. The talk will assume no prior knowledge of the area.