Research On Automatic Formal Modeling And Validation Of GP TEE Specification

With the continuous development of information technology,smart mobile devices are becoming more and more powerful.However,at the same time,the security of the software carried by mobile devices and the security of sensitive user information has become a major problem in this field.Trusted Execution Environment(TEE)effectively alleviates the security pain points in the field of mobile devices.To further improve the standardization and security of software developed by mobile device manufacturers,the GP(Global Platform)organization has drafted and developed TEE-oriented specifications and standards.However,due to the ambiguity of natural language and other reasons,the consistency between GP specifications and TEE specific implementations is still not guaranteed.To solve the above problems,based on the theories related to software formalmethods,this thesis first proposed a formal requirements modeling framework oriented to GP TEE specification,then designed and realized an automated modeling verification prototype system matching the framework,and further took OP-TEE as the modeling verification target,and demonstrates the effectiveness of the proposed framework and the designed system through comparative experiments.The main work and innovation of this thesis are as follows:(1)Tee FRMF,a formal requirements modeling framework oriented to GP TEE specification,is proposed.The core of the framework is a set of template-guided requirements specification method TGReq and corresponding transformation mapping rules.By limiting input,TGReq guides users to fill templates,extracts key structures in requirements specifications and filters secondary information,and provides structured and formal descriptions of data,terms,security properties,execution processes and call relations.The mapping rules transform the requirements specification into an intermediate model based on Finite State Machine(FSM)to adapt to different validation backends and enhance the scalability of the framework.(2)Based on the SBIP verification tool,a complete requirements modeling and verification prototype system is formed by integrating the requirements modeling functionality into the verification tool in the form of a plug-in.Firstly,an automatic transformation algorithm from intermediate model to verification model is given for BIP verification language,and then the framework and a series of transformation rules are combined to implement each functional module.Based on this system,automatic modeling and verification work can be realized,which greatly improves the work efficiency.(3)The security requirement statute of GP TEE basic specification and the behavior specification of OP-TEE are established and the consistency between them is proved.Firstly,by analyzing the characteristics of GP specification,the corresponding data dictionary and glossary are extracted and established,and a semi-formal security requirement specification is formed.Further,OP-TEE,an excellent open source solution in the field of TEE,was selected as the target,and an automated modeling verification prototype system designed in this thesis is used to build the OP-TEE implementation layer API interface model,the abstraction layer functional module model,and the GP TEE security property model,and the conformance of OP-TEE implementation with the GP specification is successfully verified.