一種形式化的互聯網地址機制通用框架

朱 亮 徐 恪 徐 磊

(清華大學計算機科學與技術系 北京 100084)(tshbruce@gmail.com)

一種形式化的互聯網地址機制通用框架

朱 亮 徐 恪 徐 磊

(清華大學計算機科學與技術系 北京 100084)(tshbruce@gmail.com)

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

互聯網體系結構；通用框架；形式化；地址機制；正確性證明

以IP地址機制為核心的互聯網體系結構取得了巨大成功，既能兼容異構的底層技術，也支撐著層出不窮的網絡應用，保證了互聯網的泛在連接性和旺盛的生命力.隨著互聯網與經濟、社會以及傳統行業各領域的深度融合，“互聯網+”代表著一種新的社會經濟形態而誕生，以互聯網為紐帶催生了大量的創新應用，全面提升了社會發展力[1].

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

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

1 抽象通信模型

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

1.1 模型定義

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

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

我們首先定義5個概念：

1) 消息(message).通信中的抽象數據交換單元.在實際網絡中，消息可實例化為分組或MAC幀等具體格式.對于該通信模型，我們只關注其抽象結構而非比特層面的視圖.一般來說，消息包含了一組頭部域(源信息和目的信息等)用來指示轉發狀態，我們將這樣的頭部域稱之為轉發指令(forwarding instructions,fi)，fi可在消息傳遞過程中被特定網絡實體重寫.

2) 抽象通信對象(abstract communication object, ACO).參與網絡通信的一般性抽象對象，也是原型系統實現的核心抽象類，以下簡稱對象.ACO可理解為網絡中的一層協議棧或是交換引擎等通信組件.除了消息傳遞，ACO內部還包含一些功能組件對輸入的消息進行處理.實際的網絡實體可通過繼承ACO并與其他子組件(緩存等)通過特定機制聚合而產生.

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

4) ACO內部通常維護著一組映射表(local switching table)，交換服務(switching service)通過查詢本地映射表或是第三方ACO(如分布式映射系統)，根據返回的結果對轉發指令fi進行相應處理.交換過程通過執行抽象對象，轉發指令二元組之間的映射以指明消息的后續轉發狀態，對象B查找本地交換表獲取A和C的映射關系可表示為SPB(A,fi):A,fi|→C,fi′.

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

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

對象ACO的行為由接口域和交換行為構成.接口域是輸入和輸出端口對消息操作原語的并集，定義了消息在端口上的轉發操作，如發送、接收、調用等；交換服務描述了轉發指令層面上的交換行為，通過查詢映射表獲取相應的fi，以指明該消息后續的轉發狀態；當上述過程完成之后，適配服務根據獲取的轉發指令對轉發的消息進行適配處理，并依據通信角色輸出到相應的實例化通道上.

基于該抽象模型的語義描述，對于特定對象而言，1次抽象通信可被表述為基本通信組件基于3種消息操作的交互過程，即交換(switching)、轉發(forwarding)、適配(adaption).抽象組件可通過聚合、繼承而構造具體的通信實體，實現了模型的可擴展性；而交互過程的抽象保證了不同類型操作模式的松耦合以及模塊化特性，以便本文更加清晰地解構互聯網地址機制中復雜的交互過程.

1.2 基本通信性質

通過對該基本通信模型的觀察，我們推導出以下重要通信公理化性質，其中→表示事件發生的先后順序.

性質1. 直接轉發(direct forwarding).

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

性質2. 交換(switching).

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

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

性質3. 傳遞性(transitivity).

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

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

