一種形式化的互聯(lián)網(wǎng)地址機(jī)制通用框架

朱 亮 徐 恪 徐 磊

(清華大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)系 北京 100084)(tshbruce@gmail.com)

一種形式化的互聯(lián)網(wǎng)地址機(jī)制通用框架

朱 亮 徐 恪 徐 磊

(清華大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)系 北京 100084)(tshbruce@gmail.com)

地址機(jī)制作為互聯(lián)網(wǎng)體系結(jié)構(gòu)中的核心組成部分，其演進(jìn)性決定了對(duì)上層網(wǎng)絡(luò)創(chuàng)新應(yīng)用的承載能力.傳統(tǒng)IP地址的缺陷導(dǎo)致當(dāng)前互聯(lián)網(wǎng)陷入僵化，大量新型地址機(jī)制的異構(gòu)性使研究者很難以統(tǒng)一方法論解釋和把握未來(lái)互聯(lián)網(wǎng)地址體系的演進(jìn)發(fā)展.針對(duì)上述問(wèn)題，通過(guò)對(duì)互聯(lián)網(wǎng)地址機(jī)制的演化進(jìn)行深入研究，抽象最小化核心特征，提出一種能夠容納異構(gòu)地址策略構(gòu)建乃至并存的通用框架，包括：1) 完備的形式化概念模型，賦予地址常量的精確定義，并形成相關(guān)設(shè)計(jì)原則及約束規(guī)范的一致性理論基礎(chǔ)；2) 抽象多維度、可擴(kuò)展的接口原語(yǔ)以構(gòu)建3種核心交互模式，并結(jié)合通信公理化性質(zhì)以及語(yǔ)義，構(gòu)造一個(gè)地址交互過(guò)程的正確性證明框架；3) 推導(dǎo)出通用地址引擎原型，允許靈活構(gòu)建地址策略，支持異構(gòu)地址機(jī)制的評(píng)估、演進(jìn)以及共存，以更好地支撐互聯(lián)網(wǎng)頂層生態(tài)的不斷演化.

互聯(lián)網(wǎng)體系結(jié)構(gòu)；通用框架；形式化；地址機(jī)制；正確性證明

以IP地址機(jī)制為核心的互聯(lián)網(wǎng)體系結(jié)構(gòu)取得了巨大成功，既能兼容異構(gòu)的底層技術(shù)，也支撐著層出不窮的網(wǎng)絡(luò)應(yīng)用，保證了互聯(lián)網(wǎng)的泛在連接性和旺盛的生命力.隨著互聯(lián)網(wǎng)與經(jīng)濟(jì)、社會(huì)以及傳統(tǒng)行業(yè)各領(lǐng)域的深度融合，“互聯(lián)網(wǎng)+”代表著一種新的社會(huì)經(jīng)濟(jì)形態(tài)而誕生，以互聯(lián)網(wǎng)為紐帶催生了大量的創(chuàng)新應(yīng)用，全面提升了社會(huì)發(fā)展力[1].

然而，在網(wǎng)絡(luò)應(yīng)用繁榮發(fā)展，規(guī)模不斷增長(zhǎng)的同時(shí)，作為基礎(chǔ)設(shè)施的互聯(lián)網(wǎng)體系結(jié)構(gòu)正面臨著擴(kuò)展性、移動(dòng)性以及安全性等方面的一系列挑戰(zhàn)，限制了對(duì)上層新型應(yīng)用的承載能力，學(xué)術(shù)界開(kāi)始基于應(yīng)用的適應(yīng)能力來(lái)評(píng)估互聯(lián)網(wǎng)的可演進(jìn)性[2-4].同時(shí)，研究者們也開(kāi)始了對(duì)互聯(lián)網(wǎng)的的重新思考,并認(rèn)為傳統(tǒng)地址機(jī)制的缺陷，諸如語(yǔ)義過(guò)載等問(wèn)題是限制體系結(jié)構(gòu)演進(jìn)的主要原因，而IP地址是造成互聯(lián)網(wǎng)僵化的主要隱式約束[5].盡管在互聯(lián)網(wǎng)體系結(jié)構(gòu)如何發(fā)展這一問(wèn)題上存在著諸多爭(zhēng)議[6-7]，但地址機(jī)制需要?jiǎng)?chuàng)新已成為學(xué)術(shù)界的一致共識(shí)，大量修補(bǔ)或革新機(jī)制被提出，例如NAT(network address translation)、IPv6地址過(guò)渡策略、大量的地址安全[8]以及空間分離等方案[9-13].上述地址相關(guān)機(jī)制對(duì)傳統(tǒng)互聯(lián)網(wǎng)進(jìn)行了擴(kuò)展甚至本質(zhì)上的革新，然而卻缺乏統(tǒng)一的指導(dǎo)原則和理論基礎(chǔ)，導(dǎo)致了設(shè)計(jì)的隨意性，從而難以進(jìn)行一致性的分析和評(píng)估.同時(shí)，缺少一種定義完備的通用模型去表述和解釋這些機(jī)制，一些基本概念如名字、地址等都無(wú)法清晰定義，更不用說(shuō)尋址、映射等復(fù)雜交互過(guò)程，其異構(gòu)性和多樣性導(dǎo)致我們很難以一種統(tǒng)一的方法論把握未來(lái)互聯(lián)網(wǎng)地址體系的演進(jìn)和發(fā)展.另外，地址是互聯(lián)網(wǎng)體系結(jié)構(gòu)中的核心組件同時(shí)也是最具可塑性部分，地址體系的靈活性決定了體系結(jié)構(gòu)中其他組件的可演進(jìn)性[14].因此，我們認(rèn)為，固定的地址機(jī)制或許難以支撐未來(lái)互聯(lián)網(wǎng)需求，未來(lái)可能是多種策略并存以滿足互聯(lián)網(wǎng)頂層生態(tài)的不斷演化.

針對(duì)上述問(wèn)題，本文介紹了一種能夠容納地址機(jī)制多樣性的通用地址框架，異構(gòu)的地址機(jī)制都可以利用框架內(nèi)定義的概念與過(guò)程交互模型構(gòu)建部署.該框架通過(guò)一個(gè)精煉的最小化靜態(tài)核心而獨(dú)立于具體實(shí)現(xiàn)細(xì)節(jié)，從而滿足最大限度的設(shè)計(jì)靈活性.同時(shí)，通用模型提供了相關(guān)設(shè)計(jì)原則的約束規(guī)范以及過(guò)程交互的正確性證明，保證了地址機(jī)制定義的一致性和準(zhǔn)確性.本文對(duì)當(dāng)前地址體系演進(jìn)進(jìn)行了深入研究，提出了：1)完備的形式化概念模型，包括相關(guān)設(shè)計(jì)原則約束，賦予地址體系的一致性定義；2)抽象多維度的轉(zhuǎn)發(fā)、交換接口原語(yǔ)，基于這些可擴(kuò)展的標(biāo)準(zhǔn)接口，可以靈活定義3類基本交互模式以構(gòu)造具備正確性驗(yàn)證機(jī)制的地址抽象通信過(guò)程；3)基于概念和交互模型，推導(dǎo)出通用地址引擎作為該通用框架的原型系統(tǒng)，支持地址機(jī)制的演進(jìn)以及多樣性共存，以更好地支撐頂層的網(wǎng)絡(luò)應(yīng)用.

1 抽象通信模型

在介紹概念框架之前，我們首先引入一種抽象通信模型.該模型抽象了地址機(jī)制的核心組件及其通信過(guò)程，可獨(dú)立于具體實(shí)現(xiàn)策略去研究分析，并推導(dǎo)出一些重要通信公理化性質(zhì)，作為概念模型以及通信正確性證明的理論基礎(chǔ).

1.1 模型定義

抽象通信模型如圖1所示.

Fig. 1 Abstract communication model圖1 抽象通信模型

