spitojava：由spi演算自动生成的java代码的密码协议

1、spitojava：由spi演算自动生成的java代码的密码协议 摘要:这项工作的目的是描述一个自动生成java代码实现在 正式规范中描述的协议语言spi演算的加密ospitojava是spi 演算的一组工具的一部分，还包括一个预处理器，一个分析 器和一个安全分析仪。后者可以较为正式地分析协议和检测 协议的缺陷。当一个协议进行了分析并且对其已经达到的正 确性有足够的信心，spi2java可以生成一个相应的正确的 java实现的协议，从而大大减少在编码阶段引入的安全缺陷 的风险。1简介一个在现代计算机科学中最具挑战性的实际问题是如 何保证设计和实现正确的安全协议。这样的协议扮演的角色 是实现安全

2、冃标，例如通过使用加密技术实现身份认证，保 密性和完整性。出于这个原因，他们也被称为加密协议。最近，许多研究工作一直致力于分析加密协议的逻辑正 确性的问题（如11）,而实现正确性的问题还 没有被认为是这么多。其中一个可能的方法，从正式规范7 12 9实现自动牛成以确保实施正确性。如果代码发牛器是 这样的，在生成的代码忠实地实现了本说明书和避免编程错 误，可能会导致安全漏洞，实施正确的可取的。因此，如果 源规范在逻辑上是正确的，那么它就实现了。在本文中我们 将展示如何将这种方法可在框架屮投入实践，其中目标代码 语言是java和密码协议在spi演算1中被指定，这个过程代 数规范语言专门为这种协议定

3、制。2spi演算该spi演算在1屮被定义为一个扩展口演算与加密 基元。它是一个为描述和分析加密协议而设计的过程代数语 言。该spi演算有两个基本的语言：术语，表示数据和流程， 以代表的行为。在本文屮，我们只介绍一些功能spi演算， 通过一个例子，由于有限的空间。图。fig.l显示了 spi calculus 1规范安德鲁5密钥交换协议。a->b： a,na®a) cab<a,na>.pbo>cab(xa, xna).b->a： (na,klab)kabcab(xm5g). (ftceystore) keystore<b>. keystore(

4、kab). case xmsg ofxna?xklabkab in xna is na(*3keystore) keystore<xa>. keystore(kab).(®klab) cab<xna,klabkab>.a->b： najklabcab<naxklab>.cab(xmsgcypher). case xmsgcypher of xnewnaklab in xnewna is xna keystore<xa,klab>.b->a： nbcab(dimy). keystore<b,xkla&>.(

5、snb) cab<nb>.a->b： ooklabcab<mxklab>.0cab(wcypher). case cypher of xklab in 0inst(m)>(pa(m)|pbo)figure 1. the andrew protocol spi calculus specification本说明书是由两个过程描述命名为pa和pb,这代表了 该协议的两个角色。该研究过程所表示的相互作用场景：pa 和pb同时运行的一个实例。发起者角色的过程pa和研究所 过程是由m数据参数化，且必须被发送。m作为一个参数 明传，因为这是由安全分析工具3所需的。与睦相

6、反，在其 他协议参数都是隐式的。fig.l的左侧一栏显示交换的消息使用非正式的，直观的 表示经常遇到在文献屮，其屮a-b： o意味着a发送消息 给b。中间一栏显示pa的spi演算规范流程，而右边栏展 示过程中pb的行为。安德鲁协议假定每个进程都有一个其 屮对称密钥存储的本地密钥库。由于密钥存储区明确参与协 议，它必须在spi演算中被建模。我们简单的建模策略是表 示密钥存储作为单独的进程(在fig.l中没有显示)，其与相 应的协议交互主要通过专用的通信信道(密钥-存储通道)。 获取和存储密钥的操作被建模为在密钥存储通道有区别地 输入和输出。更准确地说，个密钥存储在个允许其独特 的标识的别名下的密

7、钥存储区中。所以，检索存储的密钥的 操作由下式表示 keystore < xa > .keystore(kab)其中的 keystore表示交互通道，xa是别名和kab是摘录自密钥 存储区保存的可变量。相应的存储操作是由语句keystore< xa, klab >说明，其中klab是必须根据该别名为xa被 存储的密钥。注意密钥存储区的可见性是由运算符所限制 的，所以它被认为是私有的过程。在安德鲁协议运行的屮， 五种信息在pa和pb的通道cab之间交换：1) pa的发送 的pb其 标识符a和随机数na。pb收到的消息，并将这 两个字段分别存储在变量xa和xna中。2) p

