Root-of-Trust Abstractions for Symbolic Analysis: Application to Attestation Protocols

Abstract

A key component in building trusted computing services is a highly secure anchor that serves as a Root-of-Trust (RoT). There are several works that conduct formal analysis on the security of such commodity RoTs (or parts of it), and also a few ones devoted to verifying the trusted computing service as a whole. However, most of the existing schemes try to verify security without differentiating the internal cryptography mechanisms of the underlying hardware token from the client application cryptography. This approach limits, to some extent, the reasoning that can be made about the level of assurance of the overall system by automated reasoning tools. In this work, we present a methodology that enables the use of formal verification tools towards verifying complex protocols using trusted computing. The focus is on reasoning about the overall application security, provided from the integration of the RoT services, and how these can translate to larger systems when the underlying cryptographic engine is considered perfectly secure. Using the Tamarin prover, we demonstrate the feasibility of our approach by instantiating it for a TPM-based remote attestation service, which is one of the core security services needed in today’s increased attack landscape.

Appendices

A Create a TPM Key with PCR Policy

We show a simplified example on the usage of EA. We note that, for clarity, we are omitting many details on TPM internals and TPM objects; see [3, 25,26,27]. In brief, the user executes the command TPM2_StartAuthSession(TRIAL) in order to initiate a fresh trial session. The TPM creates a handle $trial_\text {sh}$ for this session, initiates the policy digest $trial_\text {pd}$ to zero and returns $trial_\text {sh}$ to the user. The user executes the command TPM2_PolicyPCR($trial_\text {sh}, pcr_\text {h}, swHash$), which asks the TPM to update the policy digest of the trial session as:

where $H(\ )$ is a hash function. The user executes TPM2_PolicyGetDigest($trial_\text {sh}$) in order to obtain $trial_\text {pd}$ and calls TPM2_Create($trial_{pd}$). The TPM will create a new object (key) $k = (key_{priv}, key_{pub})$ with authorization policy $key_\text {ap} = trial_\text {pd}$ and returns to the user the protected object blob. Now the user creates a policy session s with $\texttt {TPM2\_StartAuthSession}\texttt {(EA)}$ and the TPM sets $s_\text {pd} = nil$ and returns the handle $s_\text {h}$ to the Client. Then, the Client executes the command $\texttt {TPM2\_PolicyPCR}(s_\text {h}, pcr_h, swHash)$ in order to update the policy digest $s_\text {pd}$, and then $\texttt {TPM2\_Load}(s_\text {h}, objectBlob)$ and obtains $k_\text {h}, k_\text {pub}, k_\text {name}$. This procedure is summarized in Fig. 4.

Fig. 4.

Create a TPM key with PCR policy

B SAPiC Syntax

Figure 5 describes the SAPiC syntax. The syntax allows to define a protocol as a process. It is then translated into a set of Tamarin MSRs that adhere to the semantics of the calculus, which is a dialect of the applied pi-calculus [1]. The calculus comprises an order-sorted term algebra with infinite sets of publicly known names $PN$, freshly generated names $FN$, and variables $\mathcal {V}$. It also comprises a signature $\varSigma$, i.e., a set of function symbols, each with an arity. Messages are elements from a set of terms $\mathcal {T}$ over $PN$, $FN$, and $\mathcal {V}$, built by applying the function symbols in $\varSigma$. Events in SAPiC are similar to Tamarin action facts, and they annotate specific parts of the process to be used to define security properties. We denote $\mathcal {F}$ the set of Tamarin action and state facts. As opposed to the applied pi-calculus [1], SAPiC’s input construct in (M, N); P performs pattern matching instead of variable binding. See [4, 15] for the complete details.

Fig. 5.

SAPiC syntax. Notation: $n \in FN , x \in \mathcal {V}, M, N \in \mathcal {T}, F \in \mathcal {F}$.