我們首先定義5個(gè)概念：

1) 消息(message).通信中的抽象數(shù)據(jù)交換單元.在實(shí)際網(wǎng)絡(luò)中，消息可實(shí)例化為分組或MAC幀等具體格式.對(duì)于該通信模型，我們只關(guān)注其抽象結(jié)構(gòu)而非比特層面的視圖.一般來(lái)說(shuō)，消息包含了一組頭部域(源信息和目的信息等)用來(lái)指示轉(zhuǎn)發(fā)狀態(tài)，我們將這樣的頭部域稱之為轉(zhuǎn)發(fā)指令(forwarding instructions,fi)，fi可在消息傳遞過(guò)程中被特定網(wǎng)絡(luò)實(shí)體重寫(xiě).

2) 抽象通信對(duì)象(abstract communication object, ACO).參與網(wǎng)絡(luò)通信的一般性抽象對(duì)象，也是原型系統(tǒng)實(shí)現(xiàn)的核心抽象類，以下簡(jiǎn)稱對(duì)象.ACO可理解為網(wǎng)絡(luò)中的一層協(xié)議?；蚴墙粨Q引擎等通信組件.除了消息傳遞，ACO內(nèi)部還包含一些功能組件對(duì)輸入的消息進(jìn)行處理.實(shí)際的網(wǎng)絡(luò)實(shí)體可通過(guò)繼承ACO并與其他子組件(緩存等)通過(guò)特定機(jī)制聚合而產(chǎn)生.

3) ACO通過(guò)端口(port)進(jìn)行通信.消息m在ACOA的輸入端口(sink ports, SIP)和輸出端口(source ports, SOP)接收和發(fā)送，可分別表示為m?ASIP以及m!ASOP.端口不僅表示物理的網(wǎng)絡(luò)接口，還定義了ACO在外部邏輯交互點(diǎn)上的操作.所有端口的操作行為構(gòu)成了ACO的接口域(interface)，規(guī)定了該ACO的外部行為規(guī)范.

4) ACO內(nèi)部通常維護(hù)著一組映射表(local switching table)，交換服務(wù)(switching service)通過(guò)查詢本地映射表或是第三方ACO(如分布式映射系統(tǒng))，根據(jù)返回的結(jié)果對(duì)轉(zhuǎn)發(fā)指令fi進(jìn)行相應(yīng)處理.交換過(guò)程通過(guò)執(zhí)行抽象對(duì)象，轉(zhuǎn)發(fā)指令二元組之間的映射以指明消息的后續(xù)轉(zhuǎn)發(fā)狀態(tài)，對(duì)象B查找本地交換表獲取A和C的映射關(guān)系可表示為SPB(A,fi):A,fi|→C,fi′.

5) 端口通過(guò)邏輯鏈路相連，ACO之間所有的邏輯鏈路組成通道(channel).通道規(guī)定了ACO的角色(role)以及交互規(guī)則和行為規(guī)范.實(shí)際通信中，考慮OAΙC≠?即A，C的行為語(yǔ)義不匹配，若想實(shí)現(xiàn)通信，則需要將不匹配的行為映射到C的輸入域中，稱之為適配服務(wù)(adaption service)，可表示為AP(m):m|→m′(消息結(jié)構(gòu)層面上的適配).適配服務(wù)可存在于中間件，考慮到通道的可重用性，我們定義適配服務(wù)邏輯上由通道提供.

為更清晰闡述該模型的組合語(yǔ)義，下面采用BNF范式對(duì)抽象通信模型的組件對(duì)象進(jìn)行形式化規(guī)約，其中：“…”表示非終結(jié)符，“[…]”表示出現(xiàn) 0 次或者多次，“[…]+”表示出現(xiàn) 1 次或者多次.

對(duì)象ACO的行為由接口域和交換行為構(gòu)成.接口域是輸入和輸出端口對(duì)消息操作原語(yǔ)的并集，定義了消息在端口上的轉(zhuǎn)發(fā)操作，如發(fā)送、接收、調(diào)用等；交換服務(wù)描述了轉(zhuǎn)發(fā)指令層面上的交換行為，通過(guò)查詢映射表獲取相應(yīng)的fi，以指明該消息后續(xù)的轉(zhuǎn)發(fā)狀態(tài)；當(dāng)上述過(guò)程完成之后，適配服務(wù)根據(jù)獲取的轉(zhuǎn)發(fā)指令對(duì)轉(zhuǎn)發(fā)的消息進(jìn)行適配處理，并依據(jù)通信角色輸出到相應(yīng)的實(shí)例化通道上.

基于該抽象模型的語(yǔ)義描述，對(duì)于特定對(duì)象而言，1次抽象通信可被表述為基本通信組件基于3種消息操作的交互過(guò)程，即交換(switching)、轉(zhuǎn)發(fā)(forwarding)、適配(adaption).抽象組件可通過(guò)聚合、繼承而構(gòu)造具體的通信實(shí)體，實(shí)現(xiàn)了模型的可擴(kuò)展性；而交互過(guò)程的抽象保證了不同類型操作模式的松耦合以及模塊化特性，以便本文更加清晰地解構(gòu)互聯(lián)網(wǎng)地址機(jī)制中復(fù)雜的交互過(guò)程.

1.2 基本通信性質(zhì)

通過(guò)對(duì)該基本通信模型的觀察，我們推導(dǎo)出以下重要通信公理化性質(zhì)，其中→表示事件發(fā)生的先后順序.

性質(zhì)1. 直接轉(zhuǎn)發(fā)(direct forwarding).

?ACOA,C,m?m!ASOP→m?CSIP.

性質(zhì)2. 交換(switching).

?ACOA,C,fi:?C,fi′∈SPB(A,fi)?

fi?ASIP→SPB(A,fi)→fi′!ASOP.

性質(zhì)3. 傳遞性(transitivity).

?ACOA,B,C,m,m′:?(m!ASOP→m?BSIP)∧

(m′!BSOP→m′?CSIP)?m!ASOP→m′?CSIP.

性質(zhì)4. 可達(dá)性(reachability).

?ACOA,C,fi,m,m′:?SPA(A,fi),AP(m),

(m!ASOP→m?BSIP)∧(m′!BSOP→m′?CSIP)?

m!ASOP→SPA(A,fi)→AP(m)→m′?CSIP.

性質(zhì)5. 可返回性(returnabilty).

?ACOA,C,m:?m!ASOP→m?CSIP?

m!CSOP→m′?ASIP.

性質(zhì)1表明了對(duì)象間的直接通信，消息從A的輸出端口發(fā)送，在C的輸入端口接收.性質(zhì)2描述了本地交換行為，B接受含有轉(zhuǎn)發(fā)指令fi的消息，查找fi的映射關(guān)系，根據(jù)返回結(jié)果對(duì)fi進(jìn)行相應(yīng)操作，再將含有fi′的消息輸出到端口進(jìn)行轉(zhuǎn)發(fā).SPB返回一組結(jié)果，即一對(duì)多映射的情況，可涵蓋網(wǎng)絡(luò)中多宿主(網(wǎng)絡(luò)接口對(duì)應(yīng)多個(gè)IP地址)以及移動(dòng)性設(shè)計(jì)(身份標(biāo)識(shí)對(duì)應(yīng)多個(gè)位置標(biāo)識(shí))等實(shí)際場(chǎng)景.性質(zhì)3說(shuō)明了轉(zhuǎn)發(fā)過(guò)程的可復(fù)合特性.性質(zhì)4通過(guò)性質(zhì)2與性質(zhì)3的結(jié)合，表明了消息的可達(dá)性，即經(jīng)過(guò)交換、適配、轉(zhuǎn)發(fā)復(fù)合后可到達(dá)的一組對(duì)象集合.性質(zhì)5說(shuō)明直接通信的逆向可返回性.

