自定义博客皮肤VIP专享

*博客头图:

格式为PNG、JPG,宽度*高度大于1920*100像素,不超过2MB,主视觉建议放在右侧,请参照线上博客头图

请上传大于1920*100像素的图片!

博客底图:

图片格式为PNG、JPG,不超过1MB,可上下左右平铺至整个背景

栏目图:

图片格式为PNG、JPG,图片宽度*高度为300*38像素,不超过0.5MB

主标题颜色:

RGB颜色,例如:#AFAFAF

Hover:

RGB颜色,例如:#AFAFAF

副标题颜色:

RGB颜色,例如:#AFAFAF

自定义博客皮肤

-+

Canliture

hello, 程序分析! 微信交流:trustxyz

  • 博客(121)
  • 收藏
  • 关注

原创 SVF——C/C++指针分析/(数据)依赖分析框架

这篇文章包括:SVF介绍,SVF源码解读,SVF优势与不足,如何扩展改进

2023-08-21 10:23:46 1758 2

原创 Clion调试C/C++代码——问题与解决方法

Debugger之前是Bundled LLDB(Clion自带的LLDB),现在切换成Bundled GDB就OK了。在Clion调试的时候,发现打断点开始Debug运行的时候,只能进入汇编代码进行调试,不能调试源代码。功能,输入变量进去回车,结果显示不了具体的字符串值,只显示类型信息。调试的时候想看std::string变量的值,于是使用Clion的。我的调试器工具链配置的是LLDB,换成GDB就行了。后续遇到问题再更新。

2023-08-17 09:51:05 2219 1

原创 CLion开发,编译,配置LLVM,SVF,Z3

LLVM,Z3都安装好后,我的SVF版本是2.6,打开CLion就可以直接跑了。如果SVF找不到Z3,可以设置一下CMake变量,例如。解压后再创建一个目录叫做z3-build。构建类型:RelWithDebInfo。

2023-07-07 16:44:32 693

原创 How to review a paper?

How to review a paper?

2023-02-07 15:31:08 290 2

原创 CGO‘11-Flow-Sensitive Pointer Analysis for Millions of Lines of Code-百万行规模的流敏感稀疏指针分析

这篇文章发表在2011的CGO上, 该文章提出的技术是利用`两阶段分析`完成对百万行代码的`流敏感`指针分析技术。

2022-12-28 17:34:10 449 2

原创 PLDI‘21-Path-Sensitive Sparse Analysis without Path Conditions-基于程序依赖图的路径敏感稀疏分析

这篇文章是港科大团队在PLDI 2021会议上发表的文章。在这之前,作者在PLDI 2018发表Pinpoint。这篇文章在Pinpoint上改进。在Pinpoint的设计中,存储摘要的时候仍然需要`缓存大量的路径条件`,以及在应用摘要时进行`大量的克隆`,导致逻辑公式大小进行指数级的增长。而在PLDI 2021中,作者进一步提出,我们可以不用构建Value Flow Graph了!直接在程序依赖图(Program Dependence Graph)上就可以达到相同的路径敏感检测效果。

2022-12-28 17:25:34 746 1

原创 2010‘FSE-Practical and Effective Symbolic Analysis for Buffer Overflow Detection 利用符号分析方法检测缓冲区溢出

作者在本文提出一个新的利用符号分析来检测缓冲区溢出的方法,该方法是路径敏感的,能够处理循环等复杂特性。该方法能够在11分钟内分析860万行代码,误报率低于10%。

2022-12-28 17:17:31 227

原创 FSE‘03-ARCHER: Using Symbolic, Path-sensitive Analysis to Detect Memory Access Errors-路径敏感缓冲区溢出检测

这次读一读FSE‘03上发表的检查内存越界的paper。它是`路径敏感`的,同时能够分析`百万行`规模的代码。作者分析了几个大的开源项目如OpenBSD, SendEmail, PostgreSQL, Linux内核,平均误报率低于35%。

2022-12-28 17:09:50 135

原创 ICSE‘08 - Calysto: Scalable and Precise Extended Static Checking - 路径敏感bug-finding工具Calysto

这篇文章要讨论的是2008年在ICSE会议上发表的静态分析工具论文: `Calysto`。这个bug-finding工具有比较好的精度的同时,又能检测比较大规模的代码。

2022-12-28 17:05:05 202

原创 ICSE‘22 Precise Divide-By-Zero Detection with Affirmative Evidence 数值除零bug检测

今天要讨论的是ICSE'22, 它利用VFG进行数值程序分析,检测程序中可能出现的除零bug。

2022-12-28 16:59:01 484

原创 TOPLAS‘07: Effective Field-Sensitive Pointer Analysis for C 字段敏感C程序指针分析

