| With the software engineering scale is continually expanding,the complexity and the scale of software systems are increasing.Errors and omissions of software system are hard to be detected in the design stage.Besides,data security in the application systems is also facing new challenges.In addition,with the development of software systems,the later we found software errors,the more expensive it cost.Therefore,it's necessary to ensure the reliability of the software in the design and modeling stages,and improve the quality of the software.It is an effective way to combine the mainstream software development methods and formal methods.In this paper,UML2.3 model is extended to combine the advantages of UML and formal method,and a formalization framework is proposed based on the characteristics of application systems.First of all,our methods analyzes the requirements of system,and disassembles key functions,then according to the different functions,the method extend UML class diagram,sequence diagram and state machine diagram for the system modeling.According to the corresponding mapping rules and transformation algorithm,the XMI file derived by UML can be automatically transformed to formal specification,and finally through the formal analysis toolkit ProVerif,security properties can be verified and the output results.ProVerif also provide counterexamples for unsatisfied properties,which allow developers to quickly find flaws of the system.According to the process of lightweight formal framework,this paper implements the formal verification tool based on extended UML2.3,and automatically converts the system model to formal language,and achieves security properties verification.This paper use case study,a conference management application named ConfiChair to proves the validity of the method proposed in this paper.We model and verify data privacy,accessibility,unlinkability and other safety features,analyzes the vulnerabilities of system,and shows the corresponding attack path. |
PDF Full Text Request