抽象通信模型針對(duì)轉(zhuǎn)發(fā)指令fi的不同操作模式，抽象出基本交互模式，涵蓋了地址體系的核心通信過(guò)程.事實(shí)上，上述基本性質(zhì)同樣可歸納為2.1節(jié)中提到的核心抽象過(guò)程，即交換、適配和轉(zhuǎn)發(fā).該模型可實(shí)例化為任何一種地址機(jī)制的交互場(chǎng)景，為了使結(jié)構(gòu)更加清晰，本文將基于上述抽象模型和通信性質(zhì)，從與轉(zhuǎn)發(fā)指令實(shí)例相關(guān)的概念模型以及組件間交互的動(dòng)態(tài)過(guò)程框架2個(gè)方面分別進(jìn)行闡述和討論.

2 地址機(jī)制的統(tǒng)一概念模型

互聯(lián)網(wǎng)地址機(jī)制自設(shè)計(jì)以來(lái)，一直存在著相關(guān)概念定義的爭(zhēng)論[15]，基本通信術(shù)語(yǔ)缺少統(tǒng)一、明確的定義.另外對(duì)于一些過(guò)程模式如綁定、尋址等存在著概念層面上的歧義和不一致性.為保證通用的設(shè)計(jì)原則和理念，我們將針對(duì)以上概念提出一套合理、統(tǒng)一的解釋模型，并基于集合論以及關(guān)系代數(shù)賦予了形式化說(shuō)明.基于該模型進(jìn)行地址標(biāo)識(shí)機(jī)制設(shè)計(jì)時(shí)，設(shè)計(jì)理念可被精確且一致地表達(dá)，同時(shí)相關(guān)設(shè)計(jì)原則可依據(jù)模型進(jìn)行規(guī)范性檢查.

2.1 命名空間

為了對(duì)分布式系統(tǒng)中的實(shí)體進(jìn)行區(qū)分和訪問(wèn),有必要給其中的對(duì)象分配標(biāo)識(shí).命名(naming)就是給互聯(lián)網(wǎng)的用戶、設(shè)備、服務(wù)和數(shù)據(jù)等ACO分配與其自身相關(guān)聯(lián)的語(yǔ)法符號(hào)(symbols).命名空間(namespace)是由特定語(yǔ)義范疇(semantic scope)內(nèi)的命名關(guān)系構(gòu)成的集族，指標(biāo)集為{aco,symbols}.語(yǔ)義范疇內(nèi)的通信對(duì)象遵循相同命名規(guī)范，滿足以下定義.

定義1. 語(yǔ)義范疇.

{aco|(fi!ASOP→fi′?CSIP)∧
(C,fi′≠?∈SPB(A,fi)∧(fi=fi′)}.

其中,(fi!ASOP→fi′?CSIP) 表示轉(zhuǎn)發(fā)指令fi被改寫(xiě)為fi′后，從A發(fā)送到C的輸入端口上.C,fi′≠?∈SPB(A,fi) 表明了B查找通信對(duì)象A，C的映射關(guān)系，且結(jié)果不為空.結(jié)合通信性質(zhì)2，4可知，具備可達(dá)性，并且操作相同協(xié)議頭部的一組通信對(duì)象集合構(gòu)成了特定的語(yǔ)義范疇,如圖2所示：

Fig. 2 Naming and resolving in the current Internet圖2 當(dāng)前互聯(lián)網(wǎng)命名解析層次式模型

例如當(dāng)前互聯(lián)網(wǎng)協(xié)議棧中HTTP ACO 與IP ACO則分別屬于2個(gè)不同的語(yǔ)義范疇，從而關(guān)聯(lián)著不同的命名空間.命名空間應(yīng)被看作aco,symbols的集合，命名對(duì)象決定了命名空間語(yǔ)義上的概念范疇，即標(biāo)識(shí)何種類型或何種屬性；命名規(guī)范則體現(xiàn)了語(yǔ)法上的表現(xiàn)方式.我們引入集合：可命名對(duì)象O，屬于特定semantic scope的對(duì)象SO，任意符號(hào)集合S，其中SO∈O.則命名空間定義如下：

定義2. 命名與命名空間.

?aco:O,n:S(acoNn?(aco|→n)∈
O×S){acoNn|aco∈SO∧n∈S}.

命名可以使用二元中綴關(guān)系acoNn來(lái)表示，即將n作為對(duì)象aco的名字，是一種多對(duì)多的關(guān)系，即1個(gè)對(duì)象可以有多個(gè)名字，1個(gè)名字可以標(biāo)識(shí)一組對(duì)象，分別對(duì)應(yīng)于當(dāng)前互聯(lián)網(wǎng)中的多宿主以及組播.值得注意的是，這里所說(shuō)的命名是廣義上的概念，其上下文依賴其語(yǔ)義范疇：即不僅是針對(duì)名字分配，還包括對(duì)身份、位置等抽象屬性的命名，例如對(duì)象名字與其附著點(diǎn)(attachment point)的命名空間分別被稱為名字空間和地址空間(address space).

2.2 綁定、解析和尋址

命名空間的語(yǔ)義被限制在一定概念范圍內(nèi)導(dǎo)致不同語(yǔ)義范疇內(nèi)的通信組件無(wú)法直接交互.為實(shí)現(xiàn)通信，綁定(binding)提供了訪問(wèn)異構(gòu)命名空間的入口，也就是說(shuō)，綁定關(guān)系B實(shí)際上構(gòu)造了基于semantic scope的拓?fù)洌瑸楸苊饨馕鏊姥h(huán)，該拓?fù)鋺?yīng)為有向無(wú)環(huán)圖(DAG).綁定關(guān)系存在于不同語(yǔ)義范疇中的抽象通信對(duì)象之間：

定義3. 綁定.

?acox:SOx,acoy:SOy·(acoxBacoy?
(acox|→acoy)∈SOx× SOy)∧(SOx≠SOy).

從命名空間的角度而言，Saltzer認(rèn)為綁定引用了名字和對(duì)象之間的關(guān)系[16]，而根據(jù)上述定義，綁定產(chǎn)生于不同命名空間之間，可描述為?acoxNnx,acoyNny·acox,nx|→acoy,ny.當(dāng)前互聯(lián)網(wǎng)TCPIP體系中，HTTP|→IPv4以及IPv4|→Ethernet的綁定關(guān)系分別存儲(chǔ)在DNS系統(tǒng)和ARP表中.如圖2所示，如果2個(gè)semanticscope組件之間存在綁定關(guān)系，則滿足通信性質(zhì)1，我們稱之為鄰居(neighbors).

由通信性質(zhì)5可知，解析(resolving)可看作是與綁定具有相同基數(shù)(cardinality)的逆關(guān)系，包含所有有序?qū)cox,nx|→acoy,ny的轉(zhuǎn)置矩陣，表示為B-1=acoy,ny|→acox,nx.對(duì)于acoy,ny∈SOy的解析過(guò)程定義如下：

定義4. 解析.

?(acox|→acoy)∈B:β(acoy,ny∈SOy)=
{acox,nx∈SOx,e}.

解析過(guò)程返回一組有序?qū)Φ募?，e表示指向下一個(gè)semantic scope入口引用.事實(shí)上，解析也是鄰居發(fā)現(xiàn)的過(guò)程.對(duì)綁定拓?fù)溥M(jìn)行遞歸或者分布式的解析過(guò)程為尋址(addressing)，目的是為了獲取最終可用于轉(zhuǎn)發(fā)的標(biāo)識(shí)符.結(jié)合通信的可傳遞性(性質(zhì)4)，引入2種關(guān)系概念.

1) 關(guān)系復(fù)合.對(duì)于任意二元關(guān)系R:X?Y,S:Y?Z來(lái)說(shuō)，R°S={x:X;z:Z|(?y:Y·(xRy∧ySz))·x|→z}；例如(x|→y)∈R,(y|→z)∈S?(x|→z)∈R°S.

