Abstract
When formalising the rules of trust in the remote attestation of TPM-based computer systems it is paramount that the rules are precisely understood, supporting unambiguous communication of information about system requirements between engineers. We present a diagrammatic approach to modelling rules of trust using an extended version of concept diagrams. Within the context of our proof-of-concept Network Function Virtualisation and Attestation environment, these rules allow different level of trust to be explored and, importantly, allow us to identify when a computer system should not be trusted. To ensure that the modelling approach can be applied to general systems, we include generic patterns for extending our domain model and rules of trust. Consequently, through the use of a formal, yet accessible, diagrammatic notation, domain experts can define rules of trust for their systems.
Stapleton, Shams, and Jamnik were funded by a Leverhulme Trust Research Project Grant (RPG- 2016-082) for the project entitled Accessible Reasoning with Diagrams. Oliver was supported by the EU-funded SCOTT and Secredas projects.
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
Abrial, J.: The B-Book: Assigning Programs to Meanings. CUP, Cambridge (1996)
Alharbi, E., Howse, J., Stapleton, G., Hamie, A., Touloumis, A.: Visual logics help people: an evaluation of diagrammatic, textual and symbolic notations. In: Visual Languages and Human-Centric Computing, pp. 255–259. IEEE (2017)
Baader, F., Horrocks, I., Sattler, U.: Description logics as ontology languages for the semantic web. In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning. LNCS (LNAI), vol. 2605, pp. 228–248. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32254-2_14
Chapman, P., Stapleton, G., Howse, J., Oliver, I.: Deriving sound inference rules for concept diagrams. In: IEEE Symposium on Visual Languages and Human-Centric Computing, pp. 87–94. IEEE (2011)
Dai, W., et al.: TEE: a virtual DRTM based execution environment for secure cloud-end computing. Future Gener. Comput. Syst. 49, 47–57 (2015)
Gurr, C.: Effective diagrammatic communication: syntactic, semantic and pragmatic issues. J. Vis. Lang. Comput. 10(4), 317–342 (1999)
Hou, T., Chapman, P., Blake, A.: Antipattern comprehension: an empirical evaluation. In: Formal Ontology in Information Systems. Frontiers in Artificial Intelligence, vol. 283, pp. 211–224. IOS Press (2016)
Howse, J., Stapleton, G., Taylor, K., Chapman, P.: Visualizing ontologies: a case study. In: Aroyo, L., Welty, C., Alani, H., Taylor, J., Bernstein, A., Kagal, L., Noy, N., Blomqvist, E. (eds.) ISWC 2011. LNCS, vol. 7031, pp. 257–272. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25073-6_17
Oliver, I., Holtmanns, S., Miche, Y., Lal, S., Hippeläinen, L., Kalliola, A., Ravidas, S.: Experiences in trusted cloud computing. In: Yan, Z., Molva, R., Mazurczyk, W., Kantola, R. (eds.) NSS 2017. LNCS, vol. 10394, pp. 19–30. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-64701-2_2
Sato, Y., Masuda, S., Someya, Y., Tsujii, T., Watanabe, S.: An fMRI analysis of the efficacy of Euler diagrams in logical reasoning. In: IEEE Symposium on Visual Languages and Human-Centric Computing, pp. 143–151. IEEE (2015)
Sato, Y., Mineshima, K.: How diagrams can support syllogistic reasoning: an experimental study. J. Log. Lang. Inf. 24, 409–455 (2015)
Shams, Z., Sato, Y., Jamnik, M., Stapleton, G.: Accessible reasoning with diagrams: from cognition to automation. In: Chapman, P., Stapleton, G., Moktefi, A., Perez-Kriz, S., Bellucci, F. (eds.) Diagrams 2018. LNCS (LNAI), vol. 10871, pp. 247–263. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91376-6_25
Shimojima, A.: Semantic Properties of Diagrams and Their Cognitive Potentials. CSLI Publications, Stanford (2015)
Spivey, J.: The Z Notation: A Reference Manual. Prentice Hall, New York (1989)
Stapleton, G., Howse, J., Chapman, P., Delaney, A., Burton, J., Oliver, I.: Formalizing concept diagrams. In: 19th International Conference on Distributed Multimedia Systems, pp. 182–187. Knowledge Systems Institute (2013)
Yang, Y., Shiwei, X., Hunguo, Z., Fan, Z.: Using first order logic to reason about TCG’s TPM specification. In: International Forum on Information Technology and Applications, pp. 259–263. IEEE (2009)
Zimmer, V., Dasari, R., Brogan, S.: TCG-based firmware: white paper by Intel Corporation and IBM Corporation Trusted Platforms (2009). https://people.eecs.berkeley.edu/kubitron/cs194-24/hand-outs/SF09_EFIS001_UEFI_PI_TCG_White_Paper.pdf. Accessed May 2018
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Oliver, I., Howse, J., Stapleton, G., Shams, Z., Jamnik, M. (2019). Exploring and Conceptualising Attestation. In: Endres, D., Alam, M., Şotropa, D. (eds) Graph-Based Representation and Reasoning. ICCS 2019. Lecture Notes in Computer Science(), vol 11530. Springer, Cham. https://doi.org/10.1007/978-3-030-23182-8_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-23182-8_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-23181-1
Online ISBN: 978-3-030-23182-8
eBook Packages: Computer ScienceComputer Science (R0)