{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:50:22Z","timestamp":1740099022413,"version":"3.37.3"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319723587"},{"type":"electronic","value":"9783319723594"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-72359-4_47","type":"book-chapter","created":{"date-parts":[[2017,12,7]],"date-time":"2017-12-07T11:19:11Z","timestamp":1512645551000},"page":"759-769","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Using the B Method to Formalize Access Control Mechanism with TrustZone Hardware Isolation (Short Paper)"],"prefix":"10.1007","author":[{"given":"Lu","family":"Ren","sequence":"first","affiliation":[]},{"given":"Rui","family":"Chang","sequence":"additional","affiliation":[]},{"given":"Qing","family":"Yin","sequence":"additional","affiliation":[]},{"given":"Wei","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,12,8]]},"reference":[{"key":"47_CR1","doi-asserted-by":"publisher","unstructured":"Sun, H., Sun, K., Wang, Y., Jing, J., Wang, H.: TrustICE: hardware-assisted isolated computing environments on mobile devices. In: 2015 45th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks, pp. 367\u2013378. IEEE Press, New York (2015). \nhttps:\/\/doi.org\/10.1109\/DSN.2015.11","DOI":"10.1109\/DSN.2015.11"},{"key":"47_CR2","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., et al.: seL4: formal verification of an OS kernel. In: ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207\u2013220. ACM, New York (2009). \nhttp:\/\/dx.doi.org\/10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"47_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/11955757_23","volume-title":"B 2007: Formal Specification and Development in B","author":"S Hoffmann","year":"2006","unstructured":"Hoffmann, S., Haugou, G., Gabriele, S., Burdy, L.: The B-method for the construction of microkernel-based systems. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 257\u2013259. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11955757_23"},{"key":"47_CR4","volume-title":"Understanding the Linux Kernel","author":"DP Bovet","year":"2001","unstructured":"Bovet, D.P., Cesati, M.: Understanding the Linux Kernel. Oreilly Media, Sebastopol (2001)"},{"key":"47_CR5","unstructured":"ARM. ARM Security Technology Building a secure system using TrustZone technology (white paper). ARM Limited (2009)"},{"key":"47_CR6","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"47_CR7","unstructured":"Presentation of the B method\u00a0|\u00a0M\u00e9thode B. \nhttp:\/\/www.methode-b.com\/en\/b-method\/\n\n. Accessed 1 July 2017"},{"key":"47_CR8","unstructured":"Atelier B. \nhttps:\/\/www.atelierb.eu\/en\/\n\n. Accessed 1 July 2017"},{"key":"47_CR9","unstructured":"The ProB Animator and Modelchecker. \nhttps:\/\/www3.hhu.de\/stups\/prob\/\n\n. Accessed 1 July 2017"},{"issue":"23","key":"47_CR10","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1145\/358818.358825","volume":"23","author":"BJ Walker","year":"1980","unstructured":"Walker, B.J., Kemmerer, R.A., Popek, G.J.: Specification and verification of the UCLA Unix security kernel. Commun. ACM 23(23), 118\u2013131 (1980). \nhttps:\/\/doi.org\/10.1145\/358818.358825","journal-title":"Commun. ACM"},{"issue":"1","key":"47_CR11","doi-asserted-by":"publisher","first-page":"1125","DOI":"10.2174\/1874110X01509011125","volume":"9","author":"D Chen","year":"2015","unstructured":"Chen, D., Sun, Y., Chen, Z.: A formal specification in B of an operating system. Open Cybern. Syst. J. 9(1), 1125\u20131129 (2015). \nhttps:\/\/doi.org\/10.2174\/1874110X01509011125","journal-title":"Open Cybern. Syst. J."},{"key":"47_CR12","first-page":"506","volume":"68","author":"K Kawamorita","year":"2010","unstructured":"Kawamorita, K., Kasahara, R., Mochizuki, Y., Noguchi, K.: Application of formal methods for designing a separation kernel for embedded systems. World Acad. Sci. Eng. Technol. 68, 506\u2013514 (2010)","journal-title":"World Acad. Sci. Eng. Technol."}],"container-title":["Lecture Notes in Computer Science","Information Security Practice and Experience"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-72359-4_47","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,12,7]],"date-time":"2017-12-07T11:39:42Z","timestamp":1512646782000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-72359-4_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319723587","9783319723594"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-72359-4_47","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}