2) 自反傳遞閉包.對(duì)于任意二元同類關(guān)系R,Rk表示對(duì)其進(jìn)行k次復(fù)合，即R2=R°R.則自反傳遞閉包由包括R0在內(nèi)的所有的R關(guān)系復(fù)合的并集構(gòu)成，即：

基于以上關(guān)系運(yùn)算，尋址過(guò)程可定義如下：

定義5. 尋址.

A(aco,n)=
β(aco1,n1,e1) °β(aco2,n2,e2) °…
°β(acok,nk,ek)=βk.

定義6. 名字作用域.

NScope(acox,nx)={acoy,ny|
(acox,nx|→acoy,ny)∈β*k}.

2.3 名字、地址、身份標(biāo)識(shí)和位置標(biāo)識(shí)

基于上述概念模型，我們推導(dǎo)出以下通信名詞的一致性形式化定義：名字(name)、地址(address)、身份標(biāo)識(shí)(identifier)、位置標(biāo)識(shí)(locator)，并對(duì)它們之間的關(guān)系進(jìn)行了闡明.

定義7. name & address：

?acox:SOx,acoy:SOy,nx,ny；

?acoxNnx?nx=name ofacox；

?acoxNnx,acoyNny，acoxBacoy?ny=address ofacox.

如果通信對(duì)象acox與符號(hào)nx之間存在命名關(guān)系，則nx是acox的名字；而地址則基于綁定關(guān)系，acox的地址則是另一個(gè)語(yǔ)義范疇內(nèi)所綁定通信對(duì)象acoy的名字ny.例如在尋址過(guò)程中，相對(duì)于HTTP ACO而言，URL是名字，而解析得到的IP則是其地址.類似Shoch的定義，地址指明了“where it is”，但按照我們的定義，是基于semantic scope而言的相對(duì)位置.對(duì)應(yīng)于name scope (定義6)，地址的作用域稱之為位置空間(location space).實(shí)際上，地址是尋址過(guò)程所引入的一種中間形式，當(dāng)名字包含位置屬性時(shí)，同樣可被用作路由，比如基于名字的路由(route-by-name)[17].名字和地址基于命名和綁定關(guān)系，是對(duì)象的屬性；而身份標(biāo)識(shí)與位置標(biāo)識(shí)則是針對(duì)通信中命名空間的角色而言，規(guī)定了該命名空間所承擔(dān)的語(yǔ)義.

定義8. Identifier & Locator:

對(duì)于在特定name scope內(nèi)唯一的語(yǔ)法符號(hào)n,?aco,n,aco,n′∈NScope(aco,n):

?oNn,oNn′,acoNn,aco′Nn?
(n=n′)∧(o=o′),

則n稱為aco的身份標(biāo)識(shí);?A(aco,n),?ek=null,則返回的一組nk為aco的位置標(biāo)識(shí).

在特定name scope內(nèi)，明確、唯一標(biāo)識(shí)對(duì)象的符號(hào)n稱為身份標(biāo)識(shí).在形式化定義中，唯一性以及對(duì)象和名字的一對(duì)一映射保證了無(wú)歧義性.位置標(biāo)識(shí)為尋址過(guò)程正常結(jié)束后(ek=null)返回的標(biāo)識(shí)，用于指明后續(xù)的轉(zhuǎn)發(fā)操作.就實(shí)際網(wǎng)絡(luò)而言，MAC地址和IP地址可分別看作是局域網(wǎng)和互聯(lián)網(wǎng)通信的位置標(biāo)識(shí).可以看出，在當(dāng)前TCP/IP體系中，IP地址承擔(dān)了IP ACO位置標(biāo)識(shí)和身份標(biāo)識(shí)的雙重角色，從而導(dǎo)致了移動(dòng)性問(wèn)題.

圖2為當(dāng)前互聯(lián)網(wǎng)的層次式解析模型，為保證通用性，圖3基于semantic scope說(shuō)明了地址機(jī)制概念模型及其關(guān)系.對(duì)通信對(duì)象而言，名字和地址是基于命名和綁定關(guān)系而產(chǎn)生的屬性，而身份標(biāo)識(shí)和位置標(biāo)識(shí)則是命名空間在通信中承擔(dān)的角色.身份標(biāo)識(shí)和位置標(biāo)識(shí)可以產(chǎn)生自同一命名空間.滿足定義8的名字可用作身份標(biāo)識(shí)，當(dāng)網(wǎng)絡(luò)對(duì)象相對(duì)于邏輯位置不發(fā)生移動(dòng)，即實(shí)體與其位置屬性靜態(tài)綁定時(shí)，地址同樣可以作為身份標(biāo)識(shí)使用.地址若要作為位置標(biāo)識(shí)使用，必須在特定位置空間內(nèi)能唯一標(biāo)識(shí)相對(duì)位置；而包含位置屬性，能在特定空間中唯一定位的名字也可以成為位置標(biāo)識(shí).

Fig. 3 The conceptual framework illustrated based on semantic scope圖3 基于semantic scope的地址機(jī)制概念框架

3 地址機(jī)制的通信交互模式

上述概念模型為地址策略的設(shè)計(jì)提供了明確的解釋視圖以及統(tǒng)一的設(shè)計(jì)原則.本節(jié)中，我們將對(duì)地址機(jī)制中的動(dòng)態(tài)交互過(guò)程進(jìn)行多維度抽象，獲取核心的標(biāo)準(zhǔn)接口以及交互模式，以構(gòu)造一種可以兼容異構(gòu)地址機(jī)制的最小化通用過(guò)程處理框架.在進(jìn)行地址機(jī)制設(shè)計(jì)時(shí)，該框架能夠依據(jù)交互模式以及行為語(yǔ)義對(duì)通信行為進(jìn)行正確性檢查.

3.1 交互模式與原語(yǔ)

根據(jù)抽象通信模型的規(guī)約描述，從消息傳遞的角度來(lái)看，抽象通信對(duì)象ACO的外部行為由接口行為和交換行為共同構(gòu)成.接下來(lái)我們將介紹這些行為的具體操作語(yǔ)義，同時(shí)也作為交互過(guò)程正確性的證明基礎(chǔ).通信順序進(jìn)程(communicating sequential processes, CSP)[18]是一種適合描述并發(fā)和通信系統(tǒng)的常用形式化描述技術(shù)，其描述可導(dǎo)入模型檢驗(yàn)器進(jìn)行相關(guān)性質(zhì)的驗(yàn)證.我們選用CSP相關(guān)符號(hào)來(lái)刻畫(huà)交互行為語(yǔ)義.CSP 的基本單元是進(jìn)程(process)，進(jìn)程刻畫(huà)了通信對(duì)象的行為模式，對(duì)象行為集合構(gòu)成了該進(jìn)程的事件集αP.“a→P”表示先執(zhí)行事件a然后進(jìn)程P，√ 表示1個(gè)成功執(zhí)行的事件.為方面描述，定義=√→STOP，代表該進(jìn)程成功終止(類似于CSP中的SKIP).P‖Q為進(jìn)程P和Q的并發(fā)進(jìn)程，PQ代表行為為P或者Q的行為的進(jìn)程，內(nèi)部選擇算子表示該進(jìn)程能夠自主選擇進(jìn)程.PQ表示該復(fù)合進(jìn)程行為依據(jù)第1個(gè)事件來(lái)決定的進(jìn)程，選擇復(fù)合算子說(shuō)明該進(jìn)程的選擇只能由外部環(huán)境觸發(fā).

接口域(I/F)定義了轉(zhuǎn)發(fā)操作，包括一組成對(duì)出現(xiàn)的事件，如send/receive,invoke/return等.交換服務(wù)SP描述了本地或者全局協(xié)作的交換行為，由定義4可知，交換行為的目的是為了尋址.對(duì)象aco的操作行為語(yǔ)義可以形式加以規(guī)約:

