Dissertation > Excellent graduate degree dissertation topics show

A Pointer Logic for Safety Verification of Pointer Programs

Author: HuaBaoJian
Tutor: ChenYiYun
School: University of Science and Technology of China
Course: Computer Software and Theory
Keywords: software safety program verification Hoare logic pointer logic
CLC: TP311.52
Type: PhD thesis
Year: 2008
Downloads: 141
Quote: 0
Read: Download Dissertation


Nowadays, information technologies play more and more important roles in all aspects of our world: industries, governments, bussiness, and schools. Once a node in this network collapses, an expensice catastrophe would happen. As a result, the requirement for software safety and security becomes more and more urgent. To moderate this disparity, developing high-assurance software based on formal methods is an essential approach. Among various formal methods, language-based approach to software security has attracted widespread attention in the past decade. These approaches help reduce the Trusted Computing Base of software systems by starting from the base of software, that is, programming languages and compilers.One promising approach for high secure software development in the future is the software property proving-based framework. In this framework, programmers design safety policies and decribe them as software specifications, which are fed to the compilers along with normal program code. In order to prove these programs satisfy these specifications, the compiler generates verification conditions, which are proved automatically or interatively by the programmers. A compiler translates these program code, along with those verification conditions and proofs, and such kind of compilers are called certifying compiler. At the assembly level, an independent proof checker checks the object code to ensure it satisfy its specifications. The key benifit of this framework is that it offers source-level proof methods, instead of at assembly-level, which makes the process of program development more effecient. Meanwhile, making use of a certifing compiler greatly reduces the trusted computing base by removing the compier and prover from the TCB.As an integral part of the above framework, this thesis investigates pointer logic and its application to source code proving. This thesis designs PointerC, a C-like imperative language which retains C’s explicit memory management facilities. The primary design motivation for PointerC is our goal to study more expressive safetye polies beyond type safety such as memory safety. And this thesis makes use of a static discipline combining type system and pointer logic system.This thesis proposes a novel program logic, i.e., the pointer logic. The primary goal for the design of pointer logic is: on on hand, traditional type system are weak and could not check the value-related safety obligations; on the other hand, Hoare logic can not handle pointer operations directly. The pointer logic extends traditional Hoare logic with new predicates and operations, and presents new deduction rules. The pointer logic has been implemented in our prototype certifying compiler and has been employed to prove some nontrivial pointer programs. This thesis proves pointer logic soundness with respect to operational semantics.This thesis investigates the application of the pointer logic to a small object-oriented language. To be specific, this thesis designs a small object-oriented language Cool, presents its syntax, static and dynamic semantics. Comparing with the pointer logic for PointerC, the pointer logic for Cool can also serve as a static garbage detection tool, which is capable to detect garbages in two ways: stack-allocation and static detection. Stack-allocation reduces the existence of garbage by allocating objects on stacks, instead of in heaps. And static garbage could detect some static garbages at compile time.The work presented in this thesis is the first step to the investigation of property proving-based software safety research. And this work provides a method to the safety verifications of larger and more practical saftware systems.

Related Dissertations

  1. The Research of Software Formal Verification Technology Based on Hoare Logic,TP311.52
  2. A program verification tool design and implementation,TP311.53
  3. The Modelling and Application of a New Model of Software Reliability and Safety,TP311.52
  4. Analysis and Designs of Tax Bank Treasury Electronic Payment Platform System,TP311.52
  5. Embedded System Supported Safety Critical Software Design for Railway Signal,U284.362
  6. Analysis and Check of Type Conversion and Control Flow Safety Vulnerability,TP309
  7. Software Safety Assurance Framework and Safety Technology Application,TP311.52
  8. Pointer Logic’s Extensions and Applications,TP311.52
  9. Research on Relationship and Transition between the Software Reliability and Safety,TP311.52
  10. Certifying the Safety of Assembly Pointer Programs,TP313
  11. Certifying Concurrent Porgrams Using Transactional Memory,TP311.11
  12. Research on Testing and Evaluating Theory of Reliability and Safety for High Dependability Software,TP311.52
  13. Certifying Compilation in an Infrastructure for Developing Trustable Software,TP311.52
  14. A Modular Approach on Building Certified Software System,TP311.52
  15. Slicing Execution for Verification of C Programs,TP312.1
  16. Constraint Based Prolog Semantics and Its Applications in the Testing, Analysis and Verification of Prolog Programs,TP311.52
  17. The Research of Partitioned Symbolic Execution Model and Its Environment Interaction Problem,TP311.11
  18. Concurrent Object-oriented Program Slicing and Its Application in Program Verification,TP311.11
  19. Research on Methods of Security Assurance Based on Computer-Assisted Proof,TP309
  20. Verifying Parallel Low-Level Programs for Multi-core Processor,TP332.3
  21. Verify with dynamic thread creation and exit multithreaded programs,TP311.53

CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > Computer software > Program design,software engineering > Software Engineering > Software Development
© 2012 www.DissertationTopic.Net  Mobile