8、b从它的本地 密钥存储区中检索与pa共享的kab,并建立一个新的密钥 klab,与xna 一起用kab进行加密，并将结果发送给pa。 pa接收到该消息，并通过从它的本地密钥存储区中检索出 的kab进行解密。通过计算被存储在xna和xklab的明 文（na和klab）得到的两个字段 和na和xna的值进行 匹配检查。3） pa发送用共享密钥klab加密的随机数na 给pbopb解密该消息，并检查收到的随机数xnewna和xna 之间的匹配。随后的pb将klab存储在其本地密钥库中的 别名下，从而覆盖kabo 4） pb发送pa的一个新的随机 数nb。pa的接收随机数并在其本地密钥库中用klab取

9、代 kab0现在的密钥就完全一致。5）pa的使用klab加密 秘 密信息m,并将其发送到的pbo pb收到的加密邮件，将 其解密并存储m在变量x。3工具架构生成的代码为每个协议的角色组织成一个独立的程序, 并且这种方案在任何一个协议的新会话被执行时可以被激 活。因此，spi2java在一个时间生成一个单一的协议和色（例 如fig.l中的pa）0进程指定只有特定的实例场景（像fig.l 屮的机构）是不相关的，并在代码生成时被忽略。该spi2java程序是由两个模块组成：术语打印和描述检 查部分和java代码自动生成模块。所生成的代码是基于java库的模块实现，在一个可配置的方式，可以发生在spi

10、演算 描述的基本操作。fig2显示出在整个工具架构的数据流。4术语打印和描述检查模块spi演算不是类型化的,所以术语打印及描述检查负责填补协议规范和实现关注的数据类型之间的信息差距。特别 是，该功能块自动 检查在协议的作用过程是否条件变量被 持续地使用，而且如果这个检查是积极的，自动分配具体的java类型给条件变量。长期型分配是由一个算法与最专业的安全地代表它的java类相关联的任何条件变量来执行。用户可以手动执行更专门类型的若干变量通过被读取的规范文件和通过该模块 进行解释。手动指定一个更特殊类型是可能的，但不是必需 的。例如，如果一个进程不能对术语进行任何操作除了把它 送出来，消息类型是对

11、于这个术语来说完全恰当的。我们用组织三个专业化水平的类层次结构（图3只显示了一些类，由于空间有限，虽然spi2java处理所有的spi演 算的功能）的，可以通过信道传送术语及另一种对于通信信 道简单的层次结构，由于通道类依赖于应用传输库，并在过 程中的作用（客户端/服务器）。因此，半它是一个通用的用 于发送/接收消息或当它代表存储密钥和/或数字证书本地密 钥库的接入点时可能是专业化的通信信道的密钥库通信信 道，一个术语将作为通道类型。下面图3中是对类术语的含 义的简要说明。消息是专业化程度较低的类型，因为它代表 任何消息。每当算法是不能够为它确定一个更专业的类型时, 一个术语的类型则为消息。名

12、称是表示任何非结构性的spi 演算术语（即spi演算名称）的特殊类型的一部分。名称是 由不能被实例化一个类来实现的，因为这个类的对象总是更 专业具体的类的对象。名称可以是任何级别3类对象，但它 甚至可以是一个新的用户定义派生类的对象。信道id表示 一个信道标识符。它对于为一个服务器角色打开一个新的通 信信道发送在现有的信道上的信息是来说是有用的。 sharedkeyt代表一个在对称加密系统中使用有密钥ononcet 表示一个随机选择的比特序列。标识符代表的一些以独特的 方式标识一个实体的信息。例如，它可以被用作别名来标识 存储在密钥库内部的一个密钥。hasht表示对某些数据应用 加密散列函数后

13、的结果。sharedkeyciphered代表对一些数据 的对称加密操作的结果。该操作可以是加密或解密。pairt 表示的一对可能是异构类型的对象的容器。对象的元组被翻 译，里面的程序，到嵌套配对对象。5安全类库安全类安全库提供了一组以灵活和可配置的方式实现 类中的所有基本数据类型和加密操作可以抽象地表示在spi 演算。这个库作为对安全供应商，负责提供加密算法的具体 实现的通用接口。被用于测试安全类和生成的代码是指那些 sun?和【aik?。这个库在很大程度上依赖于java序列去构建 数据包在通信信道发送和/或加密。安全类库，设计了特殊照 顾，追求儿个目标：1）有严格的对应关系，据此，各spi

