作者: Adam Humphries，Kartik Cating-Subramanian，Michael K. Reiter
出处：NDSS2021

背景

符号执行的速度一直是一个很大的问题，很多研究认为SMT求解和状态爆炸是符号执行的瓶颈。但是作者发现某些情况下，执行的速度慢是约束表达式收集的时候慢，并且是由具体执行造成的。因为大多数的符号执行工具即使是用具体值执行也会对目标程序进行解释。之所以要解释，是因为我们要追踪符号变量，沿着执行路径收集符号约束。但是作者在openssl这个程序中发现只有2.7%的指令是有符号值的。针对这个问题作者提出了一种新的符号执行方法。

insight

事务指逻辑上的一组操作，是恢复和并发控制的基本单位。比如一个线程想要用xbegin申请一个共享资源，xbegin就会开启一个事务，也就是这个线程对内存或者寄存器的任何修改要么全部提交，要么全部撤销然后回滚。在一个线程在修改共享资源的时候，另一个线程如果也访问同一个共享资源，那么就会产生冲突，至少一个线程的事务会被回滚。但是如果两个线程不对同一个共享资源进行读或者写的情况下，它们应该是可以同时进行的。因此，Intel提供了一个硬件支持叫做Intel transactional synchronization instructions(TSX)，它能够检测多个线程同时访问共享资源的时候有没有冲突，允许上述情况下两个线程同时运行，因此它的性能会更好。
TASE主要的一个亮点就是借鉴TSX的思路来提升符号执行的速度。 TASE假设在事务内的代码是没有对符号值的读和写的操作的。如果有，那就必须停掉这个事务改用解释器执行。因此对于事务性的操作就先用具体执行，遇到有符号值的操作就停止，进行模拟执行。然后再切换到具体执行。

方法设计与实现

overview：TASE设置了一个“fast path” 和一个“slow path”来分别处理具体和符号操作。主要流程如下：
1. 首先他需要输入C源代码以及程序用到的任何C库。“fast path” 就是在源码上插桩，然后用自定义的LLVM TASE编译器编译生成二进制文件。
2. 在执行程序的时候用一个poison值来标记包含符号值的字节。在执行事务性操作后检查poison的值是否被读或者修改，如果有那就回滚。
3. 如果在一个事务中没有办法实际执行完成，那就切换到“slow path”，一直执行到下一个事务的入口再切回去。
Transactional execution
目前，作者把16个基本块一组视为一个事务，然后每次执行事务的时候它会记录成功执行的基本块的数量，当事务因为对poison值读或者写而执行失败的时候，就按照记录的数量重新执行，然后从出错的那个基本块开始用“slow path”。
但是如果是别的原因造成事务失败，比如page fault，TASE会尽可能地多执行基本块，策略如下图：
Poison checking：
1. 首先以双字节为单位对有符号值的内存地址poison。
2. 在编译阶段在程序中进行插桩，主要的功能是监控所有的读和写操作，把它们涉及的值记到SIMD里面。
3. 在每个基本块结束时检查SIMD看poison的值是否被读或者写。
Interpretation
在启动interpreter的时候要先保存一个GPRs的快照。在解释器中对主存的读写时直接对被读写的地址执行的，同时在解释器中模拟执行，这样在解释结束后可以通过上下文切换恢复到fast path。TASE沿用了KLEE的解释器，对x86的每条指令提供LLVM IR解释。
State Management
从具体执行到符号执行进行切换有状态爆炸问题，TASE不能在单个地址空间并发处理多个执行状态，因为会导致事务异常。TASE在目标程序遇到一个依赖符号变量的控制流指令的时候，启动解释器，然后根据控制流用fork创建执行状态。这里它也没有直接说怎么解决状态爆炸，而是说有的情况下设置子进程的优先级，把优先级低的暂时停止之后再启动。

论文阅读_TASE: Reducing Latency of Symbolic Execution with Transactional Memory相关推荐

情感分析论文阅读之《Aspect Level Sentiment Classification with Deep Memory Network》
本文利用了加入了attention机制的QA系统中的深度记忆网络,本文将aspect word的上下文信息作为memory m中存储的内容.实现了一个针对aspect-level的情感分类模型. ...
【论文阅读笔记】ISSTA 2021-Synthesize solving strategy for symbolic execution
文章目录前言 1.基本信息 2.主要内容 3.亮点 4.不足 5.其他前言创作开始时间:2021年8月1日17:08:35 1.基本信息看到标题比较感兴趣,想读一下. Chen Z, Chen ...
[fuzz论文阅读] Symbolic execution for software testing: three decades later
Symbolic execution for software testing: three decades later 背景介绍技术难点路径探索约束求解内存建模关键目标生成一组具体的测试 ...
【论文分享】Chopped Symbolic Execution
论文名:Chopped Symbolic Execution 来源会议:ICSE 2018 论文下载地址:https://dl.acm.org/doi/10.1145/3180155.3180251 ...
【bsauce读论文】Vetting Imbalance Reference Counting in Linux kernel with Symbolic Execution
文章目录 1.简介 2.背景 3.方法 4.静态分析 (1)收集refcount信息: (2)构造 flow chain 5.符号执行 5-1 追踪 reference change 和 refcou ...
[论文阅读] (12)英文论文引言introduction如何撰写及精句摘抄——以入侵检测系统(IDS)为例
<娜璋带你读论文>系列主要是督促自己阅读优秀论文及听取学术讲座,并分享给大家,希望您喜欢.由于作者的英文水平和学术能力不高,需要不断提升,所以还请大家批评指正,非常欢迎大家给我留言评论,学 ...
[论文阅读] (03) 清华张超老师 - GreyOne: Discover Vulnerabilities with Data Flow Sensitive Fuzzing
数据流敏感的漏洞挖掘方法 Discover Vulnerabilities with Flow Sensitive Fuzzing Chao Zhang 清华大学 2nd International ...
【论文阅读】A Gentle Introduction to Graph Neural Networks [图神经网络入门]（6）
[论文阅读]A Gentle Introduction to Graph Neural Networks [图神经网络入门](6) GNN playground Some empirical GNN ...
[软件自动修复领域] 前沿论文阅读（2019年8月12日）
文章目录前言论文列表 Automated Program Repair: A Step towards Software Automation Getafix: Learning to fix b ...
【论文阅读NO.00001】Fuzzing: A Survey for Roadmap
[论文阅读NO.00001]Fuzzing: A Survey for Roadmap 0x00.一切开始之前 Abstract 0x01. INTRODUCTION 0x02. OVERVIEW O ...

论文阅读_TASE: Reducing Latency of Symbolic Execution with Transactional Memory

背景

insight

方法设计与实现

论文阅读_TASE: Reducing Latency of Symbolic Execution with Transactional Memory相关推荐

最新文章

热门文章