Pyre-Check项目中的Pysa交互式污染模型探索指南

概述

Pyre-Check作为一款静态类型检查工具，其Pysa组件专门用于进行安全分析。当Pysa完成代码分析后，它会生成详细的JSON输出，包含对可调用对象污染状态的最终视图以及发现的问题。本文将介绍如何使用explore_pysa_models.py脚本交互式探索这些污染模型，帮助开发者深入理解Pysa的分析结果。

准备工作

在开始探索前，需要确保已经使用Pysa对代码库进行了分析。假设分析结果保存在/tmp/output_dir目录中：

$ pyre analyze --save-results-to /tmp/output_dir

分析完成后，Pysa会在指定目录生成一个或多个taint-output.json文件，包含所有可调用对象的污染信息。

启动模型探索器

加载分析结果到探索脚本：

$ python3 -i scripts/explore_pysa_models.py

启动后，交互式环境会显示可用命令列表，包括：

• index('/path/to/results-directory') - 索引指定目录中的所有污染模型
• callables_containing('foo.bar') - 查找名称包含指定字符串的所有可调用对象
• callables_matching(r'foo\..*') - 使用正则表达式匹配可调用对象
• get_model('foo.bar') - 获取指定可调用对象的模型
• print_model('foo.bar') - 美化输出指定可调用对象的模型
• get_issues('foo.bar') - 获取指定可调用对象中的所有问题
• print_issues('foo.bar') - 美化输出指定可调用对象中的问题

基本使用示例

1. 索引分析结果

>>> index('/tmp/output_dir')
Indexing `/tmp/output_dir/taint-output.json`
Indexed 307120 models

2. 查找相关可调用对象

>>> callables_containing('HttpRequest')
['django.http.request.HttpRequest.__init__', 'django.http.request.HttpRequest.body', ...]

3. 查看模型详情

使用get_model()获取原始模型数据：

>>> get_model('django.http.request.HttpRequest.__init_')
{
  'callable': 'django.http.request.HttpRequest.__init__',
  'sources': [],
  'sinks': [],
  'tito': [{
    'port': 'formal(self)',
    'taint': [{
      'decl': None,
      'leaves': [{
        'kind': 'LocalReturn',
        'name': ''
      }]
    }]
  }]
}

使用print_model()获取美化输出：

>>> print_model('django.http.request.HttpRequest.body')
{
  "callable": "django.http.request.HttpRequest.body",
  "sources": [
    {
      "port": "result",
      "taint": [
        {
          "decl": null,
          "kinds": [
            {
              "kind": "UserControlled"
            }
          ]
        },
      ]
    }
  ],
  "sinks": [],
  ...
}

高级功能

1. 过滤模型输出

print_model()支持多种过滤选项：

print_model(
    'django.http.request.HttpRequest.body',
    kind='UserControlled',      # 按污染类型过滤
    caller_port='result',      # 按调用端口过滤
    remove_sources=False,      # 是否移除源信息
    remove_sinks=False,        # 是否移除汇信息
    remove_tito=False,         # 是否移除TITO信息
    remove_tito_positions=True, # 是否移除TITO位置信息
    remove_features=True,      # 是否移除特征信息
    remove_leaf_names=True     # 是否移除叶节点名称
)

2. 查看安全问题

>>> print_issues('foo.bar.log_errors')  # 查看特定函数中的安全问题

3. 直接操作模型数据

>>> print_json(get_model('django.http.request.HttpRequest.body')["sources"])

技术解析

Pysa的污染模型包含几个关键部分：

1. Sources（源）：表示用户可控的输入点，如HTTP请求参数
2. Sinks（汇）：表示潜在的危险操作点，如数据库查询
3. Taint-In-Taint-Out (TITO)：表示污染如何在函数间传播

理解这些概念对于有效使用模型探索器至关重要。例如，当看到UserControlled源时，表示该点接收用户输入；而看到SQL汇时，表示该点可能执行SQL查询。

最佳实践

1. 逐步探索：先使用callables_containing缩小范围，再深入查看具体模型
2. 关注关键点：优先检查已知的安全敏感函数
3. 验证预期：确认Pysa的模型是否符合你对代码安全性的理解
4. 组合查询：结合多种过滤条件快速定位问题

通过交互式探索Pysa模型，开发者可以更深入地理解代码中的安全数据流，验证安全假设，并快速定位潜在的安全问题。这种探索方式特别适合在复杂代码库中调查特定安全问题时使用。