第九章:Dynamic Symbolic Execution
文章目录
- Dynamic Symbolic Execution
- overview
- motivation
- dynamic symbolic execution
- 常用的其他技术对比
- Random Testing
- symbolic execution
- Combined static and symbolic - Dynamic Execution (DSE)
- step1: 初始化两个具体的值 x,y
- step2: 根据定义得出 z 的 concrete value 和 symbolic state
- step3: 判断符合哪一个 path condition
- step4:对条件取反,并生成新的 concrete value
- step5:再次判断
- step6:再次取反 constrain 并得到新的 test
- step7: 再次重新初始化后开始
- 书上内容 Symbolic Execution
- symbolic test oracles
- test input generation
- Limitation
- Dynamic Symbolic Execution
- difference between symbolic 和 DSE
- DSE 的好处
- DSE 的 limitation
Dynamic Symbolic Execution
overview
Dynamic Symbolic Execution(DSE),也称为符号执行或符号化测试,是一种程序分析技术,用于自动发现软件中的错误。它是通过将程序的实际执行与抽象的符号执行相结合来完成的,这可以帮助发现程序中的各种路径,并验证这些路径上是否存在问题,如错误或安全漏洞。
motivation
-
编写和维护测试是繁琐且容易出错的。
-
idea:
- Generate regression test suite
回归测试套件(regression test suite)是一组测试用例,它们被设计用来验证软件在修改后(比如说,修复了bug或添加了新功能)仍然按照预期工作,既有功能没有因为新的代码变动而发生故障。回归测试的关键目的是确保新的代码更改没有引入新的缺陷到已有的功能中,即没有“回归”或倒退。
- Execute all reachable statements
- Catch any assertion violations
-
new technique: dynamic symbolic execution
dynamic symbolic execution

- 存储程序状态的具体和符号化表示
- 解决约束以指导分支点处的执行
- 探索被测试单元的所有执行路径
-
一种常用的 dynamic symbolic execution 是 hybrid analysis

-
程序可以看成是一个 binary tree,可能有无限的深度(因为可能存在循环),这个 tree 称为 computation tree
-
每个 node 代表 一个条件语句的执行
-
每条 edge 表示执行一系列非条件语句。也就是说,如果 node2是一个条件语句,那么 left 的分支就是使得 node2 条件为 false 的执行操作,而 node2 右边的分支就是使得其为 true 的执行操作
-
树上的每条路径表示 inputs 的一个等价类
-
实例:

-
通常会用 assert 来 if 不满足时抛出错误的操作
-
还有因为这个里面没有循环操作,因此这个树是有界的
常用的其他技术对比
Random Testing

- 如果使用 random testing,对于一个 if 条件,可能非常难测到,比如上面的例子
symbolic execution

-
symbolic execution 的核心是一个 test prover,而不使用任何具体的值
-
当程序在第一个分支的时候,test prover 会证明是否存在一个 x 使得 x ∗ 3 = = 15 x*3==15 x∗3==15 这个条件成立;test prover 会说 “存在”,那么这个 condition 为 true 的分支就会成功执行;接下来会询问是否存在 x 使得 x ∗ 3 ! = 15 x*3!=15 x∗3!=15 这个条件成立(也就是 condition 的 else 分支),test prover 会说 “存在”,因此第一个 condition 的 else 也会成功执行
-
接下来是第二层分支,继续询问 test prover,是否存在 x x x 满足 x ∗ 3 = = 15 & & x % 5 = = 0 x*3==15 ~\&\& ~x \% 5==0 x∗3==15 && x%5==0 ,test prover 会说 “存在”,那么
print(ok)成功可达;然后询问 else 的 condition,即是否存咋 x x x 满足 x ∗ 3 = = 15 & & x % 5 ! = 0 x*3==15 ~\&\& ~x \% 5!=0 x∗3==15 && x%5!=0,test prover 会说 “不存在”;因此这个 else 永远不可达,无论在什么条件下。 -
这成功避免了 random testing 的无法进入分支的问题。但他也存在自己的问题,那就是,在大型程序中,这种 if else 的叠加会迅速爆炸,因为条件太多了且都是级联的。
-
另外一个缺点是 symbolic execution 可能不够强大

