一种形式化的互联网地址机制通用框架

朱 亮 徐 恪 徐 磊

(清华大学计算机科学与技术系 北京 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