当前位置: 首页 > news >正文

第九章: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 x3==15 这个条件成立;test prover 会说 “存在”,那么这个 condition 为 true 的分支就会成功执行;接下来会询问是否存在 x 使得 x ∗ 3 ! = 15 x*3!=15 x3!=15 这个条件成立(也就是 condition 的 else 分支),test prover 会说 “存在”,因此第一个 condition 的 else 也会成功执行

  • 接下来是第二层分支,继续询问 test prover,是否存在 x x x 满足 x ∗ 3 = = 15   & &   x % 5 = = 0 x*3==15 ~\&\& ~x \% 5==0 x3==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 x3==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字体&#xff0c;可以参考我的…...

Sandcastle生成文档

下载: https://github.com/EWSoftware/SHFB/releases 使用Sandcastle生成Api文档需要使用对应程序集的注释xml 程序集dll作为数据源&#xff0c;通过对xml dll数据解析生成文档&#xff1b;所以主体步骤如下&#xff1a; 程序集资源生成创建配置.shfbproj项目编译构建文档 …...

P1368 【模板】最小表示法

题目描述 小敏和小燕是一对好朋友。 他们正在玩一种神奇的游戏&#xff0c;叫 Minecraft。 他们现在要做一个由方块构成的长条工艺品。但是方块现在是乱的&#xff0c;而且由于机器的要求&#xff0c;他们只能做到把这个工艺品最左边的方块放到最右边。 他们想&#xff0c;…...

【Hive】内部表(Managed Table)和外部表(External Table)相关知识点

在Hive中,有两种类型的表:外部表(External Table)和内部表(Managed Table)。它们在数据存储和管理方式上存在一些重要的区别。 本文就来对这些知识做一个总结。 1、如何在hive中创建内部表和外部表? 2、内部表和外部表的一些区别。 3、怎么查看一个表是内部表还是外部表…...

Linux应用开发之网络套接字编程(实例篇)

服务端与客户端单连接 服务端代码 #include <sys/socket.h> #include <sys/types.h> #include <netinet/in.h> #include <stdio.h> #include <stdlib.h> #include <string.h> #include <arpa/inet.h> #include <pthread.h> …...

MPNet:旋转机械轻量化故障诊断模型详解python代码复现

目录 一、问题背景与挑战 二、MPNet核心架构 2.1 多分支特征融合模块(MBFM) 2.2 残差注意力金字塔模块(RAPM) 2.2.1 空间金字塔注意力(SPA) 2.2.2 金字塔残差块(PRBlock) 2.3 分类器设计 三、关键技术突破 3.1 多尺度特征融合 3.2 轻量化设计策略 3.3 抗噪声…...

java_网络服务相关_gateway_nacos_feign区别联系

1. spring-cloud-starter-gateway 作用&#xff1a;作为微服务架构的网关&#xff0c;统一入口&#xff0c;处理所有外部请求。 核心能力&#xff1a; 路由转发&#xff08;基于路径、服务名等&#xff09;过滤器&#xff08;鉴权、限流、日志、Header 处理&#xff09;支持负…...

MongoDB学习和应用(高效的非关系型数据库)

一丶 MongoDB简介 对于社交类软件的功能&#xff0c;我们需要对它的功能特点进行分析&#xff1a; 数据量会随着用户数增大而增大读多写少价值较低非好友看不到其动态信息地理位置的查询… 针对以上特点进行分析各大存储工具&#xff1a; mysql&#xff1a;关系型数据库&am…...

多场景 OkHttpClient 管理器 - Android 网络通信解决方案

下面是一个完整的 Android 实现&#xff0c;展示如何创建和管理多个 OkHttpClient 实例&#xff0c;分别用于长连接、普通 HTTP 请求和文件下载场景。 <?xml version"1.0" encoding"utf-8"?> <LinearLayout xmlns:android"http://schemas…...

YSYX学习记录(八)

C语言&#xff0c;练习0&#xff1a; 先创建一个文件夹&#xff0c;我用的是物理机&#xff1a; 安装build-essential 练习1&#xff1a; 我注释掉了 #include <stdio.h> 出现下面错误 在你的文本编辑器中打开ex1文件&#xff0c;随机修改或删除一部分&#xff0c;之后…...

unix/linux,sudo,其发展历程详细时间线、由来、历史背景

sudo 的诞生和演化,本身就是一部 Unix/Linux 系统管理哲学变迁的微缩史。来,让我们拨开时间的迷雾,一同探寻 sudo 那波澜壮阔(也颇为实用主义)的发展历程。 历史背景:su的时代与困境 ( 20 世纪 70 年代 - 80 年代初) 在 sudo 出现之前,Unix 系统管理员和需要特权操作的…...

前端开发面试题总结-JavaScript篇(一)

文章目录 JavaScript高频问答一、作用域与闭包1.什么是闭包&#xff08;Closure&#xff09;&#xff1f;闭包有什么应用场景和潜在问题&#xff1f;2.解释 JavaScript 的作用域链&#xff08;Scope Chain&#xff09; 二、原型与继承3.原型链是什么&#xff1f;如何实现继承&a…...

Unit 1 深度强化学习简介

Deep RL Course ——Unit 1 Introduction 从理论和实践层面深入学习深度强化学习。学会使用知名的深度强化学习库&#xff0c;例如 Stable Baselines3、RL Baselines3 Zoo、Sample Factory 和 CleanRL。在独特的环境中训练智能体&#xff0c;比如 SnowballFight、Huggy the Do…...

IoT/HCIP实验-3/LiteOS操作系统内核实验(任务、内存、信号量、CMSIS..)

文章目录 概述HelloWorld 工程C/C配置编译器主配置Makefile脚本烧录器主配置运行结果程序调用栈 任务管理实验实验结果osal 系统适配层osal_task_create 其他实验实验源码内存管理实验互斥锁实验信号量实验 CMISIS接口实验还是得JlINKCMSIS 简介LiteOS->CMSIS任务间消息交互…...