Semmle QL发现Facebook Fizz DoS漏洞分析报告

1. 漏洞概述

漏洞类型：拒绝服务(DoS)漏洞
影响对象：使用Facebook Fizz TLS库的服务器
漏洞奖励：$10,000美元
发现方式：使用Semmle QL查询语言进行静态代码分析
漏洞修复时间：2019年2月20日报告，2月25日发布补丁

2. 漏洞技术细节

2.1 漏洞位置

漏洞存在于Fizz库的PlaintextRecordLayer.cpp文件中，具体在第42行的整数溢出问题：

auto length = cursor.readBE<uint16_t>();
if (buf.chainLength() < (cursor - buf.front()) + length) {
  return folly::none;
}
length += sizeof(ContentType) + sizeof(ProtocolVersion) + sizeof(uint16_t);
buf.trimStart(length);
continue;

2.2 漏洞触发机制

1. 攻击者可以控制length值（通过发送恶意网络包）
2. 当设置length = 0xFFFB时：
   • length +=操作会导致整数溢出，使length变为0
   • trimStart(0)调用不会消耗任何数据
   • 导致程序进入无限循环状态

2.3 漏洞影响

• 攻击者只需发送约64KB的恶意数据包
• 普通1Mbps上传带宽每秒可发送2个这样的数据包
• 可导致服务器CPU资源耗尽，造成拒绝服务
• 攻击成本极低但影响严重

3. Semmle QL分析技术

3.1 Semmle QL简介

Semmle QL是一种声明式、面向对象的查询语言，用于：

• 将代码视为数据
• 将分析问题转化为数据库查询
• 支持大规模代码自动化审查

3.2 漏洞发现过程

3.2.1 基础查询

查找从较大数据类型向较小数据类型的转换（可能溢出的地方）：

import cpp
import semmle.code.cpp.ir.IR

from ConvertInstruction conv
where conv.getResultSize() < conv.getUnary().getResultSize()
select conv

3.2.2 改进查询

加入污点跟踪(taint tracking)技术，专门查找基于用户输入的不安全转换：

import cpp
import semmle.code.cpp.ir.dataflow.TaintTracking
import semmle.code.cpp.ir.IR
import DataFlow::PathGraph

class EndianConvert extends Function {
  EndianConvert() {
    this.getName() = "big" and
    this.getDeclaringType().getName().matches("Endian")
  }
}

class Cfg extends TaintTracking::Configuration {
  Cfg() { this = "FizzOverflowIR" }
  
  override predicate isSource(DataFlow::Node source) {
    source.(CallInstruction).getCallTarget().(FunctionInstruction).getFunctionSymbol() instanceof
      EndianConvert
  }
  
  override predicate isSink(DataFlow::Node sink) {
    sink.getResultSize() < sink.(ConvertInstruction).getUnary().getResultSize()
  }
}

from Cfg cfg, DataFlow::PathNode source, DataFlow::PathNode sink, ConvertInstruction conv,
  Type inputType, Type outputType
where
  cfg.hasFlowPath(source, sink) and
  conv = sink.getNode() and
  inputType = conv.getUnary().getResultType() and
  outputType = conv.getResultType()
select sink, source, sink,
  "Conversion of untrusted data from " + inputType + " to " + outputType + "."

3.2.3 查询关键点

1. 污点源定义：识别Endian::big()调用作为不可信输入源
2. 污点传播：跟踪数据流从源到潜在危险操作
3. 危险操作识别：查找可能导致整数溢出的类型转换

3.3 中间表示(IR)技术

Semmle QL使用中间表示技术统一处理不同语法形式的相同操作：

4. 漏洞修复方案

修复方法很简单：使用比uint16_t更大的数据类型来计算加法，避免整数溢出。

5. 漏洞验证与利用

5.1 PoC构造要点

1. 建立与目标服务器的TCP连接
2. 发送约64KB的恶意payload（设置length = 0xFFFB）
3. 立即关闭socket连接
4. 服务器将陷入无限循环

5.2 验证注意事项

• 仅建议在测试环境中验证
• 实际攻击可能造成服务中断
• Facebook已修复其所有服务器

6. 经验总结

1. 静态分析优势：能发现Fuzzing难以触发的代码路径问题
2. 查询设计要点：
   • 结合数据流分析和污点跟踪
   • 准确定义不可信输入源
   • 识别危险操作模式
3. 高质量代码审查：即使经过严格审查的代码也可能存在漏洞
4. 整数溢出风险：需要特别关注类型转换和算术操作

7. 学习资源

1. Semmle QL官方文档
2. LGTM在线分析平台
3. QL for Eclipse工具
4. Facebook Fizz开源代码库

8. 时间线

• 2019-02-20：漏洞提交给Facebook
• 2019-02-20：Facebook验证并开始修复
• 2019-02-25：Github发布补丁
• 2019-03-13：确认$10,000奖金

这份报告详细记录了使用Semmle QL发现Facebook Fizz DoS漏洞的全过程，包括技术细节、分析方法、修复方案和学习要点，可作为静态代码分析和漏洞挖掘的典型案例参考。