性質4. 可達性(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.

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

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

m!CSOP→m′?ASIP.

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

抽象通信模型針對轉發指令fi的不同操作模式，抽象出基本交互模式，涵蓋了地址體系的核心通信過程.事實上，上述基本性質同樣可歸納為2.1節中提到的核心抽象過程，即交換、適配和轉發.該模型可實例化為任何一種地址機制的交互場景，為了使結構更加清晰，本文將基于上述抽象模型和通信性質，從與轉發指令實例相關的概念模型以及組件間交互的動態過程框架2個方面分別進行闡述和討論.

2 地址機制的統一概念模型

互聯網地址機制自設計以來，一直存在著相關概念定義的爭論[15]，基本通信術語缺少統一、明確的定義.另外對于一些過程模式如綁定、尋址等存在著概念層面上的歧義和不一致性.為保證通用的設計原則和理念，我們將針對以上概念提出一套合理、統一的解釋模型，并基于集合論以及關系代數賦予了形式化說明.基于該模型進行地址標識機制設計時，設計理念可被精確且一致地表達，同時相關設計原則可依據模型進行規范性檢查.

2.1 命名空間

為了對分布式系統中的實體進行區分和訪問,有必要給其中的對象分配標識.命名(naming)就是給互聯網的用戶、設備、服務和數據等ACO分配與其自身相關聯的語法符號(symbols).命名空間(namespace)是由特定語義范疇(semantic scope)內的命名關系構成的集族，指標集為{aco,symbols}.語義范疇內的通信對象遵循相同命名規范，滿足以下定義.

定義1. 語義范疇.

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

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

Fig. 2 Naming and resolving in the current Internet圖2 當前互聯網命名解析層次式模型

例如當前互聯網協議棧中HTTP ACO 與IP ACO則分別屬于2個不同的語義范疇，從而關聯著不同的命名空間.命名空間應被看作aco,symbols的集合，命名對象決定了命名空間語義上的概念范疇，即標識何種類型或何種屬性；命名規范則體現了語法上的表現方式.我們引入集合：可命名對象O，屬于特定semantic scope的對象SO，任意符號集合S，其中SO∈O.則命名空間定義如下：

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

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

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

2.2 綁定、解析和尋址

命名空間的語義被限制在一定概念范圍內導致不同語義范疇內的通信組件無法直接交互.為實現通信，綁定(binding)提供了訪問異構命名空間的入口，也就是說，綁定關系B實際上構造了基于semantic scope的拓撲，為避免解析死循環，該拓撲應為有向無環圖(DAG).綁定關系存在于不同語義范疇中的抽象通信對象之間：

定義3. 綁定.

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

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

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

定義4. 解析.

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

解析過程返回一組有序對的集合，e表示指向下一個semantic scope入口引用.事實上，解析也是鄰居發現的過程.對綁定拓撲進行遞歸或者分布式的解析過程為尋址(addressing)，目的是為了獲取最終可用于轉發的標識符.結合通信的可傳遞性(性質4)，引入2種關系概念.

1) 關系復合.對于任意二元關系R:X?Y,S:Y?Z來說，R°S={x:X;z:Z|(?y:Y·(xRy∧ySz))·x|→z}；例如(x|→y)∈R,(y|→z)∈S?(x|→z)∈R°S.

2) 自反傳遞閉包.對于任意二元同類關系R,Rk表示對其進行k次復合，即R2=R°R.則自反傳遞閉包由包括R0在內的所有的R關系復合的并集構成，即：

基于以上關系運算，尋址過程可定義如下：

定義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 名字、地址、身份標識和位置標識

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

定義7. name & address：

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

?acoxNnx?nx=name ofacox；

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

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

定義8. Identifier & Locator:

對于在特定name scope內唯一的語法符號n,?aco,n,aco,n′∈NScope(aco,n):

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

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

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

圖2為當前互聯網的層次式解析模型，為保證通用性，圖3基于semantic scope說明了地址機制概念模型及其關系.對通信對象而言，名字和地址是基于命名和綁定關系而產生的屬性，而身份標識和位置標識則是命名空間在通信中承擔的角色.身份標識和位置標識可以產生自同一命名空間.滿足定義8的名字可用作身份標識，當網絡對象相對于邏輯位置不發生移動，即實體與其位置屬性靜態綁定時，地址同樣可以作為身份標識使用.地址若要作為位置標識使用，必須在特定位置空間內能唯一標識相對位置；而包含位置屬性，能在特定空間中唯一定位的名字也可以成為位置標識.

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

3 地址機制的通信交互模式

上述概念模型為地址策略的設計提供了明確的解釋視圖以及統一的設計原則.本節中，我們將對地址機制中的動態交互過程進行多維度抽象，獲取核心的標準接口以及交互模式，以構造一種可以兼容異構地址機制的最小化通用過程處理框架.在進行地址機制設計時，該框架能夠依據交互模式以及行為語義對通信行為進行正確性檢查.

3.1 交互模式與原語

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

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

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

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

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

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

1) 轉發模式

fiGetfi(msg)：

從消息中獲取相應轉發指令fi并返回，具體的轉發信息可依據具體機制實例化.

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

對應于通信性質1，將消息發送到對端的輸入端口，值得注意的是，從邏輯上來說，該消息還沒有進行適配處理.

接收消息并返回該消息和發送方aco.

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

將消息拷貝到輸出端口.

2) 尋址模式

messagerequest(aco,fi)：

將請求解析的fi放入請求消息中.

該原語執行解析操作，映射系統的具體實現機制可以靈活定義，不在本文討論的范圍內.由性質2可知，該原語返回一組aco,fi.

messageresponse(fi,aco)：

將查詢的結果放在響應消息中.

3) 適配模式

encap(fi,msg)：

為消息封裝1個協議相關的頭部，通常用于隧道的入口處或協議層之間.

fidecap(fi,msg)：

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

