线程间Bug检测工具Canary

Canary

  • 1.Introduction
  • 2.Approach
    • 2.1.数据依赖分析
    • 2.2.线程间依赖分析
  • 3.Bug检测
  • 4.Evaluation
  • 参考文献

1.Introduction

主要做跨线程value-flow bug检查,下面代码中两个函数中存在指向关系:1. x→o1x \rightarrow o_1xo1, b→o2b \rightarrow o_2bo2 以及赋值关系: o1=ao_1 = ao1=a。考虑跨线程的数据流存在 y=xy = xy=xo1=bo_1 = bo1=b(覆盖掉 aaa)。如果 θ1\theta_1θ1 满足,那么 o1=ao_1 = ao1=a,因此 c=ac = ac=aprint 操作安全。如果 θ2\theta_2θ2 满足,那么线程执行完后根本不会执行 print 操作,因此没有bug。但是现有静态分析工具可能会错误判断 free(b)print(*c) 存在use-after-free。

请添加图片描述

作者提出了Canary,对上面代码可构造如下value-flow graph,其中 b@l13→c@l6b@l_{13} \rightarrow c@l_6b@l13c@l6 对应 *y = bc = *xx, y 都指向了共同的堆对象 o1o_1o1,路径条件为 θ1∧¬θ1\theta_1 \wedge \neg \theta_1θ1¬θ1。同时线程间执行需要保证语句的先后顺序,用 O2>O1O_2 > O_1O2>O1 表示 l2l_2l2l1l_1l1 后执行,那么还存在偏序关系 O13>O3∧O14>O3O_{13} > O_3 \wedge O_{14} > O_3O13>O3O14>O3。随后Canary会调用SMT求解上面约束条件验证该bug存在条件不可行。

请添加图片描述

相比顺序程序,并发程序分析的核心在于,对于 l1:∗x=ql_1: *x = ql1:x=q, l2:p=∗yl_2: p = *yl2:p=y,不仅要分析 x,yx, yx,y 别名的路径条件;还要分析 l1→l2l_1 \rightarrow l_2l1l2 路径下 x,yx, yx,y 可能指向的内存是否会被其它线程覆写。

2.Approach

分为数据依赖分析和线程间依赖分析。

2.1.数据依赖分析

规则如下和pinpoint类似,自底向上对每个函数生成summary再分析其caller,先进行代码转换方便暴露每个函数的side-effect。转换的规则应该覆用了pinpoint的,对于下面代码。

int f(v1, v2, ...) {...return v0;
}

转换后可能为:

int f(v1, v2, ... , F1, F2, ...) {(vj, k) = Fi; /* for all (i, j, k). */...;Rp =(vq,r); /* for all (p,q,r). */return {v0, R1, R2, ...};
}

对于调用点:

// 转换前
u0 = f(u1, u2, ...);
// 转换后
Ai =(uj, k); /* for all (i, j, k). */
{u0, C1, C2, ... } = f(u1, u2, ... ,A1,A2, ...);(uq,r) = Cp =; /* for all (p,q,r). */

在分析函数 FFF 时按照每个指令在CFG中的逆后序处理每条指令。分析完后 Trans(F)\text{Trans}(F)Trans(F) 记录了 FFF 在其形参 viv_ivi 的副作用。

请添加图片描述

线程内指令的分析规则基于flow-, path-sensitive指针分析,如下所示。这里暂时不考虑线程间的关系,碰到 fork 调用直接跳过。

