A rule-based static analysis tool for network protocol implementations
[Overview | Current activities | Papers | Download | People]
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. The goal of PISTACHIO is to close the gap by introducing a new technique for checking that a C implementation of a protocol matches its description in an RFC or similar document. Rules are used to describe what should happen in every round of communication and to enforce constraints on ordering of operations and data values. PISTACHIO has proved successfull on the LSH implementation of SSH2 and the RCP implementation which is part of Cygwin's netutils package and is currently being run against the OpenSSH implementation of SSH2.
PISTACHIO has been applied successfully to two protocol implementations - the LSH implementation of SSH2 and the RCP implementation which is part of Cygwin's netutils package. We are currently running PISTACHIO on the OpenSSH implementation of SSH2 and plan to experiment on other protocols as well.
Last update: May 23, 2007.
This page is maintained by Octavian Udrea.
For questions or comments about PISTACHIO, send email to udrea at cs.umd.edu.