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

【软件分析/静态分析】学习笔记01——Introduction

🔗 课程链接:李樾老师和谭天老师的:南京大学《软件分析》课程01(Introduction)_哔哩哔哩_bilibili

目录

一、静态程序分析介绍

1.1 PL and Static Analysis 程序语言和静态分析

1.2 为什么要学 Static Analysis?

1.3 什么是静态分析 ?

1.4 静态分析的特征和例子

1.4.1 sound and complete (no perfect static analysis)

1.4.2 false negatives or false positives (useful static analysis)

1.4.3 Static Analysis 例子 — Bird's Eye View

1.5 静态分析大致步骤—举个例子🌰

1.5.1 Abstraction(抽象)

1.5.2 Over-approximation(近似): Transfer Functions(转换函数)

1.5.3 Over-approximation(近似): Control Flow(控制流)

1.5.4 总结


一、静态程序分析介绍

1.1 PL and Static Analysis 程序语言和静态分析

PL (Programming Languages, 程序语言)

Static Analysis(静态分析)

如下图所示,PL可以分为三个主题:理论、环境和应用

  • 理论:语言设计、语言的类型系统、形式语义和逻辑……
  • 环境:编译、运行时系统……
  • 应用:程序分析、程序验证、程序合成……

程序语言的分类

  •  命令形语言:C、Java
  •  函数式语言:JavaScript、
  •  逻辑式语言:一条条逻辑声明出来的语言

挑战
        这么多年来,语言的核心没有变,但是软件越来越复杂,如何保证大规模复杂程序的安全性、可靠性……?

1.2 为什么要学 Static Analysis?

从代码层面来看,静态分析可以做很多事情,后续也会详细讲到:

  • 对程序可靠性Program Reliability
        空指针引用 null pointer dereference, 内存泄漏 memory leak……
  • 对安全性 Program Security
         私有信息泄露 private infomation leak, 注入攻击injection attack……
  • 编译优化 Compiler Optimization
        死代码消除 Dead code elimination,code motion……
  • 程序理解 Program Understanding
        IDE call hierarchy, type indication……

对于程序员,静态分析可以帮助写更高质量的代码。

1.3 什么是静态分析 ?

Static analysis analyzes a program P to reason about its behaviors and
determines whether it satisfies some properties before running P.

静态分析(static analysis) 是在程序运行之前,分析其行为,确定它是是否能满足某些特性要求:

  • 有没有一些程序泄露
  • 有没有空指针引用异常?
  • 所有的变量variable 用之前都初始化了吗?
  • 所有的cast operation是安全的吗?
  • v1和v2会不会指向相同的内存地址?
  • 程序中的断言语句 assert 会失败吗?
  • 死代码?
  • ……

但是,根据Rice' Theorem(大米定理/莱斯定理),不存在一个方法可以给出一个确切的答案Yes or No,原文如下:

"Any non-trivial property of the behavior ofprograms in a r.e.language is undecidable."

这句话里的一些词:

  • r.e.(recursively enumerable) = recognizable by a Turing-machine
    r.e. language递归可枚举的语言(图灵机可识别的语言,可以理解为现代的编程语言,C 、JAVA)
  • non-trivial property:≈ 一些有趣/有价值的性质 ≈ 与动态运行时行为runtime behaviors相关的性质,就像前边列举的空指针、内存变量什么的。
  • undecidable: 给不出确切答案

可以这么理解:    

        一个递归可枚举的语言(图灵机可识别的语言,可以理解为现代的编程语言,C 、JAVA),他的一些non-trivail property(与程序运行时行为相关的性质,例如是否有空指针、有没有内存泄漏)是不能确定的(例如不能准确地说有空指针或者没有)。

再学术一点的理解:

        一个 完美的静态分析(perfect static analysis) 是满足 sound and complete 的(sound 和 comlete是 静态分析的两个特征,见1.4.1).
        大米定理就是在告诉我们,不存在完美的静态分析,可以准确地回答Truth,也就是不能同时满足sound 和 complete.

1.4 静态分析的特征和例子

为什么没有一个perfect的呢,因为一些情况其实不可避免,导致分析要么太“过”(sound),要么太“保守”(complete)。