指令类型示例规则
allocal,φ:p=&ol, \varphi: p = \&ol,φ:p=&o(φ,o)∈pts(p)(\varphi, o) \in \text{pts}(p)(φ,o)pts(p)
copyl,φ:p=ql, \varphi: p = ql,φ:p=q(γ∧φ,o)∈pts(p)∣∀(γ,o)∈pts(q)(\gamma \wedge \varphi, o) \in \text{pts}(p) \mid \forall (\gamma, o) \in \text{pts}(q)(γφ,o)pts(p)(γ,o)pts(q)
loadl,φ:p=∗yl, \varphi: p = *yl,φ:p=y(γ∧φ,o′)∈pts(p)∣∀(_,o)∈pts(y),∀(γ,o′)∈ptsINl(o)(\gamma \wedge \varphi, o^{'}) \in \text{pts}(p) \mid \forall (\_, o) \in \text{pts}(y), \forall (\gamma, o^{'}) \in \text{pts}_{\text{IN}_l}(o)(γφ,o)pts(p)(_,o)pts(y),(γ,o)ptsINl(o)
storel,φ:∗x=ql, \varphi: *x = ql,φ:x=q(1). pts(x)=∅∣x→(γ,o)\text{pts}(x) = \emptyset \mid x \rightarrow (\gamma, o)pts(x)=x(γ,o) (strong update), (2).(γ∧φ,o)∈pts(o′)∣∀(γ,o)∈pts(q),∀(γ′,o′)∈pts(x)(\gamma \wedge \varphi, o) \in \text{pts}(o^{'}) \mid \forall (\gamma, o) \in \text{pts}(q), \forall (\gamma^{'}, o^{'}) \in \text{pts}(x)(γφ,o)pts(o)(γ,o)pts(q),(γ,o)pts(x)
calll,φ:(x0,...,xn)=f(v1,...,vn)l, \varphi: (x_0, ..., x_n) = f(v_1, ..., v_n)l,φ:(x0,...,xn)=f(v1,...,vn)(φ,Trans(f,pts(vi)))∈pts(xi)∣∀i∈[1,n](\varphi, \text{Trans}(f, \text{pts}(v_i))) \in \text{pts}(x_i) \mid \forall i \in [1, n](φ,Trans(f,pts(vi)))pts(xi)i[1,n]

2.2.线程间依赖分析

这一步是Canary的核心,当 l1:∗x=ql_1: *x = ql1:x=ql2:p=∗yl_2: p = *yl2:p=y 在不同线程时,x,yx, yx,y 别名的前提除了本身必须可能指向同一块内存外还必须满足 O2>O1O_2 > O_1O2>O1,这步包括依赖边构造依赖条件计算两个步骤。

2.2.1.依赖边构造

需要识别线程共享内存,这些内存对象被称为escaped memory。用 EspObj\text{EspObj}EspObj 表示程序中所有escaped memory object,Pted(o)\text{Pted}(o)Pted(o) 表示指向 ooo 的所有指针。在线程内数据依赖分析基础上,作者定义下面规则,其中ttt 表示某个线程,t′t^{'}t 表示其它线程。

  • 计算 EspObj\text{EspObj}EspObj

    • step 1: 将 fork 调用中传递的object添加进 EspObj\text{EspObj}EspObj

    • step 2: 根据已有的 EspObj\text{EspObj}EspObjstore 指令更新集合,o′∈EspObj∣(c1).∀l:∗x=q(c2)(,o)∈pts(x)(,o′)∈pts(q)(c3)o∈EspObjo^{'} \in \text{EspObj} \mid (c1).\forall l: *x=q \;\; (c2) (_, o) \in \text{pts}(x) \; (_, o^{'}) \in \text{pts}(q) \;\; (c3) o \in \text{EspObj}oEspObj(c1).∀l:x=q(c2)(,o)pts(x)(,o)pts(q)(c3)oEspObj

  • 计算 Pted\text{Pted}Pted: 对EspObj\text{EspObj}EspObj 中的每个 ooo 找到能传播到的所有指针,存入集合 NNNσ\sigmaσ 为遍历过程中的路径条件:(n,σ)∈Pted(o)(n, \sigma) \in \text{Pted}(o)(n,σ)Pted(o)

  • 计算依赖边:: l1→l2∣(c1).∀l1,φ1:∗x=q∈t(c2).∀l2,φ2:p=∗y∈t′(c3).(x,α),(y,β)∈Pted(o),(c4).o∈EspObjl_1 \rightarrow l_2 \mid (c1).\forall l_1, \varphi_1: *x = q \in t \;\; (c2).\forall l_2, \varphi_2: p = *y \in t^{'} \;\; (c3).(x, \alpha), (y, \beta) \in \text{Pted}(o), (c4).o \in \text{EspObj}l1l2(c1).∀l1,φ1:x=qt(c2).∀l2,φ2:p=yt(c3).(x,α),(y,β)Pted(o),(c4).oEspObj

这个示例中 EspObj={o1,o2}\text{EspObj} = \{o_1, o_2\}EspObj={o1,o2}, Pted(o1)={x,y}\text{Pted}(o_1) = \{x, y\}Pted(o1)={x,y}, Pted(o2)={b,c}\text{Pted}(o_2) = \{b, c\}Pted(o2)={b,c}(paper中这么写的,有点迷惑,fact的路径条件应该是被忽略了)。

请添加图片描述
2.2.2.依赖条件计算

一个value-flow edge: l1,φ1:∗x=q⟶l2,φ2:p=∗yl_1, \varphi_1: *x = q \longrightarrow l_2, \varphi_2: p = *yl1,φ1:x=ql2,φ2:p=y 的路径条件包括 x,yx, yx,y 的别名条件 Φalias\Phi_{\text{alias}}Φalias 以及 O2>O1O_2 > O_1O2>O1 的条件 Φls\Phi_{\text{ls}}Φls

Φalias=⋁(φ1∧φ2∧α∧β)∣∀(α,o)∈pts(x),(β,o)∈pts(y)\Phi_{\text{alias}} = \bigvee (\varphi_1 \wedge \varphi_2 \wedge \alpha \wedge \beta) \mid \forall (\alpha, o) \in \text{pts}(x), (\beta, o) \in \text{pts}(y)Φalias=(φ1φ2αβ)(α,o)pts(x),(β,o)pts(y),上面示例中:*y = b -> c = *x 的条件为 θ1∧¬θ1\theta_1 \wedge \neg \theta_1θ1¬θ1

Φls\Phi_{\text{ls}}Φls 的计算中需要保证 (1) store sload l 的执行顺序 Ol>OsO_l > O_sOl>Os,同时 (2) s→ls \rightarrow lsl 之间没有其它 store 语句会写入 ooo。让 S(l)S(l)S(l) 表示 lll 数据依赖的所有 store 语句。那么 Φls=⋀s,s′∈S(l)(Os<Ol⋀∀s′≠sOs′<Os∨Ol<Os′)\Phi_{\text{ls}} = \bigwedge\limits_{s,s^{'} \in S(l)} (O_s < O_l \bigwedge\limits_{\forall s^{'} \neq s} O_{s^{'}} < O_s \vee O_l < O_{s^{'}})Φls=s,sS(l)(Os<Ols=sOs<OsOl<Os)Os′<Os∨Ol<Os′O_{s^{'}} < O_s \vee O_l < O_{s^{'}}Os<OsOl<Os 表示 ssslll 之间不存在其它 store 语句会修改 lll 引用的内存。

3.Bug检测

这里主要检测线程间use after free。其中source为 free 点,sink为 use 点。其中存在source - sink路径 π=⟨v1@l1,v2@l2,...,vk@lk⟩\pi = \langle v_1@l_1, v_2@l_2, ..., v_k@l_k \rangleπ=v1@l1,v2@l2,...,vk@lk,bug存在的条件 Φall(π)=Φguards(π)∧Φpo(π)\Phi_{\text{all}}(\pi) = \Phi_{\text{guards}}(\pi) \wedge \Phi_{\text{po}}(\pi)Φall(π)=Φguards(π)Φpo(π)

  • Φguards(π)=⋀i∈[1,k−1]Φguards(vi@li→vi+1@li+1)\Phi_{\text{guards}}(\pi) = \bigwedge\limits_{i \in [1, k-1]} \Phi_{\text{guards}}(v_i@l_i \rightarrow v_{i+1}@l_{i+1})Φguards(π)=i[1,k1]Φguards(vi@livi+1@li+1) 为数据依赖的路径条件。

  • Φpo(π)=⋀i∈[1,k−1]⋀j∈[i,k−1]Φpo(vi@li→...→vj@lj)\Phi_{\text{po}}(\pi) = \bigwedge\limits_{i \in [1, k-1]} \bigwedge\limits_{j \in [i, k-1]} \Phi_{\text{po}}(v_i@l_i \rightarrow ... \rightarrow v_j@l_j)Φpo(π)=i[1,k1]j[i,k1]Φpo(vi@li...vj@lj) 为语句偏序关系约束。

4.Evaluation

和FASM以及Saber进行了比较,采用了20个开源程序进行评估。

请添加图片描述

请添加图片描述

参考文献

[1].Yuandao Cai, Peisen Yao, and Charles Zhang. 2021. Canary: practical static detection of inter-thread value-flow bugs. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021). Association for Computing Machinery, New York, NY, USA, 1126–1140. https://doi.org/10.1145/3453483.3454099

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。
如若转载,请注明出处:http://www.pswp.cn/web/94510.shtml
繁体地址,请注明出处:http://hk.pswp.cn/web/94510.shtml

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈email:809451989@qq.com,一经查实,立即删除!

相关文章

AEB 强制来临,东软睿驰Next-Cube-Lite有望成为汽车安全普惠“破局器”

AEB 强制时代正在悄然谱写“普惠安全”的行业底色。日前&#xff0c;备受关注的强制性国家标准《轻型汽车自动紧急制动系统技术要求及试验方法》&#xff08;以下简称“新国标”&#xff09;意见征求阶段已经结束。该标准将替代现行国标GB/T 39901-2021&#xff0c;计划于2028年…

css的white-space: pre

用户从别的地方复制的配置文件&#xff0c;粘贴到输入框内&#xff0c;需要保留原始格式发送给后端。核心步骤&#xff1a;### 1. 格式保持机制 - white-space: pre &#xff1a;这是最关键的CSS属性&#xff0c;确保所有空格、制表符、换行符都被保留 - wrap"off" &…

【AI解读源码系列】ant design mobile——Space间距

前言 笔者目前业务主要围绕ant design mobile组件库来交付H5前端工作。 故此出此专栏来解读每一个组件是如何实现的。 本文基于AI来解读Space组件。 文档链接&#xff1a; https://mobile.ant.design/zh/components/space 源码&#xff1a; https://github.com/ant-design/ant-…

《用餐》,午餐食堂即景小诗分享(手机/小视频/光盘/养生)

大妈食堂碎碎念&#xff0c;怪罪手机延工期。 笔记模板由python脚本于2025-08-21 19:34:46创建&#xff0c;本篇笔记适合喜欢友善生活和诗的coder翻阅。 学习的细节是欢悦的历程 博客的核心价值&#xff1a;在于输出思考与经验&#xff0c;而不仅仅是知识的简单复述。 Python官…

高通平台WIFI学习-- 基于WCN6750 Tri-Band 2x2 MIMO 802.11ax的讲解

一 前言: 官方资料显示WLAN支持如下的Key features ■ Compliant with IEEE 802.11a/b/g/n/ac/ax ■ Supports 2x2 multi-user multiple-input multiple-output (MU-MIMO) ■ Up to 2.9 Gbps data rate (2x2 160 MHz) ■ Tri-band 2.4 GHz/5 GHz/6 GHz support ■ 20 MHz…

javaweb开发笔记——XML_Tomcat10_HTTP

第四章 XML_Tomcat10_HTTP 一 XML XML是EXtensible Markup Language的缩写&#xff0c;翻译过来就是可扩展标记语言。所以很明显&#xff0c;XML和HTML一样都是标记语言&#xff0c;也就是说它们的基本语法都是标签。 可扩展 三个字表面上的意思是XML允许自定义格式。但这不代…

Python从入门到自动化运维

文章目录IPO编程方式、print、input函数print() -- 输出信息到屏幕input() -- 读取用户的输入基本数据类型int、float、bool、str常用 str 操作方法格式化字符串的三种方式数据验证方法字符串拼接字符串去重数据类型转换函数容器类型列表(list)&#xff1a;可变、可重复、有序元…

【数据可视化-98】2025年上半年地方财政收入Top 20城市可视化分析:Python + Pyecharts打造炫酷暗黑主题大屏

&#x1f9d1; 博主简介&#xff1a;曾任某智慧城市类企业算法总监&#xff0c;目前在美国市场的物流公司从事高级算法工程师一职&#xff0c;深耕人工智能领域&#xff0c;精通python数据挖掘、可视化、机器学习等&#xff0c;发表过AI相关的专利并多次在AI类比赛中获奖。CSDN…

【基础-单选】向服务器提交表单数据,以下哪种请求方式比较合适

向服务器提交表单数据&#xff0c;以下哪种请求方式比较合适A.RequestMethod.GET B.RequestMethod.PUT C.RequestMethod.POST D.RequestMethod.DELETE 解释如下&#xff1a; 在HarmonyOS应用开发中&#xff0c;向服务器提交表单数据&#xff0c;C. RequestMethod.POST 是比较合…

论文阅读:Code as Policies: Language Model Programs for Embodied Control

地址&#xff1a;Code as Policies: Language Model Programs for Embodied Control 摘要 针对代码补全任务训练的大型语言模型&#xff08;LLMs&#xff09;已被证实能够从文档字符串&#xff08;docstrings&#xff09;中合成简单的 Python 程序。研究发现&#xff0c;这些…

Vue 3 customRef 完全指南:自定义响应式引用的终极教程

&#x1f4d6; 概述 customRef() 是 Vue 3 中用于创建自定义响应式引用的组合式 API。它允许开发者完全控制响应式数据的读取和写入行为&#xff0c;为复杂的响应式逻辑提供了强大的灵活性。 &#x1f3af; 基本概念 什么是 customRef&#xff1f; customRef() 是一个工厂函数…

Java项目-苍穹外卖_Day1

项目来源&#xff1a; 【黑马程序员 Java项目实战《苍穹外卖》】 [https://www.bilibili.com/video/BV1TP411v7v6] ZZHow(ZZHow1024) 软件开发整体介绍 软件开发流程 需求分析&#xff1a;需求规格说明书、产品原型。设计&#xff1a;UI 设计、数据库设计、接口设计。编码…

面试可能问到的问题思考-MySQL

MySQL 1. 数据库与缓存的一致性 引入缓存&#xff0c;因为缓存只是数据库数据的副本&#xff0c;那么就可能存在副本和原数据不一致的情况 一致性 ACID里面的C&#xff0c;和CAP中的C不是一个概念&#xff0c;虽然都叫一致性。CAP中的C&#xff0c;指的是多个副本之间逻辑上…

【Java】 Spring Security 赋能 OAuth 2.0:构建安全高效的现代认证体系

还在为高昂的AI开发成本发愁?这本书教你如何在个人电脑上引爆DeepSeek的澎湃算力! 在当今数字化时代,认证与授权已成为应用系统安全的核心。OAuth 2.0 作为一种开放标准协议,广泛应用于第三方授权场景中,而 Spring Security 则提供了强大的框架支持来实现这一协议。本文深…

实际工作几月后常用相关命令笔记记录

目前&#xff0c;我这只工程师幼崽经历几个月的工作&#xff0c;不能说是收获很多&#xff0c;也算是成长经验1吧。主要工作后才知道好多东西都是自己不会的不了解的&#xff0c;但是工作需要不一定自己完全吃透&#xff0c;在合适的地方正确的使用一般情况就ok了&#xff0c;所…

突破传统文本切片的瓶颈:AntSK-FileChunk语义切片技术详解前言:为什么我们需要重新思考文本切片?

在当今大语言模型&#xff08;LLM&#xff09;应用蓬勃发展的时代&#xff0c;我们面临着一个看似简单却至关重要的问题&#xff1a;如何有效地处理长文本&#xff1f;无论是构建知识库、实现RAG&#xff08;检索增强生成&#xff09;系统&#xff0c;还是进行文档智能分析&…

LeetCode-542. 01 矩阵

1、题目描述给定一个由 0 和 1 组成的矩阵 mat &#xff0c;请输出一个大小相同的矩阵&#xff0c;其中每一个格子是 mat 中对应位置元素到最近的 0 的距离。两个相邻元素间的距离为 1 。示例 1&#xff1a;输入&#xff1a;mat [[0,0,0],[0,1,0],[0,0,0]] 输出&#xff1a;[[…

Elasticsearch如何确保数据一致性?

Elasticsearch 通过多种机制确保数据在分布式环境中的一致性&#xff0c;但由于其分布式和近实时&#xff08;Near Real-Time, NRT&#xff09;的特性&#xff0c;它提供的是最终一致性&#xff08;Eventual Consistency&#xff09;&#xff0c;而非强一致性。以下是核心机制和…

2026毕设选题-大数据-基于 Spring Boot的化妆品推荐系统的设计与实现

技术范围&#xff1a;大数据、物联网、SpringBoot、Vue、SSM、HLMT、小程序、PHP、Nodejs、Python、爬虫、数据可视化、安卓App、机器学习等设计与开发。 主要内容&#xff1a;功能设计、开题报告、任务书、中期检查PPT、系统功能实现、代码编写、论文编写和辅导、论文降重、长…

数据结构算法:顺序表

数据结构&#xff1a;顺序表一.寄包柜1.题目如何创建数组&#xff1f;1. 需求本质2. 传统静态数组的缺陷3. 动态方案&#xff1a;向量的数组4. 核心逻辑5. 关键优势总结2.解题思路2.1题目分析2.2具体解题逻辑拆解步骤2.3总结2.4参考代码二.移动零1.题目2.解题思路2.1**解题核心…