当前位置:网站首页>[Nanjing University] - [software analysis] course learning notes (I) -introduction
[Nanjing University] - [software analysis] course learning notes (I) -introduction
2022-07-07 08:42:00 【Xihang】
List of articles
Nanjing University Static program analysis
introduction
1. program language and static analysis
programing language :
- theory
- Language design
- Type system
- Semantics and logic
- …
- Environmental Science
- compiler
- Runtime system
- …
- application
- Program analysis
- Program validation
- Program synthesis
- …
background : In the past decade , The core of language is basically unchanged , But the program has become significantly larger and more complex ;
Challenge : How to ensure the reliability of large-scale and complex programs 、 Security and other commitments
2. why we learn static analysis
The reliability of the program reliability:
- null pointer dereference Null pointer reference
- There is no reference define, Will bring a lot bug
- memory leak Memory leak
- malloc No, free, Too much memory will lead to crash
The security of the program security:
- private information leak Disclosure of private information
- injection attack Injection attack
Compiler optimization
- dead code elimination Dead code elimination
- code motion Code movement
Program understanding
- IDE call hierarchy Call level
- type indication Type indication
3. what is static analysis
Static analysis analyzes a program P to reason about its behaviors and determines whether it satisfies some properties before running P.
Static analysis through the analysis program P To infer its behavior , And running P Before determining whether it meets certain properties
- Does P contain any private information leaks?
- Does P dereference any null potinters?
- Are all the cast operations in P safe? Type conversion operators
- Can v1 and v2 in P point to the same memory location?
- Will certain assert statements in P fail?
- Is this piece of code in P dead(so that it could be eliminated)?
Rice theory Rice theorem : There is no way to determine whether a program satisfies some nontrivial properties .
Any non-trivial property of the behavior of programs in a r.e. language is undecidable
r.e. (recursively enumerable) = recognizable by a Turing-machine
Recursively enumerable languages are languages recognized by Turing machines
non-trivial Not simple , important
The above expression is a perfect static analysis It doesn't exist
From an academic point of view , One perfect Of static analysis There are two conditions that need to be met :
- sound:over approximate contain true
- complete: under approximate true contain
So we don't pursue perfect static analysis , It's about pursuing useful static analysis:
- Compromise soundness(false negatives) Compromise under reporting control
- Compromise completeness (false positives) Compromise false alarm control
Mostly compromising completeness: Sound but not fully-precise static analysis
Most static analysis pursues Soundness, It will cause false positives
Soundness is critical to a collection of important(static-analysis) applications such as compiler optimization and program verification.
Static analysis: ensure (or get close to) soundness, while making good trade-offs between analysis precision and analysis speed.
Make sure soundness, And make a trade-off between analysis accuracy and analysis speed
4. static analysis features and examples
Abstraction + Over-approximation
Abstract and over approximate
- abstraction
- over-approximation
- transfer function
- control flows
Example:
Determine the symbols of all variables in a given program : just 、 Negative or 0.
- T:unknow Positive but negative (over-approximation Over approximate )
- bottom:undefined, Divide by zero operation , Throw exception operation
transfer function It defines how to evaluate different program states on abstract values , And it should be defined according to the semantics of analysis problems and different program states
- 1 The problem is divide by zero 、 Throw an exception , It should be undefined;
- 2 The problem is that the subscript is negative , Throw an exception , It should also be for undefined
- 3 The problem is over-approximated, That is, false positives , In the actual procedure a=x+y=9, So it won't report an error , This boundary will be blurred in the process of abstracting into symbols , Cause false positives
Control flow analysis ,y The two values of are two branch, Taking different branches will make z Change the value of . And it is impossible to enumerate all paths in practice , The space is huge , therefore flow merging Is used by many static analysis .
边栏推荐
- Input and output of floating point data (C language)
- Practice of combining rook CEPH and rainbow, a cloud native storage solution
- 南京商品房买卖启用电子合同,君子签助力房屋交易在线网签备案
- Thirteen forms of lambda in kotlin
- Opencv learning notes II - basic image operations
- 数据中台落地实施之法
- 数据分析方法论与前人经验总结2【笔记干货】
- 調用華為遊戲多媒體服務的創建引擎接口返回錯誤碼1002,錯誤信息:the params is error
- Opencv learning note 3 - image smoothing / denoising
- [Chongqing Guangdong education] organic electronics (Bilingual) reference materials of Nanjing University of Posts and Telecommunications
猜你喜欢
Data type - integer (C language)
Virtual address space
[paper reading] icml2020: can autonomous vehicles identify, recover from, and adapt to distribution shifts?
What is the method of manual wiring in PCB design in 22protel DXP_ Chengdu electromechanical Development Undertaking
Obsidan之数学公式的输入
[Yu Yue education] higher vocational English reference materials of Nanjing Polytechnic University
Through the "last mile" of legal services for the masses, fangzheng Puhua labor and personnel law self-service consulting service platform has been frequently "praised"
路由信息协议——RIP
【踩坑】nacos注册一直连接localhost:8848,no available server
Greenplum6.x常用语句
随机推荐
A single game with goods increased by 100000, and the rural anchor sold men's clothes on top of the list?
AVL balanced binary search tree
Golang 编译约束/条件编译 ( // +build <tags> )
Qt Charts使用(重写QChartView,实现一些自定义功能)
oracle一次性说清楚,多种分隔符的一个字段拆分多行,再多行多列多种分隔符拆多行,最终处理超亿亿。。亿级别数据量
uniapp 微信小程序监测网络
Input of mathematical formula of obsidan
What are the advantages of commas in conditional statements- What is the advantage of commas in a conditional statement?
登山小分队(dfs)
Opencv learning note 3 - image smoothing / denoising
You should use Google related products with caution
opencv 将16位图像数据转为8位、8转16
Through the "last mile" of legal services for the masses, fangzheng Puhua labor and personnel law self-service consulting service platform has been frequently "praised"
AVL平衡二叉搜索树
Iptables' state module (FTP service exercise)
单场带货涨粉10万,农村主播竟将男装卖爆单?
2-3 lookup tree
MES系統,是企業生產的必要選擇
Other 7 features of TCP [sliding window mechanism ▲]
Rainbow 5.7.1 supports docking with multiple public clouds and clusters for abnormal alarms