Show simple item record

dc.contributor.authorBradley, Adam D.en_US
dc.contributor.authorBestavros, Azeren_US
dc.contributor.authorKfoury, Assaf J.en_US
dc.date.accessioned2011-10-20T04:42:44Z
dc.date.available2011-10-20T04:42:44Z
dc.date.issued2002-05-22
dc.identifier.urihttps://hdl.handle.net/2144/1663
dc.description.abstractAs new multi-party edge services are deployed on the Internet, application-layer protocols with complex communication models and event dependencies are increasingly being specified and adopted. To ensure that such protocols (and compositions thereof with existing protocols) do not result in undesirable behaviors (e.g., livelocks) there needs to be a methodology for the automated checking of the "safety" of these protocols. In this paper, we present ingredients of such a methodology. Specifically, we show how SPIN, a tool from the formal systems verification community, can be used to quickly identify problematic behaviors of application-layer protocols with non-trivial communication models—such as HTTP with the addition of the "100 Continue" mechanism. As a case study, we examine several versions of the specification for the Continue mechanism; our experiments mechanically uncovered multi-version interoperability problems, including some which motivated revisions of HTTP/1.1 and some which persist even with the current version of the protocol. One such problem resembles a classic degradation-of-service attack, but can arise between well-meaning peers. We also discuss how the methods we employ can be used to make explicit the requirements for hardening a protocol's implementation against potentially malicious peers, and for verifying an implementation's interoperability with the full range of allowable peer behaviors.en_US
dc.description.sponsorshipNational Science Foundation (ANI-9986397, CCR-9988529, ITR-0113193); GAANN Fellowship, U.S. Department of Educationen_US
dc.language.isoen_US
dc.publisherBoston University Computer Science Departmenten_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-2002-017
dc.subjectFormal verificationen_US
dc.subjectHTTPen_US
dc.subjectInteroperabilityen_US
dc.subjectModel checkingen_US
dc.subjectProtocol compositionen_US
dc.titleSafe Composition of Web Communication Protocols for Extensible Edge Servicesen_US
dc.typeTechnical Reporten_US


This item appears in the following Collection(s)

Show simple item record