Program Verification Method Research Based On Type Systems

Software is ubiquitous in our daily life today. Although we do not notice their existence sometimes, the influence of software becomes greater. The dependability of software is important in many areas such as aviation and space industries, finance, medical treatment, automotive electronics, etc. With the continuous development of software engineering, the scale of software becomes larger; complexity becomes higher; pattern becomes various and application scene becomes wider. Network and dynamic become common in the running environment of software. Due to these factors, guaranteeing dependability of software becomes very difficult. Finding more effective method to guaranteeing software's dependability is always a main concern in academia and industry. Software's dependability can be guaranteed at any phase and product in software development cycle. Guarantee of dependability based on code is an effective and important method, because code reflects the running behaviors of software directly. Among this method, conventional test method can't guarantee dependability completely while because of completeness and soundness, program verification becomes more and more valued.There is a lot of C code in system software. Verification of C-like programs including pointer operation, variable reference and heap manipulating is always a challenge. This paper focuses on static program verification method based on type systems for C-like programs. The main idea is guaranteeing program's dependability through ensuring it well typed. Existing verification methods are difficult to use or limited. By ingenious amalgamation of type systems and verification methods based on Hoare logic, the proposed method can verify deep property without increasing the programming's complexity and therefore improve the usability and efficiency of program verification. In order to give precise secure formal semantic to low level C-like languages, we propose a safe typed memory model. This model supports low level memory operation and has certain abstract to make things convenient for applications which need shielding the details. Memory model can describe access control and its type features ensure strict safety which means read data is always well typed. Complete abstract property of memory model is presented and a concrete implementation is given. We design an extended type system to verify C-like programs. It is based on advanced type systems like refined type, subtype, dynamic type, etc., so it can accurately describe pointer variables and operations, implicitly represent property of data structure in heap. The type system is open and easy to extend. By formal describing type system and formal defining source language's operational semantics based on typed memory model, we have proved the soundness of type system. In order to improve the automation and accuracy, we take advantage of effective automatic theory provers like SMT solvers for type checking. The code including extended type to be verified are converted to common codes and type checked by traditional type check method. If the check passes, the codes are converted to Boogie codes. This conversion process encodes the static and dynamic semantics of source codes and avoids loss of information for program verification. Type check algorithm in this way only needs a syntax directed conversion algorithm instead of specifically complex type check algorithm, so it has strong generality, good extensibility and high automation.