کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
426596 686119 2008 28 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Rule-based static analysis of network protocol implementations
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Rule-based static analysis of network protocol implementations
چکیده انگلیسی

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 this work is to close this gap by introducing a new technique for checking that a C implementation of a protocol matches its description in an RFC or similar standards document. We present a static (compile-time) source code analysis tool called Pistachio that checks C code against a rule-based specification of its behavior. Rules describe what should happen during each round of communication, and can be used to enforce constraints on ordering of operations and on data values. Our analysis 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 we confirmed by hand and checked against each project’s bug databases.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 206, Issues 2–4, February–April 2008, Pages 130-157