Research On Automated Techniques Of Software Trustworthiness Verification

Defects and vulnerabilities are widely existing in all kinds of software and difficult to avoid, leading to software failures bringing enormous loss, or even disastrous damage. An effective way to deal with this problem is to design effective and reasonable automated methods for sufficient verification of software trustworthiness. The research on trustworthiness verification in this paper is carried out from two aspects:static analysis and dynamic testing.From static aspect, a static code verification method based on rule matching is proposed for critical programming standards. Rule matching is hard to execute directly on C++ code due to its flexibility and complexity. To solve this, a code representation model for expressing and storing code information in a specific format is build. A parse tree model,as well as a storage and transformation model, is build to complete the parsing process of extracting rule related information from code, and translating it into an formatted intermediate representation. A rule base model is designed to describe all the valid rules of specific secure standard, for use in executing rule matching on formatted intermediate representation and feedbacking defects against security rules. From dynamic aspect, a test generation and verification method based on NFSM is proposed. To solve problem that uncertain behaviors in software design specification are difficult to describe and generate test cases, a hierarchical modeling method is proposed. In this method, states with uncertain transitions are clustered and modeled into hierarchies where uncertain transitions are converted to deterministic ones between hierarchical sub state machines. To solve problem that loops in software control flow are hard to describe precisely, a test generation method generating cases from regex model is proposed: construct regex model corresponding to FSM model according to the equivalence relation between FSM and regex; then design transition covering algorithms to generate cases from regex model. To improve verification ability and test adequacy of test cases, different trigger parameters are added into regex model as case features for generating different test sequences with different features. As a complementary means of static method, dynamic testing finds out non-conformance faults, runtime failures, and defects undiscovered in static phase, providing further support for reliability and robustness verification of software systems.