Wed Oct 17, 2007, 11:00-12:00, 4549 Boelter Hall

Rule-Based Static Analysis of Network Protocol Implementations

Jeff Foster
University of Maryland

Today's software systems communicate over the Internet using standard
protocols that have been heavily scrutinized, providing some assurance
of resistance to malicious attacks and general robustness.  However,
the software that implements those protocols may still contain
mistakes, and an incorrect implementation could lead to
vulnerabilities even in the most well-understood protocol.  Pistachio
is a novel tool that closes this gap by allowing developers to check
whether the source code implementing a network protocol matches the
protocol's description in an RFC or similar standards document.
Pistachio uses static (compile-time) analysis to reason about C source
code, and includes a rule-based specification language to describe
protocols.  Rules capture what should happen during each round of
communication, and can be used to enforce constraints on ordering of
operations and on data values.  Pistachio is not guaranteed sound due
to some heuristic approximations it makes, but has a low false
negative rate in practice when compared to known bug reports.  We have
applied Pistachio to two different implementations of SSH2 and an
implementation of RCP.  Pistachio discovered a multitude of bugs,
including security vulnerabilities, that were confirmed against each
project's bug databases.

About the speaker:  
Jeff Foster is an Assistant Professor in the Computer Science 
Department and UMIACS at the University of Maryland, College Park.  
He is a member of the programming languages group at Maryland, 
and also part of CHESS.  The goal of Jeff Foster's research 
is to develop practical tools and techniques to improve 
software quality.  He is interested in programming languages, 
software engineering, advanced static type systems, scalable 
constraint-based analysis, and building tools that implement his ideas. 
In the past he worked on the BANE Project and was a member of the 
Open Source Quality Project.  As part of his research he has developed 
cqual, a tool for adding type qualifiers to C programs.

Host: Jens Palsberg