14、演 算的术语对应于一个java类中的安全类库，如图fig.3所示。 请注意，每个spi演算语句相当于个简单的java构造调用一 个术语对象的方法。2）类和方法隐藏加密算法行为和管理 的内部复杂性。3）用户能够（通过一个特殊的类，其中常 量可以修改）的方式来定制类的内部行为，为每个不同类型 的加密操作选择安全提供程序，算法和相关参数。4）已经 注意到，实现了生成的代码效率，得益于类执行效率。5） 每个类的实现一直保持尽可能接近它的抽象模型，并已经避 免，可导致已知安全漏洞的编程错误。需要注意的是一个完 整的遵循是无法实现的，因为所使用的加密技术是不完美的。 事实上加密操作的实现只能近似于加密算法

15、的理想化的行 为。例如，假设完美的加密条件（完美加密）的不同消息的哈希值永远不会发生碰撞。6传输层接口安全类库包含三个接口，一个名为的channelld来表示一 个信道标识符，channelt来表示一个通用的客户端/服务器 通信通道，并servert代表通用服务器进程等待传入的客 户端请求。所有这些类是与所使用的传输层库的相互作用点o 以这种方式，为所生成的代码实现层独立。用户可以通过规 范性文件来指定它。传输层的类隐藏传输层管理和启用任何spi演算的输入/ 输出操作到适当的java代码的直接翻译。7 java代码自动生成器java的自动生成提供了 java实现的spi演算描述的协议 的作用，

16、并部分地被规范文件影响，用户可以指定几个实现 选择，例如哪个角色（客户端/服务器）必须分配给spi演算 的进程，什么条件都返回参数，哪些传输库必须被使用。生 成的代码使用了 it.polito安全类和已选择的传输模块库提供 的类和方法。从spi演算规范，以及相关的规范文件开始， 代码生成器将java协议的实现类写在协议文件中。代码牛成 器也产生一个应用程序框架（在应用程序文件之上）和其他 一些对启动客户端应用程序/服务器有用的类文件，因为用户 通常会使用的握手协议作为一个目标应用程序的前奏。该协 议文件是由spi演算的行为表达语法指导翻译生成的。更确切地说，spi演算的语法树被访问，并为每个s

17、pi演算的操 作，前面有一个说明注解的产生的java代码来实现它。后者 增强了代码的可读性，使通信与spi演算规范可见。图。4 显示了最有意思的一段在协议文件屮生成的安德鲁协议的pa的过程代码。返回对象由getreturnparameter (inti)(这 里没有显示)的方法检索。当一个错误异常产生发生时生成classcastexceptions 这可能发生在信息接收和反序列化操作1: / cb) «c 1 02 si. <i al an itolaifl/4:pely4$:/ : h»i of «<uun /<a ，7；sh4：4 酣an丄

18、a / z 亠p伍j ! 99«»«丄亠0 二 .花工英liaculkhii! dlj dixtffstrni k町st口可htlatciiidhlcal3u-ju ph 】.j 2|> ?4(1$k /<ii 厶*_、 2 w >uixta 3t w 2 )|acxeat j 2cmjjmdi 皿_ld_2 i；-*/ - 232425li曲3113meuf d：3s n4343-43dt：三1354 5738分 qx»ua： tie ad| j |：.qi ldwiiifi-i ,| ,§中/-2二二"；| 工】