-
上述条件对于 test prover 来说是困难的,因此可能存在误报
Combined static and symbolic - Dynamic Execution (DSE)

step1: 初始化两个具体的值 x,y
- 除了两个具体的值之外,x,y 分别的 symbolic 的 state 也会记录下来,现在是 x = x 0 , y = y 0 x=x_0, y=y_0 x=x0,y=y0

step2: 根据定义得出 z 的 concrete value 和 symbolic state
- 可以计算出 z = 14 z=14
相关文章:
第九章:Dynamic Symbolic Execution
文章目录 Dynamic Symbolic Executionoverviewmotivationdynamic symbolic execution常用的其他技术对比Random Testingsymbolic executionCombined static and symbolic - Dynamic Execution (DSE)step1: 初始化两个具体的值 x,ystep2: 根据定义得出 z 的 concrete value 和 s…...
在搜索引擎中屏蔽csdn
csdn是一个很好的技术博客,里面信息很丰富,我也喜欢在csdn上做技术笔记。 但是CSDN体量太大,文章质量良莠不齐。当在搜索引擎搜索技术问题时,搜索结果中CSDN的内容占比太多,导致难以从其他优秀的博客平台中获取信息。因…...
Linux开发工具的使用(vim、gcc/g++ 、make/makefile)
文章目录 一 :vim1:vim基本概念2:vim的常用三种模式3:vim三种模式的相互转换4:vim命令模式下的命令集- 移动光标-删除文字-剪切/删除-复制-替换-撤销和恢复-跳转至指定行 5:vim底行模式下的命令集 二:gcc/g1:gcc/g的作用2:gcc/g的语法3:预处理4:编译5:汇编6:链接7:函…...
MySQL(10):创建和管理表
基础知识 在 MySQL 中,一个完整的数据存储过程总共有 4 步,分别是:创建数据库、确认字段、创建数据表、插入数据。 要先创建一个数据库,而不是直接创建数据表:从系统架构的层次上看,MySQL 数据库系统从大到…...
Python赋值给另一个变量且不改变原变量
Python赋值给另一个变量且不改变原变量 在Python中,如果你想将一个变量的值赋给另一个变量,同时保持原变量不变,你可以使用复制(copy)而不是引用(reference)。Python中的变量通常是通过引用&…...
PHP进销存ERP系统源码
PHP进销存ERP系统源码 系统介绍: 扫描入库库存预警仓库管理商品管理供应商管理。 1、电脑端手机端,手机实时共享,手机端一目了然。 2、多商户Saas营销版 无限开商户,用户前端自行注册,后台管理员审核开通 3、管理…...
npm i 报错:Cannot read properties of null (reading ‘refs‘)
问题: 旧项目要更改东西,重新部署上线的时候,发现页面显示有异常。当时在开发环境是没有问题的。后经排查是一个引入swiper的页面报错了,只要注释掉swiper插件,就没问题了,但这肯定是不行的。 原因: npm和…...
C#学习中关于Visual Studio中ctrl+D快捷键(快速复制当前行)失效的解决办法
1、进入VisualStudio主界面点击工具——>再点击选项 2、进入选项界面后点击环境——>再点击键盘,我们可用看到右边的界面的映射方案是VisualC#2005 3、 最后点击下拉框,选择默认值,点击之后确定即可恢复ctrlD的快捷键功能 4、此时可以正…...
银河E8,吉利版Model 3:5米大车身、45寸大屏、首批8295座舱芯
作者 | Amy 编辑 | 德新 吉利银河E8在曝光后多次引爆热搜,李书福更是赞誉有加,称其为「买了就直接享受」。这款备受瞩目的车型于 10月30日晚首次亮相。 虽然新车外观在今年上海车展上早已曝光,但这次的发布会却带来了不少惊喜。新车架构以及…...
技术分享 | 被测项目需求你理解到位了么?
需求分析是开始测试工作的第一步,产品会先产出一个需求文档,然后会组织需求宣讲,在需求宣讲中分析需求中是否存在问题,然后宣讲结束后,通过需求文档分析测试点并且预估排期。所以对于需求的理解非常重要。 需求文档 …...
[MRCTF2020]你传你呢1
提示 只对php以及phtml文件之类的做了防护content-type.htaccess文件 这里就不整那么麻烦直接抓包测试 首先对后缀测试看过滤了哪些 (php php3 pht php5 phtml phps) 全部被ban了 到这里的后续思路通过上传一些配置文件把上传的图片都以php文件执行 尝试上传图片码, 直接上传成…...
一些对程序员有用的网站
当你遇到问题时 Stack Overflow:订阅他们的每周新闻和任何你感兴趣的主题Google:全球最大搜索引擎必应:在你无法使用Google的时候CSDN:聊胜于无AI导航一号AI导航二号 新闻篇 OSCHINA:中文开源技术交流社区 针对初学…...
小程序使用echarts(超详细教程)
小程序使用echarts第一步就是先引用到小程序里面,可以直接从这里下载 文件很多,我们值下载 ec-canvas 就好,下载完成后,直接放在pages同级目录下 index.js 在我们需要的页面的 js 文件顶部引入 // pages/index/index.js impor…...
js控制输入框中的光标位置
主要逻辑 主要应用selectionStart、selectionEnd来实现 <!DOCTYPE html> <html lang"en"><head><meta charset"UTF-8"><meta name"viewport" content"widthdevice-width, initial-scale1.0"><title…...
Openssl生成证书-nginx使用ssl
Openssl生成证书并用nginx使用 安装openssl yum install openssl -y创库目录存放证书 mkdir /etc/nginx/cert cd /etc/nginx/cert配置本地解析 cat >>/etc/hosts << EOF 10.10.10.21 kubernetes-master.com EOF10.10.10.21 主机ip、 kubernetes-master.com 本…...
Go语言实现数据结构栈和队列
Go语言实现数据结构栈和队列 1、栈 package mainimport "fmt"func main(){// 创建栈stack : make([]int, 0)// push压入栈stack append(stack, 10)// pop弹出v : stack[len(stack)-1]// 10fmt.Println(v)stack stack[:len(stack)-1]// 检查栈空// truefmt.Printl…...
【vscode】Window11环境下vscode使用Fira Code字体【教程】
【vscode】Window11环境下vscode使用Fira Code字体【教程】 文章目录 【vscode】Window11环境下vscode使用Fira Code字体【教程】1. 下载Fira Code字体2. 安装Fira Code字体3. 配置vscode4. 效果如下Reference 如果想要在Ubuntu环境下使用Fira Code字体,可以参考我的…...
Sandcastle生成文档
下载: https://github.com/EWSoftware/SHFB/releases 使用Sandcastle生成Api文档需要使用对应程序集的注释xml 程序集dll作为数据源,通过对xml dll数据解析生成文档;所以主体步骤如下: 程序集资源生成创建配置.shfbproj项目编译构建文档 …...
P1368 【模板】最小表示法
题目描述 小敏和小燕是一对好朋友。 他们正在玩一种神奇的游戏,叫 Minecraft。 他们现在要做一个由方块构成的长条工艺品。但是方块现在是乱的,而且由于机器的要求,他们只能做到把这个工艺品最左边的方块放到最右边。 他们想,…...
【Hive】内部表(Managed Table)和外部表(External Table)相关知识点
在Hive中,有两种类型的表:外部表(External Table)和内部表(Managed Table)。它们在数据存储和管理方式上存在一些重要的区别。 本文就来对这些知识做一个总结。 1、如何在hive中创建内部表和外部表? 2、内部表和外部表的一些区别。 3、怎么查看一个表是内部表还是外部表…...
树莓派超全系列教程文档--(62)使用rpicam-app通过网络流式传输视频
使用rpicam-app通过网络流式传输视频 使用 rpicam-app 通过网络流式传输视频UDPTCPRTSPlibavGStreamerRTPlibcamerasrc GStreamer 元素 文章来源: http://raspberry.dns8844.cn/documentation 原文网址 使用 rpicam-app 通过网络流式传输视频 本节介绍来自 rpica…...
《用户共鸣指数(E)驱动品牌大模型种草:如何抢占大模型搜索结果情感高地》
在注意力分散、内容高度同质化的时代,情感连接已成为品牌破圈的关键通道。我们在服务大量品牌客户的过程中发现,消费者对内容的“有感”程度,正日益成为影响品牌传播效率与转化率的核心变量。在生成式AI驱动的内容生成与推荐环境中࿰…...
AI书签管理工具开发全记录(十九):嵌入资源处理
1.前言 📝 在上一篇文章中,我们完成了书签的导入导出功能。本篇文章我们研究如何处理嵌入资源,方便后续将资源打包到一个可执行文件中。 2.embed介绍 🎯 Go 1.16 引入了革命性的 embed 包,彻底改变了静态资源管理的…...
【Java学习笔记】BigInteger 和 BigDecimal 类
BigInteger 和 BigDecimal 类 二者共有的常见方法 方法功能add加subtract减multiply乘divide除 注意点:传参类型必须是类对象 一、BigInteger 1. 作用:适合保存比较大的整型数 2. 使用说明 创建BigInteger对象 传入字符串 3. 代码示例 import j…...
Mysql中select查询语句的执行过程
目录 1、介绍 1.1、组件介绍 1.2、Sql执行顺序 2、执行流程 2.1. 连接与认证 2.2. 查询缓存 2.3. 语法解析(Parser) 2.4、执行sql 1. 预处理(Preprocessor) 2. 查询优化器(Optimizer) 3. 执行器…...
Pydantic + Function Calling的结合
1、Pydantic Pydantic 是一个 Python 库,用于数据验证和设置管理,通过 Python 类型注解强制执行数据类型。它广泛用于 API 开发(如 FastAPI)、配置管理和数据解析,核心功能包括: 数据验证:通过…...
算法刷题-回溯
今天给大家分享的还是一道关于dfs回溯的问题,对于这类问题大家还是要多刷和总结,总体难度还是偏大。 对于回溯问题有几个关键点: 1.首先对于这类回溯可以节点可以随机选择的问题,要做mian函数中循环调用dfs(i&#x…...
五、jmeter脚本参数化
目录 1、脚本参数化 1.1 用户定义的变量 1.1.1 添加及引用方式 1.1.2 测试得出用户定义变量的特点 1.2 用户参数 1.2.1 概念 1.2.2 位置不同效果不同 1.2.3、用户参数的勾选框 - 每次迭代更新一次 总结用户定义的变量、用户参数 1.3 csv数据文件参数化 1、脚本参数化 …...
【汇编逆向系列】六、函数调用包含多个参数之多个整型-参数压栈顺序,rcx,rdx,r8,r9寄存器
从本章节开始,进入到函数有多个参数的情况,前面几个章节中介绍了整型和浮点型使用了不同的寄存器在进行函数传参,ECX是整型的第一个参数的寄存器,那么多个参数的情况下函数如何传参,下面展开介绍参数为整型时候的几种情…...
【多线程初阶】单例模式 指令重排序问题
文章目录 1.单例模式1)饿汉模式2)懒汉模式①.单线程版本②.多线程版本 2.分析单例模式里的线程安全问题1)饿汉模式2)懒汉模式懒汉模式是如何出现线程安全问题的 3.解决问题进一步优化加锁导致的执行效率优化预防内存可见性问题 4.解决指令重排序问题 1.单例模式 单例模式确保某…...
