Group of Software Security In Progress

GoSSIP @ LoCCS.Shanghai Jiao Tong University

A Messy State of the Union: Taming the Composite State Machines of TLS

作者:Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cedric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Y ves Strub, Jean Karim Zinzindohoue

单位:INRIA Paris-Rocquencourt, Microsoft Research, IMDEA Software Institute

Introduction:

  1. 设计了一个综合状态机能处理多种TLS协议模式(版本、扩展、认证模式、密钥交换方法的不同组合);
  2. 基于综合状态机测试了主流TLS开源实现,并发现若干严重漏洞,分析认为它们源自不同正确状态机的错误组合;
  3. 给出第一个C语言写的验证过的TLS综合状态机实现,可嵌入OpenSSL;
  4. 密码协议库的核心组件需要形式化验证,这能通过本文方法实现。

  5. TLS的安全性可以分解到组成模块的安全性:密钥交换算法(Ephemeral DH)、传输加密方案(AES-GCM with SHA256)

  6. Composite State Machines:SSL链接建立过程的状态机没有标准化,且不同实现的状态机也不同。
  7. 有时为了代码复用将状态机简单组合会带来问题序列: Figure 1

order of message: distinguish between truly optional messages, and messages whose presence if fully prescribed not prematurely calculate session parameters and secrets

Figure 2

Testing implementations with FlexTLS

文章提出了一种protocol-aware state machine fuzzing.

  • generate arbitrary sequences of valid TLS messages to test
  • implementations. 定义偏移序列,利用偏移序列来确定检测状态机错误。 Figure 3

State machine flaws in TLS implementations

  • OpenSSL:

    • Early CCS: OpenSSL 1.0.1g, CCS严格意义上不是handshake message,不出现handshake log中,不受客户端或服务器端状态机控制,可以出现在ServerHello后的任意位置。Receiving a CCS message triggers the setup of a recore key derived from the session key. CVE-2014-0224.
    • DH Certificate: client忽略ClientKeyExchange,可能导致client impersonation。
    • Server-Gated Crypto(SGC): SGC允许客户端收到serverhello后重新握手,但是表明某些extension是否被使用的信息会在新握手中消失。
    • Export RSA: 512 bit RSA modulus.
    • Static DH: 使用DHE或者ECDHE时,如果证书包含ECDH公钥,而且客户端不接受ServerKeyExchange,则会回滚到static ECDH,用服务器证书的公钥,导致前向安全性丢失。
  • JSSE: OpenJDK 6,7,8都存在下列问题。

    • Client Flaws: 消息序号检测,可以skip消息。会导致server impersonation attack。
      • 允许服务器skip ServerCCS,从而记录层不加密;
      • 允许服务器skip any combination of the ServerCertificate, ServerKeyExchange, ServerHelloDone.
    • Server Flaws: 消息序号检测,或上一条是CKE,或ClientcertificateVerifiy。
      • 允许skip ServerCCS,从而记录层不加密;
      • skip any combination of the ServerCertificate, ServerKeyExchange, ServerHelloDone.
      • CKE后可以发任意数量clienthello,clientcertificate,CKE,CCV等。这些行为会破坏Server状态。
  • Other implementations:
    • NSS:
      • DHE 或 ECDHE中允许skip ServerKeyExchange,会导致Static DH等,影响前向安全性。
      • renegotiation时,Server CCS和ServerFInished之间接收Allication Data,如果certificate换了会出错。
    • Mono:MS .NET framework
      • skip CCS message
      • skip ClientCertificateVerify。可能导致客户端伪造。
      • ServerKeyExhange后还可以发送ServerCertificate。证书替换攻击。
    • CyaSSL:
      • skip CCS
      • skip serverKeyExchange和ServerHelloDone
      • Skip ClientCertificateVerify
    • GnuTLS: skip ClientCertificate
    • miTLS and others: miTLS is a verified implementation. no deviant trace.

Attacks on TLS implementations

Early Finished: Server impersonation(Java, CyaSSL)

构造一个场景:

Figure 4

这种情况在JSSE中可行,即(4)中略过密钥协商的过程直接ServerFinished,导致所有通信全部明文。JSSE中,ServerFinished内容是前面通信内容的MAC,key是master secret。 对于CyaSSL,情况类似,除了ServerFinished是12个0. client接收ServerCCS时就生产MAC存在本地,收到ServerFinished后在将它和ServerCCS匹配。这个攻击依赖于未初始化的内存。

Skip verify:Client impersonation(Mono,CyaSSL, OpenSSL)

Figure 5

  • Mono中,步骤(5)略过了对client身份的验证。
  • CyaSSL:类似,只是(6)的信息M也要略过。
  • OpenSSL:(5)(6)略过了客户端身份验证。

Skip ServerKeyExchange:Forward Secrecy Rollback(NSS,OpenSSL):

Figure 6

  • ServerKeyExchange被攻击者拦截了,理论上client应该拒绝后续信息,NSS和OpenSSLim会降级到不支持前向安全性的密钥交换方式。
  • Inject ServerKeyExhange: RSA_Export flash-back 略。

A Verified State Machine for OpenSSL

系统化状态机测试能发现漏洞,但是不能保证所有漏洞被发现。形式化验证一个给定的状态机实现是否匹配TLS标准是有价值的,建立自动化验证框架更有价值。本文试图对OpenSSLim的full state machine进行证明。

  • OpenSSL Clients and Servers:消息处理异常复杂
  • A new state machine:提出一个新的状态机结构让OpenSSL消息序列更容易理解。

把状态机形式化为一个逻辑不变量isValidState

Figure 7

Summary and responsible disclosure:

8个TLS实现中6个有严重的状态机问题,并能利用它们发起9个不同的攻击。3个实现允许略过CCS信息。这篇论文提到的漏洞已报,已修复或修复中。