| With the rapid development of technology,people can find computers in more and more fields.While the computer brings convenience,it also brings some security problems that cannot be ignored.Computer system failures or vulnerabilities may be used by some hackers to attack users’ computers,causing serious damage to users’ lives and property.Security vulnerabilities in component systems that may cause harm has become a problem that cannot be ignoredand.How to detect security problems in the operation of component systems has become a hot research topic in software testing.Formal methods are a mathematical theory-based approach for ensuring security of software development.According to the component specification file,the developer builds the component’s own security specification and builds an abstract model for testing.Therefore,in this thesis,we choose the formal method to test the cross-subject internetware.We first propose a test framework for detecting vulnerabilities in crosssubject internetware based on the formal method.We build formal models and generate Musmv models and test components by these two models.After that,we do furthur research on case generation method and generate test cases by building test requirement models and marking migration systems.Finally,based on the research in this thesis,a prototype system for detecting vulnerabilities in cross-subject network components based on formalism is designed and implemented.The main work of this paper is as follows:1.We propose a formalization-based vulnerability detection framework for crosssubject internetware.In this framework,we choose a monad as the medium of abstract computation,and use a formal description language to construct an error propagation model after an error is generated during the operation of the components.Then,we analyze the types of errors which generated during the operation of the components and classify them into explicit and implicit vulnerabilities and design the detection algorithm separately.We do further research on syntactic semantics between the formal language and the NuSmv(New Symbolic Model)language and design a conversion method to convert the formal model to the NuSmv model through four aspects.We can use this framework for further test on the cross-subject internetware.2.We propose a test case generation method based on test requirement model.First,we select the features of the system under test and quantify them to give a test feature model,then we select the test targets of the system and divide them,we label the section with a specific test target as the object and give a test target grouping and description model.Then we select the test target nodes and generate the test target description model.Finally,we filter out the components that are concerned from the test requirements and give the test requirement description model view.After obtaining the above four model views,we can construct the test requirement metamodel.We obtain the state diagram ensemble of the system by the tool,and then we transform the state diagram ensemble of the system into the mark migration system according to the algorithm.We transform the test target description model into the mark migration system of the test target,test cases are then generated by the marker migration system.It is finally demonstrated experimentally that the method proposed in this paper can optimize the migration path and generate fewer test cases.3.A prototype system for cross-subject internetware component vulnerability detection based on formalization is designed and implemented.The specific modules of this prototype system are: component analysis module,formal verification and testing module,test requirement modeling module and test case generation module.At the same time,the system runs through the idea of humanized design,it can be easy to operate. |