aco=IF‖SP, whereαaco=αIF ∪αSP.

當(dāng)上述過(guò)程完成之后，適配服務(wù)對(duì)轉(zhuǎn)發(fā)的消息進(jìn)行適配處理，并輸出到實(shí)例化的通道上.根據(jù)以上描述，對(duì)于特定對(duì)象，完成的通信過(guò)程(COMM)可定表述為3種抽象交互模式的組合:尋址(addressing)、轉(zhuǎn)發(fā)(forwarding)、適配(adaption).采用CSP的并發(fā)進(jìn)程形式定義為

COMM=I/F(m)‖SP(aco,fi)‖AP(m).

基于上述觀察，我們對(duì)每一種交互模式分別定義標(biāo)準(zhǔn)的接口(事件表)，這些原語(yǔ)涵蓋了整個(gè)轉(zhuǎn)發(fā)、尋址的抽象過(guò)程，可以靈活構(gòu)造地址機(jī)制中所期望的交互行為.所有的通信對(duì)象支持相同的接口組，具體實(shí)現(xiàn)機(jī)制可以根據(jù)實(shí)際通信場(chǎng)景靈活設(shè)計(jì).消息類型message以及fi分別抽象引用了通信分組以及用于轉(zhuǎn)發(fā)決策的頭部域，在具體的實(shí)現(xiàn)中，將被替換為具體協(xié)議相關(guān)的數(shù)據(jù)結(jié)構(gòu)，如身份標(biāo)識(shí)、位置標(biāo)識(shí)等.另外，對(duì)象類型aco同樣可以被繼承，擴(kuò)展成為實(shí)際的通信主體.

1) 轉(zhuǎn)發(fā)模式

fiGetfi(msg)：

從消息中獲取相應(yīng)轉(zhuǎn)發(fā)指令fi并返回，具體的轉(zhuǎn)發(fā)信息可依據(jù)具體機(jī)制實(shí)例化.

send(aco,msg)?msg!ASOP→msg!CSOP：

對(duì)應(yīng)于通信性質(zhì)1，將消息發(fā)送到對(duì)端的輸入端口，值得注意的是，從邏輯上來(lái)說(shuō)，該消息還沒(méi)有進(jìn)行適配處理.

接收消息并返回該消息和發(fā)送方aco.

messagecopy(msg)?msg?ASIP→msg!ASOP：

將消息拷貝到輸出端口.

2) 尋址模式

messagerequest(aco,fi)：

將請(qǐng)求解析的fi放入請(qǐng)求消息中.

該原語(yǔ)執(zhí)行解析操作，映射系統(tǒng)的具體實(shí)現(xiàn)機(jī)制可以靈活定義，不在本文討論的范圍內(nèi).由性質(zhì)2可知，該原語(yǔ)返回一組aco,fi.

messageresponse(fi,aco)：

將查詢的結(jié)果放在響應(yīng)消息中.

3) 適配模式

encap(fi,msg)：

為消息封裝1個(gè)協(xié)議相關(guān)的頭部，通常用于隧道的入口處或協(xié)議層之間.

fidecap(fi,msg)：

解封裝，從消息中移除新增的頭部前綴.通常用于隧道的出口處.

encrypt(method,msg)：

使用加密機(jī)制對(duì)消息進(jìn)行加密，具體的加密方法可以靈活定義.

swap(fi,msg)：

對(duì)消息中轉(zhuǎn)發(fā)指令fi進(jìn)行替換，例如MPLS和NAT中的標(biāo)簽交換.

deliver(msg)：

消息不經(jīng)過(guò)任何處理，直接轉(zhuǎn)發(fā).

3.2 通道實(shí)例及語(yǔ)義規(guī)約

在圖1的通信模型中，適配服務(wù)作為通道行為的一部分提供，目的在于分離對(duì)象的轉(zhuǎn)發(fā)行為與對(duì)象間的交互行為，實(shí)現(xiàn)通道實(shí)例的可重用，從而降低通信過(guò)程的復(fù)雜性.通信對(duì)象的自身行為被封裝，交互行為的語(yǔ)義規(guī)約到通道上，可作為獨(dú)立于具體通信機(jī)制的多語(yǔ)義連接件使用.通道實(shí)例基于角色(role)和粘合劑(glue)進(jìn)行語(yǔ)義說(shuō)明.role描述了aco所期望的外部行為規(guī)范；glue用于規(guī)定各個(gè)role的行為時(shí)序，協(xié)調(diào)抽象通信對(duì)象間的交互行為.基于適配模式對(duì)消息的操作，我們定義通道實(shí)例:

ChannelEncap-Channel=

rolesender=(encap(fi,msg)→send(aco,msg)→√)；

rolereceiver=(receive(aco,msg)→√)；

glueEglue=(encap(fi,msg)→send(aco,msg)→receive(aco,msg)→√).

該通道實(shí)例對(duì)消息進(jìn)行封裝操作，可連接不同協(xié)議層實(shí)現(xiàn)通信.考慮消息從傳輸層加上IP頭部，再發(fā)送給網(wǎng)絡(luò)層接收.

ChannelTunnel=

rolepeer=(encap(fi,msg)→send(aco,msg)→√)；

rolepeer=(decap(fi,msg)→receive(aco,msg)→√)；

glueTglue=(encap(fi,msg)→send(aco,msg)→decap(fi,msg)→receive(aco,msg)→√).

ChannelGateway-Channel=

rolesender=(swap(fi,msg)→send(aco,msg)→√)；

rolereceiver=(receive(aco,msg)→√)；

glueGglue=(swap(fi,msg)→send(aco,msg)→receive(aco,msg)→√).

通道的網(wǎng)關(guān)模型.該模型與封裝方式的區(qū)別在于替換而不是封裝標(biāo)簽，例如NAT以及MPLS中的標(biāo)簽交換.

ChannelCS-Channel=

roleclient=(request(aco,fi)→receive());

roleserver=(lookup(aco,fi)→response(msg,aco));

glueCglue=(request(aco，fi)→lookup(aco,fi)→response(msg,aco)→receive()).

客戶服務(wù)器交互通道，適用于解析請(qǐng)求或者過(guò)程調(diào)用等通信連接.注意客戶角色使用內(nèi)部選擇符而服務(wù)器角色使用的是外部選擇符，也就是說(shuō)，客戶端能夠主動(dòng)結(jié)束請(qǐng)求，而服務(wù)器不能主動(dòng)結(jié)束服務(wù)，只能由外部觸發(fā)決定其結(jié)束與否.基于該通道設(shè)計(jì)客戶服務(wù)器模型可以根據(jù)通道語(yǔ)義得到有效驗(yàn)證.另外，我們還定義了加密通道、轉(zhuǎn)發(fā)通道等其他實(shí)例，這里不再一一贅述.

該通用過(guò)程框架包含了經(jīng)過(guò)觀察、精心選擇和構(gòu)造的核心接口原語(yǔ)，可快速靈活地構(gòu)建交互模式實(shí)例，通信對(duì)象之間通過(guò)通道實(shí)例交互，實(shí)現(xiàn)轉(zhuǎn)發(fā)與交互行為的松耦合.

4 構(gòu)造與驗(yàn)證實(shí)例

為論證上述概念模型與交互過(guò)程框架該的完備性和正確性，我們以ID/Locator地址分離體系中的映射-封裝機(jī)制(map-encap)[9]為例，來(lái)說(shuō)明一種地址方案如何在該框架內(nèi)表述和構(gòu)造并得到有效驗(yàn)證.