1.4.1 sound and complete (no perfect static analysis)

        如图所示,complete和sound的关系:

  • truth:是这个程序中理论上的所有的正确的答案
  • complete:指的是,报出来的,都是对的,但是不全
  • sound:包含了所有正确答案,

1.4.2 false negatives or false positives (useful static analysis)

既然没有perfect静态分析,为什么还要去研究呢?因为可以对一方妥协,由此就有了useful static analysis(有用的静态分析)。

Useful static analysis:

  • Compromise soundness (false negatives,假阴性) : 妥协soundness,就是不sound,会产生漏报(错的没检测到)
  • Compromise completeness(false positives,假阳性):妥协completeness,不complete,会产生误报(对的说是错的)

在绝大Useful静态分析中,我们所研究的更多是妥协completeness:要求分析是 Sound 的,虽然并不全都准确(not fully-precise)(宁可错杀100不可放过一个),可以误报,但是不能漏。

soundness越好,分析就越好。

1.4.3 Static Analysis 例子 — Bird's Eye View

        如下图,对左侧的代码进行分析的时候,产生的2个分析结果

        这两个分析结果都是对的,没有产生漏报,都满足sound,且:
                1 更准确但是昂贵;
                2 不够准确但是cheep;
        还有一些可能的分析结果如下:
                3. x = 0, 1, 2, 3, 4
                4. x = 1, 2, 3, 4
        其中,3产生了误报,都是涵盖了所有情况,也是sound,是对的;都是4漏了0,是错误的。

一句话概括静态分析

        静态分析是在确保(or 尽量接近)soundness的同时,在分析精度(precision)速度(speed)之间做一个平衡,这才是一个Useful 静态分析

在实际分析中,可能不存在真正的soundness的,例如java的反射机制、Java的动态类机制,都会影响到soundness,所以是“尽量接近”soundness。

1.5 静态分析大致步骤—举个例子🌰

从技术层面分析静态分析的大致步骤,用两个词来总结静态分析:
Static Analysis = Abstraction + Over-approximation 

以下通过一个例子来初步感受一下静态分析:

例如:要给一个程序的所有变量判断正负(+,0,-),需要以下两步:

  • Abstraction
  • Over-approximation
    • Transfer functions
    • Control flows

1.5.1 Abstraction(抽象)

  •   抽象就是把具体的域值映射到抽象域里。

        如下图,将左边的变量映射到右边不同的正负情况。抽象成不同的符号。

   

  • \top (unknown):如果当前数值会因为变量改变而呈现为不同的状态
  • \perp (undefined): 经过判断肯定不符合int定义的,例如一个除以0的数或者字符等。

1.5.2 Over-approximation(近似): Transfer Functions(转换函数)

        在完成抽象之后,我们需要做的就是近似,其中一部就是用到转换函数,转换函数的作用可以概括为如下两句:

  • 在静态分析中,转换函数定义了一种转换规则:如何评估关于抽象值的不同程序语句
  • 根据“要分析的问题/目标”和不同程序中的“语义(semantics)”来进行评估。

        针对于这个例子要分析的问题,转换的规则如下图所示:
                

         利用以上规则,来评估一下具体的程序语句,如下:

                

  • 对于变量c:我们找到了一个除以零的错误
  • 对于变量p:y是负数,我们找到了一个负数索引的错误
  • 对于变量q:因为a不确定是否为负数,而判定其为undefined,但其实a并不是负数,这里就是一个误报

        通过判断符号,我们成功找到了两个错误 c 和 p,说明静态分析是很有用的useful,但是Over-approximation 的静态分析也产生了误报 假阳性 false positives

