Pointer Logic's Extensions And Applications

Nowadays,software technique is widely used.However,the architecture of software is more and more complicated as its size grows,and it is more and more difficult to guarantee its safety.In the programming language such as C,C++ or Java,pointers or references are commonly used to achieve high performance. But the flexibility of pointers is apt to cause errors such as null pointer reference, dangling pointer deference and memory leaks which are difficult to find.Once these errors occur,the system would crash.And more seriously,they can be taken advantage of by hackers.On the other hand,the reason that pointer errors are hard to detect is because distinct pointers might be aliased to each other,i.e., two different names could refer to the same memory address.Modifying the value of one pointer could affect the value of the other,which exhibits great difficulties for debugging and reasoning.As a result,the research on the safety of pointer programs plays an important role in software security.As the research of pointer program safety is challenging,while software test can not guarantee its soundness,pointer program verification becomes a hot research topic.However,the current verification methods bear lots of defects-either they have to introduce stack or heap which is not the syntax of the programming language to capture the programming running state,or they generate complicated verification conditions which can not be automatedly proved.The introduction of stack and heap needs to know the exact memory address,but isomorphic heaps are indistinguishable.Storeless memory models not only get over these problems, but also lead to automated verification because of its nice properties.In essence pointer logic is based on the method of Storeless memory models,but still lacks the description of an abstract storeless model,which leads to the algorithmic style description of the inference rules,hindering the exploration of pointer logic essence.Furthermore,pointer logic lack support for pointer arithmetic,and the implementation PLCC(V1) generates verification conditions which has to be proved in interactive theorem prove in COQ.Based on the above consideration,this thesis proposes a storeless model and probes into its properties such as right regularity,prefix closure etc..Meanwhile, the thesis focuses on the well-formedness of pointer logic's assertion language, and rephrases pointer logie's inference rules.In order to verify widely used data structures,the thesis proposes frame rule in Pointer Logic and the rule for func- tion call.Furthermore,the source language and assertion language are extended to support pointer arithmetic,while Pointer Logic rules are extended to ensure the safety of pointer arithmetic.Formerly in Pointer Logic the sets are unnamed which can not handle programs containing function calls under some circumstances. Thus this thesis proposes Pointer Logic with labels to verify programs with arbitrary function call.As to the implementation,automatic deduction algorithms for Pointer Logic rules are designed and the unfolding mechanism are proposed to deal with the user-defined predicates.At last,the work in thesis is implemented in PLCC(V2).The main contributions and characteristics of this dissertation are:●It presents a more effective storeless memory model which not only enjoys the nice properties of existing storeless models,but also overcomes their shortcomings such as redundancy and high costs.●It perfects Pointer Logic by rephrasing Pointer Logic rules on the abstract model.Because the model is simple and efficient,the thesis can discover a flaw in former Pointer Logic rules:the no_leak function would reject correct programs in some circumstances,while in this thesis the rule is corrected.●It extends Pointer Logic.Compared to former Pointer Logic,the thesis extends pointer logic in local reasoning,pointer arithmetic on dynamic arrays and pointer set with labels to verify programs including arbitrary function call.As a result,Pointer Logic can guarantee more programs' safety properties.●This thesis designs efficient algorithms and proposes unfolding mechanism to automate Pointer Logic rule deduction,and all are implemented in an automated verification tool PLCC(V2).Compared to PLCC(V1) which requires the programmer to prove the verification condition it generates,this work implements a newer version to automatedly reason about the properties of pointer programs.Moreover,PLCC(V2) can verify the operations on widely used data structures such as singly-linked lists,doubly-linked circular lists and trees etc.,including the famous Schorr-Waite tree traversal algorithm which is always considered as the milestone for pointer formalizations.