Reliability And Safety Verification Of System Program Based On Model Checking

Large exponent ascent of complexity of software makes more and more bugs, manual test is already crumbling. Experts in computer theory suggest Model Checking as future trends.This paper chooses two pointed model checking tools:CBMC and MOPS, complementing each other, to check OpenSSH system which is widely used in network application, utilizing the specialty of these two tools, mutual checking each other's checking result and gives a prove on consistency of the results.CBMC is a Bounded Model Checker for ANSI-C and C++ programs, it is good at checking the reliability of programs such as allowing verifying array bounds, buffer overflows, pointer safety, it also support user-specified assertions to model and check programs.MOPS is model checker designed to finding security bugs in C programs. It can be used to check whether a program satisfy a temporal safety property. Temporal safety property dictates the order of a specific sequence of operations which is critical in program's safety.OpenSSH is a free encryption tool, it encrypts all data flow including passwords, efficiently defends network sniffer, connection interception, and other network level attack. Reliability or safety bug's existence in OpenSSH may result in heavy loss, thus this paper takes this tool as the subject of the experiment.This paper described using the two tools to check the experiment subject separately first, then use the other tool to model the effective bug reported and do the double check. Finally uses formal method to prove the consistency of the checking results.