1.5.3 Over-approximation(近似): Control Flow(控制流)

  • 近似还要有控制流,也就是程序执行的流,要将所有流汇聚的地方,进行合并抽象 flow merging

        如下图左侧的程序片段转为右侧的控制流,然后判断符号,[ z = x + y ] 是汇聚的点,所以要枚举其所有分支,进行合并,即 [ y = \top

        在静态分析中,如果程序很复杂,我们无法在实际应用中枚举所有的路径,分支流合flow merging (作为over-approximation 的一种方式)是常用的分支推断技术,提升了Soundness,也降低了Completeness,也导致了不可避免的误报问题。

1.5.4 总结

        抽象就是将具体值,转为符号值。因为在Abstraction抽象过程中进行了值域空间的 降维抽象 ,所以在转换函数映射中,静态符号执行和动态实际实行的结果之间,是存在差异的,这是不可避免的。

        近似就是将每个语句,和每个语句之间的关联进行抽象,化为图来说,就是每个节点,和每个节点之间的箭头
        · transfer funtions 是对每个语句的近似;
        · control flow 的近似就是 每个箭头 的近似

        将每个语句,以及不同语句之间的箭头 都进行近似,就实现了对整个程序近似

相关文章:

【软件分析/静态分析】学习笔记01——Introduction

🔗 课程链接:李樾老师和谭天老师的:南京大学《软件分析》课程01(Introduction)_哔哩哔哩_bilibili 目录 一、静态程序分析介绍 1.1 PL and Static Analysis 程序语言和静态分析 1.2 为什么要学 Static Analysis? …...

Java数组

文章目录 前言一维数组数组定义创建数组数组的内存模型数组数据初始化数组元素访问遍历数组length常见数组异常 二分查找数组的操作数组的复制数组的排序 二维数组扩展 Java中定义数组的语法如下: 数据类型[] 数组名 new 数据类型[数组长度]; 数据类型指的是数组中…...

【数据库原理入门】

数据库原理:深入探索与实践指南 引言 在我们的日常生活中,数据库无处不在,从在线购物、银行交易到社交媒体,都离不开数据库。要想成为一名出色的开发者,理解数据库原理是非常重要的。本文将以简明易懂的方式&#xf…...

练习Vue烘培坊项目

烘培坊项目 文章目录 烘培坊项目项目概述项目页面展示后台管理页面登录页面文章详情页面稿件发布页面 项目关键代码实现后台管理页面稿件管理页面内容列表页面文章详情页面烘培坊主页面注册页面登录页面个人信息页面稿件发布页面 项目概述 烘培坊(Bakery&#xff0…...

API测试| 了解API接口测试| API接口测试指南

什么是API? API是一个缩写,它代表了一个 pplication P AGC软件覆盖整个房间。API是用于构建软件应用程序的一组例程,协议和工具。API指定一个软件程序应如何与其他软件程序进行交互。 例行程序:执行特定任务的程序。例程也称为过…...

使用canvas给图片添加水印

上接文章“图片处理” canvas元素其实就是一个画布,我们可以很方便地绘制一些文字、线条、图形等,它也可以将一个img标签里渲染的图片画在画布上。 我们在上传文件到后端的时候,使用input标签读取用户本地文件后得到的其实是一个Blob对象&a…...

栈和队列的概念和实现

栈 栈 定义:只能在一端进行插入或删除操作的的线性表 主要特点:后进先出 存储结构的实现 顺序存储结构 链式存储结构 用途:通常作为一种临时存放数据的容器。如果后存入的元素先处理则使用栈。比如用于保存函…...

PostgreSQL 源码部署

文章目录 说明1. 准备工作1.1 源码包下载1.2 解压安装目录1.3 安装依赖包1.4 添加用户1.5 创建数据目录 2. 编译安装2.1 源码编译2.2 配置环境变量2.3 初始化数据库2.4 启动数据库2.5 连接数据库 3. 参数调整3.1 配置 pg_hba3.2 监听相关2.4 日志文件2.5 内存参数 说明 本篇文…...

医疗IT系统安科瑞隔离电源装置在医院的应用

【摘要】介绍该三级综合医院采用安科瑞隔离电源系统5件套,使用落地式配电柜安装方式,从而实现将TN系统转化为IT系统,以及系统绝缘情况监测。 【关键词】医用隔离电源系统;IT系统;绝缘情况监测;三级综合医院…...

高压放大器在3D打印中的应用

随着3D打印技术的快速发展,高压放大器在3D打印中的应用越来越受到人们的关注。高压放大器在3D打印中扮演着非常重要的角色,可以提高3D打印的效率和精度,从而实现更高的打印质量。本文将详细介绍高压放大器在3D打印中的应用及其原理。 高压放…...

chatgpt赋能python:Python中的三角函数介绍

Python中的三角函数介绍 Python作为一种高级编程语言,可以处理基础算术运算、三角函数等高等数学的操作。其中,三角函数是常用的数学函数之一,Pyhon中的三角函数包括正弦函数、余弦函数、正切函数等。 正弦函数 正弦函数在三角学中是最基本…...

异常检测论文1

本文仅作为个人阅读文献&#xff0c;做笔记记录。 <> \usepackage[dvipsnames]{xcolor} 一、摘要部分&#xff1a; 我们发现&#xff0c;现有的数据集偏向于局部结构异常&#xff0c;如划痕、凹痕或污染。特别是&#xff0c;它们缺乏违反逻辑约束形式的异常&#xff0…...

linux搭建hadoop环境

1、安装JDK   &#xff08;1&#xff09;下载安装JDK&#xff1a;确保计算机联网之后命令行输入下面命令安装JDK    sudo apt-get install sun-java8-jdk   &#xff08;2&#xff09;配置计算机Java环境&#xff1a;打开/etc/profile&#xff0c;在文件最后输入下面…...

02 Maven创建及使用

maven作用 主要用作基于java平台的项目 maven能提供一种项目配置 maven能自动从maven的中央仓库帮我们自动下载并管路项目依赖的jar包 提供了标准的目录结构 中央仓库两种类型:共有的中央仓库:私有中央仓库 使用mvn -v查看是否安装成功 修改本地仓库的的位置 在setting…...

如何在 Rocky Linux 上检查磁盘空间?

在 Rocky Linux 上检查磁盘空间是系统管理和维护的重要任务之一。磁盘空间的监控和管理可以帮助我们及时发现和解决存储空间不足的问题&#xff0c;以确保系统的正常运行。本文将详细介绍在 Rocky Linux 上检查磁盘空间的方法。 方法 1&#xff1a;使用 df 命令 df 命令是 Li…...

【软考系统规划与管理师笔记】第2篇 信息技术知识1

目录 1 软件工程 1.1 软件需求分析与定义 1.2 软件设计、测试与维护 1.3 软件质量保证及质量评价 1.4 软件配置管理 1.5 软件过程管理 1.6 软件复用 2 面向对象系统分析与设计 2.1 面向对象设计的基本概念 2.2统一建模语言与可视化建模 3. 应用集成技术 3.1 数据库与…...

【无标题】ELISA-3(加装跟踪装置)—让群体协作更智能!

群体智能是近年来发展迅速的一个人工智能学科领域&#xff0c;通过对蚂蚁、蜜蜂等为代表的社会性昆虫群体行为的研究&#xff0c;实现分布式等智能行为。作为新一代人工智能的重要方向&#xff0c;群体智能通常用于无人机、机器人集群的协同作业。目前&#xff0c;群体智能在基…...

Dubbo源码解析一服务暴露与发现

Dubbo 服务暴露与发现 1. Spring中自定义Schema1.1 案例使用1.2 dubbo中的相关对象 2. 服务暴露机制2.1 术语解释2.2 流程机制2.3 源码分析2.3.1 导出入口2.3.2 导出服务到本地2.3.3 导出服务到远程(重点)2.3.4 开启Netty服务2.3.5 服务注册2.3.6 总结 3. 服务发现3.1 服务发现…...

有哪些工具软件一旦用了就离不开?

&#x1f496;前言 目前&#xff0c;随着科技的快速发展&#xff0c;电脑已经进入了许许多多人的生活 &#xff0c;在平日的学习、工作和生活里&#xff0c;我们会用的各种各样的强大软件。市面上除了某些大公司开发在强大软件&#xff0c;还有各路大神开发具有某些功能的强大…...

ObjectARX如何判断点和多段线的关系

目录 1 基本思路2 相关知识点2.1 ECS坐标系概述2.2 其他点坐标转换接口2.3 如何获取多段线的顶点ECS坐标 3 实现例程3.1 接口实现3.2 测试代码 4 实现效果 在CAD的二次开发中&#xff0c;点和多段线的关系是一个非常重要且常见的问题&#xff0c;本文实现例程以张帆所著《Objec…...

MFC内存泄露

1、泄露代码示例 void X::SetApplicationBtn() {CMFCRibbonApplicationButton* pBtn GetApplicationButton();// 获取 Ribbon Bar 指针// 创建自定义按钮CCustomRibbonAppButton* pCustomButton new CCustomRibbonAppButton();pCustomButton->SetImage(IDB_BITMAP_Jdp26)…...

QMC5883L的驱动

简介 本篇文章的代码已经上传到了github上面&#xff0c;开源代码 作为一个电子罗盘模块&#xff0c;我们可以通过I2C从中获取偏航角yaw&#xff0c;相对于六轴陀螺仪的yaw&#xff0c;qmc5883l几乎不会零飘并且成本较低。 参考资料 QMC5883L磁场传感器驱动 QMC5883L磁力计…...

UDP(Echoserver)

网络命令 Ping 命令 检测网络是否连通 使用方法: ping -c 次数 网址ping -c 3 www.baidu.comnetstat 命令 netstat 是一个用来查看网络状态的重要工具. 语法&#xff1a;netstat [选项] 功能&#xff1a;查看网络状态 常用选项&#xff1a; n 拒绝显示别名&#…...

Golang dig框架与GraphQL的完美结合

将 Go 的 Dig 依赖注入框架与 GraphQL 结合使用&#xff0c;可以显著提升应用程序的可维护性、可测试性以及灵活性。 Dig 是一个强大的依赖注入容器&#xff0c;能够帮助开发者更好地管理复杂的依赖关系&#xff0c;而 GraphQL 则是一种用于 API 的查询语言&#xff0c;能够提…...

cf2117E

原题链接&#xff1a;https://codeforces.com/contest/2117/problem/E 题目背景&#xff1a; 给定两个数组a,b&#xff0c;可以执行多次以下操作&#xff1a;选择 i (1 < i < n - 1)&#xff0c;并设置 或&#xff0c;也可以在执行上述操作前执行一次删除任意 和 。求…...

页面渲染流程与性能优化

页面渲染流程与性能优化详解&#xff08;完整版&#xff09; 一、现代浏览器渲染流程&#xff08;详细说明&#xff09; 1. 构建DOM树 浏览器接收到HTML文档后&#xff0c;会逐步解析并构建DOM&#xff08;Document Object Model&#xff09;树。具体过程如下&#xff1a; (…...

涂鸦T5AI手搓语音、emoji、otto机器人从入门到实战

“&#x1f916;手搓TuyaAI语音指令 &#x1f60d;秒变表情包大师&#xff0c;让萌系Otto机器人&#x1f525;玩出智能新花样&#xff01;开整&#xff01;” &#x1f916; Otto机器人 → 直接点明主体 手搓TuyaAI语音 → 强调 自主编程/自定义 语音控制&#xff08;TuyaAI…...

【JavaSE】绘图与事件入门学习笔记

-Java绘图坐标体系 坐标体系-介绍 坐标原点位于左上角&#xff0c;以像素为单位。 在Java坐标系中,第一个是x坐标,表示当前位置为水平方向&#xff0c;距离坐标原点x个像素;第二个是y坐标&#xff0c;表示当前位置为垂直方向&#xff0c;距离坐标原点y个像素。 坐标体系-像素 …...

优选算法第十二讲:队列 + 宽搜 优先级队列

优选算法第十二讲&#xff1a;队列 宽搜 && 优先级队列 1.N叉树的层序遍历2.二叉树的锯齿型层序遍历3.二叉树最大宽度4.在每个树行中找最大值5.优先级队列 -- 最后一块石头的重量6.数据流中的第K大元素7.前K个高频单词8.数据流的中位数 1.N叉树的层序遍历 2.二叉树的锯…...

基于matlab策略迭代和值迭代法的动态规划

经典的基于策略迭代和值迭代法的动态规划matlab代码&#xff0c;实现机器人的最优运输 Dynamic-Programming-master/Environment.pdf , 104724 Dynamic-Programming-master/README.md , 506 Dynamic-Programming-master/generalizedPolicyIteration.m , 1970 Dynamic-Programm…...