ASPIER: An Automated Framework for Verifying Security Protocol Implementations

Sagar Chaki, Anupam Datta, Proceedings of the 22nd IEEE Computer Security Foundations (CSF) Symposium, page 172-185, July 8-10, 2009.

Abstract: We present ASPIER -- the first framework that combines software model checking with a standard protocol security model to automatically analyze authentication and secrecy properties of protocol implementations in C. The technical approach extends the iterative abstraction-refinement methodology for software model checking with a domain-specific protocol and symbolic attacker model. We have implemented the ASPIER tool and used it to verify authentication and secrecy properties of a part of an industrial strength protocol implementation -- the handshake in OpenSSL -- for configurations consisting of up to 3 servers and 3 clients. We have also implemented two distinct methods for reasoning about attacker message derivations, and evaluated them in the context of OpenSSL verification. ASPIER detected the version-rollback vulnerability in OpenSSL 0.9.6c source code and successfully verified the implementation when clients and servers are only willing to run SSL 3.0.

PDF