南京大学-软件分析-课程01-Introduction

news2024/12/17 4:56:49

1. PL and Static Analysis

程序语言和静态分析。

2. Why We Learn Static Analysis?

  • 提高程序的可靠性(空指针,内存泄漏)
  • 提高程序的安全性 (隐私泄露,注入攻击)
  • 编译优化(死代码删除)
  • 程序理解(继承关系,类型提示)

3. What is Static Analysis?

静态分析分析程序 P,通过在运行 P 之前推断其行为并确定其是否满足某些属性。

  • P 是否包含任何私人信息泄露?
  • P 是否引用任何空指针?
  • P 中的所有强制类型转换操作是否安全?
  • P 中,v1v2 是否可能指向相同的内存位置?
  • P 中的某些断言语句是否会失败?
  • P 中的这段代码是否是无效的(以便将其删除)?

不幸的是,根据赖斯定理(Rice’s Theorem),没有一种方法可以确定 P 是否满足这类非平凡属性,即,不能给出确切的答案:是或否。
在这里插入图片描述

一个Perfect的静态程序分析是即Sound又Complete的。
Sound指包含所有的问题,但可能会存在假阳的情况(误报)。
Complete指指出的问题全部是正确的,但可能会存在假阴的情况(漏报)。

有用的静态分析(妥协其中的一方):

  • Compromise soundness,变得不Sound,只包含一部分的Truth(false negative 漏报)
  • Compromise completeness,变得不Complete,会包含一部分的假bug(false positive 误报)
  • 一般上都是妥协completeness,(Sound但是不精确)虽然会造成误报(不准确),宁可多排查几个漏洞,但也不能放过一个漏洞
  • 但是soundness对于一系列重要的(静态分析)应用程序,如编译器优化和程序验证,至关重要。

我们需要在确保soundness的情况下,确保分析的精度和分析的速度。

4. Static Analysis Features and Examples

两个词来总结静态分析:
“Abstraction + Over-approximation” 在程序分析和验证领域通常指的是一种方法或技术,其中同时使用了抽象(Abstraction)和过度逼近(Over-approximation)的策略。
• Abstraction
• Over-approximation
 • Transfer functions
 • Control flows

  1. Abstraction(抽象): 抽象是一种将复杂系统简化为更易于处理的形式的技术。在程序分析中,可以通过去除细节或简化计算来创建抽象模型,使得问题变得更易解决。这有助于降低分析的复杂性,但可能会损失一些精确性。
  2. Over-approximation(过度逼近): 过度逼近是一种保守的分析方法,它倾向于报告可能的属性而不是确切的属性。这种方法的目标是确保不会漏掉任何可能导致问题的情况,即使这可能导致一些误报。通过过度逼近,可以更容易地检测到潜在的错误或问题。

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

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

相关文章

【Web】SCU新生赛个人wp及完赛感想

目录 一些碎碎念: Web Guideline 2048 ezupload hardupload ezphp ezweb ezsql webbuilder tarit tarit_revenge VipDinner simplespi 一些碎碎念: scu新生赛是我全心全力打的第二场比赛,历时七天,期间不免煎熬&…

Fabric链码部署-go语言

最近在搞Fabric,今天刚刚明白如何把自己的链码部署并能跑通 网上的中文教程完全不友好,上来直接开始写代码,我连新建什么文件夹都不知道啊!! 于是痛定思痛,爆肝了一周多的官方文档 准备自己写一个&#…