encrypt(method,msg)：

使用加密機制對消息進行加密，具體的加密方法可以靈活定義.

swap(fi,msg)：

對消息中轉發指令fi進行替換，例如MPLS和NAT中的標簽交換.

deliver(msg)：

消息不經過任何處理，直接轉發.

3.2 通道實例及語義規約

在圖1的通信模型中，適配服務作為通道行為的一部分提供，目的在于分離對象的轉發行為與對象間的交互行為，實現通道實例的可重用，從而降低通信過程的復雜性.通信對象的自身行為被封裝，交互行為的語義規約到通道上，可作為獨立于具體通信機制的多語義連接件使用.通道實例基于角色(role)和粘合劑(glue)進行語義說明.role描述了aco所期望的外部行為規范；glue用于規定各個role的行為時序，協調抽象通信對象間的交互行為.基于適配模式對消息的操作，我們定義通道實例:

ChannelEncap-Channel=

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

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

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

該通道實例對消息進行封裝操作，可連接不同協議層實現通信.考慮消息從傳輸層加上IP頭部，再發送給網絡層接收.

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)→√).

通道的網關模型.該模型與封裝方式的區別在于替換而不是封裝標簽，例如NAT以及MPLS中的標簽交換.

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()).

客戶服務器交互通道，適用于解析請求或者過程調用等通信連接.注意客戶角色使用內部選擇符而服務器角色使用的是外部選擇符，也就是說，客戶端能夠主動結束請求，而服務器不能主動結束服務，只能由外部觸發決定其結束與否.基于該通道設計客戶服務器模型可以根據通道語義得到有效驗證.另外，我們還定義了加密通道、轉發通道等其他實例，這里不再一一贅述.

該通用過程框架包含了經過觀察、精心選擇和構造的核心接口原語，可快速靈活地構建交互模式實例，通信對象之間通過通道實例交互，實現轉發與交互行為的松耦合.

4 構造與驗證實例

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

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

Fig. 4 Abstract processing of map-encap scheme圖4 Map-encap地址機制抽象過程

4.1 配置定義

考慮到配置描述的精確性和可重用性，我們基于XML對地址方案進行描述，并提出了3類XML描述規范(schema):通信實體定義、拓撲配置以及命名空間語法語義規則.描述規范嚴格對應于本文提出的概念模型，以保證一致性的設計約束規范檢查.圖5為map-encap地址機制的XML描述，限于篇幅，我們截取部分定義，并省略過多的XML語法符號.

通信實體配置定義了對象的繼承或聚合機制；拓撲描述實體基于通道實例的連接關系，同時包含了交互行為的語義約束；命名空間包括語義規范和語法規則2個方面.本文第2節定義的概念約束了語義規范的設計，并能夠進行檢查；語法規則規定了數據類型，比如以正則表達式匹配地址格式等.基于上述3類XML schema，地址機制可被靈活定義描述，同時保證設計方案的一致性和正確性.

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

4.2 交互過程

在3.1節中，我們提出了一組精煉的核心接口原語，為驗證其通用性，我們以圖4中ITRA的通信行為為例，基于上述原語來構建3種基本交互模式，從而實現map-encap地址機制抽象通信過程.另外，我們基于斷言技術，用一組謂詞公式來刻畫程序在執行過程中的狀態，通過考察各斷言能否成立，實現對程序正確性的證明；圖6以偽代碼形式刻畫了ITRA的一般抽象通信行為，并插入了適當的斷言.

可以看出，基于標準接口構建的3種基本交互模式完成了ITRA的通信行為，而諸如lookup等接口則依賴于具體協議機制實現.在實現中，并不需要所有的抽象對象都具有完備的接口實現，這里描述的是通用的交互過程，任何實際策略均可通過與具體協議相關的繼承、改寫、實例化而獲得.

Fig. 6 The abstract processing圖6 抽象通信過程

4.3 程序正確性證明

程序正確性證明指的是通過形式化的推導，評價一個程序是否符合特定規范.本節我們使用Hoare邏輯，以1.1節以及3.1節中的通信性質和行為語義為證明依據，來證明上述抽象過程的正確性.文獻[19]針對轉發過程中名字和地址的移除模式，利用Hoare邏輯證明了轉發過程的正確性.圖7為Hoare邏輯的規則描述.

Fig. 7 Hoare logic rules圖7 Hoare 邏輯的規則描述

