分类

类型:
不限 游戏开发 计算机程序开发 Android开发 网站开发 笔记总结 其他
评分:
不限 10 9 8 7 6 5 4 3 2 1
原创:
不限
年份:
不限 2018 2019 2020 2021

技术文章列表

  • 【课程笔记】南大软件分析课程9——污点分析


    最近在看“静态分析”技术相关的文章,看到这个系列的笔记和视频教程,感觉介绍得很好,通俗易懂,而且还比较详细,故转载分享,同时也备份保留下,方便自己今后阅读。(PS:建议大家一边看笔记,一边看视频,加深理解)原作者:bsauce原文链接:https://www.jianshu.com/p/f43218636968

    首先非常感谢南京大学李樾和谭添老师的无私分享,之前学习程序分析是看的北大熊英飞老师的ppt,但是很多地方没看懂,正如李樾老师所说的那样,熊英飞老师的授课涵盖非常广,不听课只看ppt的话,理解起来还是很有难度的。但李樾老师的视频就讲解的非常易懂,示例都是精心挑选的,所以墙裂推荐。
    推送门:南大课件 南大视频课程 北大课件

    目录
    信息流安全保密性和完整性显示流和隐藏信道-Explicit Flows and Covert Channels污点分析
    重点显示流和隐藏信道,使用污点分析来检测信息流漏洞。
    1.信息流安全访问控制:关注信息访问。
    信息流安全:关注信息传播。
    信息流:x->y表示x的值流向y。
    信息等级:对不同变量进行分级,即安全等级,H-高密级,L-低密级。
    安全策略:非干涉策略,高密级变量H的信息不能影响(流向)低密级变量L。
    2.保密性和完整性保密性—信息泄露,读保护;完整性—信息篡改,写保护。
    完整性错误类型:命令注入、SQL注入、XSS攻击、… 。都属于注入错误。
    完整性更宽泛的定义:准确性、完整性、一致性。准确性表示关键数据不被不可信数据破坏;完整性表示系统存储了所有的数据;一致性表示发送的数据和接收的数据是一致的。
    3.显示流和隐藏信道-Explicit Flows and Covert Channels显示流:直接的数值传递。由于显示流能泄露更多信息,所以本课程关注显示流的信息泄露。
    隐式信息流—侧信道:程序可能会以一些意想不到的方式泄露数据。
    // Eg1 隐式流if (secret_H < 0) public_L = 1; else Public_L = 0;// Eg2 终止信道while(secret_H < 0) { ... };// Eg3 时间信道if (secret_H < 0) for (int i = 0; i< 1000000; ++i) { ... };// Eg4 异常if (secret_H < 0) throw new Exception("...");// Eg5 如果访问数组越界,则可以推断secret可以为负数int sa_H[] = getSecretArray();sa_H[secret_H] = 0;
    covert channels:信道指的是传递信息的机制,原本目的不是为了传递信息的信道。
    4.污点分析说明:使用最广的信息流分析技术,需将程序数据分为两类,把感兴趣的数据标记为污点数据。
    (1)概念Sources & Sink:Sources是污点数据的源,一般是有些函数的返回值,如read();Sink是特定的程序点,某些敏感函数。
    保密性:Source是秘密数据,sink是泄露点,信息泄露漏洞。
    x = getPassword(); // source y = x;log(y); // sink
    完整性:Source是不可信数据,Sink是关键计算,注入漏洞。
    x = readInput(); // source cmd = "..." + x; execute(cmd); // sink
    (2)污点分析定义:关注的是,污点数据是否能流向sink点。或者说,sink点处的指针指向哪些污点数据。
    TA/PTA对比:污点分析与指针分析,一个是污点数据的流向,一个是抽象对象的流向。可把污点数据看作是对象,source看作allocation-site,借助指针分析来实现污点分析。
    标记:tit_it​i​​表示调用点i返回的污点数据,指针集就包含普通对象 + 污点数据。

    输入:source(返回污点数据的函数),sink(违反安全规则的函数)
    输出:TaintFlows—<tit_it​i​​, m>,表示tit_it​i​​这个污点数据会流向m函数,污点数据和sink函数这个pair的集合就是TaintFlows。
    规则:主要规则不变,关键是Sources和Sink调用的处理。

    Sources:对于产生污点源的函数调用m,将返回值标记为污点值tlt_lt​l​​,并更新接收变量r的指向。
    Sink:对于Sink函数调用m,若所传参数的指向集包含污点tjt_jt​j​​,则将<tj,m><t_j, m><t​j​​,m>加入TaintFlows。



    示例:第3行产生新对象o11o_{11}o​11​​的同时,产生的污点数据t3t_3t​3​​;最终指针分析发现,t3t_3t​3​​会流向sink函数log()。

    问答:实现分析器用到:分析Java用Soot/WALA;分析C++用LLVM;有的用Datalog实现分析器(如DOOP分析框架)。
    隐藏信道的论文:Implicit Flows: Can’t Live With ‘Em, Can’t Live Without ‘Em
    LLVM指针分析工具:SVF
    0 留言 2020-07-21 14:23:35 奖励30点积分
  • 【课程笔记】南大软件分析课程8——指针分析-上下文敏感


    最近在看“静态分析”技术相关的文章,看到这个系列的笔记和视频教程,感觉介绍得很好,通俗易懂,而且还比较详细,故转载分享,同时也备份保留下,方便自己今后阅读。(PS:建议大家一边看笔记,一边看视频,加深理解)原作者:bsauce原文链接:https://www.jianshu.com/p/5ab79839f686

    首先非常感谢南京大学李樾和谭添老师的无私分享,之前学习程序分析是看的北大熊英飞老师的ppt,但是很多地方没看懂,正如李樾老师所说的那样,熊英飞老师的授课涵盖非常广,不听课只看ppt的话,理解起来还是很有难度的。但李樾老师的视频就讲解的非常易懂,示例都是精心挑选的,所以墙裂推荐。
    推送门:南大课件 南大视频课程 北大课件

    目录
    介绍Context Sensitive Pointer Analysis:RulesContext Sensitive Pointer Analysis:AlgorithmsContext Sensitivity Variants—上下文的选取
    重点
    上下文敏感指针分析的完整算法(一般其他教程中很少涉及到)。上下文敏感概念,堆对象的上下文敏感表示,上下文敏感指针分析的规则。上下文的三种选择,以及效率、准确度的对比。
    1.上下文不敏感的问题说明:上下文敏感分析是对指针分析的准确性提升最有效的技术。
    (1)问题
    问题:上下文不敏感时,分析常量传播这个问题,由于没有明确调用id()的上下文,会把不同的调用混合在一起,对id函数内的变量n只有一种表示(没有对局部变量进行区分),导致n指向的对象集合增大,将i识别为非常量NAC。实际上,x.get()的值只来自于One()对象,i应该是常量1。
    解决:根据调用的上下文(主要有3种:如根据调用点所在的行数——call-site sensitivity)来区分局部变量。
    (2)上下文敏感分析概念:

    call-site sensitivity (call-string):根据调用点位置的不同来区分上下文,3:id(n1) / 4:id(n2)。
    Cloning-Based Context Sensitivity:每种上下文对应一个节点,标记调用者行数。克隆多少数据,后面会讨论。



    Context-Sensitive Heap:面向对象程序(如Java)会频繁修改堆对象,称为heap-insensitive。所以不仅要给变量加上下文,也要给堆抽象加上下文,称为heap context(本课程是基于allocate-site来进行堆抽象的)。
    堆抽象上下文示例:

    堆抽象上下文不敏感:如果不区分8 X x = new X();调用的堆抽象的上下文,导致只有1个o8.f,把两个上下文调用产生的o8.f指向集合都合并了,得出了o8.f的错误指向的结果。
    堆抽象上下文敏感:用不同的调用者来区分堆抽象,如3:o8、4:o8是不同的堆抽象。所以说,既要根据上下文的不同来区分局部变量,也要区分堆抽象,例如:3:p是给变量加上下文,3:o8是给堆抽象加上下文。
    2.Context Sensitive Pointer Analysis:Rules标记:根据调用者的行数来区分不同上下文,只要区分了函数、变量、堆对象,就能够区分实例域、上下文敏感的指针(变量+对象域)。C—上下文(暂时用调用点的行数表示),O—对象,F—对象中的域。

    规则:跟之前区别不大,只是增加了个上下文标记,注意load表示和之前有区别。

    call指令规则:

    上下文对于Dispatch(oi, k)(找目标函数)没有影响,根据oi指向和函数签名k找到目标函数。select(c, l, c’:oi, m)根据调用时的信息来给调用目标函数选择上下文(c是调用者的上下文,l是调用者的行号,c’:oi是x对象的指向集合,m是目标函数),ct表示目标函数的上下文(后面会将如何Select如何选择上下文)。c是可以累积的,一连串的调用,上下文将用一连串的行数来表示。
    传递this变量:ct:mthisc^t:m_{this}c​t​​:m​this​​是目标函数ct:mc^t:mc​t​​:m的this变量
    传递参数:ct:mpjc^t:m_{pj}c​t​​:m​pj​​是目标函数ct:mc^t:mc​t​​:m的第j个形参。
    传递返回值:ct:mretc^t:m_{ret}c​t​​:m​ret​​是目标函数ct:mc^t:mc​t​​:m的返回值


    3.Context Sensitive Pointer Analysis:Algorithms区别:和过程间指针分析相比,仍然分为两个过程,分别是构造PFG和根据PFG传递指向信息。主要区别是添加了上下文。
    PFG构造:边添加规则和之前一样,Assign、Store、Load、Call,Call需要加参数传递、返回值传递的边。

    符号:

    S:可达语句的集合(就是RM中的语句)Sm:函数m中的语句RM:可达函数的集合CG:调用图的边
    算法:被调用函数的上下文暂时用ct表示,之后会解释Select()函数。

    先处理New、Assign指令。AddReachable(c:m)只多了上下文。遍历WL,Propagate()和原来相同。处理Store、Load指令,AddEdge()只多了上下文。处理Call指令,ProcessCall(),多了一行ct=Select(c,l,c’:oi,m),在找到调用目标函数之后,需选择被调用的函数的上下文。
    4.Context Sensitivity Variants—上下文的选取上下文的选取主要采用3类:

    Call-Site SensitivityObject SensitivityType Sensitivity…
    说明:Select(c,l,c’:oi,m),c—调用者上下文,l—调用者,c’:oi—接收对象(含堆的上下文信息)。
    (1)Call-Site Sensitivity原理:又称为k-call-site sensitivity / k-CFA,不断添加调用行号。1991年Olin Shivers提出。

    Select(c,l,c’:oi,m) = (l’,…,l’’, l)

    问题:如果函数调用自身,导致无限递归,如何限制上下文长度?
    解决:k-limiting Context Abstraction。只取最后k个上下文,通常取k<=3。例如,函数的上下文通常取2,堆上下文通常取1。
    示例:采用1-Call-Site。
    interface Number { int get(); }class One implements Number { public int get() { return 1; }}class Two implements Number { public int get() { return 2; }}1 class C {2 static void main() {3 C c = new C();4 c.m();5 }67 Number id(Number n) {8 return n;9 }10 void m() {11 Number n1,n2,x,y;12 n1 = new One();13 n2 = new Two();14 x = this.id(n1);15 y = this.id(n2);16 x.get();17 }18 }



    WL
    正处理
    PFG
    指针集
    RM
    CG
    处理语句
    算法语句




    1




    {[]:C.main()}

    3
    AddReachable(mentry)—加入RM


    2
    [<[]:c, {o3}>]





    3
    AddReachable(mentry)—处理New


    3
    []
    <[]:c, {o3}>

    pt([]:c) ={o3};



    While开头,Propagate()—遍历WL更新指针


    4
    [⟨[4]:C.mthis, {o3}⟩]





    4
    ProcessCall()—this指针加入WL


    5
    [⟨[4]:C.mthis, {o3}⟩]




    {[ ]:4 → [4]:C.m()};

    ProcessCall()——函数加入CG


    6
    [⟨[4]:C.mthis, {o3}⟩,⟨[4]:n1, {o12⟩,⟨[4]:n2, {o13⟩]

    没有参数/返回值

    {[]:C.main(), [4]:C.m()}

    12,13
    ProcessCall():AddReachable(m)处理m函数中的New


    7
    [⟨[4]:n1, {o12⟩,⟨[4]:n2, {o13⟩]
    ⟨[4]:C.mthis, {o3}⟩

    pt([]:c) ={o3};pt([4]:C.mthis)={o3};



    While开头,Propagate()—遍历WL更新指针


    8
    [⟨[4]:n1, {o12⟩,⟨[4]:n2, {o13⟩]






    ProcessCall():处理m中的this调用


    9
    [⟨[4]:n1, {o12⟩,⟨[4]:n2, {o13⟩]





    14
    ProcessCall():Select(c,l,c’:oi)选择上下文ct=[14]


    10
    [⟨[4]:n1, {o12⟩,⟨[4]:n2, {o13⟩]



    {[]:C.main(), [4]:C.m(),[14]:C.id(Number)}
    {[ ]:4 → [4]:C.m();[4]:14 → [14]:C.id(Number)};

    ProcessCall():AddReachable([14]:C.id(Number))


    11
    [⟨[4]:n1, {o12⟩,⟨[4]:n2, {o13⟩]

    [4]:n1→[14]:n→[4]:x;




    ProcessCall():AddEdge()参数边/返回值边


    12
    [⟨[4]:n1, {o12⟩,⟨[4]:n2, {o13⟩]

    [4]:n1→[14]:n→[4]:x;[4]:n2→[15]:n→[4]:y;

    {[]:C.main(), [4]:C.m(),[14]:C.id(Number),[15]:C.id(Number)}
    {[ ]:4 → [4]:C.m();[4]:14 → [14]:C.id(Number),[4]:15 → [15]:C.id(Number)};
    15
    ProcessCall()同理


    13
    []
    [⟨[4]:n1, {o12⟩,⟨[4]:n2, {o13⟩]





    While开头—遍历WL更新指针


    14
    []





    16
    While开头,ProcessCall()—处理x.get()



    上下文不敏感vs上下文敏感(1-Call-Site):

    (2)Object Sensitivity原理:针对面向对象语言,用receiver object来表示上下文。对比1层的调用点敏感和对象敏感,时间和准确性上对象敏感显然更优,这是由面向对象语言的特点所确定的。

    Select(c,l,c’:oi,m) = [oj, … , ok, oi] (c’ = [oj, … , ok])

    示例:选取1-object,最终pt(x)=o3pt(x)=o_3pt(x)=o​3​​。

    对比:对比1-Call-Site和1-object上下文,在这个示例中1-object明显更准确。原因是面向对象语言的特性,多态性产生很多继承链,一层一层调用子对象,其中最关键的是receiver object,receiver object决定了调用者的根源。本例有多层调用,若采用2-Call-Site就不会出错。


    示例2:在本示例中,1-Call-Site明显更准确。因为同一个receiver object用不同参数多次调用了子函数,导致局部变量无法区分。

    结论:所以理论上,对象敏感与callsite敏感的准确度无法比较。但是对于面向对象语言,对象敏感的准确度要优于callsite敏感。
    (3)Type Sensitivity原理:牺牲精度,提高速度。基于创建点所在的类型,是基于对象敏感粗粒度的抽象,精度较低。

    Select(c,l,c’:oi,m) = [𝑡′,…,𝑡′′,InType(𝑜𝑖)] 其中𝑐′ = [𝑡′, … , 𝑡′′]


    (4)总体对比精度:object > type > call-site
    效率:type > object > call-site
    本课老师提出选择上下文的方法,对代码的特点有针对性的选择上下文方法,见A Principled Approach to Selective Context Sensitivity for Pointer Analysis。厉害了!
    0 留言 2020-07-19 16:50:53 奖励30点积分
  • 【课程笔记】南大软件分析课程7——指针分析基础


    最近在看“静态分析”技术相关的文章,看到这个系列的笔记和视频教程,感觉介绍得很好,通俗易懂,而且还比较详细,故转载分享,同时也备份保留下,方便自己今后阅读。(PS:建议大家一边看笔记,一边看视频,加深理解)原作者:bsauce原文链接:https://www.jianshu.com/p/5cbc5bb5c4da

    首先非常感谢南京大学李樾和谭添老师的无私分享,之前学习程序分析是看的北大熊英飞老师的ppt,但是很多地方没看懂,正如李樾老师所说的那样,熊英飞老师的授课涵盖非常广,不听课只看ppt的话,理解起来还是很有难度的。但李樾老师的视频就讲解的非常易懂,示例都是精心挑选的,所以墙裂推荐。
    推送门:南大课件 南大视频课程 北大课件

    目录
    指针分析规则如何实现指针分析指针分析算法指针分析如何处理函数调用(过程间指针分析)
    重点理解指针分析的规则、指针流图PFG、指针分析算法。
    理解指针分析调用函数的规则、过程间指针分析算法、实时调用图构建。
    1.指针分析规则首先分析前4种语句:New / Assign / Store / Load。
    指针分析的域和相应的记法:变量/函数/对象/实例域/指针,用pt表示程序中的指向关系(映射)。

    规则:采用推导形式,横线上面是条件,横线下面是结论。

    New:创建对象,将new T()对应的对象oi加入到x的指针集。
    Assign:将y的指针集加入到x对应的指针集。
    Store:让oi的field指向oj。
    Load:Store的反操作。


    2.如何实现指针分析算法要求:全程序指针分析,要容易理解和实现。
    本质:在指针(变量/域)之间传递指向信息。Andersen-style分析(很普遍)——很多solving system把指针分析看作是一种包含关系,eg,x = y,x包含y。
    问题:当一个指针的指向集发生变化,必须更新与它相关的其他指针。如何表示这种传递关系?PFG。
    PFG:用指针流图PFG来表示指针之间的关系,PFG是有向图。

    Nodes:Pointer = V U (O x F) 节点n表示一个变量或抽象对象的域。Edges:Pointer X Pointer 边x -> y 表示指针x指向的对象may会流入指针y。
    Edges添加规则:根据程序语句 + 对应的规则。

    示例:

    PTA步骤:

    构造PFG(根据以上示例,PFG也受指向关系影响)
    根据PFG传播指向信息

    3.指针分析算法(1)过程内PTA算法
    符号:

    S:程序语句的集合。WL:Work list,待合并的指针信息,二元组的集合,<指针n,指向的对象集合pts>。pts将被加入到n的指向集pt(n)中。PFG:指针流图。
    步骤:对每种语句都是基于第1小节的规则来实现。

    对S中所有类似New x = new T()的语句,将<x, {oi}>加入到WL。
    对S中所有类似Assign x = y的语句,调用AddEdge()将y -> x加入到PFG,<x, pt(y)>加入到WL(传播指向信息)。
    遍历WL,取一个元素<n, pts>,除去pts中与pt(n)重复的对象得到Δ\DeltaΔ,调用Propagate(n,Δ\DeltaΔ)将Δ\DeltaΔ加入到pt(n),且取出PFG中所有n指向的边n->s,将<s, pts>加入到WL(根据PFG将指向信息传递给同名指针)。
    如果n表示一个变量x(x跟Store/Load指令相关),对Δ\DeltaΔ中的每个对象oi。对S中所有类似 Store x.f = y 的语句,调用AddEdge()将y -> oi.f加入到PFG,<oi.f, pt(y)>加入到WL(传播指向信息);对S中所有类似Load y = x.f的语句,调用AddEdge()将oi.f -> y加入到PFG,<y, pt(oi.f)>加入到WL(传播指向信息)。

    问题:

    为什么要去重?避免冗余,英文叫做Differential propagation差异传播。
    指针集用什么数据结构存储?混合集 Hibra-set,集合元素小于16个用hash set,大于16个用big-rector 位存储。
    开源项目有哪些?Soot、WALA、Chord。

    (2)示例1 b = new C(); 2 a = b;3 c = new C(); 4 c.f = a;5 d = c;6 c.f = d; 7 e = d.f;

    4.指针分析如何处理函数调用构造调用图技术对比:

    CHA:基于声明类型,不精确,引入错误的调用边和指针关系。
    指针分析:基于pt(a),即a指向的类型,更精确,构造更准的CG并对指针分析有正反馈(所以过程间指针分析和CG构造同时进行,很复杂)。

    void foo(A a) { // pt(a) = ??? ... b = a.bar(); // pt(b) = ??? 把a的指向分析清楚了,就能确定a.bar()到底调用哪个对象的bar()函数,那么b的指向也明确了。 ... }
    (1)调用语句规则call语句规则:主要分为4步。


    找目标函数m:Dispatch(oi, k)——找出pt(x),也即oi类型对象中的k函数。
    receiver object:把x指向的对象(pt(x))传到m函数的this变量,即mthism_{this}m​this​​。
    传参数:pt(aj), 1<=j<=n 传给m函数,即p(mpj)p(m{pj})p(mpj), 1<=j<=n。建立PFG边,a1−>ma_1->ma​1​​−>m{p1},…,an->m{pn}。
    传返回值:pt(mret)pt(m{ret})pt(mret)传给pt(r)。建立PFG边,r<−mr<-mr<−m{ret}。

    问题:为什么PFG中不添加x−>mthisx->m{this}x−>mthis边?因为mmm{this}只和自己这个对象相关,而可能有pt(x)={new A, new B, new C},指定对象的x只流向对应的对象,是无法跨对象传递的。
    (2)过程间PTA算法问题:由于指针分析和CG构造互相影响,所以每次迭代只分析可达的函数和语句。然后不断发现和分析新的可达函数。
    可达示例:

    算法:黄色背景的代码是和过程内分析不同的地方。

    符号:

    mentry:入口main函数
    Sm:函数m中的语句
    S:可达语句的集合(就是RM中的语句)
    RM:可达函数的集合
    CG:调用图的边

    步骤:基于调用规则来实现。

    首先调用AddReachable(mentry)AddReachable(m^{entry})AddReachable(m​entry​​),将入口函数mentrym^{entry}m​entry​​的语句加到S中。处理New x = new T()语句,把<x, {oi}>加入到WL;处理Assign x = y语句,调用AddEdge(y, x)加入边到PFG。
    跟过程内指针分析一样,遍历WL,取一个元素<n, pts>,除去pts中与pt(n)重复的对象得到Δ\DeltaΔ,调用Propagate(n,Δ\DeltaΔ)将Δ\DeltaΔ加入到pt(n),且取出PFG中所有n指向的边n->s,将<s, pts>加入到WL(根据PFG将指向信息传递给同名指针)。
    如果n表示一个变量x(x跟Store/Load指令相关),对Δ\DeltaΔ中的每个对象oi。对S中所有类似 Store x.f = y 的语句,调用AddEdge()将y -> oi.f加入到PFG,<oi.f, pt(y)>加入到WL(传播指向信息);对S中所有类似 Load y = x.f 的语句,调用AddEdge()将oi.f -> y加入到PFG,<y, pt(oi.f)>加入到WL(传播指向信息)。
    最后调用ProcessCall(x, oi),处理与x相关的call指令。取出S中类似r = x.k(a1,...,an)的调用语句L,首先调用Dispatch(oi, k)解出调用的目标函数m,把<mthis, {oi}>加入到WL(传递接收对象,上下文敏感分析将用到),将L->m这条调用边加入到CG;调用AddReachable(m)将新的语句加入到S,并处理New/Assign语句;调用AddEdge()将实参->形参、返回值->r边加入到PFG(传递参数、返回值),并将<形参,pt(实参)>、<r,pt(返回值)>加入到WL。

    问题:为什么ProcessCall(x, oi)中,要判断L->m这条边是否已经加入到CG?因为x可能指向多个对象,就会多次处理L这个调用指令,可能x中别的对象oj早就已经将这条边加入进去了。
    (3)示例class A { static void main(){ A a = new A(); A b = new B(); A c = b.foo(a); } A foo(Ax){...}}class B extends A { A foo(A y) { A r=newA(); return r; }}




    WL
    正处理
    PFG
    指针集
    RM
    CG
    语句
    算法语句




    1
    []

    {}

    {}
    {}

    初始化


    2
    []



    {A.main()}

    1,2
    AddReachable(mentry)


    3
    [<a,{o3}>, <b,{o4}>]





    3,4



    4
    [<b,{o4}>]
    <a,{o3}>

    pt(a)={o3};



    while开头


    5
    []
    <b,{o4}>

    pt(b)={o4}



    while开头


    6
    []





    5
    ProcessCall(b, o4)


    7
    [<B.foothis, {o4}>]




    {5->B.foo(A)}

    m=Dispatch(o4, foo())=B.foo();添加到调用图


    8
    [<B.foothis, {o4}>, <r, o11>]



    {A.main(), B.foo()}


    AddReachable(B.foo());添加到可达函数


    9
    [<B.foothis, {o4}>, <r, o11>, <y, {o3}>]

    {a->y, r->c}




    AddEdge();添加参数边、返回值边


    10
    [<r, o11>, <y, {o3}>]
    <B.foothis, {o4}>

    pt(B.foothis)={o4};



    while开头,B.foothis没有调用任何函数


    11
    [<y, {o3}>, <c, {o11}>]
    <r, o11>

    pt(r)={o11};



    while开头


    12

    <y, {o3}>, <c, {o11}>

    pt(y)={o3};pt(c)={o11}



    while开头



    如果是CHA的话,CG={5->B.foo(A), 5->A.foo(A)},错误识别为调用边。
    结果:

    问题:没有入口函数的?如对库函数处理,生成调用库函数的程序。
    0 留言 2020-07-19 11:55:31 奖励30点积分
  • 【课程笔记】南大软件分析课程6——指针分析介绍


    最近在看“静态分析”技术相关的文章,看到这个系列的笔记和视频教程,感觉介绍得很好,通俗易懂,而且还比较详细,故转载分享,同时也备份保留下,方便自己今后阅读。(PS:建议大家一边看笔记,一边看视频,加深理解)原作者:bsauce原文链接:https://www.jianshu.com/p/9d15edf2604e

    首先非常感谢南京大学李樾和谭添老师的无私分享,之前学习程序分析是看的北大熊英飞老师的ppt,但是很多地方没看懂,正如李樾老师所说的那样,熊英飞老师的授课涵盖非常广,不听课只看ppt的话,理解起来还是很有难度的。但李樾老师的视频就讲解的非常易懂,示例都是精心挑选的,所以墙裂推荐。
    推送门:南大课件 南大视频课程 北大课件

    目录
    Motivation指针分析介绍影响指针分析的关键要素分析哪些语句
    重点什么是指针分析?影响指针分析的关键因素是什么?指针分析要分析哪些指令?
    1.Motivation指针分析必要性

    2.指针分析目标:分析程序指针可以指向哪些内存。对于Java等面向对象语言,主要分析指针指向哪个对象。
    说明:指针分析属于may analysis,分析的结果是某指针所有可能指向哪些对象,是个over-approximation集合。
    示例:面向对象语言中的指针指向问题。对于setB()函数,this指向new A(),因为是调用者是a.setB();setB()中的b是x传过来的,所以b指向new B(),A.b指向 new B()。

    区别:

    指针分析:分析指针所有可能指向的对象。
    别名分析:分析两个指针是否指向相同的对象,可通过指针分析来推导得到。

    应用:基本信息(别名分析/调用图),编译优化(嵌入虚拟调用),漏洞(空指针),安全分析(信息流)。
    3.影响指针分析的关键要素指标:精度(precision)& 效率(efficiency)。
    影响因素:本课程,我们主要分析分配点的堆抽象技术、上下文敏感/不敏感、流不敏感、全程序分析。

    (1)堆抽象(内存建模)问题:程序动态执行时,堆对象个数理论上是无穷无尽的,但静态分析无法处理这个问题。所以为保证指针分析可以终止,我们采用堆抽象技术,将无穷的具体对象抽象成有限的抽象对象。也即,将有共性的对象抽象成1个静态对象,从而限制静态分析对象的个数。
    // 示例for (...) { A a = new A();}
    技术概览

    我们只学习Allocation-Site技术,最常见也最常被使用。
    Allocation-Site原理:将动态对象抽象成它们的创建点(Allocation-Site),来表示在该点创建的所有动态对象。Allocation-Site个数是有限的。
    示例:循环创建了3个对象,我们用O2来抽象表示这3个动态对象。

    (2)上下文敏感 Context Sensitivity问题:考虑是否区分不同call-site对同一函数的调用。

    Context-sensitive:根据某函数调用上下文的不同,多次分析同一函数。
    Context-insensitive:每个函数只分析一次。


    (3)流敏感 Flow Sensitivity问题:考虑语句顺序(控制流)的影响 vs 把程序当做无序语句的集合。
    方法:流敏感会在每个程序点都保存一份指针指向关系映射,而流不敏感则对整个程序保存一份指向关系映射。
    说明:目前流敏感对Java提升不大,不过在C中很有效,本课程分析的是Java,所以重点讨论流不敏感技术。
    指针分析示例:

    (4)分析范围 Analysis Scope问题:分析程序的哪一部分?

    Whole-program 全程序:分析全程序的指向关系。
    Demand-driven 需求驱动:只分析影响特定域的指针的指向关系。

    4.分析哪些语句问题:哪些语句会影响指针指向,那就只分析这些语句。
    Java指针类型:

    Lacal variable: x
    Static field:C.f (有时称为全局变量)——不分析
    Instance field: x.f (对象的field)
    Array element: array[i] ——不分析,因为静态分析无法确定下标,所以将array中所有成员映射到一个field中,等价于Instance field,所以不重复分析。如下图所示:


    影响指针指向的语句:
    1. New: x = new T()2. Assign:x = y3. Store: x.f = y4. Load: y = x.f5. Call: r = x.k(a,...) - Static call: C.foo() - Special call: super.foo() / x.<init>() / this.privateFoo() - **Virtual call**:x.foo()
    复杂的内存访问可以通过引入临时变量,转化为三地址代码:
    x.f.g.h = y;// 转化为t1 = x.f;t2 = t1.g;t2.h = y;
    0 留言 2020-07-17 11:33:24 奖励30点积分
  • 【课程笔记】南大软件分析课程5——过程间分析


    最近在看“静态分析”技术相关的文章,看到这个系列的笔记和视频教程,感觉介绍得很好,通俗易懂,而且还比较详细,故转载分享,同时也备份保留下,方便自己今后阅读。(PS:建议大家一边看笔记,一边看视频,加深理解)原作者:bsauce原文链接:https://www.jianshu.com/p/2d14c0ae41cd

    首先非常感谢南京大学李樾和谭添老师的无私分享,之前学习程序分析是看的北大熊英飞老师的ppt,但是很多地方没看懂,正如李樾老师所说的那样,熊英飞老师的授课涵盖非常广,不听课只看ppt的话,理解起来还是很有难度的。但李樾老师的视频就讲解的非常易懂,示例都是精心挑选的,所以墙裂推荐。
    推送门:南大课件 南大视频课程 北大课件

    目录
    Motivation调用图构建过程间控制流分析过程间数据流分析
    重点:学习如何利用类层级分析来构建调用图;过程间控制流/数据流分析;过程间的常量传播。
    1.Motivation问题:过程内的分析未考虑函数调用,导致分析不精确。
    过程间分析:Inter-procedural Analysis,考虑函数调用,又称为全程序分析(Whole Program Analysis),需要构建调用图,加入Call edges和Return edges。
    2.调用图构建(1)调用图定义:本质是调用边的集合,从调用点(call-sites)到目标函数(target methods / callees)的边。
    示例:

    应用:是所有过程间分析(跨函数分析)的基础,程序优化,程序理解,程序调试。
    (2)面向对象语言的调用图构造(Java)代表性算法:从上往下精度变高,速度变慢,重点分析第1、4个算法。

    Class hierarchy analysis(CHA)Rapid type analysis(RTA)Variable type analysis(VTA)Pointer analysis(k-CFA)
    Java调用分类:

    Method Dispatch:最难的是Virtual call,其中关键步骤是Method Dispatch,就是找到最终调用的实际函数。
    virtual call在程序运行时才能得到,基于2个要素得到:

    reciever object的具体类型:c
    调用点的函数签名:m。(通过signature可以唯一确定一个函数)

    signature = 函数所在的类 + 函数名 + 描述符描述符 = 返回类型 + 参数类型
    简记为C.foo(P, Q, R)


    (3)Method Dispatch(virtual call)定义:用Dispatch(c, m)来模拟动态Method Dispatch过程,c表示reciever object,m表示函数签名。

    解释:若该类的非抽象方法(实际可执行的函数主体)中包含和m相同名字、传递/返回参数的m‘,则直接返回;否则到c的父类中找。
    示例:

    (4)Class Hirarchy Analysis (CHA) 类层级分析目的:根据每个virtual call 的 receiver varible 的声明类型来求解所有可能调用的目标函数。如 A a = ... ; a.foo(); 这个a就是receiver varible,声明类型就是A。假定a可以指向A以及A所有子类对象,CHA的过程就是从A和子类中去找目标函数。
    算法:Resolve(cs)——利用CHA算法找到调用点所有可能的调用目标。

    算法示例:

    算法应用:

    错误:以上b.foo()的调用目标 C.foo()和D.foo()是错误的,因为已经指定了是B类型,所以b.foo()根本不会调用C、D的foo()。因为CHA只考虑声明类型,也就是B,导致准确度下降。多态性就是说,父类可以引用子类的对象,如B b=new C()。
    优缺点:CHA优点是速度快,只考虑声明类型,忽略数据流和控制流;缺点是准确度低。
    总结:本类中有同名函数就在本类和子类找,没有就从父类找,接着找父类的子类中的同名函数(CHA分析)。
    (5)利用CHA构造调用图算法:遍历每个函数中的每个调用指令,调用CHA的Resolve()找到对应的目标函数和调用边,函数+调用边=调用图。

    示例:

    3.过程间控制流分析定义:过程间控制流图ICFG = CFG + (Call edges + Return edges)。

    Call edges:连接调用点和目标函数入口Return edges:从return语句连到Return site(Call site后面一条语句)
    示例:

    4.过程间数据流分析说明:对ICFG进行数据流分析,没有标准的一套算法。
    对比:

    常量传播数据流分析:

    Node transfer:与过程内分析相同,对每个调用点,将等号左边部分去掉。Call edge transfer:传参Return edge transfer:传返回值
    常量传播示例:

    说明:黄色背景边必须有,从b = addOne(a)到c=b-3,a通过此边传递,b通过addOne()传递。若a也通过addOne()传递,会额外消耗系统资源。
    0 留言 2020-07-15 10:12:26 奖励30点积分
  • 【课程笔记】南大软件分析课程4——数据流分析基础


    最近在看“静态分析”技术相关的文章,看到这个系列的笔记和视频教程,感觉介绍得很好,通俗易懂,而且还比较详细,故转载分享,同时也备份保留下,方便自己今后阅读。(PS:建议大家一边看笔记,一边看视频,加深理解)原作者:bsauce原文链接:https://www.jianshu.com/p/d314b316b332

    首先非常感谢南京大学李樾和谭添老师的无私分享,之前学习程序分析是看的北大熊英飞老师的ppt,但是很多地方没看懂,正如李樾老师所说的那样,熊英飞老师的授课涵盖非常广,不听课只看ppt的话,理解起来还是很有难度的。但李樾老师的视频就讲解的非常易懂,示例都是精心挑选的,所以墙裂推荐。
    推送门:南大课件 南大视频课程 北大课件

    关于这一节zcc的笔记已经够完美了,我就直接在他基础上记录了。
    目录
    迭代算法-另一个角度偏序(Partial Order)上下界(Upper and Lower Bounds)格(Lattice),半格(Semilattice),全格和格点积(Complete and Product Lattice)数据流分析框架(via Lattice)单调性与不动点定理(Monotonicity and Fixed Point Theorem)迭代算法转化为不动点理论从lattice的角度看may/must分析分配性(Distributivity)和MOP常量传播Worklist算法
    重点上节课是介绍了3种数据流分析迭代算法,本节课将从数学理论的角度来讨论数据流分析,加深对数据流分析算法的理解。
    1.迭代算法-另一个角度本质:常见的数据流迭代算法,目的是通过迭代计算,最终得到一个稳定的不变的解。
    (1)理论定义1:给定有k个节点(基本块)的CFG,迭代算法就是在每次迭代时,更新每个节点n的OUT[n]。
    定义2:设数据流分析的值域是V,可定义一个k-元组:(OUT[n1],OUT[n2],..,OUT[nk])(OUT[n_1],OUT[n_2], .. , OUT[n_k])(OUT[n​1​​],OUT[n​2​​],..,OUT[n​k​​])是集合 (V1×V2..×Vk)(V_1 \times V_2 .. \times V_k)(V​1​​×V​2​​..×V​k​​) (幂集,记为VkV_kV​k​​)的一个元素,表示每次迭代后k个节点整体的值。
    定义3:每一次迭代可看作是Vk映射到新的Vk,通过转换规则和控制流来映射,记作函数F:Vk→VkF:V_k \rightarrow V_kF:V​k​​→V​k​​。
    迭代算法本质:通过不断迭代,直到相邻两次迭代的k-元组值一样,算法结束。
    (2)图示
    不动点:当Xi = F(Xi)时,就是不动点。
    问题:

    迭代算法是否一定会停止(到达不动点)?迭代算法如果会终止,会得到几个解(几个不动点)?迭代几次会得到解(到达不动点)?
    2.偏序(Partial Order)定义:给定偏序集(P,⊑)(P, \sqsubseteq)(P,⊑),⊑\sqsubseteq⊑是集合PPP上的二元关系,若满足以下性质则为偏序集:

    自反性Reflexivity:∀x∈P, x⊑x
    对称性Antisymmetry:∀x,y∈P, x⊑y∧y⊑x ⇒ x=y
    传递性Transitivity:∀x,y∈P, x⊑y ∧ y⊑z ⇒ x⊑z

    例子:

    P是整数集,⊑\sqsubseteq⊑表示≤\leq≤,是偏序集;若⊑\sqsubseteq⊑表示<,则显然不是偏序集
    P是英文单词集合,⊑\sqsubseteq⊑表示子串关系(可以存在两个元素不具有偏序关系,不可比性),是偏序集

    3.上下界(Upper and Lower Bounds)(1)定义定义:给定偏序集(P, \sqsubseteq),且有P的子集S⊆P:

    ∀x∈S, x⊑u, 其中u∈P,则u是子集S的上界 (注意,u并不一定属于S集)
    ∀x∈S, l⊑x, 其中l∈P,则l是S的下界

    最小上界:least upper bound(lub 或者称为join),用⊔S表示。上确界?
    定义:对于子集S的任何一个上界u,均有⊔S⊑u。
    最大下界:greatest lower bound(glb 或者称为meet),用⊓S表示。下确界?
    定义:对于子集S的任何一个下界l,均有l⊑⊓S。
    (2)示例若S只包含两个元素,a、b(S = {a, b})那么上界可以表示为a⊔b,下界可以表示为a⊓b。

    (3)特性
    并非每个偏序集都有上下确界


    如果存在上下确界,则是唯一的
    利用传递性和反证法即可证明。
    4.格(Lattice),(半格)Semilattice,全格,格点积(Complete and Product Lattice)都是基于上下确界来定义的。
    (1)格定义:给定一个偏序集(P,⊑),∀a,b∈P,如果存在a⊔b和a⊓b,那么就称该偏序集为格。偏序集中的任意两个元素构成的集合均存在最小上界和最大下界,那么该偏序集就是格。
    例子:

    (S, ⊑)中S是整数子集,⊑\sqsubseteq⊑是≤\leq≤,是格点
    (S, ⊑)中S是英文单词集,⊑\sqsubseteq⊑表示子串关系,不是格点,因为单词pin和sin就没有上确界
    (S, ⊑)中S是{a, b, c}的幂集,⊑\sqsubseteq⊑表示⊆\subseteq⊆子集,是格点

    (2)半格定义:给定一个偏序集(P,⊑),∀a,b∈P:

    当且仅当a⊔b存在(上确界),该偏序集叫做 join semilatice
    当且仅当a⊓b存在(下确界),该偏序集叫做 meet semilatice

    (3)全格定义:对于格点 (S, ⊑\sqsubseteq⊑) (前提是格点)的任意子集S,⊔S上确界和⊓S下确界都存在,则为全格complete lattice。
    例子:

    P是整数集,⊑\sqsubseteq⊑是≤\leq≤,不是全格,因为P的子集正整数集没有上确界
    (S, ⊑)中S是{a, b, c}的幂集,⊑\sqsubseteq⊑表示⊆\subseteq⊆子集,是全格

    符号:⊤=⊔P\top = \sqcup P⊤=⊔P,叫做top;⊥=⊓P\perp = \sqcap P⊥=⊓P,叫做bottom。
    性质:有穷的格点必然是complete lattice。全格一定有穷吗? 不一定,如实数界[0, 1]。
    (4)格点积定义:给定一组格,L1=(P1,⊑1)L_1=(P_1, \sqsubseteq 1)L​1​​=(P​1​​,⊑1),L2=(P2,⊑2)L_2=(P_2, \sqsubseteq 2)L​2​​=(P​2​​,⊑2),.. ,Ln=(Pn,⊑n)L_n=(P_n, \sqsubseteq n)L​n​​=(P​n​​,⊑n),都有上确界⊔i\sqcup i⊔i和下确界⊓i\sqcap i⊓i,则定义格点积 Ln=(P,⊑)Ln = (P, \sqsubseteq)Ln=(P,⊑):
    P=P1×..×PnP = P_1 \times .. \times P_nP=P​1​​×..×P​n​​(x1,..xn)⊑(y1,..yn)⇔(x1⊑y1)∧..∧(xn⊑yn)(x_1, .. x_n) \sqsubseteq (y_1, .. y_n) \Leftrightarrow (x_1 \sqsubseteq y_1) \wedge .. \wedge (x_n \sqsubseteq y_n)(x​1​​,..x​n​​)⊑(y​1​​,..y​n​​)⇔(x​1​​⊑y​1​​)∧..∧(x​n​​⊑y​n​​)(x1,..xn)⊔(y1,..yn)=(x1⊔y1,..,xn⊔yn)(x_1, .. x_n) \sqcup (y_1, .. y_n) = (x1 \sqcup y_1, .., x_n \sqcup y_n)(x​1​​,..x​n​​)⊔(y​1​​,..y​n​​)=(x1⊔y​1​​,..,x​n​​⊔y​n​​)(x1,..xn)⊓(y1,..yn)=(x1⊓y1,..,xn⊓yn)(x_1, .. x_n) \sqcap (y_1, .. y_n) = (x_1 \sqcap y_1, .., x_n \sqcap y_n)(x​1​​,..x​n​​)⊓(y​1​​,..y​n​​)=(x​1​​⊓y​1​​,..,x​n​​⊓y​n​​)性质:格点积也是格点;格点都是全格,则格点积也是全格。
    5.数据流分析框架(via Lattice)数据流分析框架(D, L, F) :

    D—方向
    L—格点(值域V,meet ⊓\sqcap⊓ 或 join ⊔\sqcup⊔ 操作)
    F—转换规则V→VV \rightarrow VV→V。

    数据流分析可以看做是迭代算法对格点 利用转换规则和 meet/join操作。
    6.单调性与不动点定理(Monotonicity and Fixed Point Theorem)目标问题:迭代算法一定会停止(到达不动点)吗?
    (1)单调性定义:函数f:L→Lf: L \rightarrow Lf:L→L,满足∀x,y∈L,x⊑y⇒f(x)⊑f(y),则为单调的。
    (2)不动点理论定义:给定一个完全lattice(L,⊑),如果f:L→L是单调的,并且L有限
    那么我们能得到最小不动点,通过迭代:f(⊥),f(f(⊥)),…,fk(⊥)直到找到最小的一个不动点。
    同理 我们能得到最大不动点,通过迭代:f(⊤),f(f(⊤)),…,fk(⊤)直到找到最大的一个不动点。
    (3)证明不动点的存在性;
    最小不动点证明。
    7.迭代算法转化为不动点理论问题:我们如何在理论上证明迭代算法有解、有最优解、何时到达不动点?那就是将迭代算法转化为不动点理论。因为不动点理论已经证明了,单调、有限的完全lattice,存在不动点,且从⊤开始能找到最大不动点,从⊥开始能找到最小不动点。
    目标:证明迭代算法是一个完全lattice(L,⊑)lattice(L, \sqsubseteq)lattice(L,⊑),是有限的,单调的。

    (1)完全lattice证明根据第5小节,迭代算法每个节点(基本块)的值域相当于一个lattice,每次迭代的k个基本块的值域就是一个k-元组。k-元组可看作lattice积,根据格点积性质:若Lk中每一个lattice都是完全的,则Lk也是完全的。
    (2)L是有限的迭代算法中,值域是0/1,是有限的,则lattice有限,则Lk也有限。
    (3)F是单调的函数F:BB中转换函数fi:L → L + BB分支之间的控制流影响(汇聚是join ⊔\sqcup⊔ / meet ⊓\sqcap⊓ 操作,分叉是拷贝操作)。

    转换函数:BB的gen、kill是固定的,值域一旦变成1,就不会变回0,显然单调。
    join/meet操作:L × L → L 。证明:∀x,y,z∈L,且有x⊑y需要证明x⊔z⊑y⊔z。

    总结:迭代算法是完全lattice,且是有限、单调的,所以一定有解、有最优解。
    (4)算法何时到达不动点?定义:lattice高度—从lattice的top到bottom之间最长的路径。

    最坏情况迭代次数:设有n个块,每次迭代只有1个BB的OUT/IN值的其中1位发生变化(则从top→bottom这1位都变化),则最多迭 (n × h) 次。
    8.从lattice的角度看may/must分析说明:may 和 must 分析算法都是从不安全到安全(是否安全取决于safe-aprroximate过程),从准确到不准确。

    (1)may分析以 Reaching Definitions分析为例:

    从⊥\perp⊥开始,⊥\perp⊥表示所有定义都不可达,是不安全的结果(因为这个分析的应用目的是为了查错,查看变量是否需要初始化。首先在Entry中给每个变量一个假定义,标记所有变量为都为未初始化状态,⊥\perp⊥表示所有的假定义都无法到达,说明所有变量在中间都进行了赋值,那就不需要对任何变量进行初始化,这是不安全的,可能导致未初始化错误)。
    ⊤\top⊤表示所有Entry中的假定义都可达,从查错角度来说,需要对每个变量都进行初始化,非常安全!但是这句话没有用,我都要初始化的话还做这个分析干嘛?
    Truth:表明最准确的验证结果,假设{a,c}是truth,那么包括其以上的都是safe的,以下的都是unsafe,就是上图的阴影和非阴影。
    从⊥\perp⊥到⊤\top⊤,得到的最小不动点最准确,离Truth最近。上面还有多个不动点,越往上越不准。


    (2)must分析以available expressions分析为例:

    从⊤\top⊤开始,表示所有表达式可用。如果用在表达式计算优化中,那么有很多已经被重定义的表达式也被优化了(实际上不能被优化),那么该优化就是错误的,不安全!
    ⊥\perp⊥表示没有表达式可用,都不需要优化,很安全!但没有用。
    从⊤\top⊤到⊥\perp⊥,就是从不安全到安全,存在一个Truth,代表准确的结果。
    从⊤\top⊤到⊥\perp⊥,达到一个最大不动点,离truth最近的最优解。

    迭代算法转化到lattice上,may/must分析分别初始化为最小值⊥\perp⊥和最大值⊤\top⊤,最后求最小上界/最大下界。
    9.分配性(Distributivity)和MOP目的:MOP(meet-over-all-paths)衡量迭代算法的精度。
    (1)概念定义:最终将所有的路径一起来进行join/meet操作。
    路径P = 在cfg图上从entry到基本块si的一条路径(P = Entry → s1 → s2 → … → s~i )。
    路径P上的转移函数Fp:该路径上所有语句的转移函数的组合fs1,fs2,… ,fsi-1,从而构成FP。
    MOP:从entry到si所有路径的FP的meet操作。本质—求这些值的最小上界/最大下界。

    MOP准确性:有些路径不会被执行,所以不准确;若路径包含循环,或者路径爆炸,所以实操性不高,只能作为理论的一种衡量方式。
    (2)MOP vs 迭代算法
    对于以上的CFG,抽象出itter和MOP公式。
    证明:

    根据最小上界的定义,有x⊑x⊔y和 y⊑x⊔y。
    由于转换函数是单调的,则有F(x)⊑F(x⊔y)和F(y)⊑F(x⊔y),所以F(x⊔y)就是F(x)和F(y)的上界。
    根据定义,F(x)⊔F(y)是F(x)和F(y)的最小上界。
    所以F(x)⊔F(y)⊑F(x⊔y)。

    结论:所以,MOP更准确。若F满足分配律,则迭代算法和MOP精确度一样 F(x⊔y)=F(x)⊔F(y)。一般,对于控制流的join/meet,是进行集合的交或并操作,则满足分配律。
    10.常量传播 (constant propagation)问题描述:在程序点p处的变量x,判断x是否一定指向常量值。
    类别:must分析,因为要考虑经过p点所有路径上,x的值必须都一样,才算作一定指向常量。
    表示:CFG每个节点的OUT是pair(x, v)的集合,表示变量x是否指向常数v。
    数据流分析框架(D, L, F)(1)D:forward更直观
    (2)L:lattice

    变量值域:所有实数。must分析,所以⊤\top⊤是UNDEF未定义(unsafe),⊥\perp⊥是NAC非常量(safe)。
    meet操作:must分析, ⊓\sqcap⊓。在每个路径汇聚点PC,对流入的所有变量进行meet操作,但并非常见的交和并,所以不满足分配律。

    NAC⊓v=NACNAC \sqcap v = NACNAC⊓v=NAC
    UNDEF⊓v=vUNDEF \sqcap v = vUNDEF⊓v=v 未初始化的变量不是我们分析的目标
    c⊓v=?c⊓c=c c1⊓c2=NACc \sqcap v = ? c \sqcap c = c \space c1 \sqcap c2 =NACc⊓v=?c⊓c=c c1⊓c2=NAC

    (3)F转换函数
    OUT[s] = gen U (IN[s] - {(x, _})
    输出 = BB中新被赋值的 U 输入 - BB中相关变量值已经不是f常量的部分。
    对所有的赋值语句进行分析(不是赋值语句则不管,用val(x)表示x指向的值):

    (4)性质:不满足分配律

    可以发现,MOP更准确。F(X⊓Y)⊑F(X)⊓F(Y)F(X \sqcap Y) \sqsubseteq F(X) \sqcap F(Y)F(X⊓Y)⊑F(X)⊓F(Y),但是是单调的。
    11.Worklist算法本质:对迭代算法进行优化,采用队列来存储需要处理的基本块,减少大量的冗余的计算。
    0 留言 2020-07-13 22:12:43 奖励30点积分
  • 基于Web在线考试系统的设计与实现

    1 课题背景与意义1.1课题开发背景当今社会,考试已经是我们必不可少的东西了,从小到大我们已经考过无数次了,以后还要考,不管是国内还是国外的各大厂家,都在不断的推出一系列的考试、认证。又是要我们去考试。我们国家的自考或是成考,以及各省市的各种考试,现在都在朝着信息化的道路前进在走。我们相信在今后这一系列的考试将会走向网络化考试的。这样才是符合信息技术发展的方向。我们要给不同的考试同一个好的解决方案。 这个方案在技术上来讲我们是采用B/S模式。 在windows/Linux平台上,使用IE浏览器,完成抽题、考试、交卷等考试任务。方便,简单的完成各种考试,这也是我们的目的所在。
    考点模块通过网络获取题库,按照题库中的抽题策略,自动给每个考生生成一份试卷,考生在线作答,考试结果数据通过网络回收,系统自动进行判分,生成考试成绩和统计数据。“在线考试系统”是集合现代考试理论、方法和现代信息技术手段的智能化网上考试系统,为学生个性化学习提供“灵活、方便、科学、公平”的“个别化考试服务”,是终结性评价系统。学生可以随时、随地进行课程结业考试。
    1.2 课题开发意义用Browser/Web模式来设计考试系统比较合适,服务器端我们采用SQL SERVER数据库系统和JSP组件来构成考试的应用服务系统;客户端采用浏览器来完成考试全过程,同时可进行远程系统维护和管理。利用网络和数据库技术,结合目前硬件价格普遍下跌与宽带网大力建设的有利优势,应用JAVA Server Page技术,开发了基于B/S模式多用户在线考试系统这一程序。它运用方便、操作简单,效率很高(同时,它要求计算机配置也很高,尤其是服务器端).基于Web技术的网络考试系统可以借助于遍布全球的因特网进行,因此考试既可以在本地进行,也可以在异地进行,大大拓展了考试的灵活性。试卷可以根据题库中的内容即时生成,可避免考试前的压题;而且可以采用大量标准化试题,从而使用计算机判卷,大大提高阅卷效率;还可以直接把成绩送到数据库中,进行统计、排序等操作。考生通过姓名、准考证号码和口令进行登录,考试答案也存放在服务器中,这样考试的公平性、答案的安全性可以得到有效的保证。因此,采用网络考试方式将是以后考试发展的趋势。
    2 系统需求分析2.1 项目要求本系统作为一个在线的考试系统,要求实现网络考试系统的各项基本功能。从维护和安全的角度看,可以把系统设计成B/S模式的,可以让用户通过浏览器直接访问位于服务器上的考试题以及对系统进行远程维护。
    系统前台主要有考生注册和登录模块、在线考试模块、查询成绩模块以及退出登录等;系统后台主要有考生信息、考题信息、考试成绩信息、考试套题和课程信息等管理模块。
    (1)注册和登录模块考生要进入考试系统,首先需要注册一个学生证号。在注册页中输入考生的基本信息,包括学生证号、学生姓名、密码、密码问题、问题答案、性别和所学专业等。其中为防止注册的学生证号重复,在这里应用了AJAX无刷新检测用户名的技术。登录只需核实注册信息即可。
    (2)在线考试当考生准备考试时,首先需要阅读考试规则,在同意所列出的考试规则的前提下,才能选择专业和考试课程,然后才能进入考试页面开始答题。当考生提交试卷或者到达考试结束时间,系统将自动对考生提交的试卷进行评分,并给出最终成绩。
    (3)考试套题管理考试套题管理主要包括对考试题进行添加、查询、修改和删除操作。
    (4)考试题目管理考试题目管理主要包括对考试题进行添加、查询、修改和删除操作。除此之外,根据实际需要,还可以对数据库中的信息(学生信息、试题)进行维护。
    要求
    操作简单方便、界面简洁美化
    具有实时性,已注册的用户无论身处在何地,通过Internet浏览器,都可登录考试系统进行考试
    系统提供的自动交卷功能使考试到结束时间时,系统自动交卷
    提供考试时间倒计时功能,让考生随时了解考试剩余时间
    考生可以随时查看成绩
    对考生注册信息进行管理
    系统自动交卷、阅卷,保证成绩真实,准确
    系统运行稳定、安全

    2.2 开发方案选择MySql作为后台的数据库,选择myeclipse作为应用程序开发工具,应用JAVA、JSP、JavaScript、Html、Tomcat服务器技术,整个系统完全基于B/S (Browser/Server)模式进行设计,采用strus框架进行架构。
    2.3开发环境在开发网络在线考试系统时,需要具备下面的软件环境:

    操作系统:Windows8.1
    Web服务器:Tomcat7.0
    Java开发包:JDK1.7
    开发工具:myeclipse2015
    数据库:MySQL及其图形化管理工具SQLyog
    浏览器:火狐游览器

    3 总体开发3.1 开发思想3.1.1 B/S结构开发思想B/S(Browser/Server)结构即浏览器和服务器结构。它是随着Internet技术的兴起,对C/S结构的一种变化或者改进的结构。在这种结构下,用户工作界面是通过WWW浏览器来实现,极少部分事务逻辑在前端(Browser)实现,但是主要事务逻辑在服务器端(Server)实现,形成所谓三层(3-tier)结构。一个三层架构的应用程序由三部分组成,这三部分各自分布在网络中的不同地方。这三个部分分别是:工作站或表示层接口、事务逻辑、数据库以及与其相关的程序设计。在一个典型的三层架构应用程序中,应用程序的用户工作站包括提供图形用户界面(GUI)的程序设计和具体的应用程序入口表格或交互式窗口。
    以目前的技术看,局域网建立B/S结构的网络应用,并通过Internet/Intranet模式下数据库应用,相对易于把握、成本也是较低的。它是一次性到位的开发,能实现不同的人员,从不同的地点,以不同的接入方式(比如LAN, WAN, Internet/Intranet等)访问和操作共同的数据库;它能有效地保护数据平台和管理访问权限,服务器数据库也很安全 。特别是在JAVA这样的跨平台语言出现之后,B/S架构管理软件更是方便、快捷、高效。
    3.1.2 面向对象机制的设计思想所有计算机均由两种元素组成:代码和数据。精确的说,有些程序是围绕着”什么正在发生”而编写,有些则是围绕”谁正在受影响”而编写的。
    第一种编程方式叫做”面向过程的模型”,按这种模型编写的程序以一系列的线性步骤(代码)为特征,可被理解为作用于数据的代码。如 C 等过程化语言。
    第二种编程方式叫做”面向对象的模型”,按这种模型编写的程序围绕着程序的数据(对象)和针对该对象而严格定义的接口来组织程序,它的特点是数据控制代码的访问.通过把控制权转移到数据上,面向对象的模型在组织方式上有:抽象、封装、继承和多态的好处。
    3.1.3 代码分层思想由于采用B/S设计模式分层思想,同时根据软件工程的管理思想及系统分析的设计与分析的思想进行系统的开发,利用Java语言开发Web应用程序,提供String+Hibernate+Spring框架对系统的程序代码结构进行分层。分层的策略如下:

    3.2 系统功能结构设计根据网络在线考试系统的特点,可以将其分为前台和后台两个部分进行设计。前台主要用于考生注册和登录系统、在线考试、查询成绩以及修改个人资料等;后台主要用于管理员对考生信息、课程信息、考题信息和考生成绩信息等进行管理。 网络在线考试系统的前台功能如下图所示:

    网络在线考试系统的后台功能结构如下图所示:

    3.3 业务流程图设计网络在线考试的系统业务流程如下图所示:

    4 数据库设计4.1 数据库概念设计根据对系统所做的需求分析和系统设计,规划出本系统中使用的数据库实体分别为考生档案实体、管理员档案实体、课程档案实体、套题实体、考试题目实体和考生成绩实体。
    4.1.1考生档案实体考生档案实体包括编号、姓名、密码、性别、注册时间、提示问题、问题答案、专业和身份证号属性。考生档案实体的E-R图如图所示:

    4.1.2管理员档案实体管理员档案实体包括编号、管理员名、管理员密码属性。管理员档案实体的E-R图如图所示:

    4.1.3课程档案实体课程档案实体包括课程编号、课程名、添加时间属性。课程档案实体的E-R图如图所示:

    4.1.4考试题目实体考试题目实体包括编号、问题类型、所属课程、所属套题、选项A、选项B、选项C、选项D、添加时间、正确答案和备注等属性。考试题目实体的E-R图如图所示:

    4.1.5考生成绩实体考生成绩实体包括编号、准考证号、所属课程、单选题分数、多选题分数、合计分数、添加时间属性。考生成绩实体的E-R图如图所示:

    4.2 数据库逻辑设计4.2.1 tb_manager(管理员信息表)管理员信息表用来保存管理员信息,该表的结构如表所示:

    4.2.2 tb_Student(考生信息表)考生信息表用来保存考生信息,该表的结构如表所示:

    4.2.3 tb_stuResult(考生成绩信息表)考生成绩信息表用来保存考生成绩,该表中的所属课程字段whichLesson与tb_Lesson表中的Name字段相关联,并且设置为级联更新。考生成绩信息表的结构如表所示:

    4.2.4 tb_TaoTi(套题信息表)套题信息表用来保存套题信息,该表中保存着所属套题ID,套题名称,套题所属课程以及套题的添加时间信息。该表的结构如表所示:

    4.2.5 tb_Lesson(课程信息表)课程信息表用来保存课程信息,该表中保存着所属课程的ID,课程名以及课程的添加时间信息。该表的结构如表所示:

    4.2.6 tb_Questions(考试题目信息表)考试题目信息表用来保存考试题目信息。考试题目信息表的结构如表所示:

    4.3 数据表关系设计本系统设计了如图所示的数据表之间的关系,该关系实际上也反映了系统中各个实体之间的关系。

    5 详细设计5.1前台首页模块设计考生通过“考生登录”模块的验证后,可以登录到网络在线考试的前台首页,如图所示。前台首页主要用于实现前台功能导航,在该页面中只包括在线考试、成绩查询、修改个人资料和退出4个导航链接。
    由于本系统的前台首页主要用于进行系统导航,所以在实现时,采用了为图像设置热点的方法,这样可以增加页面的灵活度,使页面不至于太枯燥。下面将对如何设置图像的热点进行详细介绍。为图像设置热点,也可以称作图像映射,是指一幅图像可以建立多个超链接,即在图像上定义多个区域,每个区域链接到不同的地址,这样的区域称为热点。 图像映射有服务器端映射(Server-side-Image Map)和客户端映射(Client-side-Image Map)两种。目前使用最多的是客户端映射,因为客户端映射使图像上对应的坐标以及超链接的URL地址都在浏览器读入,省去和服务器之间互传坐标和URL的时间。

    5.2 考生信息模块设计考生信息模块主要包括考生注册、考生登录、修改个人资料以及找回密码等四个功能。考生首先要注册成为网站用户,然后才能被授权登录网站进行一系列操作的权限;登录后考生还可以修改个人的注册资料。如果考生忘记了登录密码,还可以通过网站提供的找回密码功能快速找回密码。考生信息注册模块的系统如图所示:

    考生信息模块的Action实现类Student继承了Action类。在该类中,首先需要在该类的构造方法中分别实例化考生信息模块的StudentDAO类。Action实现类的主要方法是execute(),该方法会被自动执行,这个方法本身没有具体的事务,它是根据HttpServletRequest的getParameter()方法获取的action参数值执行相应方法的。
    5.3 在线考试模块设计在线考试模块的主要功能是允许考生在网站上针对指定的课程进行考试。在该模块中,考生首先需要阅读考试规则,在同意所列出的考试规则后,才能选择考试,在选择考试课程后,系统将随机抽取试题,然后进入考试页面进行答题,当考生提交试卷或者到达考试结束时间时,系统将自动对考生提交的试卷进行评分,并给出最终考试成绩。在线考试模块的系统流程如图所示:

    考生登录到网络在线考试的前台首页后,单击“在线考试”超链接,将进入到考试规则页面,在该页面中单击“同意”按钮,即可进入到选择考试课程页面,在该页面中将以下拉列表框的形式显示需要参加考试的课程.在该页面中,单击“开始考试”按钮,将关闭当前窗口,并打开新的窗口显示试题,如图所示:

    5.4 考试题目管理模块设计网络在线考试系统的后台首页是管理员对网站信息进行管理的首页面。在该页面中,管理员可以清楚地了解网站后台管理系统包含的基本操作。

    管理员信息管理:主要包括管理员信息列表、添加管理员、修改管理员和删除管理员
    考生信息管理:主要包括查看注册考生信息列表和删除已注册的考生信息
    考生成绩查询:主要用于根据准考证号、考试课程或考试时间模糊查询考生成绩
    课程信息管理:主要包括查看课程列表、添加课程信息和删除课程信息
    套题信息管理:主要包括查看套题信息列表、添加套题信息、修改套题信息和删除套题信息
    考试题目管理:主要包括查看考试题目列表、添加考试题目、修改考试题目和删除考试题目
    退出管理:主要用于退出后台管理系统

    为了方便管理员管理,在网络在线考试系统的后台首页中显示考生成绩查询页面,其运行结果如图所示:

    管理员登录系统后,单击“考试题目管理”超链接,进入到查看考试题目列表页面,在该页面中单击“添加考试题目”超链接,进入到添加考试题目页面。在该页面的“属性课程”下拉列表框中选择“计算机专业英语”,在“所属套题”下拉列表框中将显示该课程对应的套题名称。添加考试题目页面的运行结果如图所示:

    6 软件测试6.1 软件开发技术概述Ajax技术是Asynchronous JavaScript and XML的缩写,意思是异步的JavaScript 和XML。Ajax并不是一门新的语言或技术,它是JavaScript、XML、CSS、DOM等多种已有技术的组合,它可以实现客户端的异步请求操作。这样可以实现在不需要刷新页面的情况下与服务器进行通信的效果,从而减少了用户的等待时间。
    6.2通过Ajax技术实现计时与显示剩余时间在通过Ajax技术实现计时与显示剩余时间,首先需要创建一个封装Ajax必须实现的功能的对象AjaxRequest,并将其代码保存为AjaxRequest.js,然后在开始考试页面中包含该文件,具体代码如下: <script language=“javascript” src=“..//JS/AjaxRequest.js”></script> 由于通过Ajax技术实现计时与显示剩余时间表的方法类似,下面以实现自动计时为例进行介绍。 编写调用AjaxRequest对象的函数、错误处理函数和返回值处理函数。
    计时方法showStartTime()中,首先需要获取保存在Session中的考试开始时间,并将其转化为对应的毫秒数,然后获取当前时间的毫秒数;再应用这两个时间生成两位的小时数、分钟数和秒数,并组合为新的时间;最后将其保存到showStartTime参数中,并转到输出计时时间的页面。
    参考文献[1] 刘东祥.动态网页JSP技术探究[J].时代教育,2010,(10):14-17.
    [2] 何文辉.基于JSP的动态网站开发技术[J].吉林省教育学院学报,2012,(8):18-20.
    [3] 郭利周,于长虹,郭晓萍.基于的网上考试安全体系的设计与构建[J].洛阳师范学院学 报,2013,(5):25-28.
    [4] 张洪伟.Tomcat Web开发及整合应用[M].北京.清华大学出版社. 2010.8:10-230
    [5] 周玫,袁振武.浅谈在线考试系统[J].科技广场,2008,(7):11-14.
    [6] 覃远霞.在线考试系统的设计与运用[J].应用科学,2010,(1):34-36.
    [7] 四维科技,杨易编著.JSP网络编程技术与案例[M].北京:人民邮电出版社,2006.
    [8] 范云之.基于Web数据库在线考试系统的设计与实现研究[J].商丘师范学院学报第22卷第5期 2006.10:1-20
    [9] 刘中兵,李伯华,邹晨编著.JSP数据库项目案例导航[M].北京:清华大学出版社,2013.
    [10] 覃远霞.在线考试系统的设计与运用[J].应用科学,2013,(1):34-36.
    [11] Bruce Eckel.Java编程思想[M].北京.机械工业出版社. 2008.9:30-280 [12] (美)舒尔第.Java2-The complete reference[M].北京.电子工业出版社. 2006.1:20-100
    [13] (美)Marty Hall.Servlet与JSP权威指南[M].北京v机械工业出版社. 2008.10:30-350
    [14] (美)Marty Hall.JavaScript高级程序设计[M].北京.人民邮电出版社. 2009.11:50-200
    [15](美)David Flanagan.JavaScript权威指南[M].北京.机械工业出版社. 2013.1:10-200
    附录:数据库源程序CREATE DATABASE db_exam;USE `db_exam`;CREATE TABLE `tb_lesson` ( `ID` INT(11) NOT NULL AUTO_INCREMENT, `Name` VARCHAR(60) DEFAULT NULL, `JoinTime` DATETIME DEFAULT NULL, PRIMARY KEY (`ID`)) ENGINE=INNODB AUTO_INCREMENT=34 DEFAULT CHARSET=utf-8;INSERT INTO `tb_lesson`(`ID`,`Name`,`JoinTime`) VALUES (4,'数据库原理','2015-12-01 00:00:00'),(5,'计算机文化基础','2015-12-01 00:00:00'),(8,'计算机专业英语','2015-12-01 00:00:00'),(29,'嵌入式系统','2015-12-02 00:00:00'),(31,'物联网体系结构','2015-12-05 00:00:00'),(33,'接口与通信技术','2015-12-02 10:29:10');CREATE TABLE `tb_manager` ( `ID` INT(11) NOT NULL AUTO_INCREMENT, `name` VARCHAR(30) DEFAULT NULL, `PWD` VARCHAR(30) DEFAULT NULL, PRIMARY KEY (`ID`)) ENGINE=INNODB AUTO_INCREMENT=15 DEFAULT CHARSET=utf8;INSERT INTO `tb_manager`(`ID`,`name`,`PWD`) VALUES (1,'admin','admin'),(2,'tf111','tf111');CREATE TABLE `tb_questions` ( `id` INT(11) NOT NULL AUTO_INCREMENT, `subject` VARCHAR(50) DEFAULT NULL, `type` CHAR(6) DEFAULT NULL, `joinTime` DATETIME DEFAULT NULL, `lessonId` INT(11) DEFAULT NULL, `taoTiId` INT(11) DEFAULT NULL, `optionA` VARCHAR(50) DEFAULT NULL, `optionB` VARCHAR(50) DEFAULT NULL, `optionC` VARCHAR(50) DEFAULT NULL, `optionD` VARCHAR(50) DEFAULT NULL, `answer` VARCHAR(10) DEFAULT NULL, `note` VARCHAR(50) DEFAULT NULL, PRIMARY KEY (`id`)) ENGINE=INNODB AUTO_INCREMENT=52 DEFAULT CHARSET=utf8;INSERT INTO `tb_questions`(`id`,`subject`,`type`,`joinTime`,`lessonId`,`taoTiId`,`optionA`,`optionB`,`optionC`,`optionD`,`answer`,`note`) VALUES (37,'数据库原理的老师是谁?','单选题','2015-12-01 01:00:00',5,10,'常赞杰','陈利平','姜平','以上都不是','B','空'),(39,'网络营销的发展经历几个阶段?','单选题','2015-12-01 00:00:00',29,17,'2个','3个','5个','6个','C','空'),(40,'Internet提供的基本服务有哪些?','多选题','2015-12-01 00:00:00',29,17,'E-mail','FTP','Telnet','WWW','A,B,C,D','空'),(48,'EPROM代表什么?','单选题','2015-12-01 00:00:00',8,19,'可编程存储器','可擦可编程存储器','只读存储器','可擦可编程只读存储器','D',''),(49,'对于WWW的正确解释有哪些?','多选题','2015-12-01 00:00:00',8,19,'全球网','万维网','局域网','World Wide Web的缩写','A,B,D','');CREATE TABLE `tb_student` ( `ID` VARCHAR(16) DEFAULT NULL, `name` VARCHAR(20) DEFAULT NULL, `pwd` VARCHAR(20) DEFAULT NULL, `sex` VARCHAR(2) DEFAULT NULL, `joinTime` DATETIME DEFAULT NULL, `question` VARCHAR(50) DEFAULT NULL, `answer` VARCHAR(50) DEFAULT NULL, `profession` VARCHAR(30) DEFAULT NULL, `cardNo` VARCHAR(18) DEFAULT NULL) ENGINE=INNODB DEFAULT CHARSET=utf8;INSERT INTO `tb_student`(`ID`,`name`,`pwd`,`sex`,`joinTime`,`question`,`answer`,`profession`,`cardNo`) VALUES ('CN20151201000001','王大锤','111','男','2015-12-01 00:00:00','birthday','717','广告学','220198302********'),('CN20151201000002','何小花','111','女','2015-12-01 00:00:00','birthday','1','计算机应用软件','220198007********'),('CN20151225000005','戴小超','111111','女','2015-12-01 00:00:00','我最喜欢的颜色','蓝灰色','计算机应用软件','220104************'),('CN20151229000006','熊时雨','000','男','2015-12-01 00:00:00','你好','你好','公司管理','20020'),('CN20151229000007','王明','111111','男','2015-12-01 00:00:00','你好','你好','编程','52200');CREATE TABLE `tb_sturesult` ( `id` INT(11) NOT NULL AUTO_INCREMENT, `stuId` VARCHAR(16) DEFAULT NULL, `whichLesson` VARCHAR(60) DEFAULT NULL, `resSingle` INT(11) DEFAULT NULL, `resMore` INT(11) DEFAULT NULL, `resTotal` INT(11) DEFAULT NULL, `joinTime` DATETIME DEFAULT NULL, PRIMARY KEY (`id`)) ENGINE=INNODB AUTO_INCREMENT=43 DEFAULT CHARSET=utf8;INSERT INTO `tb_sturesult`(`id`,`stuId`,`whichLesson`,`resSingle`,`resMore`,`resTotal`,`joinTime`) VALUES (1,'CN20151201000002','计算机专业英语',50,30,80,'2015-12-01 00:00:00'),(2,'CN20151201000001','物联网体系结构',0,20,20,'2015-12-01 00:00:00'),(4,'CN20151201000001','数据库原理',20,30,50,'2013-01-01 00:00:00'),(12,'CN20151201000001','计算机专业英语',40,60,100,'2015-12-01 00:00:00'),(14,'CN20151225000005','嵌入式系统',40,0,40,'2015-12-01 00:00:00'),(29,'CN20151201000002','接口与通信技术',40,60,100,'2015-12-01 00:00:00'),(30,'CN20151229000006','数据库原理',40,60,100,'2015-12-01 00:00:00'),(37,'CN20151229000007','计算机文化基础',0,0,0,'2015-12-01 00:00:00'),(38,'CN20151229000007','数据库原理',40,60,100,'2015-12-01 00:00:00'),(39,'CN20151229000006','嵌入式系统',0,0,0,'2015-12-01 00:00:00'),(40,'CN20151201000001','数据库原理',0,0,NULL,NULL),(41,'CN20151201000002','接口与通信技术',0,0,NULL,'2015-12-02 11:43:15'),(42,'CN20151201000002','计算机文化基础',40,0,40,'2015-12-02 13:10:12');CREATE TABLE `tb_taoti` ( `ID` INT(11) NOT NULL AUTO_INCREMENT, `Name` VARCHAR(50) DEFAULT NULL, `LessonID` INT(11) DEFAULT NULL, `JoinTime` DATETIME DEFAULT NULL, PRIMARY KEY (`ID`)) ENGINE=INNODB AUTO_INCREMENT=21 DEFAULT CHARSET=utf8;INSERT INTO `tb_taoti`(`ID`,`Name`,`LessonID`,`JoinTime`) VALUES (10,'2015数据库期末考试',5,'2015-01-01 00:00:00'),(17,'2015年嵌入式期末考试题',29,'2015-12-01 00:00:00'),(19,'2015年物联网体系结构考试题',8,'2015-12-01 00:00:00'),(20,'接口与通信期末考试题',31,'2015-12-01 00:00:00');
    1 留言 2019-12-20 10:08:34 奖励45点积分
  • 【课程笔记】南大软件分析课程3——数据流分析应用


    最近在看“静态分析”技术相关的文章,看到这个系列的笔记和视频教程,感觉介绍得很好,通俗易懂,而且还比较详细,故转载分享,同时也备份保留下,方便自己今后阅读。(PS:建议大家一边看笔记,一边看视频,加深理解)原作者:bsauce原文链接:https://www.jianshu.com/p/45eb5e5565d5

    首先非常感谢南京大学李樾和谭添老师的无私分享,之前学习程序分析是看的北大熊英飞老师的ppt,但是很多地方没看懂,正如李樾老师所说的那样,熊英飞老师的授课涵盖非常广,不听课只看ppt的话,理解起来还是很有难度的。但李樾老师的视频就讲解的非常易懂,示例都是精心挑选的,所以墙裂推荐。
    推送门:南大课件 南大视频课程 北大课件

    目录
    数据流分析总览预备知识Reaching Definitions Analysis (may analysis)Live Variables Analysis (may analysis)Available Expressions Analysis (must analysis)
    重点
    理解3种数据流分析的含义,如何设计类似的算法,如何优化理解种数据流分析的共性与区别理解迭代算法并弄懂算法为什么能停止

    1.数据流分析总览
    may analysis:输出可能正确的信息(需做over-approximation优化,才能成为Safe-approximation安全的近似,可以有误报-completeness),注意大多数静态分析都是may analysis
    must analysis:输出必须正确的信息(需做under-approximation优化,才能成为Safe-approximation安全的近似,可以有漏报-soundness)

    Nodes (BBs/statements)、Edges (control flows)、CFG (a program)
    例如:

    application-specific Data <- abstraction (+/-/0)
    Nodes <- Transfer function
    Edges <- Control-flow handling

    不同的数据流分析 有 不同的数据抽象表达 和 不同的安全近似策略,如 不同的 转换规则 和 控制流处理。

    2.预备知识输入/输出状态:程序执行前/执行后的状态(本质就是抽象表达的数据的状态,如变量的状态)。
    数据流分析的结果:最终得到,每一个程序点对应一个数据流值(data-flow value),表示该点所有可能程序状态的一个抽象。例如,我只关心x、y的值,我就用抽象来表示x、y所有可能的值的集合(输入/输出的值域/约束),就代表了该程序点的程序状态。

    控制流约束:约束求解做的事情,推断计算输入到输出,或反向分析。

    3.Reaching Definitions Analysis (may analysis)问题定义:给变量v一个定义d(赋值),存在一条路径使得程序点p能够到达q,且在这个过程中不能改变v的赋值。
    应用举例:检测未定义的变量,若v可达p且v没有被定义,则为未定义的变量。
    抽象表示:设程序有n条赋值语句,用n位向量来表示能reach与不能reach。
    (1)公式分析什么是definition? D: v = x op y 类似于赋值。
    Transfer Function:OUT[B]=genBU(IN[B]−killB)OUT[B] = gen_B U (IN[B] - kill_B)OUT[B]=gen​B​​U(IN[B]−kill​B​​) ——怎么理解,就是基于转换规则而得到。
    解释:基本块B的输出 = 块B内的所有变量v的定义(赋值/修改)语句 U (块B的输入 - 程序中其它所有定义了变量v的语句)。本质就是本块与前驱修改变量的语句 作用之和(去掉前驱的重复修改语句)。
    Control Flow:IN[B]=Upa predecesso of BOut[P]IN[B] = U_{p_{a \space predecesso \space of \space B}} Out[P]IN[B]=U​p​a predecesso of B​​​​Out[P] ——怎么理解,就是基于控制流而得到。
    解释:基本块B的输入 = 块B所有前驱块P的输出的并集。注意,所有前驱块意味着只要有一条路径能够到达块B,就是它的前驱,包括条件跳转与无条件跳转。

    (2)算法目的:输入CFG,计算好每个基本块的killB(程序中其它块中定义了变量v的语句)和genB(块B内的所有变量v的定义语句),输出每个基本块的IN[B]和OUT[B]。
    方法:首先所有基本块的OUT[B]初始化为空。遍历每一个基本块B,按以上两个公式计算块B的IN[B]和OUT[B],只要这次遍历时有某个块的OUT[B]发生变化,则重新遍历一次(因为程序中有循环存在,只要某块的OUT[B]变了,就意味着后继块的IN[B]变了)。

    (3)实例抽象表示:设程序有n条赋值语句,用n位向量来表示能reach与不能reach。
    说明:红色-第1次遍历;蓝色-第2次遍历;绿色-第3次遍历。
    结果:3次遍历之后,每个基本块的OUT[B]都不再变化。

    现在,我们可以回想一下,数据流分析的目标是,最后得到了,每个程序点关联一个数据流值(该点所有可能的程序状态的一个抽象表示,也就是这个n位向量)。在这个过程中,我们对个基本块,不断利用基于转换规则的语义(也就是transfer functions,构成基本块的语句集)-OUT[B]、控制流的约束-IN[B],最终得到一个稳定的安全的近似约束集。
    (4)算法会停止吗?OUT[B]=genBU(IN[B]−killB)OUT[B] = gen_B U (IN[B] - kill_B)OUT[B]=gen​B​​U(IN[B]−kill​B​​)大致理解:genB和 killB是不变的,只有IN[B]在变化,所以说OUT[B]只会增加不会减少,n向量长度是有限的,所以最终肯定会停止。具体涉及到不动点证明,后续课程会讲解。
    4.Live Variables Analysis (may analysis)问题定义:某程序点p处的变量v,从p开始到exit块的CFG中是否有某条路径用到了v,如果用到了v,则v在p点为live,否则为dead。其中有一个隐含条件,在点p和引用点之间不能重定义v。

    应用场景:可用于寄存器分配,如果寄存器满了,就需要替换掉不会被用到的变量。
    抽象表示:程序中的n个变量用长度为n bit的向量来表示,对应bit为1,则该变量为live,反之为0则为dead。
    (1)公式分析Control Flow:OUT[B]=USa successor of BIN[S]OUT[B] = U_{S_{a \space successor \space of \space B}} IN[S]OUT[B]=U​S​a successor of B​​​​IN[S]
    理解:我们是前向分析,只要有一条子路是live,父节点就是live。
    Transfer Function:IN[B]=useBU(OUT[B]−defB)IN[B] = use_B U (OUT[B] - def_B)IN[B]=use​B​​U(OUT[B]−def​B​​)
    理解:IN[B] = 本块中use出现在define之前的变量 U (OUT[B]出口的live情况 - 本块中出现了define的变量)。define指的是定义/赋值。
    特例分析:如以下图所示,第4种情况,v=v-1,实际上use出现在define之前,v是使用的。

    (2)算法目的:输入CFG,计算好每个基本块中的defB(重定义)和useB(出现在重定义之前的使用)。输出每个基本块的IN[B]和OUT[B]。
    方法:首先初始化每个基本块的IN[B]为空集。遍历每一个基本块B,按以上两个公式计算块B的OUT[B]和IN[B],只要这次遍历时有某个块的IN[B]发生变化,则重新遍历一次(因为有循环,只要某块的IN[B]变了,就意味前驱块的OUT[B]变了)。
    问题:遍历基本块的顺序有要求吗? 没有要求,但是会影响遍历的次数。

    初始化规律:一般情况下,may analysis 全部初始化为空,must analysis全部初始化为all。
    (3)实例抽象表示:程序中的n个变量用长度为n bit的向量来表示,对应bit为1,则该变量为live,反之为0则为dead。
    说明:从下往上遍历基本块,黑色-初始化;红色-第1次;蓝色-第2次;绿色-第3次。
    结果:3次遍历后,IN[B]不再变化,遍历结束。

    5.Available Expressions Analysis (must analysis)问题定义:程序点p处的表达式x op y可用需满足2个条件,一是从entry到p点必须经过x op y,二是最后一次使用x op y之后,没有重定义操作数x、y。(如果重定义了x 或 y,如x = a op2 b,则原来的表达式x op y中的x或y就会被替代)。
    应用场景:用于优化,检测全局公共子表达式。
    抽象表示:程序中的n个表达式,用长度为n bit的向量来表示,1表示可用,0表示不可用。
    说明:属于forward分析。
    (1)公式分析Transfer Function:OUT[B]=genBU(IN[B]−killB)OUT[B] = gen_B U (IN[B] - kill_B)OUT[B]=gen​B​​U(IN[B]−kill​B​​)
    理解:genB—基本块B中所有新的表达式(并且在这个表达式之后,不能对表达式中出现的变量进行重定义)—>加入到OUT;killB—从IN中删除变量被重新定义的表达式。
    Control Flow:IN[B]=∩Pa predecessor of BOUT[P]IN[B] = \cap_{P_{a \space predecessor \space of \space B}} OUT[P]IN[B]=∩​P​a predecessor of B​​​​OUT[P]
    IN[B]=∩Pa predecessor of BOUT[P]IN[B] = \cap_{P_{a \space predecessor \space of \space B}} OUT[P]IN[B]=∩​P​a predecessor of B​​​​OUT[P]理解:从entry到p点的所有路径都必须经过该表达式。

    问题:该分析为什么属于must analysis呢?因为我们允许有漏报,不能有误报,比如以上示例中,改为x=3,去掉 b=e16∗xb=e^{16}*xb=e​16​​∗x,该公式会把该表达式识别为不可用。但事实是可用的,因为把x=3替换到表达式中并不影响该表达式的形式。这里虽然漏报了,但是不影响程序分析结果的正确性。
    (2)算法目的:输入CFG,提前计算好genB和killB。
    方法:首先将OUT[entry]初始化为空,所有基本块的OUT[B]初始化为1…1。遍历每一个基本块B,按以上两个公式计算块B的IN[B]和OUT[B],只要这次遍历时有某个块的OUT[B]发生变化,则重新遍历一次(因为有循环,只要某块的OUT[B]变了,就意味后继块的IN[B]变了)。

    (3)实例抽象表示:程序中的n个表达式,用长度为n bit的向量来表示,1表示可用,0表示不可用。
    说明:黑色-初始化;红色-第1次;蓝色-第2次。
    结果:2次遍历后,OUT[B]不再变化,遍历结束。

    6.三种分析技术对比
    问题:怎样判断是May还是Must?
    Reaching Definitions表示只要从赋值语句到点p存在1条路径,则为reaching,结果不一定正确;Live Variables表示只要从点p到Exit存在1条路径使用了变量v,则为live,结果不一定正确;Available Expressions表示从Entry到点p的每一条路径都经过了该表达式,则为available,结果肯定正确。
    0 留言 2020-07-09 10:52:38 奖励30点积分
  • 【课程笔记】南大软件分析课程2——IR


    最近在看“静态分析”技术相关的文章,看到这个系列的笔记和视频教程,感觉介绍得很好,通俗易懂,而且还比较详细,故转载分享,同时也备份保留下,方便自己今后阅读。(PS:建议大家一边看笔记,一边看视频,加深理解)原作者:bsauce原文链接:https://www.jianshu.com/p/acb73f72cf46

    首先非常感谢南京大学李樾和谭添老师的无私分享,之前学习程序分析是看的北大熊英飞老师的ppt,但是很多地方没看懂,正如李樾老师所说的那样,熊英飞老师的授课涵盖非常广,不听课只看ppt的话,理解起来还是很有难度的。但李樾老师的视频就讲解的非常易懂,示例都是精心挑选的,所以墙裂推荐。
    推送门:南大课件 南大视频课程 北大课件

    目录
    编译器和静态分析的关系AST vs IRIR:3-地址代码(3AC)实际静态分析器的3AC—Soot(Java)SSA-静态单赋值基本块(BB)控制流图(CFG)
    1.编译器和静态分析的关系源码->(Scanner - 词法Lexical分析-Regular Expression)->(Parser- 语法Syntax分析-Context-Free Grammar), 生成AST ->(Type Checker - 语义Semantic分析 - Attribute Grammar),生成 Decorated AST -> Translator,生成IR,进行静态分析 -> Code Generator

    2.AST vs IR
    AST :高级,更接近于语法结构,依赖于语言种类,适用于快速类型检查,缺少控制流信息
    IR:低级,更接近于机器码,不依赖语言种类,压缩且简洁,包含控制流信息。是静态分析的基础


    3.IR:3-地址代码(3AC)// 最多1个操作符a+b+3 -> t1 = a+b t2 = t1+3Address: Name:a、b Constant: 3 编译器的临时变量:t1、t2

    4.实际静态分析器的3AC—Soot(Java)Soot-常用的Java静态分析框架
    // java IR(Jimple)基本知识invokespecial:call constructor, call superclass methods, call private methodsinvokevirtual: instance methods call (virtual dispatch)invokeinterface: cannot optimization, checking interface implementationinvokestation:call static methodsJava 7: invokedynamic -> Java static typing, dynamic language runs on JVMmethod signature: class name, return type, method name(parameter1 type, parameter2 type)
    5.SSA-静态单赋值定义:给每一个定义变量一个新的名字,传递到接下来的使用当中,每个变量有1个定义(赋值的目标变量)。

    优点:唯一的变量名可以间接体现程序流信息,简化分析过程;清楚的Define-Use信息。
    缺点:引入很多变量和phi-function;转换为机器码时效率变低(引入很多拷贝操作)。
    6.基本块(BB)定义:只有1个开头入口和1个结尾出口的最长3-地址指令序列。
    识别基本块的算法:首先确定入口指令,第一条指令是入口;任何跳转指令的目标地址是入口;任何跟在跳转指令之后的指令是入口。然后构造基本块,任何基本块包含1个入口指令和其接下来的指令。
    我的想法:对于下1条指令,若该指令不是入口,则可以加入;若该指令有多个出口,则停止加入,否则继续判断下一条指令。

    7.控制流图(CFG)控制流边:基本块A的结尾有跳转指令跳转到基本块B;原始指令序列中,B紧跟着A,且A的结尾不是无条件跳转。

    添加Entry / Exit:没有块跳转到该块 / 没有跳转到其他块。
    0 留言 2020-07-08 13:04:54 奖励30点积分
  • 【课程笔记】南大软件分析课程1——课程介绍


    最近在看“静态分析”技术相关的文章,看到这个系列的笔记和视频教程,感觉介绍得很好,通俗易懂,而且还比较详细,故转载分享,同时也备份保留下,方便自己今后阅读。(PS:建议大家一边看笔记,一边看视频,加深理解)原作者:bsauce原文链接:https://www.jianshu.com/p/8d06766d232c

    首先非常感谢南京大学李樾和谭添老师的无私分享,之前学习程序分析是看的北大熊英飞老师的ppt,但是很多地方没看懂,正如李樾老师所说的那样,熊英飞老师的授课涵盖非常广,不听课只看ppt的话,理解起来还是很有难度的。但李樾老师的视频就讲解的非常易懂,示例都是精心挑选的,所以墙裂推荐。
    推送门:南大课件 南大视频课程 北大课件
    我觉得上这门课,最大的收获就是,锻炼出一种软件分析的程序化思维。之所以做这个笔记,是为了总结和方便回看,毕竟回看笔记比回看视频快很多。
    讲数据流分析的时候,关键是首先抽象表示数据(一般是用向量),然后设计transfer function转换规则和control flow控制流规则,然后遍历基本块,根据这两个规则去计算,一旦某个基本块的抽象表示改变了,则再次遍历一遍。这对于我们以后设计数据流分析算法是很有帮助的,我们需要思考所要解决的问题到底是forward还是backward,是may还是must analysis,这相当于是一个分析模板。

    本课程主要内容:IR,数据流分析,过程间分析,CFL可达性和IFDS,指针分析,抽象解释。
    1.PL—Programming Languages
    理论:语言设计,类型系统,语义和逻辑
    环境:编译器,运行系统
    应用:程序分析,程序验证,程序合成
    技术:抽象解释(Abstract interpretation),数据流分析(Data-flow analysis, ),Hoare logic,Model checking,Symbolic execution等等

    静态分析作用:程序可靠性、程序安全性、编译优化、程序理解(调用关系、类型识别)。
    2.soundness与completeness
    soundness:对程序进行了over-approximate过拟合,不会漏报(有false positives误报)
    completeness:对程序进行了under-approximate欠拟合,不会误报(有false negatives漏报)

    很多重要领域如军工、航天领域,我们追求的是soundness,但是要平衡精度和速度。那么我们绝大多数软件分析方法都做到了completeness,那么只要能证明满足soundness,那么该分析方法就是正确的。
    那么什么样的SA是完美的呢?定义是既overapproximate又underapproximate的SA是完美的。overapproximate也叫sound,underapproximate也叫complete,他们之间的关系可以用一个图很好的表示。


    sound表示报告包含了所有的真实错误,但可能包含了误报的错误,导致误报
    complete表示报告包含的错误都是真实的错误,但可能并未包含全部的错误,造成了漏报

    3.软件分析步骤
    abstraction:抽象值,定义集合(类别)
    Safe-approximation安全近似

    Transfer Functions:对抽象值的操作,转换规则Control flows
    0 留言 2020-07-08 13:04:40 奖励30点积分
  • 污点分析技术介绍


    最近在看“污点分析”技术相关的文章,看到这篇文章介绍得不错,通俗易懂,而且还比较详细,故转载分享,同时也备份保留下,方便自己今后阅读。
    原文链接:https://github.com/firmianay/CTF-All-In-One/blob/master/doc/5.5_taint_analysis.md

    一、静态污点分析1.1 基本原理污点分析是一种跟踪并分析污点信息在程序中流动的技术。在漏洞分析中,使用污点分析技术将所感兴趣的数据(通常来自程序的外部输入)标记为污点数据,然后通过跟踪和污点数据相关的信息的流向,可以知道它们是否会影响某些关键的程序操作,进而挖掘程序漏洞。即将程序是否存在某种漏洞的问题转化为污点信息是否会被 Sink 点上的操作所使用的问题。
    污点分析常常包括以下几个部分:

    识别污点信息在程序中的产生点(Source点)并对污点信息进行标记
    利用特定的规则跟踪分析污点信息在程序中的传播过程
    在一些关键的程序点(Sink点)检测关键的操作是否会受到污点信息的影响

    举个例子:
    [...]scanf("%d", &x); // Source 点,输入数据被标记为污点信息,并且认为变量 x 是污染的[...]y = x + k; // 如果二元操作的操作数是污染的,那么操作结果也是污染的,所以变量 y 也是污染的[...]x = 0; // 如果一个被污染的变量被赋值为一个常数,那么认为它是未污染的,所以 x 转变成未污染的[...]while (i < y) // Sink 点,如果规定循环的次数不能受程序输入的影响,那么需要检查 y 是否被污染
    然而污点信息不仅可以通过数据依赖传播,还可以通过控制依赖传播。我们将通过数据依赖传播的信息流称为显式信息流,将通过控制依赖传播的信息流称为隐式信息流。
    举个例子:
    if (x > 0) y = 1;else y = 0;
    变量 y 的取值依赖于变量 x 的取值,如果变量 x 是污染的,那么变量 y 也应该是污染的。
    通常我们将使用污点分析可以检测的程序漏洞称为污点类型的漏洞,例如 SQL 注入漏洞:
    String user = getUser();String pass = getPass();String sqlQuery = "select * from login where user='" + user + "' and pass='" + pass + "'";Statement stam = con.createStatement();ResultSetrs = stam.executeQuery(sqlQuery);if (rs.next()) success = true;
    在进行污点分析时,将变量 user 和 pass 标记为污染的,由于变量 sqlQuery 的值受到 user 和 pass 的影响,所以将 sqlQuery 也标记为污染的。程序将变量 sqlQuery 作为参数构造 SQL 操作语句,于是可以判定程序存在 SQL 注入漏洞。
    使用污点分析检测程序漏洞的工作原理如下图所示:


    基于数据流的污点分析:在不考虑隐式信息流的情况下,可以将污点分析看做针对污点数据的数据流分析。根据污点传播规则跟踪污点信息或者标记路径上的变量污染情况,进而检查污点信息是否影响敏感操作
    基于依赖关系的污点分析:考虑隐式信息流,在分析过程中,根据程序中的语句或者指令之间的依赖关系,检查 Sink 点处敏感操作是否依赖于 Source 点处接收污点信息的操作

    1.2 方法实现静态污点分析系统首先对程序代码进行解析,获得程序代码的中间表示,然后在中间表示的基础上对程序代码进行控制流分析等辅助分析,以获得需要的控制流图、调用图等。在辅助分析的过程中,系统可以利用污点分析规则在中间表示上识别程序中的 Source 点和 Sink 点。最后检测系统根据污点分析规则,利用静态污点分析检查程序是否存在污点类型的漏洞。
    1.2.1 基于数据流的污点分析在基于数据流的污点分析中,常常需要一些辅助分析技术,例如别名分析、取值分析等,来提高分析精度。辅助分析和污点分析交替进行,通常沿着程序路径的方向分析污点信息的流向,检查 Source 点处程序接收的污点信息是否会影响到 Sink 点处的敏感操作。
    过程内的分析中,按照一定的顺序分析过程内的每一条语句或者指令,进而分析污点信息的流向。

    记录污点信息:在静态分析层面,程序变量的污染情况为主要关注对象。为记录污染信息,通常为变量添加一个污染标签。最简单的就是一个布尔型变量,表示变量是否被污染。更复杂的标签还可以记录变量的污染信息来自哪些 Source 点,甚至精确到 Source 点接收数据的哪一部分。当然也可以不使用污染标签,这时我们通过对变量进行跟踪的方式达到分析污点信息流向的目的。例如使用栈或者队列来记录被污染的变量
    程序语句的分析:在确定如何记录污染信息后,将对程序语句进行静态分析。通常我们主要关注赋值语句、控制转移语句以及过程调用语句三类:

    赋值语句

    对于简单的赋值语句,形如 a = b 这样的,记录语句左端的变量和右端的变量具有相同的污染状态。程序中的常量通常认为是未污染的,如果一个变量被赋值为常量,在不考虑隐式信息流的情况下,认为变量的状态在赋值后是未污染的
    对于形如 a = b + c 这样带有二元操作的赋值语句,通常规定如果右端的操作数只要有一个是被污染的,则左端的变量是污染的(除非右端计算结果为常量)
    对于和数组元素相关的赋值,如果可以通过静态分析确定数组下标的取值或者取值范围,那么就可以精确地判断数组中哪个或哪些元素是污染的。但通常静态分析不能确定一个变量是污染的,那么就简单地认为整个数组都是污染的
    对于包含字段或者包含指针操作的赋值语句,常常需要用到指向分析的分析结果

    控制转移语句

    在分析条件控制转移语句时,首先考虑语句中的路径条件可能是包含对污点数据的限制,在实际分析中常常需要识别这种限制污点数据的条件,以判断这些限制条件是否足够包含程序不会受到攻击。如果得出路径条件的限制是足够的,那么可以将相应的变量标记为未污染的
    对于循环语句,通常规定循环变量的取值范围不能受到输入的影响。例如在语句 for (i = 1; i < k; i++){} 中,可以规定循环的上界 k 不能是污染的

    过程调用语句

    可以使用过程间的分析或者直接应用过程摘要进行分析。污点分析所使用的过程摘要主要描述怎样改变与该过程相关的变量的污染状态,以及对哪些变量的污染状态进行检测。这些变量可以是过程使用的参数、参数的字段或者过程的返回值等。例如在语句 flag = obj.method(str); 中,str 是污染的,那么通过过程间的分析,将变量 obj 的字段 str 标记为污染的,而记录方法的返回值的变量 flag 标记为未污染的
    在实际的过程间分析中,可以对已经分析过的过程构建过程摘要。例如前面的语句,其过程摘要描述为:方法 method 的参数污染状态决定其接收对象的实例域 str 的污染状态,并且它的返回值是未受污染的。那么下一次分析需要时,就可以直接应用摘要进行分析


    代码的遍历:一般情况下,常常使用流敏感的方式或者路径敏感的方式进行遍历,并分析过程中的代码。如果使用流敏感的方式,可以通过对不同路径上的分析结果进行汇集,以发现程序中的数据净化规则。如果使用路径敏感的分析方式,则需要关注路径条件,如果路径条件中涉及对污染变量取值的限制,可认为路径条件对污染数据进行了净化,还可以将分析路径条件对污染数据的限制进行记录,如果在一条程序路径上,这些限制足够保证数据不会被攻击者利用,就可以将相应的变量标记为未污染的

    过程间的分析与数据流过程间分析类似,使用自底向上的分析方法,分析调用图中的每一个过程,进而对程序进行整体的分析。
    1.2.2 基于依赖关系的污点分析在基于依赖关系的污点分析中,首先利用程序的中间表示、控制流图和过程调用图构造程序完整的或者局部的程序的依赖关系。在分析程序依赖关系后,根据污点分析规则,检测 Sink 点处敏感操作是否依赖于 Source 点。
    分析程序依赖关系的过程可以看做是构建程序依赖图的过程。程序依赖图是一个有向图。它的节点是程序语句,它的有向边表示程序语句之间的依赖关系。程序依赖图的有向边常常包括数据依赖边和控制依赖边。在构建有一定规模的程序的依赖图时,需要按需地构建程序依赖关系,并且优先考虑和污点信息相关的程序代码。
    1.3 实例分析在使用污点分析方法检测程序漏洞时,污点数据相关的程序漏洞是主要关注对象,如 SQL 注入漏洞、命令注入漏洞和跨站脚本漏洞等。
    下面是一个存在 SQL 注入漏洞 ASP 程序的例子:
    <% Set pwd = "bar" Set sql1 = "SELECT companyname FROM " & Request.Cookies("hello") Set sql2 = Request.QueryString("foo") MySqlStuff pwd, sql1, sql2 Sub MySqlStuff(password, cmd1, cmd2) Set conn = Server.CreateObject("ADODB.Connection") conn.Provider = "Microsoft.Jet.OLEDB.4.0" conn.Open "c:/webdata/foo.mdb", "foo", password Set rs = conn.Execute(cmd2) Set rs = Server.CreateObject("ADODB.recordset") rs.Open cmd1, conn End Sub%>
    首先对这段代码表示为一种三地址码的形式,例如第 3 行可以表示为:
    a = "SELECT companyname FROM "b = "hello"param0 Requestparam1 bcallCookiesreturn csql1 = a & c
    解析完毕后,需要对程序代码进行控制流分析,这里只包含了一个调用关系(第 5 行)。
    接下来,需要识别程序中的 Source 点和 Sink 点以及初始的被污染的数据。
    具体的分析过程如下:

    调用 Request.Cookies(“hello”) 的返回结果是污染的,所以变量 sql1 也是污染的
    调用 Request.QueryString(“foo”) 的返回结果 sql2 是污染的
    函数 MySqlStuff 被调用,它的参数 sql1,sql2 都是污染的。分了分析函数的处理过程,根据第 6 行函数的声明,标记其参数 cmd1,cmd2 是污染的
    第 10 行是程序的 Sink 点,函数 conn.Execute 执行 SQL 操作,其参数 cmd2 是污染的,进而发现污染数据从 Source 点传播到 Sink 点。因此,认为程序存在 SQL 注入漏洞

    二、动态污点分析2.1 动态污点分析的基本原理动态污点分析是在程序运行的基础上,对数据流或控制流进行监控,从而实现对数据在内存中的显式传播、数据误用等进行跟踪和检测。动态污点分析与静态污点分析的唯一区别在于静态污点分析技术在检测时并不真正运行程序,而是通过模拟程序的执行过程来传播污点标记,而动态污点分析技术需要运行程序,同时实时传播并检测污点标记。
    动态污点分析技术可分为三个部分:

    污点数据标记:程序攻击面是程序接受输入数据的接口集,一般由程序入口点和外部函数调用组成。在污点分析中,来自外部的输入数据会被标记为污点数据。根据输入数据来源的不同,可分为三类:网络输入、文件输入和输入设备输入
    污点动态跟踪:在污点数据标记的基础上,对进程进行指令粒度的动态跟踪分析,分析每一条指令的效果,直至覆盖整个程序的运行过程,跟踪数据流的传播

    动态污点跟踪通常基于以下三种机制

    动态代码插桩:可以跟踪单个进程的污点数据流动,通过在被分析程序中插入分析代码,跟踪污点信息流在进程中的流动方向
    全系统模拟:利用全系统模拟技术,分析模拟系统中每条指令的污点信息扩散路径,可以跟踪污点数据在操作系统内的流动
    虚拟机监视器:通过在虚拟机监视器中增加分析污点信息流的功能,跟踪污点数据在整个客户机中各个虚拟机之间的流动

    污点动态跟踪通常需要影子内存(shadow memory)来映射实际内存的污染情况,从而记录内存区域和寄存器是否是被污染的。对每条语句进行分析的过程中,污点跟踪攻击根据影子内存判断是否存在污点信息的传播,从而对污点信息进行传播并将传播结果保存于影子内存中,进而追踪污点数据的流向
    一般情况下,数据移动类和算数类指令都将造成显示的信息流传播。为了跟踪污点数据的显示传播,需要在每个数据移动指令和算数指令执行前做监控,当指令的结果被其中一个操作数污染后,把结果数据对应的影子内存设置为一个指针,指向源污染点操作数指向的数据结构

    污点误用检查:在正确标记污点数据并对污点数据的传播进行实时跟踪后,就需要对攻击做出正确的检测即检测污点数据是否有非法使用的情况

    动态污点分析的优缺点:

    优点

    误报率较低检测结果的可信度较高。
    缺点

    漏报率较高:由于程序动态运行时的代码覆盖率决定的。平台相关性较高:特定的动态污点分析工具只能够解决在特定平台上运行的程序。资源消耗大:包括空间上和时间上。

    2.2 动态污点分析的方法实现2.2.1 污点数据标记污点数据通常主要是指软件系统所接受的外部输入数据,在计算机中,这些数据可能以内存临时数据的形式存储,也可能以文件的形式存储。当程序需要使用这些数据时,一般通过函数或系统调用来进行数据访问和处理,因此只需要对这些关键函数进行监控,即可得到程序读取或输出了什么污点信息。另外对于网络输入,也需要对网络操作函数进行监控。
    识别出污点数据后,需要对污点进行标记。污点生命周期是指在该生命周期的时间范围内,污点被定义为有效。污点生命周期开始于污点创建时刻,生成污点标记,结束于污点删除时刻,清除污点标记。

    污点创建

    将来自于非可靠来源的数据分配给某寄存器或内存操作数时将已经标记为污点的数据通过运算分配给某寄存器或内存操作数时
    污点删除

    将非污点数据指派给存放污点的寄存器或内存操作数时将污点数据指派给存放污点的寄存器或内存地址时,此时会删除原污点,并创建新污点一些会清除污点痕迹的算数运算或逻辑运算操作时

    2.2.2 污点动态跟踪当污点数据从一个位置传递到另一个位置时,则认为产生了污点传播。污点传播规则:



    指令类型
    传播规则
    举例说明




    拷贝或移动指令
    T(a)<-T(b)
    mov a, b


    算数运算指令
    T(a)<-T(b)
    add a, b


    堆栈操作指令
    T(esp)<-T(a)
    push a


    拷贝或移动类函数调用指令
    T(dst)<-T(src)
    call memcpy


    清零指令
    T(a)<-false
    xor a, a



    注:T(x) 的取值分为 true 和 false 两种,取值为 true 时表示 x 为污点,否则 x 不是污点。
    对于污点信息流,通过污点跟踪和函数监控,已经能够进行污点信息流流动方向的分析。但由于缺少对象级的信息,仅靠指令级的信息流动并不能完全给出要分析的软件的确切行为。因此,需要在函数监控的基础上进行视图重建,如获取文件对象和套接字对象的详细信息,以方便进一步的分析工作。
    根据漏洞分析的实际需求,污点分析应包括两方面的信息:

    污点的传播关系,对于任一污点能够获知其传播情况
    对污点数据进行处理的所有指令信息,包括指令地址、操作码、操作数以及在污点处理过程中这些指令执行的先后顺序等

    污点动态跟踪的实现通常使用:

    影子内存:真实内存中污点数据的镜像,用于存放程序执行的当前时刻所有的有效污点
    污点传播树:用于表示污点的传播关系
    污点处理指令链:用于按时间顺序存储与污点数据处理相关的所有指令

    当遇到会引起污点传播的指令时,首先对指令中的每个操作数都通过污点快速映射查找影子内存中是否存在与之对应的影子污点从而确定其是否为污点数据,然后根据污点传播规则得到该指令引起的污点传播结果,并将传播产生的新污点添加到影子内存和污点传播树中,同时将失效污点对应的影子污点删除。同时由于一条指令是否涉及污点数据的处理,需要在污点分析过程中动态确定,因此需要在污点处理指令链中记录污点数据的指令信息。
    2.2.3 污点误用检查污点敏感点,即 Sink 点,是污点数据有可能被误用的指令或系统调用点,主要分为:

    跳转地址:检查污点数据是否用于跳转对象,如返回地址、函数指针、函数指针偏移等。具体操作是在每个跳转类指令(如call、ret、jmp等)执行前进行监控分析,保证跳转对象不是污点数据所在的内存地址
    格式化字符串:检查污点数据是否用作printf系列函数的格式化字符串参数
    系统调用参数:检查特殊系统调用的特殊参数是否为污点数据
    标志位:跟踪标志位是否被感染,及被感染的标志位是否用于改变程序控制流
    地址:检查数据移动类指令的地址是否被感染

    在进行污点误用检查时,通常需要根据一些漏洞模式来进行检查,首先需要明确常见漏洞在二进制代码上的表现形式,然后将其提炼成漏洞模式,以更有效地指导自动化的安全分析。
    2.3 动态污点分析的实例分析下面我们来看一个使用动态污点分析的方法检测缓冲区溢出漏洞的例子。
    void fun(char *str){ char temp[15]; printf("in strncpy, source: %s\n", str); strncpy(temp, str, strlen(str)); // Sink 点}int main(int argc, char *argv[]){ char source[30]; gets(source); // Source 点 if (strlen(source) < 30) fun(source); else printf("too long string, %s\n", source); return 0;}
    漏洞很明显, 调用 strncpy 函数存在缓冲区溢出。
    程序接受外部输入字符串的二进制代码如下:
    0x08048609 <+51>: lea eax,[ebp-0x2a]0x0804860c <+54>: push eax0x0804860d <+55>: call 0x8048400 <gets@plt>...0x0804862c <+86>: lea eax,[ebp-0x2a]0x0804862f <+89>: push eax0x08048630 <+90>: call 0x8048566 <fun>
    程序调用 strncpy 函数的二进制代码如下:
    0x080485a1 <+59>: push DWORD PTR [ebp-0x2c]0x080485a4 <+62>: call 0x8048420 <strlen@plt>0x080485a9 <+67>: add esp,0x100x080485ac <+70>: sub esp,0x40x080485af <+73>: push eax0x080485b0 <+74>: push DWORD PTR [ebp-0x2c]0x080485b3 <+77>: lea eax,[ebp-0x1b]0x080485b6 <+80>: push eax0x080485b7 <+81>: call 0x8048440 <strncpy@plt>
    首先,在扫描该程序的二进制代码时,能够扫描到 call <gets@plt>,该函数会读入外部输入,即程序的攻击面。确定了攻击面后,我们将分析污染源数据并进行标记,即将 [ebp-0x2a] 数组(即源程序中的source)标记为污点数据。程序继续执行,该污染标记会随着该值的传播而一直传递。在进入 fun() 函数时,该污染标记通过形参实参的映射传递到参数 str 上。然后运行到 Sink 点函数 strncpy()。该函数的第二个参数即 str 和 第三个参数 strlen(str) 都是污点数据。最后在执行 strncpy() 函数时,若设定了相应的漏洞规则(目标数组小于源数组),则漏洞规则将被触发,检测出缓冲区溢出漏洞。
    0 留言 2020-07-07 09:30:59 奖励25点积分
  • 程序验证(十二):完全正确性


    版权声明:本文为CSDN博主「swy_swy_swy」的原创文章,遵循CC 4.0 BY-SA版权协议,转载请附上原文出处链接及本声明。原文链接:https://blog.csdn.net/swy_swy_swy/article/details/106844776

    一、完全正确性完全正确性(total correctness),写作:
    [P]c[Q][P]c[Q][P]c[Q]意思是:

    如果我们从一个满足PPP的环境开始执行ccc
    那么ccc一定终止
    且它的最终的环境满足QQQ

    二、良基关系(Well-Founded Relations)集合SSS上的一个二元关系≺\prec≺是一个良基关系,当且仅当:

    在SSS中不存在无限序列s1,s2,s3,..s_1,s_2,s_3,..s​1​​,s​2​​,s​3​​,..,使得对于所有i>0i > 0i>0都有si+1≺sis_{i+1}\prec s_is​i+1​​≺s​i​​
    也就是说,SSS中每个下降序列都是有限的

    2.1 词法意义上的良基关系给定集合S1,..,SnS_1,.. ,S_nS​1​​,..,S​n​​和关系≺1,..,≺n\prec_1 ,.. ,\prec_n≺​1​​,..,≺​n​​ ,令S1×..×S_1\times .. \timesS​1​​×..×
    定义关系≺\prec≺:
    (s1,..,sn)≺(t1,..,tn)⇔⋁i=1n(si≺iti∧⋀j=1i−1sj=tj)(s_1 ,.. ,s_n)\prec (t_1 ,.. ,t_n)\Leftrightarrow \bigvee ^n_{i=1} (s_i\prec_i t_i\wedge\bigwedge ^{i-1}_{j=1} s_j=t_j)(s​1​​,..,s​n​​)≺(t​1​​,..,t​n​​)⇔⋁​i=1​n​​(s​i​​≺​i​​t​i​​∧⋀​j=1​i−1​​s​j​​=t​j​​)解释一下,(s1,..,sn)≺(t1,..,tn)(s_1 ,.. ,s_n)\prec (t_1 ,.. ,t_n)(s​1​​,..,s​n​​)≺(t​1​​,..,t​n​​)当且仅当:

    在某一位置iii,si≺itis_i\prec_i t_is​i​​≺​i​​t​i​​
    而对于所有之前的位置jjj,sj=tjs_j=t_js​j​​=t​j​​

    2.2 证明完全正确性为了证明程序终止,我们需要:

    在程序的状态上构造一个良基关系≺\prec≺
    证明每一个基础路径的的输出状态都“小于”输入状态

    如果满足以上两点,那么程序一定终止,否则就存在一个程序状态的无限序列,这可以被映射到≺\prec≺上的一个无限下降序列。
    与以上两步相对应,我们需要:

    找到一个函数δ\deltaδ将程序状态映射到一个带有已知良基关系≺\prec≺的集合SSS
    证明δ\deltaδ在每一个基础路径上依据≺\prec≺都是下降的

    函数δ\deltaδ被称为秩函数(ranking function)。
    2.3 对于秩函数的注释我们用带有↓\downarrow↓的代码注释秩函数,需要在函数的循环头位置注释。
    2.4 vcvcvcvc即为:
    P→wlp(c1;..;cn,δ(x)≺δ(x′))[x/x′]P\to wlp(c_1; .. ;c_n,\delta (x)\prec \delta (x'))[x/x']P→wlp(c​1​​;..;c​n​​,δ(x)≺δ(x​′​​))[x/x​′​​]计算的时候用x′x^{\prime}x​′​​代表开始时xxx的值,计算完毕后再换回来。
    0 留言 2020-09-13 11:12:24 奖励30点积分
  • 程序验证(十一):演绎验证(下)


    版权声明:本文为CSDN博主「swy_swy_swy」的原创文章,遵循CC 4.0 BY-SA版权协议,转载请附上原文出处链接及本声明。原文链接:https://blog.csdn.net/swy_swy_swy/article/details/106797717

    一、新特征引入向Imp语言引入新的特征:

    断言注释(assertion annotation)
    过程(procedure)

    1.1 断言断言注释具有以下形式:
    {P}\{P\}{P}从语义上说,它们与运行时断言(runtime assertion)一样(比如c里面的assert)。如果当前环境使得断言表达式为假,程序停止执行。
    1.2 程序举个例子:

    这个过程就是一个带有注释的过程:

    前置条件由requires注释
    后置条件由ensures注释
    前置条件与后置条件中的自由变量可以是形式参数
    后置条件也可以包括特殊的变量rvrvrv,代表返回值(return value)

    二、部分正确性的证明一个程序(program)是部分正确的,如果对于它的每个过程(procedure)PPP都有:

    只要PPP的前置条件在过程的入口处被满足
    那么PPP的后置条件一定在过程的出口处被满足

    我们从基本思路:

    使用注释(annotation)把程序分为更简单的几部分
    独立地为每个部分生成vcvcvc,假定每个注释都成立
    根据每个部分的正确性,推出整体的正确性

    2.1 基本路径(Basic Paths)一个基本路径是一系列指令,满足:

    开始于一个过程的前置条件或循环不变量
    终止于一个循环不变量,一个断言或一个过程的后置条件
    不穿过循环:循环不变量只在路径的开头或结尾出现

    2.2 假设(assume)语句assume b的意思:

    只有当b在当前环境下为真,路径的剩余部分才可以执行
    当讨论剩余的路径时,我们可以假定b成立

    2.3 路径分割每一个assume,都引入两个分支,一个假定bbb成立,一个假定¬b\neg b¬b成立,所以在之前的例子里,有更多的基本路径。
    如何计算基本路径有多少呢?当我们计算基础路径的数量时,我们遵循深度优先的习惯。
    当遇到一个assume时:

    先假定它成立,然后生成相应的路径
    再假定它不成立,重复

    2.4 过程调用(Procedure Call)可以把过程调用替换为后置条件断言,需要引入另一个基础路径以确保前置条件成立,将前置条件与后置条件中的形式参数换为在调用中真正出现的参数。
    综上,过程调用的步骤为:
    1.给定一个过程fff具有以下原型:

    2.当fff在上下文w:=f(e1,..,en)w:=f(e_1 ,.. ,e_n)w:=f(e​1​​,..,e​n​​)中被调用时,用断言{P[e1,..,en]}\lbrace P[e_1,.. ,e_n] \rbrace{P[e​1​​,..,e​n​​]}表示调用上下文
    3.在穿过调用的路径中

    创建新的变量vvv来存放返回值
    将调用替换为后置条件的假定:


    三、vc生成当我们列举基础路径时,我们实际上得到了vcvcvc。
    注意,由于基础路径不穿过循环,所以我们只需要为三种命令生成vcvcvc:

    赋值:见上文
    序列:见上文
    assume:


    举例:
    0 留言 2020-07-03 10:12:16 奖励30点积分
  • 程序验证(十):演绎验证(上)


    版权声明:本文为CSDN博主「swy_swy_swy」的原创文章,遵循CC 4.0 BY-SA版权协议,转载请附上原文出处链接及本声明。原文链接:https://blog.csdn.net/swy_swy_swy/article/details/106751208

    一、基础路径(Basic Approach)给定一个程序ccc,由以下specification注解:
    {P}c{Q}\{P\}c\{Q\}{P}c{Q}为了证明这个三元组,我们构造一个验证条件(verification condition, VC)的集合:

    每个VC都是某个理论的一阶公式
    如果所有的VC都是永真的,那么{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbrace{P}c{Q}就是永真的

    二、谓词转换器给定一个断言QQQ和一个程序ccc,一个谓词转换器(predicate transformer)是一个函数,输出另一个断言。
    最弱前置条件(weakest precondition)谓词转换器产生一个wp(c,Q)wp(c,Q)wp(c,Q),使得:

    对于[wp(c,Q)]c[Q][wp(c,Q)]c[Q][wp(c,Q)]c[Q]是永真的,且
    对于任何满足[P]c[Q][P]c[Q][P]c[Q]的PPP,P⇒wp(c,Q)P\Rightarrow wp(c,Q)P⇒wp(c,Q),也就是说,wp(c,Q)wp(c,Q)wp(c,Q)是这种断言中最弱的

    广义最弱前置条件(weakest liberal precondition)谓词转换器产生一个wlp(c,Q)wlp(c,Q)wlp(c,Q),使得:

    对于wlp(c,Q)cQ{wlp(c,Q)}c{Q}wlp(c,Q)cQ是永真的,且
    对于wlp(c,Q)wlp(c,Q)wlp(c,Q)是这种断言中最弱的

    wlpwlpwlp为我们提供了一种逆向的思路,这也符合我们的直觉。
    三、wlp的定义我们用霍尔三元组来定义wlpwlpwlp:
    wlp(y:=x+1,(∀x.x<z→x<y)→x+1≤y)=?wlp(y:=x+1, (\forall x.x < z \to x < y) \to x+1\le y)=?wlp(y:=x+1,(∀x.x<z→x<y)→x+1≤y)=?注意,答案并不是:
    (∀x.x<z→x<x+1)→x+1≤x+1(\forall x.x < z\to x < x+1) \to x+1 \le x+1(∀x.x<z→x<x+1)→x+1≤x+1因为当我们用x+1x+1x+1替换yyy以处理:
    (∀x.x<z→x<y)(\forall x.x < z\to x < y)(∀x.x<z→x<y)时,变量xxx是被捕获的(captured)
    3.1 捕获避免代入(capture-avoiding substitution)当我们扩展P[a/x]P[a/x]P[a/x]时,我们需要:

    只代入xxx的自由形式(free occurence)
    将aaa中不自由的变量重命名以避免捕获

    3.2 数组赋值规则数组赋值的霍尔规则可以表示为:
    AsgnArr {Q[x⟨a1◃a2⟩/x]}x[a1]:=a2{Q}AsgnArr~\frac{}{\{Q[x\langle a_1\triangleleft a_2\rangle /x]\}x[a_1]:=a_2\{Q\}}AsgnArr ​{Q[x⟨a​1​​◃a​2​​⟩/x]}x[a​1​​]:=a​2​​{Q}​​​​相应的转换器即为:
    wlp(x[a1]:=a2,Q)=Q[x⟨a1◃a2⟩/x]wlp (x[a_1]:=a_2,Q)=Q[x\langle a_1\triangleleft a_2\rangle /x]wlp(x[a​1​​]:=a​2​​,Q)=Q[x⟨a​1​​◃a​2​​⟩/x]举例:计算
    wlp(b[i]:=5,b[i]=5)wlp(b[i]:=5,b[i]=5)wlp(b[i]:=5,b[i]=5)wlp(b[i]:=5,b[i]=5)=(b⟨◃5⟩[i]=5)=(5=5)=truewlp(b[i]:=5,b[i]=5)=(b\langle\triangleleft 5\rangle [i]=5)=(5=5)=truewlp(b[i]:=5,b[i]=5)=(b⟨◃5⟩[i]=5)=(5=5)=true计算
    wlp(b[n]:=x,∀i.1≤i<n→b[i]≤b[i+1])wlp(b[n]:=x,\forall i.1\le i < n\to b[i]\le b[i+1])wlp(b[n]:=x,∀i.1≤i<n→b[i]≤b[i+1])进行代入
    wlp(b[n]:=x,∀i.1≤i<n→b[i]≤b[i+1])=∀i.1≤i<n→(b⟨◃x⟩)[i]≤(b⟨n◃x⟩)[i+1]=(b⟨n◃x⟩)[n−1]≤(b⟨n◃x⟩)[n]∧∀i.1≤i<n−1→(b⟨n◃x⟩)[i]≤(b⟨n◃x⟩)[i+1]wlp(b[n]:=x,\forall i.1\le i < n\to b[i]\le b[i+1])=\forall i.1\le i < n\to (b\langle\triangleleft x\rangle)[i]\le (b\langle n\triangleleft x\rangle)[i+1]=(b\langle n\triangleleft x\rangle)[n-1]\le (b\langle n\triangleleft x\rangle)[n]\wedge \forall i.1\le i < n-1\to (b\langle n\triangleleft x\rangle)[i]\le (b\langle n\triangleleft x\rangle)[i+1]wlp(b[n]:=x,∀i.1≤i<n→b[i]≤b[i+1])=∀i.1≤i<n→(b⟨◃x⟩)[i]≤(b⟨n◃x⟩)[i+1]=(b⟨n◃x⟩)[n−1]≤(b⟨n◃x⟩)[n]∧∀i.1≤i<n−1→(b⟨n◃x⟩)[i]≤(b⟨n◃x⟩)[i+1]3.3 序列(sequencing)依据霍尔规则:
    Seq {P}c1{P′}{P′}c2{Q}{P}c1;c2{Q}Seq~\frac{\{P\}c_1\{P'\}\qquad\{P'\}c_2\{Q\}}{\{P\}c_1;c_2\{Q\}}Seq ​{P}c​1​​;c​2​​{Q}​​{P}c​1​​{P​′​​}{P​′​​}c​2​​{Q}​​相应的谓词转换器即为:
    wlp(c1;c2,Q)=wlp(c1,wlp(c2,Q))wlp(c_1;c_2,Q)=wlp(c_1,wlp(c_2,Q))wlp(c​1​​;c​2​​,Q)=wlp(c​1​​,wlp(c​2​​,Q))3.4 条件依据霍尔规则:

    相应的转换器即为:

    3.5 while循环依据等价关系:

    相应的wlpwlpwlp即为,此处略,最后转了个圈又回来了。
    3.6 近似最弱前置条件一般来说,我们无法总是算出循环的wlpwlpwlp,比如上面的情况。但是,我们可以借助于循环不变式来近似它。
    下面,我们使用这种方式表示循环:
    while b do{I}cwhile~b~do\{I\}cwhile b do{I}c这里III是由程序员提供的循环不变量。
    最为直观的想法是令:
    wlp(while b do{I}c,Q)=Iwlp(while~b~do\{I\}c,Q)=Iwlp(while b do{I}c,Q)=I但此时III可能不是最弱的前置条件。
    如果我们草率地认为:
    wlp(while b do{I}c,Q)=Iwlp(while~b~do\{I\}c,Q)=Iwlp(while b do{I}c,Q)=I我们漏了两件事情:

    没有检查I∧¬bI\wedge\neg bI∧¬b得到QQQ
    我们不知道III是否真的是一个循环不变式

    所以我们需要构造一个额外的验证条件(verification condition)的集合:

    为了在执行循环后确保QQQ能够实现,需要满足两个条件:

    一是vc(while b doIc,Q)vc(while~b~do{I}c,Q)vc(while b doIc,Q)中的每一个公式都是永真的
    二是wlp(while b doIc,Q)=Iwlp(while~b~do{I}c,Q)=Iwlp(while b doIc,Q)=I一定是永真的

    3.7 构造vcwhile是唯一一个引入额外条件的命令,但是其他的声明可能也包含循环,所以:
    vc(x:=a,Q)=∅vc(x:=a,Q)=\varnothingvc(x:=a,Q)=∅vc(c1;c2,Q)=vc(c1,wlp(c2,Q))∪vc(c2,Q)vc(c_1;c_2,Q)=vc(c_1,wlp(c_2,Q))\cup vc(c_2,Q)vc(c​1​​;c​2​​,Q)=vc(c​1​​,wlp(c​2​​,Q))∪vc(c​2​​,Q)vc(if b then c1 else c2,Q)=vc(c1,Q)∪vc(c2,Q)vc(if~b~then~c_1~else~c_2,Q)=vc(c_1,Q)\cup vc(c_2,Q)vc(if b then c​1​​ else c​2​​,Q)=vc(c​1​​,Q)∪vc(c​2​​,Q)3.8 综合综上,我们得到验证:
    {P}c{Q}\{P\}c\{Q\}{P}c{Q}的通用方法:

    计算P′=wlp(c,Q)P^{\prime}=wlp(c,Q)P​′​​=wlp(c,Q)
    计算vc(c,Q)vc(c,Q)vc(c,Q)
    检查P→P′P\to P^{\prime}P→P​′​​ 的永真性
    检查每个F∈vc(c,Q)F\in vc(c,Q)F∈vc(c,Q)的永真性

    若3,4检验均通过,那么{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbrace{P}c{Q}是永真的,但反之不一定成立,因为循环不变式可能不是最弱的前置条件。
    0 留言 2020-07-02 19:18:16 奖励30点积分
  • 程序验证(九):程序正确性规范


    版权声明:本文为CSDN博主「swy_swy_swy」的原创文章,遵循CC 4.0 BY-SA版权协议,转载请附上原文出处链接及本声明。 原文链接:https://blog.csdn.net/swy_swy_swy/article/details/106725080

    什么是程序的正确性?应当在指定的前提下,进行预定的行为,达到指定的结果。
    一、部分正确性(Partial Correctness)部分正确性指的是一个程序的停止行为。
    我们将部分正确性用霍尔三元组(Hoare triples)表达:
    {P}c{Q}\{P\}c\{Q\}{P}c{Q}
    其中ccc是一个程序
    其中PPP和QQQ是一阶逻辑的断言(assertion)
    其中P,QP, QP,Q的自由变量可以在程序的变量中随意选择
    其中PPP是先验条件(precondition),QQQ是后验条件(postcondition)

    上述{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbrace{P}c{Q}的含义:

    在一个满足PPP的环境中开始执行ccc
    如果ccc终止,那么它的最终环境将满足QQQ

    注意,部分正确性没有排除以下两点:

    程序执行不终止
    程序没有从PPP开始执行

    二、完全正确性(Total Correctness)部分正确性没有要求终止,完全正确性是一个更强的声明,写作:
    [P]c[Q][P]c[Q][P]c[Q]
    如果我们从一个满足PPP的环境开始执行ccc
    那么ccc一定终止,而且它最终的环境满足QQQ

    三、断言给定三元组:
    {P}c{Q}\{P\}c\{Q\}{P}c{Q}公式PPP与QQQ是一阶断言。
    对于Imp,有用的理论是TZ∪TAT_Z\cup T_AT​Z​​∪T​A​​。PPP或QQQ中的变量包括程序变量、量词变量、其他逻辑变量,即
    vars(Q)=pvars(Q)∪qvars(Q)∪lvars(Q)vars(Q)=pvars(Q)\cup qvars(Q)\cup lvars(Q)vars(Q)=pvars(Q)∪qvars(Q)∪lvars(Q)3.1 断言的语义由于lvars(Q)lvars(Q)lvars(Q)的存在,我们不能仅依据环境σ\sigmaσ来判断QQQ的值,所以,令α\alphaα为lvars(Q)lvars(Q)lvars(Q)的变量的一个赋值,那么:

    断言的可满足性与永真性:

    如果对于所有σ\sigmaσ,σ⊨Q\sigma\models Qσ⊨Q,那么我们写作⊨Q\models Q⊨Q。
    3.2 部分正确性的语义我们说{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbrace{P}c{Q}在σ\sigmaσ中在α\alphaα下永真,写作σ⊨α{P}c{Q}\sigma\models_{\alpha} \lbrace P \rbrace c \lbrace Q \rbraceσ⊨​α​​{P}c{Q},如果:
    ∀σ′.(σ⊨αP∧⟨c,σ⟩⇓σ′)→σ′⊨αQ\forall \sigma^{\prime}.(\sigma\models_{\alpha}P\wedge \langle c,\sigma\rangle\Downarrow\sigma^{\prime})\to\sigma^{\prime}\models_{\alpha}Q∀σ​′​​.(σ⊨​α​​P∧⟨c,σ⟩⇓σ​′​​)→σ​′​​⊨​α​​Q也就是说:

    只要σ\sigmaσ在α\alphaα下满足PPP
    而且ccc在σ\sigmaσ中执行得到σ′\sigma^{\prime}σ​′​​
    那么σ′\sigma^{\prime}σ​′​​ 在α\alphaα下满足QQQ

    我们说{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbrace{P}c{Q}是永真的,写作⊨{P}c{Q}\models \lbrace P \rbrace c \lbrace Q \rbrace⊨{P}c{Q},如果:
    ∀σ,α.σ⊨α{P}c{Q}\forall \sigma,\alpha.\sigma\models_{\alpha} \{P\}c\{Q\}∀σ,α.σ⊨​α​​{P}c{Q}也就是:
    ∀σ,σ′,α.(σ⊨αP∧⟨c,σ⟩⇓σ′)→σ′⊨αQ\forall \sigma,\sigma',\alpha. (\sigma\models_{\alpha}P\wedge\langle c,\sigma\rangle\Downarrow\sigma') \to \sigma'\models_{\alpha} Q∀σ,σ​′​​,α.(σ⊨​α​​P∧⟨c,σ⟩⇓σ​′​​)→σ​′​​⊨​α​​Q四、三元组的证明(verify)我们将引入一种逻辑,该逻辑能从已知的三元组推出新的三元组,这种逻辑叫做霍尔逻辑(Hoare logic)。
    引入规则的形式为:
    ⊢{P}c{Q}\vdash \{P\}c\{Q\}⊢{P}c{Q}4.1 跳过与赋值(skip&assignment)Skip {P}skip{P}Skip~\frac{}{\{P\} skip \{P\}}Skip ​{P}skip{P}​​​​Asgn {Q[a/x]}x:=a{Q}Asgn~ \frac{}{\{Q[a/x]\}x:=a\{Q\}}Asgn ​{Q[a/x]}x:=a{Q}​​​​其中Q[a/x]Q[a/x]Q[a/x]:在QQQ中把所有xxx换成aaa,举个例子:
    (5+x)[(x+1)/x]=5+(x+1)(5+x)[(x+1)/x]=5+(x+1)(5+x)[(x+1)/x]=5+(x+1)4.2 逻辑的加强与削弱注意,我们不能证明一个很显而易见的东西:
    ⊢{y=0}x:=1{x=1}\vdash\{y=0\}x:=1\{x=1\}⊢{y=0}x:=1{x=1}但我们可以证明:
    ⊢{1=1}x:=1{x=1}\vdash\{1=1\}x:=1\{x=1\}⊢{1=1}x:=1{x=1}于是引入前提加强(precondition strengthening):
    Pre ⊢{P′}c{Q}P⇒P′{P}c{Q}Pre~\frac{\vdash\{P'\}c\{Q\}\qquad P\Rightarrow P'}{\{P\}c\{Q\}}Pre ​{P}c{Q}​​⊢{P​′​​}c{Q}P⇒P​′​​​​例如:
    Pre Asgn ⊢{1=1}x:=1{x=1}y=0⇒1=1{y=0}x:=1{x=1}Pre~\frac{Asgn~\frac{}{\vdash\{1=1\}x:=1\{x=1\}}\qquad y=0\Rightarrow 1=1}{\{y=0\}x:=1\{x=1\}}Pre ​{y=0}x:=1{x=1}​​Asgn ​⊢{1=1}x:=1{x=1}​​​​y=0⇒1=1​​与之相似,引入一削弱后验条件的规则:
    Post ⊢{P}c{Q′}Q′⇒Q{P}c{Q}Post~\frac{\vdash\{P\}c\{Q'\}\qquad Q'\Rightarrow Q}{\{P\}c\{Q\}}Post ​{P}c{Q}​​⊢{P}c{Q​′​​}Q​′​​⇒Q​​在二者的基础上,引入序列规则(consequence rule):
    Conseq P⇒P′⊢{P′}c{Q′}Q′⇒Q{P}c{Q}Conseq~\frac{P\Rightarrow P'\qquad\vdash \{P'\}c\{Q'\}\qquad Q'\Rightarrow Q}{\{P\}c\{Q\}}Conseq ​{P}c{Q}​​P⇒P​′​​⊢{P​′​​}c{Q​′​​}Q​′​​⇒Q​​4.3 组合(composition)Seq {P}c1{P′}{P′}c2{Q}{P}c1;c2{Q}Seq~\frac{\{P\}c_1\{P'\}\qquad \{P'\}c_2\{Q\}}{\{P\}c_1;c_2\{Q\}}Seq ​{P}c​1​​;c​2​​{Q}​​{P}c​1​​{P​′​​}{P​′​​}c​2​​{Q}​​举例:使用霍尔逻辑证明swap函数
    {x=x′∧y=y′}t:=x;x:=y;y:=t{y=x′∧x=y′}\{x=x'\wedge y=y'\}t:=x;x:=y;y:=t\{y=x'\wedge x=y'\}{x=x​′​​∧y=y​′​​}t:=x;x:=y;y:=t{y=x​′​​∧x=y​′​​}1.由Asgn:
    {x=x′∧y=y′}t:=x{t=x′∧y=y′}\{x=x'\wedge y=y'\}t:=x\{t=x'\wedge y=y'\}{x=x​′​​∧y=y​′​​}t:=x{t=x​′​​∧y=y​′​​}2.由Asgn:
    {t=x′∧y=y′}x:=y{t=x′∧x=y′}\{t=x'\wedge y=y'\}x:=y\{t=x'\wedge x=y'\}{t=x​′​​∧y=y​′​​}x:=y{t=x​′​​∧x=y​′​​}3.由Asgn:
    {t=x′∧x=y′}y:=t{y=x′∧x=y′}\{t=x'\wedge x=y'\}y:=t\{y=x'\wedge x=y'\}{t=x​′​​∧x=y​′​​}y:=t{y=x​′​​∧x=y​′​​}4.由1,2,Seq:
    {x=x′∧y=y′}t:=x;x:=y{t=x′∧x=y′}\{x=x'\wedge y=y'\}t:=x;x:=y\{t=x'\wedge x=y'\}{x=x​′​​∧y=y​′​​}t:=x;x:=y{t=x​′​​∧x=y​′​​}5.最后,由3,4,Seq:
    Q.E.DQ.E.DQ.E.D4.4 条件(conditional)If {P∧b}c1{Q}{P∧¬b}c2{Q}{P}if b then c1 else c2{Q}If~\frac{\{P\wedge b\}c_1\{Q\}\qquad \{P\wedge \neg b\}c_2\{Q\}}{\{P\} if~b~then~c_1~else~c_2\{Q\}}If ​{P}if b then c​1​​ else c​2​​{Q}​​{P∧b}c​1​​{Q}{P∧¬b}c​2​​{Q}​​
    在true分支:如果bbb成立,我们需要证明{P∧b}c1Q\lbrace P\wedge b \rbrace c_1{Q}{P∧b}c​1​​Q
    在false分支:如果¬b\neg b¬b成立,我们需要证明{P∧¬b}c2{Q}\lbrace P\wedge\neg b \rbrace c_2 \lbrace Q \rbrace{P∧¬b}c​2​​{Q}

    4.5 while循环(loop)While {P∧b}c{P}{P}while b do c{P∧¬b}While~\frac{\{P\wedge b\}c\{P\}}{\{P\} while~b~do~c\{P\wedge\neg b\}}While ​{P}while b do c{P∧¬b}​​{P∧b}c{P}​​其中,PPP是循环不变量(loop invariant):

    在进入循环前成立,并且在每次迭代后保持不变
    这由前提{P∧b}c{P}\lbrace P\wedge b \rbrace c \lbrace P \rbrace{P∧b}c{P}所确定

    为了使用While,需要先证明PPP是不变量。
    五、可靠性与完备性
    之前的规则对于部分正确性都是可靠的
    对于Imp,是不完备的,因为可以归约为TPAT_{PA}T​PA​​
    0 留言 2020-07-02 09:43:51 奖励30点积分
显示 75 到 90 ,共 15 条

热门回复

  • 基于SSM的超市订单管理系统
    感谢分享,非常棒的开发
    2020-08-30 14:43:15 thumb_up( 3 )
  • 基于SSM的超市订单管理系统
    可以用吗,怎么用的
    2021-04-14 15:44:50 thumb_up( 1 )
  • 线程同步之临界区
    程序还算比较简单的,谢谢分享
    2019-04-20 12:24:58 thumb_up( 1 )
  • 基于WinPcap实现的UDP发包程序
    如果在vs 编译时出现 无法找到元数据文件 platform.winmd 应该怎么解决
    2021-03-23 09:58:16 thumb_up( 2 )
  • 机器视觉MIL Mod匹配
    You can also search within the full angular range of 360� from the nominal angle specified with M_ANGLE. Use the MmodControl()�M_ANGLE_DELTA_POS and M_ANGLE_DELTA_NEG control types to specify the angular range in the counter-clockwise and clockwise direction from the nominal angle, respectively; the default for both is 180�. The angular range limits the possible angles which can be returned as results for an occurrence. Note that the actual angle of the occurrence does not affect search speed. If you need to search for a model at discrete angles only (for example, at intervals of 90 degrees), it is typically more efficient to define several models with different expected angles, than to search through the full angular range. By default, calculations specific to angular-range search strategies are enabled. If you expect that the occurrences sought are close to the specified nominal angle, you can disable these calculations using MmodControl() with M_SEARCH_ANGLE_RANGE set to M_DISABLE. When disabled, you must specify a good nominal angle for each model, which is within the model's angular range. You can restrict which candidates are returned as occurrences by narrowing the angular-range. Note that M_SEARCH_ANGLE_RANGE must be enabled to search for a rotation-invariant non-synthetic model (for example, an image-type model of a circle).
    2021-03-20 13:27:51 thumb_up( 2 )
eject