如圖4所示，map-encap機(jī)制通過(guò)網(wǎng)絡(luò)提供功能以實(shí)現(xiàn)位置與身份相分離，身份標(biāo)識(shí)EID只在接入網(wǎng)中路由，隧道邊緣路由器(ingress tunnel router,ITR)通過(guò)查詢映射系統(tǒng)(resolver)獲取全局路由標(biāo)識(shí)RLOC，并將其封裝在消息頭部，再對(duì)端邊緣路由器ETR處解封裝.我們假定EID和RLOC分別來(lái)自IPv4以及IPv6地址空間，類似于IPv6的隧道過(guò)渡機(jī)制.為保證靜態(tài)模型與交互過(guò)程的相對(duì)獨(dú)立，對(duì)應(yīng)于概念模型和過(guò)程框架，下面我們從配置定義和交互過(guò)程定義2個(gè)方面論證map-encap地址機(jī)制的實(shí)現(xiàn).

Fig. 4 Abstract processing of map-encap scheme圖4 Map-encap地址機(jī)制抽象過(guò)程

4.1 配置定義

考慮到配置描述的精確性和可重用性，我們基于XML對(duì)地址方案進(jìn)行描述，并提出了3類XML描述規(guī)范(schema):通信實(shí)體定義、拓?fù)渑渲靡约懊臻g語(yǔ)法語(yǔ)義規(guī)則.描述規(guī)范嚴(yán)格對(duì)應(yīng)于本文提出的概念模型，以保證一致性的設(shè)計(jì)約束規(guī)范檢查.圖5為map-encap地址機(jī)制的XML描述，限于篇幅，我們截取部分定義，并省略過(guò)多的XML語(yǔ)法符號(hào).

通信實(shí)體配置定義了對(duì)象的繼承或聚合機(jī)制；拓?fù)涿枋鰧?shí)體基于通道實(shí)例的連接關(guān)系，同時(shí)包含了交互行為的語(yǔ)義約束；命名空間包括語(yǔ)義規(guī)范和語(yǔ)法規(guī)則2個(gè)方面.本文第2節(jié)定義的概念約束了語(yǔ)義規(guī)范的設(shè)計(jì)，并能夠進(jìn)行檢查；語(yǔ)法規(guī)則規(guī)定了數(shù)據(jù)類型，比如以正則表達(dá)式匹配地址格式等.基于上述3類XML schema，地址機(jī)制可被靈活定義描述，同時(shí)保證設(shè)計(jì)方案的一致性和正確性.

Fig. 5 A snippet of configuration description圖5 部分配置描述

4.2 交互過(guò)程

在3.1節(jié)中，我們提出了一組精煉的核心接口原語(yǔ)，為驗(yàn)證其通用性，我們以圖4中ITRA的通信行為為例，基于上述原語(yǔ)來(lái)構(gòu)建3種基本交互模式，從而實(shí)現(xiàn)map-encap地址機(jī)制抽象通信過(guò)程.另外，我們基于斷言技術(shù)，用一組謂詞公式來(lái)刻畫(huà)程序在執(zhí)行過(guò)程中的狀態(tài)，通過(guò)考察各斷言能否成立，實(shí)現(xiàn)對(duì)程序正確性的證明；圖6以偽代碼形式刻畫(huà)了ITRA的一般抽象通信行為，并插入了適當(dāng)?shù)臄嘌?

可以看出，基于標(biāo)準(zhǔn)接口構(gòu)建的3種基本交互模式完成了ITRA的通信行為，而諸如lookup等接口則依賴于具體協(xié)議機(jī)制實(shí)現(xiàn).在實(shí)現(xiàn)中，并不需要所有的抽象對(duì)象都具有完備的接口實(shí)現(xiàn)，這里描述的是通用的交互過(guò)程，任何實(shí)際策略均可通過(guò)與具體協(xié)議相關(guān)的繼承、改寫(xiě)、實(shí)例化而獲得.

Fig. 6 The abstract processing圖6 抽象通信過(guò)程

4.3 程序正確性證明

程序正確性證明指的是通過(guò)形式化的推導(dǎo)，評(píng)價(jià)一個(gè)程序是否符合特定規(guī)范.本節(jié)我們使用Hoare邏輯，以1.1節(jié)以及3.1節(jié)中的通信性質(zhì)和行為語(yǔ)義為證明依據(jù)，來(lái)證明上述抽象過(guò)程的正確性.文獻(xiàn)[19]針對(duì)轉(zhuǎn)發(fā)過(guò)程中名字和地址的移除模式，利用Hoare邏輯證明了轉(zhuǎn)發(fā)過(guò)程的正確性.圖7為Hoare邏輯的規(guī)則描述.

Fig. 7 Hoare logic rules圖7 Hoare 邏輯的規(guī)則描述

Hoare邏輯[20]是對(duì)斷言方法的推廣，并建立了1套公理系統(tǒng)，其公理和命題的一般形式為：{φ}Q{ψ}.其中φ,ψ為邏輯表達(dá)式，Q是1個(gè)程序段.整個(gè)表達(dá)式的含義是：如果在Q執(zhí)行之前有φ成立，并且Q能終止執(zhí)行，則必有ψ成立，通常將φ,ψ稱為前置斷言(pre-condition)和后置斷言(post-condition).為了證明不變式語(yǔ)句，Hoare公理系統(tǒng)引入了1條賦值公理和4種推理規(guī)則，如圖7所示，其中橫線上方的語(yǔ)句為假設(shè)，下方是可推導(dǎo)出的結(jié)論，其語(yǔ)義為：如果所有的假設(shè)成立，則結(jié)論必然成立.對(duì)于map-encap機(jī)制而言，合理的前置斷言應(yīng)為主機(jī)X將需要解析的fi發(fā)送到A的輸入端口；當(dāng)一系列交互過(guò)程完成后，后置斷言為：A將含有解析完畢，經(jīng)過(guò)封裝的fi′拷貝到輸出端口，基于上述規(guī)則，我們?cè)诔绦蛞约把h(huán)的開(kāi)始和結(jié)束處分別插入斷言.

φ:pre=X∧(fi!XSOP→fi?ASIP)；
σ1:fi!RSIP∧(fi=n)∧(A=?)；
σ2:fi?ASIP∧(fi=n′)∧(A≠?)；
ψ:(fi!ASOP→fi?ASIP)∧(fi=n′)∧
(msg=msg′).

下面對(duì)證明過(guò)程進(jìn)行簡(jiǎn)要說(shuō)明：為方便描述，我們將斷言之間的程序段分別以其交互模式forward-ing，addressing，adaption表示，其最終證明形式可表示為

Goal 1：{φ}process{ψ}，由順序規(guī)則可轉(zhuǎn)換為3個(gè)Hoare三元組的證明：

Goal 2:{φ} forwarding {σ1};
Goal 3:{σ1} addressing {σ2};
Goal 4:{σ2} adaption {ψ}.

1) 為證明Goal 2，即轉(zhuǎn)發(fā)后消息到達(dá)R并且尋址沒(méi)有完成，由賦值公理和推斷規(guī)則，只需證明:

[{φ}∧send()]?{σ1}?(fi!XSOP→
fi?ASIP)∧(fi!ASOP→fi?RSIP)?pre=
X∧(fi!XSOP→fi?ASIP).

由通信的傳遞性(性質(zhì)3)可知，上述推斷成立即Goal 2得證.

2) 為證明Goal 3，根據(jù)循環(huán)規(guī)則，只需證明：{σ1∧(e≠error)} if (e≠null) thenlookupelsesend{σ2},再由條件規(guī)則轉(zhuǎn)化為

Goal 5:{fi!RSIP∧(fi=n)∧(A=?)∧(e≠error)∧(e≠null)}lookup(){fi?RSIP∧(fi=n)∧(A=?)}；

Goal 6:{fi!RSIP∧(fi=n)∧(A=?)∧(e≠error)∧(e=null)}send(){fi?ASIP∧(fi=n′)∧(A≠?)}；

Goal 5的含義為尋址過(guò)程沒(méi)有結(jié)束，對(duì)其使用賦值公理、推斷規(guī)則、交換性質(zhì)(性質(zhì)2)以及尋址定義(定義6)，Goal 5得證，即：

