信令系统的过程演算及分析方法

© 2014 Yasuyuki Ibayashi和Shin-ya Nishizaki。出版社：Elsevier B.V.信息工程研究院负责评选和同行评议可在www.sciencedirect.com在线获取ScienceDirectIERI Procedia 10（2014）160 - 1682014未来信息工程信令系统的过程演算Yasuaki Ibayashi，Shin-ya Nishizaki*东京工业大学计算机科学系东京都目黑区大冈山2-12-1-W8-69邮编152-8552摘要软件系统在社会基础设施以及公共和私营部门中发挥着重要作用，例如在核心银行，企业资源规划系统，电子医疗记录系统，电话交换系统等。形式化方法，如软件验证，关注的是正确性而不是健壮性。西崎等人提出的Spice演算，是一个演算过程，使我们能够形式化和分析的通信协议对拒绝服务攻击的抵抗力。分析的核心思想是分析通信协议中发起者和响应者的代价。在本文中，我们扩展了Spice演算分析系统的目标区域，并描述了一种新的分布式系统分析方法。我们演示了一个电话交换系统的分析，作为我们的方法的一个例子。在本文中，我们扩展的Spice演算分析系统的目标区域，并显示一个新的分析方法，分布式系统。我们演示了一个电话交换系统的分析，作为我们的方法的一个例子。以七号信令系统的ISUP为目标，在Spice演算的框架下，形式化了一个基于它的简单电话网。分析了其连接建立过程和连接建立所消耗的计算开销。版权所有© 2014作者.出版社：Elsevier B.V. 这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/3.0/）。信息工程研究院负责评选和同行评议关键词：进程演算，通信协议，电话交换系统，成本分析* 通讯作者。联系电话：+81-3-5734-2772;传真：+81-3-5734-2772。电子邮件地址：nisizaki@cs.titech.ac.jp。2212-6678 © 2014作者出版社：Elsevier B.V. 这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/3.0/）。信息工程研究所负责的选择和同行评审Yasuaki Ibayashi和Shin-ya Nishizaki / IERI Procedia 10（2014）1601611. 介绍软件系统在社会基础设施以及公共和私营部门中发挥着重要作用，例如在核心银行业务、企业资源规划系统、电子病历系统、电话交换系统等。在这些基础系统中，我们不仅需要规范要求的正确性，还需要稳健性以应对意外情况。形式化方法，如软件验证，关注的是正确性而不是健壮性。在这样的IT系统中发生了许多故障。例如，日本最大的银行公司瑞穗金融集团的核心银行系统于2011年3月14日发生故障，直到23日才恢复，原因是东北地震的大量捐款造成了超负荷[7]。计算机系统的这种长时间故障可以通过系统鲁棒性的改进来减轻。形式化方法，如软件验证，关注的是正确性而不是健壮性。由Nishizaki等人提出的Spice演算[9]，是一个演算过程，它使我们能够形式化和分析通信协议对拒绝服务攻击的抵抗力，基于Milner的pi演算[6]。分析的核心思想是分析通信协议中发起者和响应者的代价。拒绝服务攻击的漏洞是由于发起者和响应者之间缺乏平衡造成的。成本分析不仅对于抵抗拒绝服务攻击非常重要，而且对于提高系统的鲁棒性以抵抗各种意外情况也非常重要。因此，在本文中，我们应用Spice演算的分布式系统的鲁棒性分析。我们进行了一个案例研究，使用电话交换系统，作为一个例子。2. 香料结石我们在本节中介绍Spice演算[9]。在微积分中，有两类表达式：一类是项的集合，另一类是过程的集合。术语表示数据，过程表示可以同时执行的一系列计算操作。spice-calculus的术语归纳定义如下：Spice演算的过程归纳定义如下：162Yasuaki Ibayashi和Shin-ya Nishizaki / IERI Procedia 10（2014）160消息发送（out M）通过端口M发送消息N。 消息接收（inp M（x）; P）通过端口M接收消息并将其绑定到变量x。并行分解（P|Q）并行执行进程P和Q。停止处理停止意味着在到终止处理结束的途中的中间状态。在我们的计算系统中，内存分配和释放显式地操作为进程（存储x=M;P）和（自由x;P），分别。匹配（matchM isN err {P};Q）是一个条件分支：如果M和N的值相等，则执行P;否则执行Q。选择（P+Q）是一个非确定性的选择;P或Q都是非确定性地执行的。Spice演算的类型系统是它的显著特征之一，它使我们能够指定每个计算机节点所需的计算成本例如，流程（P1|（Q |P2））属于A型（B <$A），即，其描述了在B上的计算机节点A和Q上执行进程P1和P2。Spice演算的类型定义如下：操作语义的Spice演算过程之间的过渡关系，计算成本附加到每个步骤的过渡。比如说，这种转变意味着， 进程P和Q分别在节点a和b上并行执行; 过程（PQ）过渡到（P 在这种转换中，匹配和存储操作是用两个匹配成本和一个存储成本来完成的分别转换关系由几个规则归纳定义（参见[9]）。以下是定义进程内计算的一个归约规则：如果假设计算M和N的成本分别为c和d，并且M和N的结果值均为V，则表达式转换为Q，转换的计算成本为（c+d+match）。下面的规则是定义进程间计算的归约规则之一：这个规则意味着如果进程表达式（inp n（x）; P）在计算机节点a上执行，则变量x的内存成本存储在a上。它被转换为表达式（x）P，表示等待消息到达的中间形式。Yasuaki Ibayashi和Shin-ya Nishizaki / IERI Procedia 10（2014）160163Fig. 1.交换电话网络图二.城市间通话3. 一个信令系统的SPICE演算3.1. 七号信令系统与ISUP在本节中，我们使用Spice演算[9]形式化了基于电话信令协议7号信令系统（SS7）[3]的交换电话网络。我们集中在一个简单的交换电话网络，其中包括两个交换机和几个电话的例子。其网络拓扑结构如图所示。1.一、在SS7中，ISDN用户部分（ISUP）定义了在公共交换网络上建立和拆除呼叫时使用的消息和协议，并管理它们中继的中继网络。ISUP在图2中被描绘为序列图。终端节点PhoneA和PhoneB正在连接，中间交换机SwitchA和SwitchB中继连接。ISUP中定义了控制消息iam、acm、anm、rel和rlc。使用的消息如下。 IAM（初始地址消息），这是发送的第一条消息，用于通知伙伴交换机必须建立呼叫。 ACM（地址完成消息），当用户达到了 ANM（应答消息），当用户拿起电话时发送。 REL（释放），当用户挂机时，发送REL以清除呼叫 RLC（Release Completed），释放完成，这是对释放的确认图3的状态转换图描述了电话的行为。电话的型号接收消息：拨号音，铃声，无音，忙音和检查。前四个消息表示来自伙伴交换机的状态通知，后一个消息给出可连接性的确认。该模型发送摘机、挂机和拨号消息，前两个消息分别描述了手机摘机和挂机的信号。后一个消息表示拨号信号。164Yasuaki Ibayashi和Shin-ya Nishizaki / IERI Procedia 10（2014）160图三.电话转换图3.2. Spice演算在Spice演算中，电话（即用户）和交换机的行为被形式化为进程。电话a及其伙伴交换机A的行为被描述为订户（a，A，B，b），该订户（a，A，B，b）与电话b及其伙伴交换机B的连接，订户（a，A，B，b）被划分为两个子过程，订户（a，A，B，b）和接收者（a，A）：Yasuaki Ibayashi和Shin-ya Nishizaki / IERI Procedia 10（2014）160165在用于通信的过程中使用的端口在图1A和1B中描绘。4和5.见图4。中间端口（在建立连接之前）图五.中间端口（建立连接后）在这里介绍论文，并在必要时添加术语，在一个与论文其余部分相同字体大小的框中。段落从这里继续，仅由标题，副标题，图像和公式分开。各节标题按数字排列，并以粗体和10磅显示。以下是对作者的进一步说明。3.3. Spice Calculus在本节中，我们将展示一种情况的成本分析，在这种情况下，拥有伙伴交换机A的用户a请求连接到拥有伙伴交换机B的用户b。这比图1和图2中提到的情况更简单。4和5.用户a1、a2、a3简化为只有一个用户a; b1、b2、b3简化为b。这种情况下的行为描述为以下过程。166Yasuaki Ibayashi和Shin-ya Nishizaki / IERI Procedia 10（2014）160通过简化描述系统的过程，我们不仅可以看到计算结果，而且可以看到总成本。Yasuaki Ibayashi和Shin-ya Nishizaki / IERI Procedia 10（2014）160167总结每个转换步骤的成本，我们可以看到总计算成本如下：4. 相关作品在过去的十年里，协议验证已经使用了几种不同的框架进行了研究。例如，Bruns等人研究了MSMIE协议，该协议允许分布式系统中的处理器通过共享内存进行通信。他们在Milner的CCS中提供了一个MSMIE协议的形式化模型，并使用自动验证工具Concurrency Risk分析了该形式化模型。通信和安全协议的定量分析由作者之一[9]研究，但也由Cervesato [2]研究，它可以使用MSR（多集重写）规范语言评估协议对各种形式的拒绝服务，猜测攻击和资源限制的弹性。Liu等人[5]在有色Petri网的框架中形式化并验证了能力交换信令（CES）协议，该协议是用于多媒体通信的H.245控制协议的子协议。5. 结论在本文中，我们提出了一个案例研究，其中我们形式化的连接建立部分的通信协议在实际使用中，信令系统7号使用香料演算提出了在以前的工作[9]。我们从计算成本的定量角度对此进行分析。从这个案例研究中，我们可以看到，Spice演算有足够的表达能力来描述实际使用的系统的协议。使用spice演算分析通信协议过于复杂，如果没有自动化软件支持，很难处理。在我们以前的工作[4]中，我们提出了一种通过数值模拟对分布式系统进行符号分析的方法。这是一个很有前途的研究方向。此外，还需要扩展Spice演算以提高其表达能力;例如，将环境演算[8]统一到Spice演算中将使我们在网络拓扑中具有更大的灵活性。168Yasuaki Ibayashi和Shin-ya Nishizaki / IERI Procedia 10（2014）160确认这项工作得到了科学研究补助金（C）（24500009）的支持引用[1] Bruns，G.，安德森，S.：通信协议的形式化与分析。Formal Aspects of Computing 6（1），92-112（1994）.[2] 切尔韦萨托岛：对定量安全分析的概念。In：D.Gollmann，F. Massacci，A.Yautsiukhin（编辑）保护质量：安全措施和安全- QoP'05，pp。131-144. Springer-Verlag Advances in InformationSecurity 23（2006）[3] 德里堡湖Hewitt，J.：7号信令系统（SS 7/C7）：协议、体系结构和服务。03 The Dog（2004）[4] 池田河成田县，Nishizaki，S.：分布式系统代价分析的模型检测与网络仿真的协同国际计算机与应用杂志33（4）（2011）[5] 刘，L.，比林顿，J.：验证能力交换信令协议。International Journal on Software Tools forTechnology Transfer 9（3-4），305-326（2007）.[6] 米尔纳河，Parrow，J.，沃克，D.：移动过程演算，第一部分和第二部分。信息与计算100（1），1-77（1992）[7] 从近期计算机系统故障看故障原因、改进方案及对策。瑞穗金融集团（2011年）。http://www.mizuho-fg.co.jp/english/csr/mizuhocsr/calendar/2010/highlight_system/plan.html[8] Nishizaki，S.：多态环境演算及其类型推理算法。高阶和符号计算，Kluwer 13（3），239-278（2000）[9] Tomioka，D.，Nishizaki，S.，Ikeda，R.：一种用于分析拒绝服务攻击的代价估计算法。软件安全-理论与系统计算机科学讲义，卷3233，页。25-44.柏林海德堡施普林格出版社（2004）。如果你愿意，可以在附录中加上一个小标题。