Abstract
Systems designed with measurement and attestation in mind are often layered, with the lower layers measuring the layers above them. Attestations of such systems, which we call layered attestations, must bundle together the results of a diverse set of application-specific measurements of various parts of the system. Some methods of layered attestation are more trustworthy than others especially in the presence of an adversary that can dynamically corrupt system components. It is therefore important for system designers to understand the trust consequences of different designs. This paper presents a formal framework for reasoning about layered attestations. We identify inference principles based on the causal effects of dynamic corruption, and we propose a method for bundling evidence that is robust to such corruptions.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Berger, S., Cáceres, R., Goldman, K.A., Perez, R., Sailer, R., van Doorn, L.: vTPM: virtualizing the trusted platform module. In: Proceedings of the 15th USENIX Security Symposium, Vancouver, BC, Canada, July 31–August 4, 2006 (2006)
Berger, S., Goldman, K.A., Pendarakis, D.E., Safford, D., Valdez, E., Zohar, M.: Scalable attestation: a step toward secure and trusted clouds. IEEE Cloud Comput. 2(5), 10–18 (2015)
Cabuk, S., Chen, L., Plaquin, D., Ryan, M.: Trusted integrity measurement and reporting for virtualized platforms. In: Chen, L., Yung, M. (eds.) INTRUST 2009. LNCS, vol. 6163, pp. 180–196. Springer, Heidelberg (2010)
Coker, G., Guttman, J.D., Loscocco, P., Herzog, A.L., Millen, J.K., O’Hanlon, B., Ramsdell, J.D., Segall, A., Sheehy, J., Sniffen, B.T.: Principles of remote attestation. Int. J. Inf. Sec. 10(2), 63–81 (2011)
Cucurull, J., Guasch, S.: Virtual TPM for a secure cloud: fallacy or reality? Universidad de Alicante (2014)
Davi, L., Sadeghi, A.-R., Winandy, M.: Dynamic integrity measurement and attestation: towards defense against return-oriented programming attacks. In: Proceedings of the 4th ACM Workshop on Scalable Trusted Computing, STC 2009, Chicago, Illinois, USA, 13 November 2009, pp. 49–54 (2009)
Kil, C., Sezer, E.C., Azab, A.M., Ning, P., Zhang, X.: Remote attestation to dynamic system properties: towards providing complete system integrity evidence. In: Proceedings of the 2009 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2009, Estoril, Lisbon, Portugal, 29 June–2 July, 2009, pp. 115–124 (2009)
Loscocco, P., Wilson, P.W., Aaron Pendergrass, J., Durward McDonell, C.: Linux kernel integrity measurement using contextual inspection. In: Proceedings of the 2nd ACM Workshop on Scalable Trusted Computing, STC 2007, Alexandria, VA, USA, 2 November 2007, pp. 21–29 (2007)
Maliszewski, R., Sun, N., Wang, S., Wei, J., Qiaowei, R.: Trusted boot (tboot). http://sourceforge.net/p/tboot/wiki/Home/
Namiluko, C., Martin, A.: Provenance-based model for verifying trust-properties. In: Katzenbeisser, S., Weippl, E., Camp, L.J., Volkamer, M., Reiter, M., Zhang, X. (eds.) Trust 2012. LNCS, vol. 7344, pp. 255–272. Springer, Heidelberg (2012)
Lo Presti, S.: A tree of trust rooted in extended trusted computing. In: Proceedings of the Second Conference on Advances in Computer Security and Forensics Programme (ACSF), pp. 13–20 (2007)
Xen Project. http://www.xenproject.org
QEMU. http://wiki.qemu.org
Rowe, P.D.: Confining adversary actions via measurement. In: Proceeding of the 3rd International Workshop in Graphical Models for Security, GraMSec 2016 (in press)
Sailer, R., Zhang, X., Jaeger, T., van Doorn, L.: Design and implementation of a TCG-based integrity measurement architecture. In: Proceedings of the 13th USENIX Security Symposium, San Diego, CA, USA, 9–13 August 2004, pp. 223–238 (2004)
Schmidt, A.U., Leicher, A., Brett, A., Shah, Y., Cha, I.: Tree-formed verification data for trusted platforms. Comput. Secur. 32, 19–35 (2013)
Wei, J., Calton, P., Rozas, C.V., Rajan, A., Zhu, F.: Modeling the runtime integrity of cloud servers: a scoped invariant perspective. In: Proceedings of the Second International Conference in Cloud Computing, CloudCom 2010, November 30–3 December 2010, Indianapolis, Indiana, USA, pp. 651–658 (2010)
Acknowledgments
I would like to thank Pete Loscocco for suggesting and guiding the direction of this research. Many thanks also to Perry Alexander and Joshua Guttman for their valuable feedback on earlier versions of this work. Thanks also to Sarah Helble and Aaron Pendergrass for lively discussions about measurement and attestation systems. Finally, thank you to the anonymous reviewers for helpful comments in improving the paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
A Proof of Lemmas
A Proof of Lemmas
The following is a proof of Lemma 3
Proof
By definition, the values contained in a PCR are exactly those that were previously extended into it. Thus, since \(\mathsf {ext}\) events are the only way to extend values into PCRs, there must be some event \(e_v={\mathsf {ext}}(o,v,p)\) with \(e_v\prec _E e\). \(\square \)
The following is a proof of Lemma 4
Proof
Definition 7 requires v to be derivable from the public terms \(\mathcal {P}\) and the output of previous messages. Call those outputs \(\mathcal {O}\).
First suppose \(v\in \mathcal {N}\). Since v is atomic, the only way to derive it is if \(v\in \mathcal {P}\cup \mathcal {O}\). Since \(\mathcal {P}\cap \mathcal {N}=\emptyset \), \(v\not \in \mathcal {P}\), hence \(v\in \mathcal {O}\) as required.
Now suppose v is a signature using key \({sk}(t)\in \mathcal {K}\). Then v can be derived in two ways. The first is if \(v\in \mathcal {P}\cup \mathcal {O}\). In this case, since \(v\not \in \mathcal {P}\) it must be in \(\mathcal {O}\) instead as required. The other way to derive v is to construct it from the key sk(t) and the signed message, say m. That is, we must first derive sk(t). Arguing as above, the only way to derive sk(t) is to find it in \(\mathcal {O}\), but there are no events that output such a term. \(\square \)
We conclude with the complete proof of Theorem 2.
Proof
By Lemma 6, E contains a substructure \(X_\mathcal {Q}\) of extend events that extends bottom-up. Thus by Theorem 1, Conditions 2a and 2b are possibilities. So suppose instead that E satisfies Condition 1 of Theorem 1. We must show that \(E\in \mathcal {E}(S')\). In particular, we construct \(\alpha :S'\rightarrow E\) and show that it is label- and order-preserving.
Consider the measurement events \(e_i^s\) of \(S'\). By construction, each one comes from some measurement value \(v_i\) contained in \(\mathcal {Q}\). Similarly, the well-supported measurement events \(e_i^m\) of E guaranteed by Theorem 1 are reflected by extend events \(e_i\) of E which are, in turn, those events that record each \(v_i\) in \(\mathcal {Q}\). We need to show that \(e_i^s=e_i^m\) for each i (i.e. that the labels agree), and that the orders among the \(e_i^s\) are reflected by corresponding orders among the \(e_i^m\).
Consider first the label of \(e_i^s\). It corresponds to a measurement value \(v_i\) contained in some \(p_i\) of \(\mathcal {Q}\). So \(e_i^s\) is labeled \({\mathsf {ms}}(o,o')\) where \(M(o,o')\), \(v_i\in \mathcal {MV}(o')\), and \(L(o,p_i)\). The event \(e_i^m\) also corresponds to the same \(v_i\). Lemma 3 ensures that \(e_i={\mathsf {ext}}(o,v,p_i)\) with \(L(o,p_i)\), and so the measurement event it reflects is \(e_i^m={\mathsf {ms}}(o,o')\) with \(M(o,o')\) and \(v_i\in \mathcal {MV}(o')\). Thus \(e_i^s\) and \(e_i^m\) have the same label.
We now show that if \(e_i^s\prec _{S(\mathcal {Q})}e_j^s\) then \(e_i^m\prec _E e_j^m\). The former ordering exists in \(S'\) because some quote \(Q\in \mathcal {Q}\) is contained in \(p_j\) before \(v_j\) and \(v_i\) is contained in Q, and because \(e_i^s\) is in the support of \(e_j^s\). By Corollary 1 \(e_i\prec _E e_j\) and \(e_i\) is in the support of \(e_j\) and therefore Theorem 1 ensures that the measurements they reflect are also ordered, i.e. \(e_i^m\prec _E e_j^m\).
Finally, consider any events \(e=\mathsf {att}{\text {-}}\mathsf {start}(n)\) in \(S'\). They come from nonces n found as inputs to quotes \(Q\in \mathcal {Q}\). By Lemma 4, E also has a corresponding event \(e^*\) with \({out}(e^*)=n\). Since \(\mathsf {att}{\text {-}}\mathsf {start}(n)\) events are the only ones with output of the right kind, \(e^*=\mathsf {att}{\text {-}}\mathsf {start}(n)\) as well. Thus we can extend \(\alpha \) by mapping each such e to the corresponding \(e^*\). The rules for \(S(\mathcal {Q})\) say that \(e\prec _{S(\mathcal {Q})}e'\) only when Q has n in the nonce field, and Q occurs before the value recorded by \(e'\). In E, \(e^*\) precedes the event producing Q (by Lemma 4) which in turn precedes \(e'\) by Lemmas 4 and 5. Thus the orderings in \(S(\mathcal {Q})\) involving \(\mathsf {att}{\text {-}}\mathsf {start}(n)\) events are also reflected in E. \(\square \)
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Rowe, P.D. (2016). Bundling Evidence for Layered Attestation. In: Franz, M., Papadimitratos, P. (eds) Trust and Trustworthy Computing. Trust 2016. Lecture Notes in Computer Science(), vol 9824. Springer, Cham. https://doi.org/10.1007/978-3-319-45572-3_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-45572-3_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-45571-6
Online ISBN: 978-3-319-45572-3
eBook Packages: Computer ScienceComputer Science (R0)