Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Network Semantics
Network Semantics
Network programming is complex: one has to deal with a variety of
protocols (IP, ICMP, UDP, TCP etc), concurrency, packet loss, host
failure, timeouts, the Sockets API for the protocols, and
subtle portability issues.
The protocols are typically described in RFCs using informal prose and
pseudocode to characterise the behaviour of the systems involved.
That informality has benefits, but inevitably these descriptions
are somewhat ambiguous and incomplete.
The protocols are hard to design and implement correctly; testing conformance
against the standards is challenging; and understanding the many obscure
corner cases and the failure semantics requires considerable expertise.
Ideally we would have the best of both worlds:
protocol descriptions that
are simultaneously:
clear, accessible to a broad community and easy to modify;
unambiguous, characterising exactly what behaviour is specified;
sufficiently loose, characterising exactly what is not specified,
and hence what is left to implementors (especially,
permitting high-performance implementations without over-constraining
their structure); and
directly usable as a basis for conformance testing, not
read-and-forget documents.
In this work we have established a practical
technique for rigorous protocol specification, in HOL,
that makes this ideal attainable for
protocols as complex as TCP.
We describe specification idioms that are rich enough to express the
subtleties of TCP endpoint behaviour and that scale to the full
protocol, all while remaining readable. We also describe novel
tools for automated conformance testing between specifications and
real-world implementations.
To develop the technique, and to demonstrate its feasibility, we have
produced a post-hoc specification of existing protocols: a
mathematically rigorous and experimentally-validated characterisation
of the behaviour of TCP, UDP, and the Sockets API, as implemented in
practice, at both protocol and service levels of abstraction.
The resulting specifications may be useful in their own right in several
ways. They have been extensively annotated
to make it usable as a reference for TCP/IP stack
implementors and Sockets API users, supplementing the existing
informal standards and texts. They can also provide a basis for
high-fidelity conformance testing of future implementations, and a
basis for design (and conceivably formal proof) of higher-level
communication layers.
Perhaps more significantly, the work
demonstrates that
it would be feasible to carry out
similar rigorous
specification work for new protocols, in
a tolerably light-weight style, both at design-time and during standardisation.
We believe the increased
clarity and precision over informal specifications, and the possibility of automated specification-based testing,
would make this very much worthwhile, leading to
clearer protocol designs and higher-quality implementations.
We discuss some simple ways
in which protocols could be
designed to make testing computationally straightforward.
Protocol-Level TCP Specification
A theory-oriented description of the specification idioms and symbolic
model-checking technology used for the protocol-level specification of
TCP:
A poster with a version of the `TCP state diagram' extracted from the
specification. This is rather more complete than the
usual diagram,
but is still a very abstract and simplified view of the specification
state space. It is intended to be printed at A1 size or bigger:
Peng Li, a PhD student
with Steve Zdancewic,
used the specification as the basis for a purely functional Haskell
implementation of a TCP stack for a web server. Here is
The following demonstrates the feasibility of completely formal
reasoning (in the Isabelle proof assistant) about executable code
in a fragment of OCaml above the UDP specification:
Here are papers about our earlier work focussing just on UDP, ICMP, and the
Sockets API. The first technical report and TACS paper describe a
model without time, threads, or modules, and using informal
mathematics. The ESOP paper reports on a HOL specification extended
to cover those three aspects. The SIGOPS EW paper is a position paper
reflecting on the experience of this and of Norrish's C semantics work.
This work has been funded by
an EPSRC Leadership Fellowship and a Royal Society University Research
Fellowship (Sewell),
a St Catharine's College Heller Research
Fellowship (Wansbrough),
EPSRC grant GR/N24872 Wide-area programming: Language, Semantics
and Infrastructure Design,
EPSRC grant EP/C510712 NETSEM: Rigorous Semantics for Real Systems,
EC FET-GC project IST-2001-33234 PEPITO
Peer-to-Peer Computing: Implementation and Theory,
CMI UROP internship support (Smith), and
EC Thematic Network IST-2001-38957 APPSEM 2.
National ICT Australia is funded by the Australian Government's
Backing Australia's Ability initiative, in part through the
Australian Research Council.