fi!RSIP∧(fi=n)∧(A=?)∧
(e≠error)∧(e≠null)SPR(A,fi)?
fi?RSIP∧(fi=n)∧(A=?).

同理，Goal 6的含義為尋址結(jié)束并將結(jié)果返回A，由通信傳遞性可以得到證明，即：

fi!RSIP∧(fi=n)∧(A=?)∧(e≠error)∧
(e=null)∧(fi!ASOP→fi?RSIP)?
fi?ASIP∧(fi=n′)∧(A≠?).

綜上，Goal 3得到了證明.

3) 為證明Goal 4，即A接收到解析結(jié)果并封裝在新消息中，發(fā)送到輸出端口.由賦值公理、推斷規(guī)則以及encap，copy的行為語(yǔ)義可得：

fi?ASIP∧(fi=n′)∧(A≠?)∧encap∧copy?fi?ASIP∧(fi=n′)∧(A≠?)∧msg′∧(msg!ASIP→msg′?ASOP)?(fi!ASOP→fi?ASIP)∧(fi=n′)∧(msg=msg′).Goal 4得證.

證畢.

綜上，Goal 1即上述程序描述的正確性到了證明.

5 通用地址機(jī)制引擎

當(dāng)前互聯(lián)網(wǎng)體系結(jié)構(gòu)只允許對(duì)頂層的應(yīng)用和技術(shù)創(chuàng)新，而作為核心的地址組件卻難以擴(kuò)展，組件之間的緊耦合特性阻礙了體系結(jié)構(gòu)的進(jìn)一步演進(jìn)，這也是當(dāng)前互聯(lián)網(wǎng)陷入僵化的主要原因之一.為增加地址標(biāo)識(shí)機(jī)制的靈活性和通用性，基于本文提出的概念與過(guò)程交互模型，我們實(shí)現(xiàn)了通用地址機(jī)制引擎(universal engine of address schemes， UEAS)原型系統(tǒng)，旨在提供一種通用平臺(tái)以容納或兼容互聯(lián)網(wǎng)地址類型的異構(gòu)性和多樣性.任何所期望的地址機(jī)制都可以在一致性和正確性的約束下，快速、靈活地構(gòu)造，并針對(duì)特定策略的性能開(kāi)銷進(jìn)行有效評(píng)估.

如圖8所示，通用地址機(jī)制引擎的結(jié)構(gòu)框架.網(wǎng)絡(luò)通信實(shí)體、命名空間語(yǔ)法語(yǔ)義和拓?fù)渑渲靡訶ML描述并存儲(chǔ)在本體庫(kù)中，以模板形式調(diào)用.最核心的抽象基類是本文一直強(qiáng)調(diào)的ACO，Message以及Channel，在引擎中以Java抽象類定義，并提供了基本的操作原語(yǔ).具體通信主體可以通過(guò)對(duì)3種抽象類的繼承或?qū)嵗@取.3種基本交互模式以及相應(yīng)的操作原語(yǔ)以類庫(kù)形式提供，供通信主體調(diào)用以構(gòu)造實(shí)際通信過(guò)程.為了進(jìn)一步增加功能的完備性，我們提供了1個(gè)組件庫(kù)供設(shè)計(jì)時(shí)以服務(wù)形式調(diào)用，包括安全機(jī)制、前綴聚合機(jī)制、地址映射機(jī)制等.我們?yōu)榻M件庫(kù)的每個(gè)服務(wù)組件指定了1個(gè)標(biāo)識(shí)符，應(yīng)用調(diào)用的時(shí)候只需傳遞這個(gè)標(biāo)識(shí)符，實(shí)現(xiàn)了組件庫(kù)的可擴(kuò)展性而無(wú)需影響已有應(yīng)用.引擎管理器解析XML配置文件以及定義交互模式，并根據(jù)本文前面介紹的概念模型與組件語(yǔ)義進(jìn)行正確性、完備性檢查，最后生成地址機(jī)制實(shí)例運(yùn)行.

Fig. 8 Universal engine of address schemes圖8 通用地址機(jī)制引擎

通用地址框架可為異構(gòu)的地址標(biāo)識(shí)方案提供統(tǒng)一的構(gòu)造、部署平臺(tái).研究人員調(diào)用或者自定義本體庫(kù)中的通信組件，基于我們預(yù)先定義的XML描述規(guī)范，將特定地址機(jī)制形成腳本描述并提交至引擎管理器；引擎管理器依據(jù)語(yǔ)法語(yǔ)義規(guī)則對(duì)該腳本進(jìn)行驗(yàn)證和解析，并調(diào)用相應(yīng)服務(wù)組件以實(shí)例化地址機(jī)制并注入運(yùn)行時(shí)網(wǎng)絡(luò).

另外，通用地址機(jī)制框架并非列舉地址體系中所有的通信組件或行為，而是通過(guò)精煉1個(gè)最小化靜態(tài)核心來(lái)保證設(shè)計(jì)的完備性和最大限度的自由性.比如框架內(nèi)并沒(méi)有限定地址的聚合機(jī)制以及映射更新機(jī)制等，而是允許設(shè)計(jì)人員根據(jù)實(shí)際地址策略靈活定義、調(diào)整以及評(píng)估，從而選擇其中最優(yōu)的設(shè)計(jì)方案.

6 結(jié)束語(yǔ)

本文通過(guò)對(duì)互聯(lián)網(wǎng)地址體系異構(gòu)及多樣性的深入研究，抽象出其本質(zhì)特征屬性，提出了完備的形式化概念模型，并利用精心構(gòu)造的最小化交互模式來(lái)靈活構(gòu)造地址機(jī)制的抽象通信過(guò)程.基于上述概念與過(guò)程框架，推導(dǎo)出可兼容異構(gòu)地址策略并存的通用平臺(tái)以及其原型系統(tǒng)，任何期望的地址機(jī)制都可以在概念及行為語(yǔ)義的約束下靈活定義實(shí)現(xiàn).

互聯(lián)網(wǎng)地址機(jī)制中的基本概念存在歧義以及不一致性，已經(jīng)在學(xué)術(shù)界爭(zhēng)論了幾十年之久.在研究與命名尋址相關(guān)的方法論之前，重新審視這些關(guān)鍵概念是具有重要意義.本文以一種形式化的概念表述，賦予這些術(shù)語(yǔ)精確而又一致的定義，同時(shí)包含了相關(guān)的設(shè)計(jì)原則約束，在實(shí)際的地址機(jī)制設(shè)計(jì)中具有一定的指導(dǎo)作用.而對(duì)于動(dòng)態(tài)的過(guò)程交互僅僅是通過(guò)定義一組核心標(biāo)準(zhǔn)接口構(gòu)造3種基本模式來(lái)實(shí)現(xiàn)，最大限度保證了設(shè)計(jì)的自由性.結(jié)合本文推導(dǎo)出的通信性質(zhì)，設(shè)計(jì)的正確性同樣可以得到有效的形式化驗(yàn)證.最后，通用地址引擎為進(jìn)一步探索互聯(lián)網(wǎng)地址機(jī)制的演進(jìn)方向提供了可能的實(shí)驗(yàn)平臺(tái).未來(lái)工作中，我們將結(jié)合資源調(diào)度，基于對(duì)應(yīng)用的支撐能力，提出相應(yīng)的評(píng)估機(jī)制，并對(duì)原型系統(tǒng)進(jìn)行完善，使其能夠獲取量化的評(píng)估結(jié)果.

[1]Zheng Qinghua. The introduction of application technology-oriented “Internet+”[J]. Journal of Computer Research and Development, 2015, 52(12): 2657-2658 (in Chinese)(鄭慶華. 面向“互聯(lián)網(wǎng)+”的應(yīng)用技術(shù)專題前言[J]. 計(jì)算機(jī)研究與發(fā)展, 2015, 52(12): 2657-2658)