19、|， dcf (.4 j lto j la /ibndpsxmeu吟; »<_ 二二丄uw丄巫 i 4,mai 厶g"*ieiji. naaorjcae si 4.11丫“ uj9 141 ujlj.ujuji i.1 ；?«il * i 11尼 i 上 c：9：上 “ li a “ <3 s uvojisal | i i*osait 19u 1 siagit ) aali_,hotxjix>l (i idubj |反 &_£_«1血 x aux hu;aju 1 it _习/-titfa-ttitaiil fiu-2

20、-i-rkt j« rmcucalfiji oiptdi uiai la cabl«! *| x| n« 2 |t aum 人 clsimi.dloifx m.x( *11 |;' l>il业】4h? l2| /口 hmj dg | cjb _g jto s iv | »idbcm 5(fc ttll jt 1|) m u*9uu«ci«i 产 1 n qxomua： at m ad i hassi4( 1 o.ul u«lu ft | |t kiff 乩二< 5.4 亠匕口 e u isi 尢 xc.m

21、 l u1ab/£ !m:m js«r|odi«rwd r i 9141 wica 1c si mi kil i “ jstrndujt ipmd2«u im! xt丄.y!隘rial ad ； : | tl c ia!bu .1ft! ib f.aul 1a lh&dbm.doj ai» 1 | ri 3udil !be> fct lh 土 .d ln tum. 91jim l;i «i nr | dfe<mcst*y：figure 4. the andrew pa protocol code7.1生成的java

22、代码特性spi2java是加上一个协议分析器3,可以检测spi演算 的规格设计方案的缺陷。使用分析器，可以达到对指泄的协 议的逻辑正确性的合理的信心。spi2java的主要目的是为了 获得协议尽可能真实于已分析的原始正式的协议规范的实 现。这是通过执行一个语法驱动的翻译那里有一个到每个 spi演算描述元素和java代码片段实现它之间的一一对应实 现。更确切地说，一个映射建立了从spi演算的行为表达式 到使用安全类库和从spi演算术语到安全类库的行为逻辑。 这种策略保证了生成的代码结构反映了氐规范的结构相同, 排除了如果编码是通过手工完成而可能产生的人为错误。值得注意的是，该spi演算，不同于其

23、他规范形式化为 仅描述了交换的消息加密协议，还可以使协议角色执行的所 有必须检查的精确规范。因此，所产生的实现包括完全指定 的检查，而不是任何可能的检查，因为这将需要从其他规范 形式，并且用一种保守的方法开始检查。还值得一提的是，该协议的安全性分析3模型的任何加 密操作在一个理想化的方式（完美加密）下。因此，即使一 个协议从逻辑角度来看已经显示出是正确的，它不能被实现 保持完全相同的语义，所以，这是不可能的，在一般情况下， 为了正式保证所生成代码的行为完全作为正式的协议规范。然而，即使这是不可能达到完美的加密，它仍然是可能逼近 完美。事实上，它有可能改变双方的安全提供者和算法对任 何类型的加密

24、操作，允许用户选择实现最佳匹配完美的加密 假设。这种能力也使得由一个错误的影响而造成的轻松替换 算法的实现在被发现之前就发生。现在让我们考虑由于编程错误而违反了生成代码的抗 扰度。因为所牛成的代码是一个简单的从（安全类和tcpip 层）库的方法调用的序列，它足以达到这种库由于编程错误 而违规产生的抗扰度的高可信度。为了实现这一点，库都经 过精心研制，并已被广泛的测试。此外，我们的库和协议的 实现，是免受以下几种实现的弱点：缓冲区溢出是因为所采 用的实现语言是java15 4,它可以不受此类攻击（除了在 jvm本身溢出）。其实java使用以下，以保障内存：数组边 界检查对每个数组的访问，没有指针

25、，内存由参考（指针是 c和c + +中最容易出错的一个方面）进行管理;对象转型受 限制（必须保证类型安全）；变量不能用在初始化前（另一个 内存保护机制）;碎片收集自动释放内存（避免内存释放错误）。 当一个消息在一个不正确的形式解释，因为所有消息都类型 化和代码总是会检查类型不一致，并且当不匹配时引发一个 界常类型缺陷。另外请注意，在我们的实现中所有消息被序 列化，所以如果一个类型的缺陷发生时，那么反序列化机制 失败并引发异常。错误的输入攻击因为它们依赖于选中的输 入参数，而在检查对象在spi演算描述中已经规定，其规范的止确性是市安全分析器程序3验证。而且我们的类的实现 提供了所有必要的检查，并

26、产生一个异常时的违反约束。总之，关于协议实施的非脆弱性的整体可以达到高可信 度。此外，该代码是高度可配置的，因为用户可以自主选择 安全提供程序，该加密算法及其参数。与此同时，仅当它真 止需要的情况f,该协议的代码实现优化所创建的每个对象: 这意味着在每一次所有活对象是只有那些严格需要。8测试和实验我们使用所有的iaik4和sun：提供商所支持的功能测试 it. polito. secureclasses库。而且我们已经用几个简单的 特定的协议例子和一些真正的已知协议测试：andrew, ksl, ssl, needham-schroeder 测试了 spi2java。9相关工作在过去的几年一些

27、工具已经发展到指定，设计，验证和 实施加密协议。虽然很多文件解决方案的验证，只有一些地 址代码自动生成7 12 90由于语言的优秀的安全架构及抗常见的安全攻击15 4,我们选择java作为冃标语言为协议的实现，如7 12 10ospi演算作为协议规范语言的选择提供了一泄相对于以 前的作品的优势，因为它允许显式指定哪些检查协议必须执 行。这意味着该代码发生器，知道什么样的控制必须被实现, 可避免产生不需要的控制，从而产生一个优化的协议代码。 所有其他的工具7 12 9,从由无上述特征的形式语言来 指定的协议开始，必须始终执行所有可能的检查。此外，所 有其他的工具7 12 10需要明确指定每个术语

28、类型，而直 接在几乎所有情况下，我们的工具是能够自动理解术语的正 确类型。加密代码生成从capsl或cil规范语言capsl 9开始。 所产生的代码包括一个演示环境，有益查看协议行为，即应 拆除或改装以供在应用程序环境中直接使用。这种环境下所 代表的“中间人”攻击，因此它接收显示于握手协议各方之 间交换的所有消息。我们的代码不包含一个演示环境，但是 我们可以在传输层中直接添加这样的功能（建立一个新的传 输库），从而使信息对一个演示应用程序重定向能够表现为 攻击者。此外在9所生成的代码是低效的，因为它通过解释 一个抽象的数据结构来运行。另一个限制是对加密算法密钥 对象，这是固定的des对称操作的

29、依赖。另一个限制是缺乏 由一个虚拟的加密操作所取代的代码的公钥加密。agvi12x具生成由协议分析仪athena 11所采取的 使用相同的协议描述的代码。12包含有关代码生成和执行 的少量信息。这些信息可能在10中被提及，然而，在网络 上是不可达的。spear ii 7提供了从在gypsie13环境中报一种抽象 的协议规范的代码生成，而对于代码生成参数和设置在图形 genie14环境中被指定。所产生的代码是基于cryptix6和 crypto-j7加密库。7个很好的特点是，它使用了公认的标 准asn描述信息，从而使生成的代码与其他非spear ii 实现沟通。上述所有项目7 12 10生成一个

30、代码，不是java的安 全性-提供-独立的我们的。提供程序的独立性是一个很好的 功能，因为如果一个安全漏洞是在一个特定的库中找到，它 可以用另一个安全提供程序，通过这个问题，而不需要修改 生成的代码。只有spear ii生成的代码7是传输层的独立 和转换来自直接实现的协议规范代码，像我们一样。10结论一个新的java的自动代码生成器在spi演算指定加密协 议已经制疋，将在安全协议规范和验证环境中被整合。 spi2java提供了协议实现与一个框架代码，有助于开发使用 协议的应用程序。spi2java具有关联一个类型到每个spi演算术语在自动 或半自动的方式，并检查抽象描述不协调的模块。随着sec

31、ureclasses库，我们已经能够隐藏的加密算法的 复杂性，并提供最大的灵活性，允许安全提供程序的选择, 算法和算法参数为每一种加密运算。此外，spi演算对象和 类z间的严格对应关系使我们能够保证有关代码的正确性 较高的可信度。传输层的模块泄义允许用户选择和替换一个 简单的方法传输协议。所产生的java代码需要优化对象的创 建吋间，避免了常见的实现攻击和维持一个高的可理解性得 益于各行为表述之前存在的注释。11承诺这项工作已经由卓越的多媒体无线通讯都灵理工大学 的中心(cercom)部分资助。参考文献1 m abadi and a. d gordon. a calculus forcrypt

32、ographicprotocols the spi calculus inf. comput,1 (148):1 - 70, 1999.2 e. m. clarke, s. jha, and w. marrero. verifying securityprotocols with brutus. acmtrans on softw. eng. andmeth.,9(4):443 - 487, 2000.3 l. durante, r. sisto, and a. valenzano. automatic testingequivalence verification of spi calcul

33、usspecifications. acmtrans, on softw. eng. and meth. , 12 (2) : 222 - 284, apr. 2003.4 t. lindholm and f yell in. the java vir tual machine specification.sun microsystems, 2nd edition. online, availableat: http:/java. sun. com/docs/books/vmspec/_5 g. lowe some new attacks upon security protocolsin 9

34、thieee comp. sec found work,pages 162 - 169, 1996.6 g lowe casper: a compiler for the analysis of securityprotocols. j. comput. secur., 6(1) : 53 - 84, 1998.7 s. luke 11 and c veldma n. automat ed at tack analisys andcode generation in a unified, multi-dimensional security protocolengineering framework comp. science hon., 20028 r. milner, j. parr