─── 《Λ 運算︰概念導引之《補充》※有名的組合子！！》

 

如果問為什麼『TCP/IP協定套組』

Core Protocols in the Internet Protocol Suite
draft-baker-ietf-core-04

Abstract

This note attempts to identify the core of the Internet Protocol Suite. The target audience is NIST, in the Smart Grid discussion, as they have requested guidance on how to profile the Internet Protocol Suite. In general, that would mean selecting what they need from the picture presented here.

Status of This Memo

This Internet-Draft is submitted in full conformance with the provisions of BCP 78 and BCP 79.

Internet-Drafts are working documents of the Internet Engineering Task Force (IETF). Note that other groups may also distribute working documents as Internet-Drafts. The list of current Internet- Drafts is at http:/⁠/⁠datatracker.ietf.org/⁠drafts/⁠current/⁠.

Internet-Drafts are draft documents valid for a maximum of six months and may be updated, replaced, or obsoleted by other documents at any time. It is inappropriate to use Internet-Drafts as reference material or to cite them other than as “work in progress.”

Copyright Notice

Copyright (c) 2009 IETF Trust and the persons identified as the document authors. All rights reserved.

This document is subject to BCP 78 and the IETF Trust’s Legal Provisions Relating to IETF Documents (http:/⁠/⁠trustee.ietf.org/⁠license-⁠info) in effect on the date of publication of this document. Please review these documents carefully, as they describe your rights and restrictions with respect to this document. Code Components extracted from this document must include Simplified BSD License text as described in Section 4.e of the Trust Legal Provisions and are provided without warranty as described in the Simplified BSD License.

───

『語義』難定呢？

Department of Computer Science and Technology

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:

1. clear, accessible to a broad community and easy to modify;
2. unambiguous, characterising exactly what behaviour is specified;
3. 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
4. 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.

Overview Paper

This paper gives a overall view of our work on TCP, UDP, and the Sockets API:

• Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API. Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, Keith Wansbrough. Draft of November 2017.

(it does not cover the ICNP 06, POPL 09, or ATS 05 papers).

───

就像問『巴別塔』到底誰『建造』的呦！

或許『功夫』流派，因『實踐』差異︰

RobinDavid/pystack

Pystack, is a python framework that allow to create small TCP/IP stacks in an easy manner in order to obtain a wanted behavior.http://www.robindavid.fr/pystack

PyStack

Pystack, is a python framework that allow to create small TCP/IP stacks in an easy manner in order to obtain a wanted behavior. The applications are multiples and there is currently no any module that provide similar functionnalities in python.

It is developped above the Scapy framework to bring some network stateful functionalities adding to it multiple protocols implementations themselves architectured into a stack which allow the different layers to communicate. All this brings the IP stack in userland and then allow to do anything on network packets like modifying the network stack behavior without patching the Linux kernel.

Full Documentation

The full documentation with examples and explanation is available here: robindavid.github.io/pystack

───

※ 註︰因為 nftables 取代 iptables 之故，pystack 需修改了。

root@kali:~/test/pystack/examples# python EchoServer.py
Traceback (most recent call last):
  File "EchoServer.py", line 32, in <module>
    echoserver.bind(8888, echoserver, False) #Bind the TCPApplication to wait for connections
  File "/usr/local/lib/python2.7/dist-packages/pystack/layers/tcp_application.py", line 75, in bind
    self.lowerLayers["default"].bind(port, app, newinstance)
  File "/usr/local/lib/python2.7/dist-packages/pystack/layers/tcp_session.py", line 197, in bind
    block_outgoing_packets("tcp", self.localIP, self.localPort, None, None)
  File "/usr/local/lib/python2.7/dist-packages/pystack/kernel_filter.py", line 38, in block_outgoing_packets
    table.append_rule('OUTPUT', rule)
  File "/usr/lib/python2.7/dist-packages/netfilter/table.py", line 108, in append_rule
    self.__run_iptables(['-A', chainname] + rule.specbits())
  File "/usr/lib/python2.7/dist-packages/netfilter/table.py", line 154, in __run_iptables
    self.__run(cmd)
  File "/usr/lib/python2.7/dist-packages/netfilter/table.py", line 170, in __run
    raise IptablesError(cmd, err)
netfilter.table.IptablesError: command: ['iptables', '-t', 'filter', '-A', 'OUTPUT', '-p', 'tcp', '-s', '5.168.168.9', '-m', 'tcp', '--sport', '8888', '-j', 'DROP']
message: iptables v1.8.1 (nf_tables): Couldn't load match `tcp':No such file or directory

Try `iptables -h' or 'iptables --help' for more information.

 

自生。

『心法』詮釋，為『修練』火候︰

https://www.redbooks.ibm.com/pubs/pdfs/redbooks/gg243376.pdf

───

左右也◎