调用别人提供的接口无法通过try catch捕获异常(C#),见鬼了

前几天做CA签名这个需求时发现一个很诡异的事情,CA签名调用的接口是由另外一个开发部门的同事(比较难沟通的那种人)封装并提供到我们这边的。我们这边只需要把数据准备好,然后调他封装的接口即可完成签名操作。但在测试过程中,发现他提供的接…

用23种设计模式打造一个cocos creator的游戏框架----(五)工厂方法模式

1、模式标准 模式名称:工厂方法模式 模式分类:创建型 模式意图:定义一个用于创建对象的接口,让子类决定实例化哪一个类。工厂方法使一个类的实例化延迟到其子类。 结构图: 适用于: 1、当一个类不知道它…

探索开源游戏的乐趣与无限可能 | 开源专题 No.47

CleverRaven/Cataclysm-DDA Stars: 9.0k License: NOASSERTION Cataclysm:Dark Days Ahead 是一个回合制的生存游戏,设定在一个后启示录世界中。尽管有些人将其描述为 “僵尸游戏”,但 Cataclysm 远不止于此。在这个残酷、持久、程序生成的世…

RocketMq集成SpringBoot(待完善)

环境 jdk1.8, springboot2.7.3 Maven依赖 <parent><groupId>org.springframework.boot</groupId><artifactId>spring-boot-starter-parent</artifactId><version>2.7.3</version><relativePath/> <!-- lookup parent from…

Sprint Boot 3.0

1. 简介 视频教程特点&#xff1a; Spring Cloud带动了Spring BootSpring Boot成就了Spring Cloud

彻底解决org.gradle.api.artifacts.DependencySubstitutions

需求背景 最近在使用android studio导入hbuilder的HBuilder-Integrate-AS工程时候报错&#xff0c;错误消息如下两种。 错误描述 第一种 Failed to notify dependency resolution listener. void org.gradle.api.artifacts.DependencySubstitutions$Substitution.with(org.g…

【工具使用-JFlash】如何使用Jflash擦除和读取MCU内部指定扇区的数据

一&#xff0c;简介 在调试的过程中&#xff0c;特别是在调试向MCU内部flash写数据的时候&#xff0c;我们常常要擦除数据区的内容&#xff0c;而不想擦除程序取。那这种情况就需要擦除指定的扇区数据即可。本文介绍一种方法&#xff0c;可以擦除MCU内部Flash中指定扇区的数据…

【数据库】简单连接嵌套查询

目录 &#x1f387;简单查询 &#x1f387;连接查询 &#x1f387;嵌套查询 分析&思考 &#x1f387;简单查询 --练习简单查询 --select * from classes --select * from student --select * from scores --1.按Schedule表的结构要求用SQL语言创建Schedule表 --字段名…

linux 应用开发笔记---【标准I/O库/文件属性及目录】

一&#xff0c;什么是标准I/O库 标准c库当中用于文件I/O操作相关的一套库函数&#xff0c;实用标准I/O需要包含头文件 二&#xff0c;文件I/O和标准I/O之间的区别 1.标准I/O是库函数&#xff0c;而文件I/O是系统调用 2.标准I/O是对文件I/O的封装 3.标准I/O相对于文件I/O具有更…

基于ssm校园活动管理平台论文

摘 要 使用旧方法对校园活动信息进行系统化管理已经不再让人们信赖了&#xff0c;把现在的网络信息技术运用在校园活动信息的管理上面可以解决许多信息管理上面的难题&#xff0c;比如处理数据时间很长&#xff0c;数据存在错误不能及时纠正等问题。 这次开发的校园活动管理平…

2024年网络安全竞赛-Web安全应用

Web安全应用 (一)拓扑图 任务环境说明: 1.获取PHP的版本号作为Flag值提交;(例如:5.2.14) 2.获取MySQL数据库的版本号作为Flag值提交;(例如:5.0.22) 3.获取系统的内核版本号作为Flag值提交;(例如:2.6.18) 4.获取网站后台管理员admin用户的密码作为Flag值提交…

【Linux】探索Linux进程状态 | 僵尸进程 | 孤儿进程

最近&#xff0c;我发现了一个超级强大的人工智能学习网站。它以通俗易懂的方式呈现复杂的概念&#xff0c;而且内容风趣幽默。我觉得它对大家可能会有所帮助&#xff0c;所以我在此分享。点击这里跳转到网站。 目录 一、进程状态1.1运行状态1.2阻塞状态1.3挂起状态 二、具体L…

C++ queue 和priority_queue

目录 1.什么是queue 2.模拟实现 3.仿函数 模板参数Compare 仿函数 4.什么是priority_queue 模拟实现 1.什么是queue 1.队列是一种容器适配器&#xff0c;专门用于在FIFO上下文(先进先出)中操作&#xff0c;其中从容器一端插入元素&#xff0c;另一端提取元素。 2.队列作为…

【数据结构】——排序篇(中)

前面我们已经了解了几大排序了&#xff0c;那么我们今天就来再了解一下剩下的快速排序法&#xff0c;这是一种非常经典的方法&#xff0c;时间复杂度是N*logN。 快速排序法&#xff1a; 基本思想为&#xff1a;任取待排序元素序列中的某元素作为基准值&#xff0c;按照该排序码…

医疗大模型产品收集

在之前的一篇文章【LLM大模型中文开源数据集集锦&#xff08;三&#xff09;】采集到了一些医疗大模型所使用的数据&#xff0c;数据中比较多的是竞赛中出现训练集&#xff0c;对话语料居多。 大模型也出现好一阵子&#xff0c;一些医疗大模型产品化、开源模型也越来越多&#…

Proteus仿真--基于51单片机的EPROM2764仿真设计

本文介绍基于51单片机的EPROM2764仿真设计&#xff08;完整仿真源文件及代码见文末链接&#xff09; 开机时&#xff0c;将写在EPROM中的图像显示在LCD上 仿真图如下 仿真运行视频 Proteus仿真--基于51单片机的EPROM2764仿真设计 附完整Proteus仿真资料代码资料 链接&#x…

PID控制参数整定(调节方法)原理+图示+MATLAB调试

PID控制参数整定&#xff08;调节方法&#xff09;原理图示MATLAB调试 Chapter1 PID控制参数整定&#xff08;调节方法&#xff09;原理图示MATLAB调试序一、P参数选取二、I的调节三、D的调节四、总结 Chapter2 PID参数调整&#xff0c;个人经验&#xff08;配输出曲线图&#…

Python基础(四、探索迷宫游戏)

Python基础&#xff08;四、探索迷宫游戏&#xff09; 游戏介绍游戏说明 游戏介绍 在这个游戏中&#xff0c;你将扮演一个勇敢的冒险者&#xff0c;进入了一个神秘的迷宫。你的任务是探索迷宫的每个房间&#xff0c;并最终找到隐藏在其中的宝藏。 游戏通过命令行界面进行交互…