[2]Xu Ke, Zhu Min, Shen Meng. The application-oriented evolvable Internet architecture[J]. Communications of the CCF, 2015, 11(6): 37-42 (in Chinese)(徐恪, 朱敏, 沈蒙. 面向應(yīng)用的可演進(jìn)互聯(lián)網(wǎng)體系結(jié)構(gòu)[J]. 中國(guó)計(jì)算機(jī)學(xué)會(huì)通訊, 2015, 11(6): 37-42)

[3]Xu Ke, Zhu Min, Lin Chuang. Internet architecture evaluation models mechanisms and methods[J]. Chinese Journal of Computers, 2012, 35(10): 1985-2006 (in Chinese)(徐恪, 朱敏, 林闖. 互聯(lián)網(wǎng)體系結(jié)構(gòu)評(píng)估模型、機(jī)制及方法研究綜述[J]. 計(jì)算機(jī)學(xué)報(bào), 2012, 35(10): 1985-2006)

[4]Zhu Min, Xu Ke, Lin Song. The evaluation method towards the application adaptability of Internet architecture[J]. Chinese Journal of Computers, 2013, 36(9): 1785-1798 (in Chinese)(朱敏, 徐恪, 林嵩. 面向應(yīng)用適應(yīng)能力的互聯(lián)網(wǎng)體系結(jié)構(gòu)評(píng)估方法[J]. 計(jì)算機(jī)學(xué)報(bào), 2013, 36(9): 1785-1798)

[5]Ahlgren B, Brunner M, Eggert L. Invariants: A new design methodology for network architectures[C] //Proc of ACM SIGCOMM’04 Workshop on Future Directions in Network Architecture. New York: ACM, 2004: 65-70

[6]Rexford J, Dovrolis C. Future Internet architecture: Clean-slate versus evolutionary research[J]. Communications of the ACM, 2010, 53(9): 36-40

[7]Feldmann A, Telekom D, Berlin L T. Internet clean-slate design: What and why?[J]. ACM SIGCOMM Computer Communication Review, 2013, 37(3): 59-64

[8]Xu Ke, Zhu Liang, Zhu Min. Architecture and key technologies of Internet address security[J]. Journal of Software, 2014, 25(1): 78-97 (inChinese)(徐恪, 朱亮, 朱敏. 互聯(lián)網(wǎng)地址安全體系與關(guān)鍵技術(shù)[J]. 軟件學(xué)報(bào), 2014, 25(1): 78-97)

[9]Ramirez W, Masip-Bruin X, Yannuzzi M. A survey and taxonomy of ID/Locator split architectures[J]. Computer Networks, 2014, 60(2): 13-33

[10]Andersen D G, Balakrishnan H, Feamster N, et al. Accountable Internet protocol (AIP)[C] //Proc of ACM SIGCOMM’08. New York: ACM, 2008: 339-350

[11]Clark D, Braden R, Falk A, et al. FARA: Reorganizing the addressing architecture[C] //Proc of ACM SIGCOMM 2003. New York: ACM, 2003: 313-321

[12]Atkinson R, Bhatti S, Hailes S. ILNP: Mobility, multi-homing, localised addressing and security through naming[J]. Telecommunication Systems, 2009, 42(4): 273-291

[13]Balakrishnan H, Lakshminarayanan K, Ratnasamy S, et al. A layered naming architecture for the Internet[C] //Proc of ACM SIGCOMM 2004. New York: ACM, 2004: 343-352

[14]Choi J, Park C, Jung H, et al. Addressing in future Internet: Problems, issues, and approaches[C] //Proc of the 3rd Int Conf on Future Internet Technologies. Piscataway, NJ: IEEE, 2008: 123-129

[15]Shoch J F. Internetworking naming, addressing, and routing[C] //Proc of the 17th IEEE Computer Conf. Piscataway, NJ: IEEE, 1978: 72-79

[16]Saltzer J. On the Naming and Binding of Network Destinations: RFC1498[S/OL]. Fremont, CA: IETF, 1993 [2015-11-19]. http://www.rfc-editor.org/rfc/rfc1498.txt

[17]Zhang L, Afanasyev A, Burke J, et al. Named data networking[C] //Proc of ACM SIGCOMM 2014. New York: ACM, 2014: 66-73

[18]Hearer C A R. Communicating sequential processes[J]. Communications of the ACM, 1978, 21(1): 666-677

[19]Karsten M, Keshav S, Prasad S, et al. An axiomatic basis for communication[C] //Proc of ACM SIGCOMM 2007. New York: ACM, 2007: 217-228

[20]Hoare C A R. An axiomatic basis for computer programming[J]. Communications of the ACM, 1969, 12(10): 576-580

A Formal General Framework of Internet Address Mechanisms

Zhu Liang, Xu Ke, and Xu Lei

(Department of Computer Science and Technology, Tsinghua University, Beijing 100084)

The address mechanism is the most essential and important part of the Internet architecture and its evolution determines the capacity of the Internet to accommodate the innovative applications. The traditional IP-based address strategy gets the current Internet into ossification which makes the architectural innovation become a consensus. Many novel address strategies make significant extensions or innovations for the traditional model but lack of common design principles and consistent expression model. It has become difficult to insight into future evolution progress of the address schemes for the diversity and heterogeneity. Moreover, we believe that a diversity address mechanism might coexist in the Internet architecture to meet the ecological evolution of network applications. To tackle the above problems, by researching the evolution of the Internet address mechanisms and abstracting a minimal architectural core, a general framework for accommodating the diversity and heterogeneity of various address strategies is proposed in this paper, including: 1) formal and verifiable conceptual model forms a consistent theoretical framework within which the invariants and design constraints can be expressed; 2) abstract multi-dimensional and extensible interface primitives and interactive patterns with the communication axioms to provide a proof framework for the Internet address schemes; 3) derive working prototype implementations—Universal Engine of Address Schemes which allows us to construct the various address mechanisms with flexibility and support the evaluation, evolution and coexistence of the Internet address strategies, in order to meet the ecological evolution of network applications.

Internet architecture; general framework; formalism; address mechanisms; correctness proof

Zhu Liang, born in 1982. PhD candidate. His main research interests include Internet architecture and its evaluation.

Xu Ke, born in 1974. Professor, PhD supervisor. His main research interest include Internet architecture, high perfor-mance router, P2P network, Internet of things and network economics.

Xu Lei, born in 1983. PhD candidate. His main research interests include datacenter networking and software-defined networking.

2015-12-20；

2016-04-19

國(guó)家自然科學(xué)基金面上項(xiàng)目(61170292，61472212)；國(guó)家科技重大專項(xiàng)基金項(xiàng)目(2015ZX03003004)；國(guó)家“八六三”高技術(shù)研究發(fā)展計(jì)劃基金項(xiàng)目(2013AA013302，2015AA015601)；國(guó)家“九七三”重點(diǎn)基礎(chǔ)研究發(fā)展計(jì)劃基金項(xiàng)目(2012CB315803)；歐盟CROWN基金項(xiàng)目(FP7-PEOPLE-2013-IRSES-610524);清華信息科學(xué)與技術(shù)國(guó)家實(shí)驗(yàn)室(籌)學(xué)科交叉基金項(xiàng)目 This work was supported by the General Program of the National Natural Science Foundation of China (61170292, 61472212), the National Science and Technology Major Project of China (2015ZX03003004), the National High Technology Research and Development Program of China (863 Program) (2013AA013302, 2015AA015601), the National Basic Research Program of China (973 Program) (2012CB315803), the EU Marie Curie Actions CROWN (FP7-PEOPLE-2013-IRSES-610524), and the Multidisciplinary Fund of Tsinghua National Laboratory for Information Science and Technology.

徐恪(xuke@mail.tsinghua.edu.cn)

TP393