Abstract
The ARM TrustZone platform has provided a trusted execution environment (TEE) for mobile device to improve system security. The Global Platform presents a TEE Internal Core API Specification to define the TEE, the TEE system architecture, and the Internal and Client API specifications. However, hackers can still attack the TEE by means of the tampering the message stored in the communication buffer that is used to exchange information between the TEE and REE world. In order to solve this problem, this paper presents a formal security model of the 
Interface and verifies the correctness of this model using Coq based on the GP specification. The formalization identifies the TA Interface specification as well as modelling the valid trace of TA Interface based on a one-session application, which can effectively detect and filter the invalid TA service request that from REE. These results are useful for the standard institutions and TEE developers to develop security TA software and prevent from hackers attack.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
GlobalPlatform Device Technology TEE Internal Core API Specification Version 1.1.1 (2016). http://www.globalplatform.org/specificationsdevice.asp
ARM TrustZone Technology. http://www.arm.com/products/processors/technologies/trustzone.php
Marche, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. J. Log. Algebraic Program. 59, 89–106 (2004)
Appel, A.W.: Verified software toolchain. In: European Symposium on Programming, Heidelberg (2011)
Leroy, X.: The CompCert verified compiler (2005–2016). http://compcert.inria.fr/
Gu, R., et al.: Deep specifications and certified abstraction layers. ACM SIGPLAN Not. 50(1) (2015). ACM
Béguelin, S.Z.: Formalisation and verification of the GlobalPlatform card specification using the B method. In: Barthe, G., Grégoire, B., Huisman, M., Lanet, J.-L. (eds.) CASSIS 2005. LNCS, vol. 3956, pp. 155–173. Springer, Heidelberg (2006). https://doi.org/10.1007/11741060_9
Yang, X., et al.: Trust-E: a trusted embedded operating system based on the ARM trustzone. In: 2014 IEEE 11th International Conference on Ubiquitous Intelligence and Computing and IEEE 11th International Conference on and Autonomic and Trusted Computing, and IEEE 14th International Conference on Scalable Computing and Communications and Its Associated Workshops (UTC-ATC-ScalCom). IEEE (2014)
GlobalPlatform Device Technology TEE Client API Specification, version 1.0 (2011). http://www.globalplatform.org/specificationsdevice.asp
GlobalPlatform Device Technology TEE Internal API Specification, version 1.0 (2011). http://www.globalplatform.org/specificationsdevice.asp
GlobalPlatform Device Technology TEE System Architecture, version 1.0 (2011). http://www.globalplatform.org/specificationsdevice.asp
Lehman, M.M.: Technical correspondence: uncertainty in computer application. Commun. ACM 33(5), 584–587 (1990)
Sewell, T.A.L., Myreen, M.O., Klein, G.: Translation validation for a verified os kernel. In: PLDI, pp. 471–482 (2013)
Focardi, R., Gorrieri, R.: Classification of security properties. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45608-2_6
Focardi, R., Gorrieri, R.: A classification of security properties for process algebras1. J. Comput. Secur. 3(1), 5–33 (1995)
McCullough, D.: Noninterference and the composability of security properties. In: Proceedings of 1988 IEEE Symposium on Security and Privacy, 1988. IEEE (1988)
Barendregt, H., Geuvers, H.: Proof assistants using dependent type systems. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, chap. 18, vol. 2, pp. 1149–1238. Elsevier (2001)
MarisaKirisame. https://github.com/ThoughtWorksInc/DeepDarkFantasy
Klein, G., Elphinstone, K., Heiser, G., et al.: seL4: formal verification of an OS kernel. In: ACM Symposium on Operating Systems Principles, pp. 207–220 (2009)
Gu, R., Shao, Z., Chen, H., Wu, X.(N.), Kim, J., Sjoberg, V., Costanzo, D.: CertiKOS: an extenisble architecture for building certified concurrent OS Kernels. In: Proceedings of 2016 USENIX Symposium on Operating Systems Design and Implementation (OSDI 2016), Savannah, GA, pp. 653–669, November 2016
Acknowledgments
The authors thank the anonymous reviewers for their very helpful comments. This work has been supported in part by the “Fundamental Research Funds for the Central Universities” grant (ZYGX2016J094), which is a large plan of the Chinese government.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Yang, X., Yang, Z., Sun, H., Liu, J. (2017). Formalizing and Verifying GP TEE TA Interface Specification Using Coq. In: Xu, M., Qin, Z., Yan, F., Fu, S. (eds) Trusted Computing and Information Security. CTCIS 2017. Communications in Computer and Information Science, vol 704. Springer, Singapore. https://doi.org/10.1007/978-981-10-7080-8_16
Download citation
DOI: https://doi.org/10.1007/978-981-10-7080-8_16
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-10-7079-2
Online ISBN: 978-981-10-7080-8
eBook Packages: Computer ScienceComputer Science (R0)