本文介绍介绍另一篇Andersen式指针分析,作者提出的方法是字段敏感的。

2022-12-28 16:43:25 558

原创 PLDI‘02 ESP: Path-Sensitive Program Verification in Polynomial Time - 路径敏感分析ESP: Property Simulation

这篇文章发表在PLDI'02, 作者的相关工作分析了1.4 millions LOC (微软word 97)。ESP同时也借鉴了Metal Checking System (Coverity) 一些想法

2022-12-28 16:27:20 231

原创 中断并发程序的静态分析

最近得研究下多任务并发程序的静态分析(包括中断),于是看了这篇文章;这篇文章是国防科大的团队在15年,16年所做的工作;主要是分析中断导致的程序并发,方法是:“将程序顺序化,然后重用经典的抽象解释方法进行分析;当然,还设计了抽象域专门处理IDPs的特性”

2022-04-09 13:50:03 809

原创 检测并发程序Bug:[PLDI2021] Canary: Practical Static Detection of Inter-thread Value-Flow Bugs

最近得研究下多任务并发程序的静态分析,于是看了这篇文章总体来说,看是看懂了,但是… … 这篇文章所做的工作有点多啊… 怕了怕了1. Canary: Practical Static Detection of Inter-thread Value-Flow Bugs这篇文章发表在PLDI 2021,并发Bug缺陷检查。首次将并发bug检测转化为source-sink可达性问题,有效减低冗余的线程交错处理。提出值流图上的thread-modular算法来捕获数据和干扰(interference.

2022-04-05 17:46:07 645 2

原创 利用OCaml实现一些数据结构和算法

利用OCaml实现常见数据结构和算法

2022-03-01 23:46:09 1230

原创 OCaml简单记录

OCaml utop 清屏;有时候使用交互式解释器utop,有强迫症,想清屏;那就用如下命令, 最好用CTRL + Lutop # Sys.command "clear";;很显然就是调用了clear命令; 例如:utop # Sys.command "cal";; 二月 2022 日 一 二 三 四 五 六 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22.

2022-02-27 14:54:01 470

原创 OCaml安装

这里记录有关OCaml。Real world OCaml V2(2021.Q4)安装配置相关 http://dev.realworldocaml.org/install.html

2022-02-23 22:10:03 1239

原创 计算机/科技/人文 相关书籍

这里记录一些正在看,或者觉得一些很有意思,很想看的书。最近看的C/C++语言相关的书,在有一些编译相关的知识后看的,非常适合我目前这个阶段去读:C语言参考手册写/学习 C/C++编译器前端必备。对于了解C语言的语法结构,绝对是没有其它书可以替代。C++程序设计语言(特别版)神书,果然C++之父写的书确实有点哲学。我从没看过有一本教编程语言的书,会在Expression/Statements章节以一个词法/语法解析器作为Introduction在有一些编译知识作为背景,更能理解作者在表达

2022-02-20 23:13:44 536 2

原创 南京大学《软件分析》课程课后作业(非Bamboo)

南京大学软件分析课程作业参考实现,非官方代码。https://github.com/canliture/nju-software-analysis-homework欢迎提bug/star/pr文档docs/org为南大课程的作业原题pdfdocs/soot为soot参考资料src/main/java/com/canliture/soot/每个子目录下的作业都有一个README,作为作业的简单说明代码com.canliture.soot.ass1第一次作业的代码实现常量传播c

2021-10-09 23:06:32 1967 2

原创 IFDS论文算法精解:应用于污点分析的例子

这里以一个污点分析的例子来说明IFDS论文中的Tabulation算法(IFDS Solver求解器)是怎么工作的。1. 这里给定两个函数,它们之间有一条从source到sink的污染路径2. 最终的有效的污点传播相关的边如下所示;其中红色边对应于FlowFunction,也叫TransferFunction或者TransferRelation等术语。表示数据流经过一条语句后的流向。绿色边PathEdge为论文中描述的PathEdge,蓝色SummaryEdge为摘要边,避免重复计算。3. 整

2021-09-23 20:20:42 2977 1

原创 C++字符串

C的字符串以及它的弱点C风格字符串被定义为以null字符结尾的字符数组字符串字面量为const char*类型,所以下面赋值得到的数组是只读的char arr[10];char str[2] = "12";char* s = "hello";另外,str不能被赋值,而s能。前者不是左值。<string.h> 中定义了c字符串常用函数。c字符串的弱点是,不够现代,操作繁琐,语义不够清晰,容易出bug。// 下面是实现将两个字符串连接并赋值给第3个字符串// 1. C++

2021-08-08 11:25:48 148

原创 C++一些关键的概念

C++创建对象:User u(... );把u本身当作一个对象User *p = new User(...);构造函数调用会创建一小块内存区域,用于存储p的值(一个内存地址),然后填充一块较大的区域,赋值符右侧所创建的User对象就存储在这块内存中。p所指向的内存地址就是User对象的存储位置u: --- --- | | | | | | | | | | --- --- p: -------

2021-08-08 02:45:27 274 1

原创 IFDS开山之作:Precise Interprocedual Dataflow Analysis via Graph Reachability

《Precise Interprocedual Dataflow Analysis via Graph Reachability》一大类的流程间数据流问题,通过将其转化为一种特殊的图可达性问题,能够在多项式时间复杂度内被精确求解。对于这类数据流问题的唯一约束就是:数据流事实必须是有限集,数据流转换函数必须在交汇操作(Union或Intersection)上是可分配的。这类数据流问题包括但不限于经典的seperable problems(也叫gen/kill,bit-vector),比如reachi.

2021-08-05 22:15:09 2657 6

原创 程序分析论文导航(Todo-List)

这里记录一些论文,我需要看的,或者一些已经看过的(虽然我看过的很少 - _ - )也可以算是todo-list吧最初是想着有时候需要看些论文,倒不是奔着学术方向走,只是有时候对这个挺感兴趣hhh;然后去网上down下来论文,有时看着看着就忘记论文的事了。这里把它记下来,算是不那么容易忘记了。这些应该算是入门吧 ??? 虽然我还没入门 … 后续打算看完一篇论文写一篇博客,记录一下学习过程。1995, IFDS开山之作:Precise Interprocedural Dataflflow An.

2021-08-05 00:01:16 601 3

原创 FlowDroid架构剖析

最近算是把FlowDroid源代码翻了一遍,并非通读,而是把整个系统的逻辑/设计整理了一下。这里稍微记录一下。由于FlowDroid能够分析Android程序,所以有一部分代码是对Android相关领域做适配,由于个人目前的工作对Android静态分析还不是很涉及,所以在分析FlowDroid源码时省略了Android相关的适配代码,主要是作通用Java相关的分析。FlowDroid几大组件:EntryPointCreator:使用EntryPointCreator指定分析的入口SourceS.

2021-08-02 21:51:07 1688 3

原创 控制流的支配者关系分析以及Soot中的实现

由于仍然有些概念不是很清晰,这里仅当学习记录。1. 支配关系我们说d dom i,节点d支配节点i,如果从entry到节点i的所有可能执行路径都包含d。所以dom关系是自反的,传递的,反对称的自反性:a dom a,每个节点都支配它自己传递性:a dom b, b dom c, 则a dom c反对称性:a dom b, b dom a, 则a与b相等根据自反偏序集的定义,dom关系是自反偏序(简称偏序)的。那么我们可以用Hasse图(哈塞图)表示支配关系,也叫支配树。2. 立即支配.

2021-07-26 00:35:52 746 1

原创 数据流分析的证明:安全性,终止性和合流性(收敛性)

数据流分析的证明:安全性,终止性和合流性(收敛性)大量的程序属性相关的问题无法在静态分析时进行确定,所以静态分析很多时候得不到精确的结果。于是我们常常采用近似法:允许在得不到精确值的时候,给出不精确的答案。而对于判定性问题,不精确的答案就是Unkonwn。求解近似解的基本方法中,其中一个,也是最基本的一个,就是对问题进行抽象。而对于软件分析中的数据流分析,常见的近似抽象方案就是对程序做抽象,引入两个近似方案。近似方案1:忽略程序的条件判断,认为所有分支都可能到达。(当然,对于静态分析就能够检测并

2021-05-17 00:36:38 452 1

原创 偏序与格理论 基础

格理论学习笔记大一上学期学离散数学,不懂什么是数学结构,数据结构。也不知道学的离散数学到底有什么用,用在什么地方。后来知道,数据结构课程中的各种数据结构都可以用离散数学中的数学定义来解释,使得这些数据结构有相对严格的数学基础。现在工作用用到了很多离散数学的知识,得慢慢学习,将以前学习的知识补回来。所以在工作中实际上有必要重新温故或者重新学一遍。跟工作实践相结合。相信能够对这些计算机基础有更深的理解,最重要的是,帮助理解工作中要用到的一些核心概念。哦,对。现代数学的基础就是集合论。偏序与格理论的

2021-05-10 23:07:55 891 1

原创 程序分析技术栈-测试/辅助证明/模型检验/保守静态分析/bug-finding

做静态Bug查找工具/漏洞检查器等等,需要静态分析的知识,而静态分析从大的技术门类来讲可置身软件工程基础技术:程序分析技术大类。这里先概述日常工作中接触比较多的静态分析技术(如IDE的代码补全,定义跳转等等),然后再站在高层地视角将静态分析技术置身于程序分析这一软件工程基础领域,让我们清楚地知道静态分析在软件基础技术中的作用域/适用范围及其特点/局限性。静态程序分析(简称静态分析),主要是在不运行程序的情况下,找到程序的语义属性。它最初在70年代在编译优化技术中引入,用于生成高效的机器码。随着对静态分.

2021-05-04 15:29:43 982 1

原创 LLVM IR / LLVM指令集入门

本文基于LLVM 12官方文档的LLVM Language Reference Manual。以学习笔记为主。所以本文会摘录一些常见/常用的指令。对于一些更加深层次的指令属性/特性,待我对LLVM有更深的理解再单独写文章记录。1. LLVM IR简介LLVM IR可以理解为LLVM平台的汇编语言,所以官方也是以语言参考手册(Language Reference Manual)的形式给出LLVM IR的文档说明。既然是汇编语言,那么就和传统的CUP类似,有特定的汇编指令集。但是它又与传统的特定平台相关.

2021-03-28 02:25:03 6943 1

原创 Bit-Vector框架(2) — Live Variables Analysis

Bit-Vector框架(2) — Live Variables Analysis#mermaid-svg-h2LkkNRYSfHXahhI .label{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);fill:#333;color:#333}#mermaid-svg-h2LkkNRYSfHXahhI .label text{fill:#333}#mermaid-svg-h2LkkNRYS

2021-01-29 15:52:30 283 1

原创 Bit-Vector框架(1) — Reaching Definition Analysis

Bit-Vector框架(1)——Reaching Definition Analysis#mermaid-svg-333SwcHNBd1lX6bv .label{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);fill:#333;color:#333}#mermaid-svg-333SwcHNBd1lX6bv .label text{fill:#333}#mermaid-svg-333Sw

2021-01-25 21:23:05 348 2

原创 《程序分析:开胃菜》概览

#mermaid-svg-IRcss6oDC5GngJjh .label{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);fill:#333;color:#333}#mermaid-svg-IRcss6oDC5GngJjh .label text{fill:#333}#mermaid-svg-IRcss6oDC5GngJjh .node rect,#mermaid-svg-IRcss6oDC5

2021-01-25 21:12:28 225 1

原创 Java正则表达式提取特定html标签内的内容

如题:使用正则表达式,怎么匹配特定html标签内的内容。比如,对于如下文本串:... ignored contentprefix content <html>inner content</html>postfix content... ignored content我们要提取出<html>标签内的内容: inner content(这里的html标签可以换成任何其它的标签,比如<p>标签)这里引入正则表达式的group概念:详细点击文章查看

2020-08-31 16:19:50 5536 5

原创 选课表SQL问题引发的小困惑

遇到一个SQL问题,突然有点蒙蔽,想想很简单,但是却突然卡壳。-- 有一个选课记录,其中-- student_id表示选课记录的学生id-- cource_id表示选课记录的课程idcreate table course_select( id int(11) NOT NULL auto_increment PRIMARY KEY, student_id varchar(20), ...

2020-02-21 11:16:54 239 1

原创 IDEA + maven打包程序成为jar包

IDEA下打包程序成为jar包

2019-12-12 20:44:59 162

原创 jdom dom4j解析阻塞,报错

在解析mybatis的mapper.xml文件时,发现saxBuilder.build函数发生·阻塞·的情况,更加严重的情况会出现下图所示的错误,也就是Connection time out经研究,对错误发生的位置的调用栈debug,最终终于发现了如下的问题:也就是说,在最底层的连接超时是因为连接不上mybatis.org,也就是说,连接mybatis.org网站超时;然后自己在浏览器中...

2019-12-10 17:33:47 337

原创 System.getenv(String)获取不到环境变量

如题,我在Windows上设置了环境变量,在Java中获取,总是获取不到。解决方法:简单粗暴 - 重启。

2019-12-07 09:38:40 4275

原创 认真读文档!

认真读文档!认真读文档!认真读文档!血的教训....// ignored some codes ...Map options = JavaCore.getOptions();JavaCore.setComplianceOptions(JavaCore.VERSION_1_5, options);parser.setCompilerOptions(options);Which ...

2019-12-04 10:51:29 168

原创 extended operands——递归数据结构的一种处理方式

AST中有关extended operands最近遇到Java语言的AST中,eclipse对于中缀表达式InfixExpression的AST一个解析后的表示方式:下面是org.eclipse.jdt.core.dom.InfixExpression#extendedOperands方法的注释:/*** Returns the live list of extended operands...

2019-11-28 18:56:59 155

空空如也

空空如也

TA创建的收藏夹 TA关注的收藏夹

TA关注的人

提示
确定要删除当前文章?
取消 删除