Hoare邏輯[20]是對斷言方法的推廣，并建立了1套公理系統，其公理和命題的一般形式為：{φ}Q{ψ}.其中φ,ψ為邏輯表達式，Q是1個程序段.整個表達式的含義是：如果在Q執行之前有φ成立，并且Q能終止執行，則必有ψ成立，通常將φ,ψ稱為前置斷言(pre-condition)和后置斷言(post-condition).為了證明不變式語句，Hoare公理系統引入了1條賦值公理和4種推理規則，如圖7所示，其中橫線上方的語句為假設，下方是可推導出的結論，其語義為：如果所有的假設成立，則結論必然成立.對于map-encap機制而言，合理的前置斷言應為主機X將需要解析的fi發送到A的輸入端口；當一系列交互過程完成后，后置斷言為：A將含有解析完畢，經過封裝的fi′拷貝到輸出端口，基于上述規則，我們在程序以及循環的開始和結束處分別插入斷言.

φ: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′).

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

Goal 1：{φ}process{ψ}，由順序規則可轉換為3個Hoare三元組的證明：

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

1) 為證明Goal 2，即轉發后消息到達R并且尋址沒有完成，由賦值公理和推斷規則，只需證明:

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

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

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

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的含義為尋址過程沒有結束，對其使用賦值公理、推斷規則、交換性質(性質2)以及尋址定義(定義6)，Goal 5得證，即：

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

同理，Goal 6的含義為尋址結束并將結果返回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接收到解析結果并封裝在新消息中，發送到輸出端口.由賦值公理、推斷規則以及encap，copy的行為語義可得：

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 通用地址機制引擎

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

如圖8所示，通用地址機制引擎的結構框架.網絡通信實體、命名空間語法語義和拓撲配置以XML描述并存儲在本體庫中，以模板形式調用.最核心的抽象基類是本文一直強調的ACO，Message以及Channel，在引擎中以Java抽象類定義，并提供了基本的操作原語.具體通信主體可以通過對3種抽象類的繼承或實例化而獲取.3種基本交互模式以及相應的操作原語以類庫形式提供，供通信主體調用以構造實際通信過程.為了進一步增加功能的完備性，我們提供了1個組件庫供設計時以服務形式調用，包括安全機制、前綴聚合機制、地址映射機制等.我們為組件庫的每個服務組件指定了1個標識符，應用調用的時候只需傳遞這個標識符，實現了組件庫的可擴展性而無需影響已有應用.引擎管理器解析XML配置文件以及定義交互模式，并根據本文前面介紹的概念模型與組件語義進行正確性、完備性檢查，最后生成地址機制實例運行.

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

通用地址框架可為異構的地址標識方案提供統一的構造、部署平臺.研究人員調用或者自定義本體庫中的通信組件，基于我們預先定義的XML描述規范，將特定地址機制形成腳本描述并提交至引擎管理器；引擎管理器依據語法語義規則對該腳本進行驗證和解析，并調用相應服務組件以實例化地址機制并注入運行時網絡.

另外，通用地址機制框架并非列舉地址體系中所有的通信組件或行為，而是通過精煉1個最小化靜態核心來保證設計的完備性和最大限度的自由性.比如框架內并沒有限定地址的聚合機制以及映射更新機制等，而是允許設計人員根據實際地址策略靈活定義、調整以及評估，從而選擇其中最優的設計方案.

6 結束語

本文通過對互聯網地址體系異構及多樣性的深入研究，抽象出其本質特征屬性，提出了完備的形式化概念模型，并利用精心構造的最小化交互模式來靈活構造地址機制的抽象通信過程.基于上述概念與過程框架，推導出可兼容異構地址策略并存的通用平臺以及其原型系統，任何期望的地址機制都可以在概念及行為語義的約束下靈活定義實現.

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

[1]Zheng Qinghua. The introduction of application technology-oriented “Internet+”[J]. Journal of Computer Research and Development, 2015, 52(12): 2657-2658 (in Chinese)(鄭慶華. 面向“互聯網+”的應用技術專題前言[J]. 計算機研究與發展, 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)(徐恪, 朱敏, 沈蒙. 面向應用的可演進互聯網體系結構[J]. 中國計算機學會通訊, 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)(徐恪, 朱敏, 林闖. 互聯網體系結構評估模型、機制及方法研究綜述[J]. 計算機學報, 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)(朱敏, 徐恪, 林嵩. 面向應用適應能力的互聯網體系結構評估方法[J]. 計算機學報, 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)(徐恪, 朱亮, 朱敏. 互聯網地址安全體系與關鍵技術[J]. 軟件學報, 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

國家自然科學基金面上項目(61170292，61472212)；國家科技重大專項基金項目(2015ZX03003004)；國家“八六三”高技術研究發展計劃基金項目(2013AA013302，2015AA015601)；國家“九七三”重點基礎研究發展計劃基金項目(2012CB315803)；歐盟CROWN基金項目(FP7-PEOPLE-2013-IRSES-610524);清華信息科學與技術國家實驗室(籌)學科交叉基金項目 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