\documentclass{report}

% Comment out if this isn't the draft!
% \usepackage[firstpageonly]{draftwatermark}

\usepackage[T1]{fontenc}

\usepackage{unicode-math}
\setmainfont{Gentium Basic}
\setmonofont{Fantasque Sans Mono}

\usepackage{microtype}

\usepackage{xcolor}
\definecolor{Thesis}{HTML}{297544}
\definecolor{Thesis2}{HTML}{65d66f}
\definecolor{BG}{HTML}{ffffff}
\definecolor{FG}{HTML}{000000}

% Secret dark theme
% \definecolor{Thesis}{HTML}{65d66f}
% \definecolor{Thesis2}{HTML}{297544}
% \definecolor{FG}{HTML}{f2f2f2}
% \definecolor{BG}{HTML}{0b1210}

\usepackage{listings}
\lstset{frame=single,basicstyle={\footnotesize\ttfamily},linewidth=0.8\textwidth}

\usepackage{graphicx}
\graphicspath{{files/}}

\usepackage[allbordercolors=Thesis]{hyperref}
\newcommand*{\requirementautorefname}{Requirement}

\usepackage{tikz}
\usetikzlibrary{arrows}

\usepackage{array}
\usepackage{booktabs}

\usepackage[labelfont=bf]{caption}

\usepackage[a4paper]{geometry}
\usepackage{parskip}

\newcommand{\unchapter}[2]{
    \setcounter{chapter}{#1}
    \setcounter{section}{0}
    \chapter*{#2}
    \addcontentsline{toc}{chapter}{#2}
}

\usepackage{setspace}
\onehalfspacing

\usepackage{multicol}

\newtheorem{requirement}{Requirement}

\color{FG}
\pagecolor{BG}

\newcommand\certificate[2]{
    \draw [fill=BG] (#1-0.15,#2) -- (#1+0.15,#2) -- (#1+0.15,#2-0.5) -- (#1,#2-0.4) -- (#1-0.15,#2-0.5) -- cycle;
    \draw [fill=BG] (#1,#2) circle (0.25cm);
    \draw [fill=BG] (#1,#2) circle (0.15cm);
}

\begin{document}

\begin{titlepage}

\vspace*{\fill}

\begin{center}
    \includegraphics{unsw}
\end{center}

\vspace{0.5cm}

\begin{center}
    \Large{}School of Computer Science and Engineering\\
    Faculty of Engineering\\
    The University of New South Wales
\end{center}

\vspace{1cm}

\begin{center}
    \Huge \textbf{Secure Boot and TPM Attestation for seL4-Based Systems}
\end{center}

\vspace{0.35cm}

\begin{center}
    \Large{}By Nicholas Berridge-Argent\\
    {\normalsize z5208292}
    
    \vspace{0.25cm}
    
    Supervised by Ihor Kuz and Ben Leslie (Breakaway Consulting)\\
    Assessed by Gernot Heiser
\end{center}

\vspace{0.75cm}

\begin{center}
    \textbf{Thesis C Report} --- Term 3, 2021\\
    Submitted \textit{24\textsuperscript{th} November 2021}
    
    \vspace{0.1cm}
    
    Thesis submitted as a requirement for the degree of\\
    Bachelor of Engineering in Software Engineering (Honours)
\end{center}

\vspace*{\fill}

\end{titlepage}

\begin{abstract}
Secure boot and TPM attestation are two important technologies for validating the integrity of a platform. In this thesis, we will evaluate current approaches to validating platform integrity in seL4-based systems, and develop an approach to integrating hardware-backed secure boot and TPM attestation into seL4-based systems.

We find that TPM attestation is possible on ARM platforms, a common platform of choice for seL4-based systems, and demonstrate a system which provides access to a TPM and TPM attestation on ARM systems for seL4. We also find that there are some flaws with this approach, and conclude by proposing some designs which take advantage of seL4 to provide better security properties.
\end{abstract}

\unchapter{0}{Acknowledgements}

I would like to thank Ihor Kuz and Ben Leslie for their guidance as supervisors for this project, as well as Gernot Heiser for his guidance and feedback as assessor. I would also like to thank my Trustworthy Systems thesis peers and fellow students, for being available to discuss ideas with in the regular student meetings.

Finally, I would like to thank my family and Julie, for all their support during both my degree and this thesis.

\tableofcontents

\unchapter{1}{Introduction}

\section{Motivation}

The year is 2011 --- and over 4 million Windows PCs are participating in a large peer-to-peer botnet, with their users and administrators none the wiser about it \cite{ArsTechAlureon}.

This botnet is formed with a unique piece of malware --- the \textit{Alureon} rootkit --- which made itself known for its ability to infect systems by modifying their \textit{Master Boot Record} (MBR) and running code before the operating system had a chance to start \cite{RegisterAlureon}. This allowed Alureon to easily evade anti-malware software, which often relies on the operating system to provide its functionality.

\autoref{fig:malware} outlines the structure of traditional malware and traditional rootkits, comparing them to Alureon. Traditional malware runs alongside normal applications, making it easier to design, but easy to defend against with operating system-level security features. Rootkits embed themselves in the operating system to avoid detection, but usually run alongside the operating system and thus can be detected or prevented with some clever programming. Alureon is able to circumvent these by running before the operating system is even loaded.

Such an attack was already theorised by security researchers, but this malware and others like it highlighted the importance of protecting a computer before the operating system has a chance to. Our current best defences against this are \textit{secure boot} and \textit{attestation}.

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \draw (0,0) rectangle (3,1);
        \node at (1.5,0.5) {\footnotesize{}Firmware};
        
        \draw (0,1.1) rectangle (3,2.1);
        \node at (1.5,1.6) {\footnotesize{}OS};
        
        \draw (0,2.2) rectangle (1.45,3.2);
        \node at (0.725,2.7) {\footnotesize{}Apps};
        
        \draw [fill=Thesis2] (1.55,2.2) rectangle (3,3.2);
        \node at (2.275,2.7) {\footnotesize{}Malware};
        
        \node at (1.5,-0.25) {\footnotesize{}Normal Malware};
        
        \draw (3.5,0) rectangle (6.5,1);
        \node at (5,0.5) {\footnotesize{}Firmware};
        
        \draw (3.5,1.1) rectangle (4.95,2.1);
        \node at (4.255,1.6) {\footnotesize{}OS};
        
        \draw [fill=Thesis2] (5.05,1.1) rectangle (6.5,2.1);
        \node at (5.775,1.6) {\footnotesize{}Malware};
        
        \draw (3.5,2.2) rectangle (6.5,3.2);
        \node at (5,2.7) {\footnotesize{}Apps};
        
        \node at (5,-0.25) {\footnotesize{}Rootkit};
        
        \draw (7,0) rectangle (10,1);
        \node at (8.5,0.5) {\footnotesize{}Firmware};
        
        \draw [fill=Thesis2] (7,1.1) rectangle (10,1.55);
        \node at (8.5,1.325) {\footnotesize{}Alureon};
        
        \draw (7,1.65) rectangle (10,2.1);
        \node at (8.5,1.875) {\footnotesize{}OS};
        
        \draw (7,2.2) rectangle (10,3.2);
        \node at (8.5,2.7) {\footnotesize{}Apps};
        
        \node at (8.5,-0.25) {\footnotesize{}Alureon Bootkit};
    \end{tikzpicture}
    \caption{Comparing normal malware, rootkits, and the Alureon bootkit.}
    \label{fig:malware}
\end{figure}

\subsection{Application to seL4}

\textit{seL4} is a \textit{microkernel}, with strong security properties guaranteed by a unique design, small \textit{Trusted Computing Base} (TCB), and comprehensive \textit{formal verification} \cite{KleinseL4}. It is popular in embedded systems where a high degree of security or reliability is required. However --- like all security solutions --- seL4 has a pre-defined scope and is not designed to protect against attacks from outside this scope. For seL4, examples of some of these out-of-scope attacks would be:

\begin{itemize}
    \item \textit{Physical attacks.} For example, an attacker attaching a signal analyser to the memory bus and reading memory transactions.
    \item \textit{Improper setup.} For example, having an untrustworthy web server share an address space with an important storage driver.
    \item \textit{Userspace vulnerabilities.} For example, running a publicly accessible database server in userspace with the password `password'.
    \item \textit{Platform attacks.} For example, an attacker modifying the boot image to be a malicious version of seL4.
\end{itemize}

This last attack vector is the one we are interested in, and is similar to the Alureon rootkit described above. Although seL4 would prevent malicious software from accessing the hardware in a privileged way, if the boot image were somehow compromised by a hardware vulnerability or by some limited physical access, then seL4-based systems would still be vulnerable to these kinds of attacks.

One possible defence would be to boot seL4 directly from \textit{Read-Only Memory} (ROM). This would successfully defend against some platform-based attacks, however:

\begin{itemize}
    \item There may still be ways to erase and re-program this ROM, depending on how it was made (for example, if it was \textit{Electronically Eraseable Programmable Read-Only Memory}).
    \item There may be ways to boot code from other sources.
    \item This would make it impossible to upgrade seL4 to enable new features (such as the recently introduced MCS kernel).
    \item If this approach was chosen by manufacturers for other operating systems (e.g. Linux) it would be impossible to install seL4 onto these systems.
\end{itemize}

Secure boot and attestation provide a more flexible and robust defence against platform-based attacks, and address all of the points listed above.

\section{Thesis Problem Statement}

Secure boot and TPM attestation are two important technologies for validating the integrity of a platform. In this thesis, we will evaluate current approaches to validating platform integrity in seL4-based systems, and develop an approach to integrating hardware-backed secure boot and TPM attestation into seL4-based systems. The result will be an seL4-based system protected by secure boot, with a CAmkES module which allows the userspace to access the TPM and provide local and remote attestation.

\unchapter{2}{Background}

First, we will need to examine some of the technologies and cryptographic primitives required to understand secure boot and attestation, then we can start to look at how secure boot and attestation work on a theoretical level and their more common implementations.

\section{Platform Security}

The \textit{platform} of a system refers to the foundational hardware and firmware that a system runs on. Depending on the context, it may also include some portion of the system's software stack. \textit{Platform security} refers to the security of this platform. In particular, where any weaknesses might exist in this platform, and mechanisms to protect or validate it.

Vulnerabilities in the platform could be used to compromise a system in spite of many protections which are applied at a higher level (in the case of Alureon, this was anti-malware software). Therefore, good \textit{defence in depth} measures need to take steps to ensure that the platform is also secured.

\subsection{Booting a System}

A large responsibility of the platform is to \textit{boot} the system. On modern systems, this will involve several stages as outlined in \autoref{fig:bootprocess}:

\begin{enumerate}
    \item The firmware will initialise parts of the hardware, and load some lower level drivers and the bootloader.
    \item The bootloader will start to configure and load the operating system. In some systems there may be multiple stages of bootloaders.
    \item The operating system will load some higher level drivers, and the rest of userspace, which the user will actually interact with.
\end{enumerate}

The user of a modern system will rarely interact with the stages before the operating system. In some cases they may never even see or notice them. However, each of them presents a challenge for platform security.

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \draw (0,0.5) rectangle (2,-0.5);
        \node at (1,0) {\small{}Firmware};

        \draw [->] (2,0) -- (3,1.5);
        \draw [->] (2,0) -- (3,-1.5);

        \draw (3,2) rectangle (5,1);
        \node at (4,1.5) {\small{}Drivers};

        \draw (3,-1) rectangle (5,-2);
        \node at (4,-1.5) {\small{}Bootloader};

        \draw (6,-1) rectangle (8,-2);
        \node at (7,-1.5) {\small{}Bootloaders...};

        \draw [->] (5,-1.5) -- (6,-1.5);
        \draw [->] (8,-1.5) -- (9,0);

        \draw (9,0.5) rectangle (11,-0.5);
        \node at (10,0) {\small{}Kernel};

        \draw [->] (11,0) -- (12,1.5);
        \draw [->] (11,0) -- (12,-1.5);

        \draw (12,2) rectangle (14,1);
        \node at (13,1.5) {\small{}Drivers};

        \draw (12,-1) rectangle (14,-2);
        \node at (13,-1.5) {\small{}Userspace};
    \end{tikzpicture}
    \caption{Boot Process for Modern Systems}
    \label{fig:bootprocess}
\end{figure}

\subsection{Evil Maid Attack}

The \textit{evil maid attack} is a hypothetical threat model proposed by security researcher Joanna Rutkowska \cite{RutkowskaBitLocker} which works based on limited physical access to a system. It describes a situation where:

\begin{enumerate}
    \item Someone (the target) is staying at a hotel, and leaves their laptop in their room while they go out.
    \item While they are gone, the evil maid enters their room and accesses their laptop.
    \item The evil maid boots the laptop's firmware and installs a new piece of malware to the MBR.
    \item The malware runs transparently underneath the operating system, and its only purpose is to collect passwords and encryption keys.
\end{enumerate}

At this point the system is already compromised, although in the full threat model the maid returns the next day after the laptop has been used for one night and uninstalls the malware, leaving no traces.

\textit{Secure boot} and \textit{attestation} both provide defences against the evil maid attack, and similar attacks targeting the platform.

\subsection{Secure Boot}

\textit{Secure boot} (also occasionally called trusted boot) is a technique for ensuring that only trusted code is ever booted on a system. To do this, it makes use of \textit{cryptographic signatures}.

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \draw (0,0) rectangle (3,1.5);
        \certificate{3}{0}
        \node at (1.5,0.75) {\small{}Bootloader};

        \draw [->] (3,0.75) -- (4,0.75);

        \draw (4,0) rectangle (7,1.5);
        \certificate{7}{0}
        \node at (5.5,0.75) {\small{}Bootloader};

        \draw [->] (7,0.75) -- (8,0.75);

        \draw (8,0) rectangle (11,1.5);
        \certificate{11}{0}
        \node at (9.5,0.75) {\small{}Kernel};

        \draw (4.5,-1) rectangle (6.5,-2);
        \node at (5.5,-1.5) {\small{}Keys};

        \draw [->] (4.5,-1.5) to [bend left] (1.5,0);
        \draw [->] (6.5,-1.5) to [bend right] (9.5,0);
        \draw [->] (5.5,-1) -- (5.5,0);
    \end{tikzpicture}
    \caption{A high-level overview of secure boot.}
    \label{fig:secureboothigh}
\end{figure}

\autoref{fig:secureboothigh} outlines the changes to the boot process with secure boot. Each stage of the boot process checks a cryptographic signature for the next stage against a list of known trusted public keys. If this signature is invalid or untrusted, that stage of the boot will refuse to boot the next stage. This forms a \textit{chain of trust}, in which each stage of the boot has established trust in the next, up to the userspace.

But this poses a question: If a system boots with secure boot, is it secure? Secure boot only produces a binary output of success or failure, a system either boots or does not boot. If it does boot, there may still be reasons why it is not secure:

\begin{itemize}
    \item The private keys used for the cryptographic signatures may have been compromised.
    \item The system may have been set up deliberately to boot an older and insecure version of an operating system, which would still have a valid signature.
    \item Secure boot may have been turned off, either through a software vulnerability or some limited physical access.
    \item There may be a bug in the secure boot implementation itself (see \textit{boothole} \cite{NVDBoothole}).
\end{itemize}

Attestation can provide a more flexible solution to platform security.

\subsection{Attestation}

\textit{Attestation} (also occasionally called \textit{measured boot}) is a technique for securely measuring the state of a system's platform and reporting that to a trusted third party (local or remote). To do this, it makes use of \textit{cryptographic hashes}, \textit{asymmetric encryption} and some \textit{secure hardware}.

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \draw (0,0) rectangle (3,1.5);
        \node at (1.5,0.75) {\small{}Bootloader};

        \draw [->] (3,0.75) -- (4,0.75);

        \draw (4,0) rectangle (7,1.5);
        \node at (5.5,0.75) {\small{}Bootloader};

        \draw [->] (7,0.75) -- (8,0.75);

        \draw (8,0) rectangle (11,1.5);
        \node at (9.5,0.75) {\small{}Kernel};

        \draw [dotted] (0,-0.5) -- (11,-0.5);
        \node [anchor=west] at (11.25,-0.5) {\small{}\textit{Isolation}};

        \draw (4.5,-1) rectangle (6.5,-2);
        \node at (5.5,-1.5) {\small{}Measurements};

        \draw [->] (1.5,0) to [bend right] (4.5,-1.5);
        \draw [->] (9.5,0) to [bend left] (6.5,-1.5);
        \draw [->] (5.5,0) -- (5.5,-1);
    \end{tikzpicture}
    \caption{A high-level overview of attestation.}
    \label{fig:attestationhigh}
\end{figure}

\autoref{fig:attestationhigh} outlines the boot process with attestation. Each stage of the boot process computes a cryptographic hash of the code and the configuration for the next stage. These are then stored in \textit{secure storage} that is backed by either hardware or firmware to prevent certain kinds of modification. This also forms a chain of trust as with secure boot, but also produces a trusted \textit{measurement} of the state of the system. This measurement can then be sent via asymmetric encryption to a trusted third party to be verified against some known secure values.

This is ideal compared to secure boot because even if an attacker could somehow disable these security measures, they would not be able to fake the produced measurements, and so would not be able to properly attest the system to a third party verifier.

However, unlike secure boot which can be done entirely within the system it protects and can stop an insecure system from running in the first place, attestation does require a third party to verify it and cannot necessarily stop an insecure system from booting.

\section{Cryptographic Primitives}

In order to fully understand how secure boot and attestation work and how they are implemented on most systems, we need to understand a few of the cryptographic primitives being used.

\subsection{Cryptographic Hashes}

A \textit{cryptographic hash function} is a function $H(x)$ which takes a sequence of bytes $x$ and produces another fixed-length sequence of bytes called a hash (also called a digest) which ``summarises'' the input bytes. Ideal cryptographic hash functions have two properties which we are interested in:

\begin{itemize}
    \item Given only the hash of a sequence of bytes $H(x)$, it should be impossible to find the original sequence of bytes $x$ except from by using brute force. In this way, the hash function is said to be a \textit{one-way function}.
    \item Given a sequence of bytes $x$ and its hash $H(x)$, it should be impossible to find another sequence of bytes $y$ such that $H(x)=H(y)$. In this case $x$ and $y$ are said to be colliding. In practice due to the pigeon hole principle each sequence of bytes has an infinite number of collisions (for instance in SHA256, there are ``only'' $2^256$ possible hash values, but many more possible input sequences), but it should be computationally difficult to find a useful collision for a given sequence of bytes.
\end{itemize}

The properties of hash functions are demonstrated in \autoref{fig:hashes}. An example of a modern, secure cryptographic hash function is \textit{SHA256}.

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \draw (0,0) rectangle (3,2);
        \node at (1.5,1) {\small\begin{tabular}{l}\texttt{open("file1");}\\\texttt{write(buf);}\\\texttt{i = j * k;}\\\texttt{return i;}\end{tabular}};

        \node [circle,draw=FG] (hash) at (4,1) {$H$};
        \draw (3,1) -- (hash);
        \draw [->] (hash) -- (5,1);

        \draw (5,0) rectangle (8,2);
        \node at (6.5,1) {\small\begin{tabular}{l}\texttt{bbdfed14fd56b1db}\\\texttt{51914e3c46bc0b4f}\\\texttt{bd74c2ebb3c1979d}\\\texttt{1a10a322d5488649}\end{tabular}};

        \node [circle,draw=FG] (unknown) at (9,1) {?};
        \draw [->] (8,1) -- (unknown);

        \draw (0,-1) rectangle (3,-3);
        \node at (1.5,-2) {\small\begin{tabular}{l}\texttt{\color{Thesis}open("file2");}\\\texttt{\color{FG}write(buf);}\\\texttt{\color{FG}i = j * k;}\\\texttt{\color{FG}return i;}\end{tabular}};

        \node [circle,draw=FG] (hash2) at (4,-2) {$H$};
        \draw (3,-2) -- (hash2);
        \draw [->] (hash2) -- (5,-2);

        \draw (5,-1) rectangle (8,-3);
        \node at (6.5,-2) {\small\begin{tabular}{l}\texttt{5104bdc22c7b4022}\\\texttt{c1807fa93cfe3b73}\\\texttt{337c7ad09b1de359}\\\texttt{f3ef6f4a2704ac8a}\end{tabular}};
    \end{tikzpicture}
    \caption{Properties of cryptographic hashes. \textit{Top:} One we have a hash, it is not possible to find the original data. \textit{Bottom:} If the input data changes, the resulting hash changes significantly.}
    \label{fig:hashes}
\end{figure}

\subsection{Asymmetric Encryption}

\textit{Asymmetric encryption} is a form of encryption where encrypting and decrypting require different keys. In particular, we have two keys: a \textit{public key} (usually denoted $K^+$) which is shared publicly, and a \textit{private key} (usually denoted $K^-$) which is kept secret. These two keys are generated in pairs, and can only be used as that particular pair. With these two keys, we have the following rules:

\begin{itemize}
    \item If some bytes are encrypted using a public key, they can only be decrypted using the corresponding private key.
    \item Similarly, if some bytes are encrypted using a private key, they can only be decrypted using the corresponding public key.
\end{itemize}

As with other encryption, it should be impossible to decrypt data without having the required key (public or private).

The properties of asymmetric encryption are demonstrated in \autoref{fig:asymcrypt}. An example of a modern, secure asymmetric encryption algorithm is \textit{RSA}.

\begin{figure}
    \centering
    \begin{tikzpicture}
        \draw (0,0) rectangle (3,2);
        \node at (1.5,1) {\small\begin{tabular}{l}\texttt{open("file1");}\\\texttt{write(buf);}\\\texttt{i = j * k;}\\\texttt{return i;}\end{tabular}};

        \node [circle,draw=FG] (privkey) at (4,1) {\small{}$K^-$};

        \draw (3,1) -- (privkey);
        \draw [->] (privkey) -- (5,1);

        \draw (5,0) rectangle (8,2);
        \node at (6.5,1) {\small\begin{tabular}{l}\texttt{89f6bc74ee91deff}\\\texttt{a4a4245af07b1f0f}\\\texttt{ffa43eb39a47e9af}\\\texttt{7e45fcfb9a852806}\end{tabular}};

        \draw (10,0) rectangle (13,2);
        \node at (11.5,1) {\small\begin{tabular}{l}\texttt{open("file1");}\\\texttt{write(buf);}\\\texttt{i = j * k;}\\\texttt{return i;}\end{tabular}};

        \node [circle,draw=FG] (pubkey) at (9,1) {\small{}$K^+$};

        \draw (8,1) -- (pubkey);
        \draw [->] (pubkey) -- (10,1);
        
        \draw (0,-1) rectangle (3,-3);
        \node at (1.5,-2) {\small\begin{tabular}{l}\texttt{open("file1");}\\\texttt{write(buf);}\\\texttt{i = j * k;}\\\texttt{return i;}\end{tabular}};

        \node [circle,draw=FG] (pubkey2) at (4,-2) {\small{}$K^+$};

        \draw (3,-2) -- (pubkey2);
        \draw [->] (pubkey2) -- (5,-2);

        \draw (5,-1) rectangle (8,-3);
        \node at (6.5,-2) {\small\begin{tabular}{l}\texttt{89f6bc74ee91deff}\\\texttt{a4a4245af07b1f0f}\\\texttt{ffa43eb39a47e9af}\\\texttt{7e45fcfb9a852806}\end{tabular}};

        \draw (10,-1) rectangle (13,-3);
        \node at (11.5,-2) {\small\begin{tabular}{l}\texttt{open("file1");}\\\texttt{write(buf);}\\\texttt{i = j * k;}\\\texttt{return i;}\end{tabular}};

        \node [circle,draw=FG] (privkey2) at (9,-2) {\small{}$K^-$};

        \draw (8,-2) -- (privkey2);
        \draw [->] (privkey2) -- (10,-2);
    \end{tikzpicture}
    \caption{Properties of asymmetric encryption. Note the switched use of public and private keys.}
    \label{fig:asymcrypt}
\end{figure}

\subsection{Cryptographic Signatures}

\textit{Cryptographic signatures} make use of both cryptographic hashes and asymmetric encryption to be able to ``sign'' a blob of data, ensuring that the data is known to be correct and valid by some trusted third party.

Suppose that person A produces a sequence of bytes they wish to sign. They take that sequence of bytes, compute the cryptographic hash of that sequence of bytes, and encrypt it with their private key. This encrypted cryptographic hash is the \textit{signature} and is distributed with that sequence of bytes.

Person B now wants to verify the integrity of that sequence of bytes. They take the sequence of bytes which they received and compute the same cryptographic hash. Then, they take the signature that was distributed with that sequence of bytes, separately request person A's public key, and decrypt the signature. If the cryptographic hashes match, we know that sequence of bytes was definitely produced by person A and was not modified.

Without a copy of person A's private key, it would not be possible to modify the sequence of bytes \textit{and} produce a signature which is valid when using person A's public key.

This does introduce some problems:

\begin{itemize}
    \item We still need to trust person A to give us the correct sequence of bytes. This is particularly important when person A is only responsible for signing bytes, and not creating them.
    \item If an attacker steals person A's private key, they can produce valid signatures for any sequence of bytes.
    \item We need a way to securely obtain person A's public key. If they are both sent over the same communications channel, an attacker could replace the sequence of bytes, signature \textit{and} public key with their own.
\end{itemize}

\subsection{Blockchain}

These days, when we think of the word ``blockchain'', we think of cryptocurrency. However, a \textit{blockchain} is actually a simpler concept than that, it is a series of blocks of data each linked using a \textit{cryptographic hash}.

Each \textit{block} starts with the hash of the previous block, meaning that modifying any one block will cause the rest of the blockchain to also be modified. By checking the hash and value of the last block, we effectively have an ordered cryptographic \textit{summary} of an entire sequence of blocks.

In some implementations, attestation uses a similar construct to a blockchain to measure the state of the platform. The properties of blockchains are demonstrated in \autoref{fig:blockchains}.

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \draw (0,0) rectangle (3,4);
        \node at (1.5,1) {\small\begin{tabular}{l}\texttt{open("file1");}\\\texttt{write(buf);}\\\texttt{i = j * k;}\\\texttt{return i;}\end{tabular}};
        \draw [dotted] (0.25,2) -- (2.75,2);
        \node at (1.5,3) {\small\begin{tabular}{l}\texttt{0000000000000000}\\\texttt{0000000000000000}\\\texttt{0000000000000000}\\\texttt{0000000000000000}\end{tabular}};

        \node [circle,draw=FG] (hash) at (3.75,3) {$H$};
        \draw (3,2) -- (hash);
        \draw [->] (hash) -- (4.5,3);

        \draw (4.5,0) rectangle (7.5,4);
        \node at (6,1) {\small\begin{tabular}{l}\texttt{fans=ON}\\\texttt{backdoor=OFF}\\\texttt{secureboot=ON}\\\texttt{debug=ON}\end{tabular}};
        \draw [dotted] (4.75,2) -- (7.25,2);
        \node at (6,3) {\small\begin{tabular}{l}\texttt{bbdfed14fd56b1db}\\\texttt{51914e3c46bc0b4f}\\\texttt{bd74c2ebb3c1979d}\\\texttt{1a10a322d5488649}\end{tabular}};
        
        \node [circle,draw=FG] (hash2) at (8.25,3) {$H$};
        \draw (7.5,2) -- (hash2);
        \draw [->] (hash2) -- (9,3);

        \draw (9,0) rectangle (12,4);
        \node at (10.5,1) {\small\begin{tabular}{l}\texttt{KEYS:}\\\texttt{6b3a55e0261b}\\\texttt{46a9d5bde718}\\\texttt{f33ae3bc9a22}\end{tabular}};
        \draw [dotted] (9.25,2) -- (11.75,2);
        \node at (10.5,3) {\small\begin{tabular}{l}\texttt{fa794b374b824eae}\\\texttt{e5c8196b73969d25}\\\texttt{5ef176d04204f480}\\\texttt{be55b4dd4d1cef58}\end{tabular}};
        
        \draw (0,-0.5) rectangle (3,-4.5);
        \node at (1.5,-3.5) {\small\begin{tabular}{l}\texttt{\color{Thesis}open("file2");}\\\texttt{\color{FG}write(buf);}\\\texttt{\color{FG}i = j * k;}\\\texttt{\color{FG}return i;}\end{tabular}};
        \draw [dotted] (0.25,-2.5) -- (2.75,-2.5);
        \node at (1.5,-1.5) {\small\begin{tabular}{l}\texttt{0000000000000000}\\\texttt{0000000000000000}\\\texttt{0000000000000000}\\\texttt{0000000000000000}\end{tabular}};

        \node [circle,draw=FG] (hash) at (3.75,-1.5) {$H$};
        \draw (3,-2.5) -- (hash);
        \draw [->] (hash) -- (4.5,-1.5);

        \draw (4.5,-0.5) rectangle (7.5,-4.5);
        \node at (6,-3.5) {\small\begin{tabular}{l}\texttt{fans=ON}\\\texttt{backdoor=OFF}\\\texttt{secureboot=ON}\\\texttt{debug=ON}\end{tabular}};
        \draw [dotted] (4.75,-2.5) -- (7.25,-2.5);
        \node at (6,-1.5) {\small\color{Thesis}\begin{tabular}{l}\texttt{5104bdc22c7b4022}\\\texttt{c1807fa93cfe3b73}\\\texttt{337c7ad09b1de359}\\\texttt{f3ef6f4a2704ac8a}\end{tabular}};
        
        \node [circle,draw=FG] (hash2) at (8.25,-1.5) {$H$};
        \draw (7.5,-2.5) -- (hash2);
        \draw [->] (hash2) -- (9,-1.5);

        \draw (9,-0.5) rectangle (12,-4.5);
        \node at (10.5,-3.5) {\small\begin{tabular}{l}\texttt{KEYS:}\\\texttt{6b3a55e0261b}\\\texttt{46a9d5bde718}\\\texttt{f33ae3bc9a22}\end{tabular}};
        \draw [dotted] (9.25,-2.5) -- (11.75,-2.5);
        \node at (10.5,-1.5) {\color{Thesis}\small\begin{tabular}{l}\texttt{40006a4f2e37bf63}\\\texttt{bf869f161c3d48e7}\\\texttt{e2a05cba947208c1}\\\texttt{1b91802491d67091}\end{tabular}};
    \end{tikzpicture}
    \caption{Properties of blockchains. If an earlier input changes, the results are seen in the final hash value.}
    \label{fig:blockchains}
\end{figure}

\section{UEFI Secure Boot}

The \textit{Unified Extensible Firmware Interface} (UEFI) is a common firmware interface for many x86 systems. Of particular interest to us, it standardises the most common implementation of secure boot, using cryptographic signatures \cite{UEFISpec}. This implementation of secure boot is shown in more depth in \autoref{fig:uefisecureboot}.

In this implementation of secure boot, any bootable or low-level code (bootloaders, drivers, the operating system) needs to include a trusted signature in order to be booted. To solve the public key distribution problem, these signatures are verified against keys which are pre-installed onto the system at the manufacturing time. Most systems include a copy of \textit{Microsoft's} public key, but some systems allow the end users to \textit{enrol} their own extra public keys under certain circumstances.

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \node at (-1,0.75) {\footnotesize{}System};
    
        \draw (0,0) rectangle (2.5,1.5);
        \node at (1.25,0.75) {\scriptsize\begin{tabular}{l}\texttt{open("file1");}\\\texttt{write(buf);}\\\texttt{i = j * k;}\\\texttt{return i;}\end{tabular}};
        \node at (1.25,-0.25) {\footnotesize{}Booting Code};
        
        \node [rectangle,draw=FG] (syshash) at (3.25,0.75) {\scriptsize{}Hash};
        \draw (2.5,0.75) -- (syshash);
        \draw [->] (syshash) -- (4,0.75);
        
        \draw (4,0) rectangle (6.5,1.5);
        \node at (5.25,0.75) {\scriptsize\begin{tabular}{l}\texttt{bbdfed14fd56b1db}\\\texttt{51914e3c46bc0b4f}\\\texttt{bd74c2ebb3c1979d}\\\texttt{1a10a322d5488649}\end{tabular}};
        \node at (5.25,-0.25) {\footnotesize{}\textit{Compare Hashes}};
        
        \node [rectangle,draw=FG] (syscrypt) at (7.25,0.75) {\scriptsize{}Decrypt};
        \draw [->] (syscrypt) -- (6.5,0.75);
        \draw (8,0.75) -- (syscrypt);
        
        \node [rectangle,draw=FG] (syskey) at (7.25,-0.75) {\scriptsize{}Public Key};
        \draw [->] (syskey) -- (syscrypt);
        
        \draw (8,0) rectangle (10.5,1.5);
        \node at (9.25,0.75) {\scriptsize\begin{tabular}{l}\texttt{89f6bc74ee91deff}\\\texttt{a4a4245af07b1f0f}\\\texttt{ffa43eb39a47e9af}\\\texttt{7e45fcfb9a852806}\end{tabular}};
        \node at (9.25,-0.25) {\footnotesize{}Signature};
        
        \draw [fill=BG] (10.35,0) -- (10.65,0) -- (10.65,-0.5) -- (10.5,-0.4) -- (10.35,-0.5) -- cycle;
        \draw [fill=BG] (10.5,0) circle (0.25cm);
        \draw [fill=BG] (10.5,0) circle (0.15cm);
        
        \draw [dotted] (-2,2.25) -- (10,2.25);
        
        \node at (-1,3.75) {\footnotesize{}Manufacturer};
    
        \draw (0,3) rectangle (2.5,4.5);
        \node at (1.25,3.75) {\scriptsize\begin{tabular}{l}\texttt{open("file1");}\\\texttt{write(buf);}\\\texttt{i = j * k;}\\\texttt{return i;}\end{tabular}};
        \node at (1.25,2.75) {\footnotesize{}Bootable Code};
        
        \node [rectangle,draw=FG] (mfhash) at (3.25,3.75) {\scriptsize{}Hash};
        \draw (2.5,3.75) -- (mfhash);
        \draw [->] (mfhash) -- (4,3.75);
        
        \draw (4,3) rectangle (6.5,4.5);
        \node at (5.25,3.75) {\scriptsize\begin{tabular}{l}\texttt{bbdfed14fd56b1db}\\\texttt{51914e3c46bc0b4f}\\\texttt{bd74c2ebb3c1979d}\\\texttt{1a10a322d5488649}\end{tabular}};
        \node at (5.25,2.75) {\footnotesize{}Hash};
        
        \node [rectangle,draw=FG] (mfcrypt) at (7.25,3.75) {\scriptsize{}Encrypt};
        \draw (6.5,3.75) -- (mfcrypt);
        \draw [->] (mfcrypt) -- (8,3.75);
        
        \node [rectangle,draw=FG] (mfkey) at (7.25,5.25) {\scriptsize{}Private Key};
        \draw [->] (mfkey) -- (mfcrypt);
        
        \draw (8,3) rectangle (10.5,4.5);
        \node at (9.25,3.75) {\scriptsize\begin{tabular}{l}\texttt{89f6bc74ee91deff}\\\texttt{a4a4245af07b1f0f}\\\texttt{ffa43eb39a47e9af}\\\texttt{7e45fcfb9a852806}\end{tabular}};
        \node at (9.25,2.75) {\footnotesize{}Signature};
        
        \draw [fill=BG] (10.35,3) -- (10.65,3) -- (10.65,2.5) -- (10.5,2.6) -- (10.35,2.5) -- cycle;
        \draw [fill=BG] (10.5,3) circle (0.25cm);
        \draw [fill=BG] (10.5,3) circle (0.15cm);
        
        \draw [->] (10.5,3.75) to [bend left] node [sloped,midway,above] {\scriptsize{}Distributed with Code} (10.5,0.75);
    \end{tikzpicture}
    \caption{Implementation of secure boot in UEFI. Implementation in other systems will be similar.}
    \label{fig:uefisecureboot}
\end{figure}

\section{Trusted Platform Module}

\begin{figure}[h]
    \centering
    \includegraphics[width=0.5\textwidth]{tpm-photo}
    \caption{A discrete hardware TPM installed on a PC motherboard. This particular TPM appears to be a SLB 9635 TT 1.2 from Infineon, implementing the older TPM 1.2 standard. Image by Wikimedia user \textit{FxJ}. Source: \url{https://en.wikipedia.org/wiki/Trusted\_Platform\_Module\#/media/File:TPM\_Asus.jpg}}
    \label{fig:tpmphoto}
\end{figure}

Attestation requires some form of secure hardware or firmware to work properly. On larger systems, this comes from a dedicated \textit{trusted platform module} (TPM) such as the one shown in \label{fig:tpmphoto}. A TPM is a module in hardware or firmware which implements an interface standardised by the \textit{trusted computing group} (TCG) as part of two separate specifications: TPM 1.2 and TPM 2.0 \cite{TPMSpec}.

A TPM might provide any number of useful functions:

\begin{itemize}
    \item A secure clock, secure counter, and / or secure random number source, all of which can be used to prevent replay attacks in secure protocols.
    \item Secure encryption and decryption functionality, so that cryptography can be performed separately from the rest of the system.
    \item Secure key storage, where private keys may be set up to never leave the TPM, or may be set up to only be used if certain conditions are met.
\end{itemize}

The feature we are most interested in are the \textit{platform configuration registers} (PCRs).

Embedded systems may not be able to justify the cost of a discrete hardware TPM and often have their own security features implemented. However, there are ways to implement a firmware TPM on some embedded systems, which we will look at in \autoref{sec:ftpm}.

\subsection{Platform Configuration Registers}

The \textit{platform configuration registers} (PCRs) are a special kind of secure storage available on a TPM. In particular, they can be read at any time, but can only be modified using a special {\sffamily{}Extend} operation:

\[
    \mathsf{Extend}\,(P,x) \: : \: P := H(P\;\|\; x)
\]

This forms what is effectively a \textit{blockchain} within a given PCR. If one PCR $P$ has {\sffamily{}Extend} called with values $x_1$, $x_2$ and $x_3$, the resulting value is:

\[
    P = H(H(H(x_1)\;\|\; x_2)\;\|\; x_3)
\]

If any one of the $x_i$ are changed, each of the hashes would change, resulting in a different final value for the PCR once it gets read.

A TPM normally has several PCRs, each for the code and configuration elements of a different stage in the boot process. Some are also typically reserved for future use, or available to be used by other userspace processes. \autoref{tab:pcralloc} shows an example PCR allocation for 24 PCRs. Not all TPMs will have the same number of PCRs, and the allocation may vary depending on the exact platform and software stack.

Although specific PCR values imply that specific events took place during the boot process, the PCR values do not reveal the whole boot process themselves. In order to make understanding the boot process easier, TPMs may also include a slightly less secured but more verbose \textit{event log} which lists all events that are used to extend the PCRs. In this way, if the PCR values are incorrect or unexpected, it is possible to see why.

Another critical detail about the PCRs is that the values in them are dependent on the order they are written. For example, if a system once loads $x_1$, $x_2$ and $x_3$ in that order, and then later loads $x_1$, $x_3$ and $x_2$ in that order, the PCR values would not match since:

\[
    H(H(H(x_1)\;\|\; x_2)\;\|\; x_3) \neq H(H(H(x_1)\;\|\; x_3)\;\|\; x_2)
\]

Because of this, great care needs to be taken to initialise the system in a pre-defined order, and no steps can be parallelised.

\begin{table}[h]
    \centering
    \begin{tabular}{ll}
        \toprule
        PCR Numbers & Hashed Contents \\
        \midrule
        0 \& 1      & BIOS \& BIOS configuration \\
        2 \& 3      & Low-level firmware \& associated configuration \\
        4 \& 5      & MBR \& MBR configuration \\
        6           & State transitions \& wake events \\
        7           & Manufacturer specific measurements \\
        8--15       & Operating-system specific measurements \\
        16          & Debugging information \\
        10          & Linux kernel \\
        11          & Linux \texttt{initramfs} \\
        12          & Linux kernel command line \\
        13          & GRUB commands \& configuration \\
        14          & Secure boot shim keys \& state \\
        15          & Unused \\
        16          & Debug measurements \\
        17--22      & Unused \\
        23          & Application specific measurements \\
        \bottomrule
    \end{tabular}
    \caption{An example PCR allocation for Linux on an x86 PC, from \cite{SpringerPCRs}.}
    \label{tab:pcralloc}
\end{table}

\subsection{TPM Attestation}

\textit{TPM attestation} is an implementation of attestation that uses the hardware / firmware security features provided by the TPM.

Starting at a small, trusted piece of software referred to as the \textit{Core Root of Trust Measurement} (CRTM), each stage of the boot will calculate a cryptographic hash of the code and the configuration of the next stages of the boot process, and will store these hashes in a PCR.

Once the system has booted into userspace, the PCR values contain a cryptographic summary of the state of the platform up to that point. To ensure that the correct values of the PCRs can be read by the third party verifier, the TPM first encrypts them with a private key that is stored securely inside the TPM. The manufacturer of the TPM publishes the corresponding public key, and the third party verifier can then decrypt the PCR values on a trusted system and check them against known good PCR values.

An attacker cannot modify part of the boot process, as an earlier part of the boot process would extend a PCR with a different value, which would cause the set of PCR values to differ. An attacker also cannot just modify the operating system's TPM driver to return fake PCR values, since the PCR values are encrypted first using an inaccessible private key. The TPM's secure clock / counter / random number source can also be used here to prevent replay attacks.

\subsection{Remote Attestation}

\textit{Remote attestation} refers to the specific variant of TPM attestation where the trusted third party is another computer accessible via. the network. The encrypted PCR values are then sent to this remote verifier, which then decrypts them and verifies they are correct.

The remote verifier can then use this information in a number of ways. For example, if the PCR values are incorrect, it could \cite{GarrettRemote}:

\begin{itemize}
    \item Prevent that system from accessing the network, or sensitive network resources such as security cameras or network attached storage.
    \item Prevent that system from \textit{being} accessed via. the network, to stop it from impersonating a trusted host on the network.
    \item Notify a system administrator.
\end{itemize}

However, notably, it cannot stop the system itself from starting unless it has control over that system's power supply. It also cannot do any of these things unless there is a connection between it and the system being verified.

\autoref{fig:remoteattestation} shows an overview of how remote attestation works using a TPM. A more detailed description including the precise commands is given later in \autoref{sec:tpmcommands}.

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \draw (0,0) rectangle (2,1);
        \node at (1,0.5) {\small{}Bootloader};

        \draw [->] (2,0.5) -- (3,0.5);

        \draw (3,0) rectangle (5,1);
        \node at (4,0.5) {\small{}Bootloader};

        \draw [->] (5,0.5) -- (6,0.5);

        \draw (6,0) rectangle (8,1);
        \node at (7,0.5) {\small{}Kernel};

        \draw [->] (8,0.5) -- (9,0.5);

        \draw (9,0) rectangle (11,1);
        \node at (10,0.5) {\small{}Userspace};

        \draw (3,-1) rectangle (5,-2);
        \node at (4,-1.5) {\small{}PCRs};

        \draw [->] (1,0) -- (3.5,-1);
        \draw [->] (4,0) -- (4,-1);
        \draw [->] (7,0) -- (4.5,-1);

        \draw [->] (5,-1.5) -- (6,-1.5);

        \draw (6,-1) rectangle (8,-2);
        \node at (7,-1.5) {\small{}Private Key};

        \draw [->] (8,-1.5) to [bend right] (10,0);

        \draw (6,2) rectangle (8,3);
        \node at (7,2.5) {\small{}Public Key};

        \draw [->] (10,1) to [bend right] (8,2.5);

        \draw (3,2) rectangle (5,3);
        \node at (4,2.5) {\small{}Verifier};

        \draw [->] (6,2.5) -- (5,2.5);

        \draw [dotted] (0,-0.5) -- (11,-0.5);
        \draw [dotted] (0,1.5) -- (11,1.5);

        \node [anchor=west] at (11.25,0.5) {\small\textit{System}};
        \node [anchor=west] at (11.25,-1.5) {\small\textit{TPM}};
        \node [anchor=west] at (11.25,2.5) {\small\textit{Remote}};
    \end{tikzpicture}
    \caption{A high-level overview of remote attestation.}
    \label{fig:remoteattestation}
\end{figure}

\subsection{Local Attestation}

\textit{Local attestation} is also possible using a TPM, in which the trusted third party is a human operator with physical access to the computer. This works slightly differently to remote attestation and makes use of a TPM's \textit{data sealing} functionality.

A TPM can be asked to keep encrypted data and the corresponding keys in secure storage, and will then only decrypt and provide this data to the userspace if the PCR values match a known good value that was set when the data was originally stored. This process is known as \textit{sealing} data.

\autoref{fig:localattestation} gives a high-level overview of how local attestation works. Local attestation can be implemented by sealing a small passphrase which can be manually inspected inside the TPM, as is done in \cite{ConstableSABLE}. When the system boots, the system will present the passphrase to the user and ask them to verify that the passphrase is correct. If any parts of the boot process have been modified, the TPM will not return the passphrase to the userspace, and the system cannot present the correct passphrase.

This differs from remote attestation in that it requires a human operator to be physically present when the system boots, but does not require any kind of remote access to a third party verifier. This would make it ideal for slightly different use cases, such as air-gapped systems.

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \draw (0,0) rectangle (2,1);
        \node at (1,0.5) {\small{}Bootloader};

        \draw [->] (2,0.5) -- (3,0.5);

        \draw (3,0) rectangle (5,1);
        \node at (4,0.5) {\small{}Bootloader};

        \draw [->] (5,0.5) -- (6,0.5);

        \draw (6,0) rectangle (8,1);
        \node at (7,0.5) {\small{}Kernel};

        \draw [->] (8,0.5) -- (9,0.5);

        \draw (9,0) rectangle (11,1);
        \node at (10,0.5) {\small{}Userspace};

        \draw (3,-1) rectangle (5,-2);
        \node at (4,-1.5) {\small{}PCRs};

        \draw [->] (1,0) -- (3.5,-1);
        \draw [->] (4,0) -- (4,-1);
        \draw [->] (7,0) -- (4.5,-1);

        \draw [->] (5,-1.5) -- (6,-1.5);

        \draw (6,-1) rectangle (8,-2);
        \node at (7,-1.5) {\small{}Passphrase};

        \draw [->] (8,-1.5) to [bend right] (10,0);

        \draw (6,2) rectangle (8,3);
        \node at (7,2.5) {\small{}Operator};

        \draw [->] (10,1) to [bend right] (8,2.5);

        \draw [dotted] (0,-0.5) -- (11,-0.5);
        \draw [dotted] (0,1.5) -- (11,1.5);

        \node [anchor=west] at (11.25,0.5) {\small\textit{System}};
        \node [anchor=west] at (11.25,-1.5) {\small\textit{TPM}};
        \node [anchor=west] at (11.25,2.5) {\small\textit{Physical}};
    \end{tikzpicture}
    \caption{A high-level overview of local attestation.}
    \label{fig:localattestation}
\end{figure}

\subsection{Storage Hierarchy}

To implement any kind of attestation, the TPM needs to store an asymmetric \textit{attestation key}, which is used to produce the signatures described above. TPMs are lightweight devices, and have a limited amount of memory and non-volatile storage. To effectively store keys, TPMs rely on a \textit{storage hierarchy} in which keys are derived from other keys.

To begin with, the TPM stores only a \textit{primary seed} for each hierarchy. This is a large securely generated random number which never leaves the TPM and never changes. The primary seed we are interested in is the primary seed for the \textit{storage hierarchy}, or the \textit{storage primary seed}. Other hierarchies (endorsement and platform hierarchies) exist for other TPM use cases.

The storage primary seed is used to generate an asymmetric \textit{storage key}. Since the storage key is generated by the fixed storage primary seed, the storage key always has the \textit{same} public and private components and can be considered to be effectively stored inside the TPM.

The storage key is used to securely store and persist objects outside the TPM. When an asymmetric key is generated in the storage hierarchy of the TPM, the private component is encrypted using the storage key and returned to the system. In this way, the system cannot read the private component of the generated key, since it does not have the storage key. When the TPM is restarted, the storage key is regenerated with the same values, and the system can reload the same generated key.

The attestation key is generated inside the storage hierarchy during provisioning, and must be provided to the TPM whenever attestation is required. If a compromised system chooses not to load the correct attestation key, then the TPM cannot produce a valid attestation. If the attestation key is somehow lost, then a new one can be generated, but the verifier will also need an updated copy of the public key.

Because TPMs also support other more general cryptographic functions, it is also possible to restrict generated keys. In the case of an attestation key, it is suggested to:

\begin{itemize}
    \item Restrict it to \textit{only producing signatures}, to avoid it being used for general enryption / decryption.
    \item Restrict it to \textit{only sign TPM generated digests}. Otherwise, an attacker could simply request the TPM to use the attestation key to sign their own, forged attestation.
\end{itemize}

\subsection{TPM Commands} \label{sec:tpmcommands}

In each of the TPM standards set out by the TCG, usage of the TPM is done entirely through commands and responses. These commands can initialise the TPM, create and manage objects stored on the TPM, and perform operations on the TPM such as generating an attestation.

As far as the standard attestation process is concerned, there are eight commands we are interested in \cite{TPMSpec}:

\begin{itemize}
    \item \texttt{TPM2\_Startup} initialises the TPM and must be called before any TPM usage.
    \item \texttt{TPM2\_Shutdown} cleanly shuts down the TPM, optionally preserving some state. This can be used to shut down the TPM between boot stages while preserving PCR values.
    \item \texttt{TPM2\_CreatePrimary} creates an object directly from a primary seed. For attestation, we can use this to generate the storage key.
    \item \texttt{TPM2\_Create} creates an object inside a hierarchy and --- where appropriate --- returns the object data. For attestation ,we can use this to generate the attestation key during provisioning.
    \item \texttt{TPM2\_Load} loads an object into a hierarchy. For attestation, we can use this to load the generated attestation key during normal operation.
    \item \texttt{TPM2\_PCR\_Extend} extends a PCR with a digest.
    \item \texttt{TPM2\_PCR\_Read} reads the value of a PCR.
    \item \texttt{TPM2\_Quote} produces a signed `quote' for some information on the TPM. For attestation, this is a quote of the PCR values, and is the value we are interested in.
\end{itemize}

Although \texttt{TPM2\_PCR\_Read} is not strictly required for attestation, it provides a significant quality-of-life improvement to the attestation process. The quote structure returned by \texttt{TPM2\_Quote} contains a digest of \textit{all} selected PCRs. If these values are wrong, it can be difficult to tell which of the PCRs has changed.

Each of these commands have several bytes of parameters and several bytes of information in their responses, which must be marshalled and unmarshalled by any software using the TPM. \autoref{fig:quoteresp} gives an example of one of these structures, and \autoref{tab:quoteresp} shows the result of unmarshalling this structure.

\begin{figure}[h]
    \centering
    \begin{tabular}{c}
        \lstinputlisting{files/quote.txt}
    \end{tabular}
    \caption{Example of the raw bytes in a quote response.}
    \label{fig:quoteresp}
\end{figure}

\begin{table}[h]
    \centering
    \begin{tabular}{lll}
        \toprule
        Value                          & Explanation \\
        \midrule
        \texttt{ff544347}              & Magic signature (\texttt{\textbackslash{}xffTCG}) \\
        \texttt{8018}                  & Quote type (PCR Quote) \\
        \texttt{0022} .. \texttt{c1d9} & Name (digest) of signing key \\
        \texttt{0000}                  & Extra data (none) \\
        \texttt{0000000003f131f0}      & Clock value \\
        \texttt{aa6945c3}              & Reset counter \\
        \texttt{2517169e}              & Restart counter \\
        \texttt{01}                    & Safe flag (the clock value is safe) \\
        \texttt{484e3fb5d3db2255}      & Firmware version identifier \\
        \texttt{00000001}              & PCR selection count (one) \\
        \texttt{000b}                  & PCR digest algorithm (SHA256) \\
        \texttt{03010000}              & Select PCR 0 only \\
        \texttt{0020} .. \texttt{ddc9} & Digest of selected PCRs \\
        \bottomrule
    \end{tabular}
    \caption{Unmarshalling the quote response in \autoref{fig:quoteresp}. The entire quote structure is signed, and the signature follows in the full response.}
    \label{tab:quoteresp}
\end{table}

With these commands, we can outline a concrete process for remote attestation, as adapted from \cite{ChiangKeys}. Parts of this process are shown in \autoref{fig:tpmcommands}. Firstly, during provisioning:

\begin{enumerate}
    \item Use \texttt{TPM2\_Startup} to initialise the TPM.
    \item Use \texttt{TPM2\_CreatePrimary} with the storage hierarchy to initialise the storage key.
    \item Use \texttt{TPM2\_Create} to create the attestation key in the storage hierarchy. Save the returned public and encrypted private components.
\end{enumerate}

Then, during normal operation of the TPM:

\begin{enumerate}
    \item Use \texttt{TPM2\_Startup} to initialise the TPM.
    \item Use \texttt{TPM2\_PCR\_Extend} several times to measure any required data.
    \item Use \texttt{TPM2\_CreatePrimary} with the storage hierarchy to initialise the storage key.
    \item Use \texttt{TPM2\_Load} to load the attestation key's public and encrypted private components.
    \item Use \texttt{TPM2\_PCR\_Read} to read the measured PCR values (optional).
    \item Use \texttt{TPM2\_Quote} to generated a signed quote of the PCR values.
    \item Repeat \texttt{TPM2\_Quote} as many times as required to prevent replay attacks.
\end{enumerate}

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \draw [dotted] (5,0) -- (5,5);
        \node at (3.5,5.5) {\small{}TPM};
        \node at (6.5,5.5) {\small{}Normal World};

        \draw (3,5) rectangle (4,4.5);
        \node at (3.5,4.75) {\footnotesize{}Seed};

        \draw (2.5,4) rectangle (4.5,3);
        \node at (3.5,3.65) {\footnotesize{}Storage Key};
        \node at (3,3.3) {\scriptsize{}$K_S^+$};
        \node at (4,3.3) {\scriptsize{}$K_S^-$};

        \draw [->] (3.5,4.5) -- (3.5,4);
        \draw [fill=FG] (3.5,4.25) circle (0.075cm);
        \draw [->] (5.25,4.25) -- (3.575,4.25);
        \node [anchor=west] at (5.5,4.25) {\scriptsize\texttt{TPM2\_CreatePrimary}};

        \draw (2.5,2.5) rectangle (4.5,1.5);
        \node at (3.5,2.15) {\footnotesize{}Attest. Key};
        \node at (3,1.8) {\scriptsize{}$K_A^+$};
        \node at (4,1.8) {\scriptsize{}$K_A^-$};

        \draw [->] (3.5,3) -- (3.5,2.5);
        \draw [fill=FG] (3.5,2.75) circle (0.075cm);
        \draw [->] (5.25,2.75) -- (3.575,2.75);
        \node [anchor=west] at (5.5,2.75) {\scriptsize\texttt{TPM2\_Create}};

        \draw (3.5,1.5) -- (3.5,1);
        \draw [->] (3.5,1) -- (5.25,1);
        \draw (5.5,1.5) rectangle (7.5,0.5);
        \node at (6.5,1.2) {\scriptsize{}$K_A^+$};
        \node at (6.5,0.8) {\scriptsize{}$K_S^+(K_A^-)$};

        \draw [dotted] (13,-1) -- (13,5);
        \node at (11.5,5.5) {\small{}TPM};
        \node at (14.5,5.5) {\small{}Normal World};

        \draw (11,5) rectangle (12,4.5);
        \node at (11.5,4.75) {\footnotesize{}Seed};

        \draw (10.5,4) rectangle (12.5,3);
        \node at (11.5,3.65) {\footnotesize{}Storage Key};
        \node at (11,3.3) {\scriptsize{}$K_S^+$};
        \node at (12,3.3) {\scriptsize{}$K_S^-$};

        \draw [->] (11.5,4.5) -- (11.5,4);
        \draw [fill=FG] (11.5,4.25) circle (0.075cm);
        \draw [->] (13.25,4.25) -- (11.575,4.25);
        \node [anchor=west] at (13.5,4.25) {\scriptsize\texttt{TPM2\_CreatePrimary}};

        \draw (10.5,2.5) rectangle (12.5,1.5);
        \node at (11.5,2.15) {\footnotesize{}Attest. Key};
        \node at (11,1.8) {\scriptsize{}$K_A^+$};
        \node at (12,1.8) {\scriptsize{}$K_A^-$};

        \draw [->] (11.5,3) -- (11.5,2.5);
        \draw [fill=FG] (11.5,2.75) circle (0.075cm);
        \draw [->] (13.25,2.75) -- (11.575,2.75);
        \node [anchor=west] at (13.5,2.75) {\scriptsize\texttt{TPM2\_Load}};

        \draw (13.5,2.5) rectangle (15.5,1.5);
        \node at (14.5,2.2) {\scriptsize{}$K_A^+$};
        \node at (14.5,1.8) {\scriptsize{}$K_S^+(K_A^-)$};

        \draw (11.5,1.5) -- (11.5,0.25);
        \draw (10.25,1.25) rectangle (11.25,0.75);
        \node at (10.75,1) {\footnotesize{}PCRs};
        \draw [->] (11.25,1) -- (11.425,1);
        \draw [fill=FG] (11.5,1) circle (0.075cm);
        \draw [->] (13.25,1) -- (11.575,1);
        \node [anchor=west] at (13.5,1) {\scriptsize\texttt{TPM2\_Quote}};

        \draw [->] (11.5,0.25) -- (13.25,0.25);
        \draw (13.5,0.75) rectangle (15.5,-0.25);
        \node at (14.5,0.45) {\scriptsize{}$Q$};
        \node at (14.5,0.05) {\scriptsize{}$K_A^-(H(Q))$};
    \end{tikzpicture}
    \caption{TPM command sequence for provisioning (left) and attestation (right).}
    \label{fig:tpmcommands}
\end{figure}

In practice, systems will continually generate new quotes. This helps to detect unexpected resets and changes in the running software, as well as helps to prevent against replay attacks.

Local attestation uses a smaller set of commands, but can still be done using only a TPM. \texttt{TPM2\_Create} can be used to create the sealed `passphrase' in the storage hierarchy, and \texttt{TPM2\_Unseal} can be used to unseal the passphrase and provide an attestation.

\section{Platform Support}

Secure boot and TPM attestion are both backed by hardware and firmware security features. Thus, their support depends on the platform being used. We will consider mainly x86 and ARM systems as a whole, since their features supported are usually similar.

\subsection{x86 Systems}

\textit{x86 systems} are typically large desktop, laptop or server machines running powerful Intel and AMD processors. seL4 can be used on these systems to provide a secure enclave while virtualising Linux-based operating systems, but this is a less common use case.

Most x86 systems will be running on a UEFI platform, which will therefore support secure boot. However, not all x86 systems will allow users to enrol their own secure boot keys. This presents a problem since often the only key installed by default is Microsoft's secure boot public key, and Microsoft will refuse to sign GPL licenced code \cite{MicrosoftSigning}.

Linux is still able to boot on some of these systems using a \textit{UEFI secure boot shim} \cite{DebianShim} --- a small piece of code signed by Microsoft which uses another public key to verify the bootloader and Linux image.

In some cases, secure boot may need to be turned off entirely to boot other code (i.e. code not signed by Microsoft) on these systems, which completely disables the protections of secure boot for non-Windows users.

Windows 10 also requires systems to have a TPM installed in order to boot. This means that most modern x86 systems will include some form or firmware or hardware TPM in order to be able to boot Windows 10.

\subsection{ARM Systems}

\textit{ARM systems} are typically low-power embedded or mobile devices that could be running processors or \textit{system on chips} (SoCs) from a wide range of manufacturers that have licenced ARM's IP. seL4 is most commonly used on these systems, as these systems are most commonly used for embedded applications.

Modern ARM processors include \textit{ARM TrustZone}, a firmware supported \textit{Trusted Execution Environment} (TEE) that provides a variety of security features. The specification for TrustZone is very minimal and only specifies the trusted execution environment --- this on its own is not enough to implement secure boot or TPM attestation. However, most SoC manufacturers will include secure storage and either a secure clock, secure random number generator, or secure counter. These features can be used to implement secure boot and attestation.

In particular, in order to run Windows 10 on ARM devices (such as the Microsoft Surface), Microsoft has implemented a firmware TPM entirely on ARM TrustZone, with a minimal amount of extra hardware requirements. This is explored later in \autoref{sec:ftpm}.

\subsection{Other Platforms}

Other up and coming platforms for seL4 are based on the RISC-V architecture, which shows great promise as a high-performance, low-power, open source processor architecture. Unfortunately since RISC-V is still fairly new compared to x86 and ARM, support for secure boot and attestation are still under active development.

In future it might be possible to revise this thesis and extend the support to RISC-V, as seL4 becomes more closely associated with RISC-V.

\section{seL4 and Microkernels}

Operating systems can be categorised based on the structure of their \textit{kernel} --- the portion of code that runs at a privileged execution level and interfaces directly with hardware. Most operating systems currently use either \textit{monolithic kernels} (e.g. Linux) that encompass almost all of the operating system's functionality, or \textit{hybrid kernels} (e.g. Darwin, Windows NT) that export some of the operating system's functionality to userspace.

\textit{Microkernels} offer a different design approach, by reducing the size of the kernel as much as possible, and providing most of the operating system's functionality in userspace. This gives different performance and design characteristics, but allows for greater security and is ideal for embedded systems.

\textit{seL4} is a \textit{third generation} microkernel based on the popular L4 family of microkernels. It is currently the fastest microkernel, and also offers strong security guarantees by means of \textit{formal verification}. In 2009 after a great research effort, the seL4 microkernel was formally verified \cite{KleinseL4}, this includes:

\begin{itemize}
    \item A \textit{functional correctness} proof that proves the implementation of seL4 is correct to a higher-level abstract specification.
    \item A proof of certain properties on top of this high-level specification, to ensure that certain performance and security guarantees are met.
    \item A proof of correct \textit{binary translation} that ensures the produced machine code matches the behaviour modelled by the implementation.
\end{itemize}

The exact scope of the verification depends on the platform being used, but all platforms can benefit from seL4's design for security and performance.

These features make seL4 ideal for embedded applications where a very high level of security is required. As such, these systems would be a great target for secure boot and attestation to be used with. The task of providing this level of platform security to seL4 is still an active area of research.

\subsection{Capabilities}

seL4 uses \textit{capability-based access control} \cite{seL4Manual}. This means that access to objects provided by the kernel is mediated through \textit{capabilities} to those objects. Any thread has an associated \textit{capability space} (CSpace), and each of the capabilities has an associated set of access rights (read, write, grant and grant reply). Capabilities can also be copied, or \textit{minted / mutated} into copies with slightly weaker access rights. These access rights have different meanings, depending on the kind of object the capability refers to.

Threads in userspace ask the kernel to act on their behalf by \textit{invoking} a capability. One capability may support a number of different operations, which can be selected using parameters to the same all-powerful \texttt{seL4\_Call} system call. The operations available also depend on the kind of object the capability refers to.

One example might be a \textit{page} object. These are architecture-dependent, but exist in some form on every architecture to enable memory mapping. Read permissions on a page capability grant the thread the ability to map the page as readable, write permissions grant the thread the ability to map it as writeable. Invoking the page capability allows the thread to map or unmap the page.

\subsection{CAmkES}

The \textit{Component Architecture for microkernel-based Embedded Systems} is a framework which is designed to tackle the complexity of building modular systems on top of seL4. It allows developers to describe a system as a set of components and component interfaces in a high-level language (the \textit{Architecture Description Language} (ADL)) and then automatically generates the infrastructure to connect these components with seL4 primitives (capabilities, communication endpoints, etc.).

This means that any userspace modules intended to be used for seL4-based systems would do well to be defined as CAmkES components, as they can be more easily integrated into existing systems.

\subsection{seL4 Boot Process}

How seL4 boots depends largely on the platform. However, the common theme is that the seL4 microkernel, the \textit{root server} image (that is, the first userspace thread, which may load more), and a special program called the \textit{ELF loader}; are built into one large boot image. The system booting seL4 initially boots the ELF loader, which loads seL4 and the root server into memory and jumps into seL4. seL4 then initialises itself and starts the root server.

\autoref{fig:sel4boot} outlines the boot process for seL4. On ARM systems, the ELF loader is usually started through U-Boot. U-Boot is a popular open source boot loader for embedded systems, providing drivers for anything necessary to boot the system. This could include power drivers (for system initialisation), storage drivers (to load images), network drivers (to pull images from the network), and even TPM drivers (for secure measurements).

U-Boot is split into a \textit{secondary program loader} (SPL) and \textit{tertiary program loader} (TPL). The SPL is more simple, and is only responsible for loading the TPL, which supports more advanced methods of system initialisation.

U-Boot supports a command line system before booting, and boots either according to a preset \textit{boot script} or according to commands entered manually over a serial console. These commands can be extended by vendors and allow developers, administrators and end users to customise their boot process.

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \draw (0,0) rectangle (2,1);
        \node at (1,0.5) {\small{}U-Boot SPL};

        \draw [->] (2,0.5) -- (3,0.5);

        \draw (3,0) rectangle (5,1);
        \node at (4,0.5) {\small{}U-Boot TPL};

        \draw [->] (5,0.5) -- (6,0.5);

        \draw (6,0) rectangle (8,1);
        \node at (7,0.5) {\small{}ELF Loader};

        \draw [->] (8,0.5) -- (9,1.25);
        \draw [->] (8,0.5) -- (9,-0.25);

        \draw (9,0.75) rectangle (11,1.75);
        \node at (10,1.25) {\small{}seL4};

        \draw (9,-0.75) rectangle (11,0.25);
        \node at (10,-0.25) {\small{}Root server};
    \end{tikzpicture}
    \caption{A high-level overview of the seL4 boot process, assuming U-Boot is the bootloader.}
    \label{fig:sel4boot}
\end{figure}

\section{ARM TrustZone}

ARM TrustZone is a firmware supported means of isolation on modern ARM processors. \autoref{fig:trustzone} gives an overview of a system running with TrustZone. It separates execution and memory on the processor into the \textit{secure world} and \textit{normal world}. The normal world hosts the familiar operating system and userspace programs, the secure world can run secure world services (also called \textit{trusted applications}) which are isolated from the normal world. This isolation is backed by a \textit{coarse context switch}: all memory is either marked as secure or non-secure, and secure memory can only be accessed in the secure world.

This kind of isolation could be achieved in theory with regular processes. However, because the secure world is available \textit{before} the normal world and because it exists concurrently to the normal world, it can be particularly useful for platform security. Measurements can be made in the bootloader, stored using TrustZone, then used from the operating system. TrustZone can also be used to measure parts of the normal world before they have a chance to boot.

Additionally, on ARM platforms, some hardware can be configured to only be accessible from TrustZone. This forms the foundation of the secure storage required to implement a TPM.

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \draw (0,0) rectangle (6,1);
        \node at (3,0.5) {Secure Monitor};

        \draw [dotted] (3,1.5) -- (3,3.75);
        \node at (1.25,4.25) {Normal World};
        \node at (4.75,4.25) {Secure World};

        \draw (0,1.5) rectangle (2.5,2.5);
        \node at (1.25,2) {Kernel};

        \draw (0,2.75) rectangle (2.5,3.75);
        \node at (1.25,3.25) {Userspace};

        \draw (3.5,1.5) rectangle (6,2.5);
        \node at (4.75,2) {Secure OS};

        \draw (3.5,2.75) rectangle (6,3.75);
        \node at (4.75,3.25) {Trusted Apps};
    \end{tikzpicture}
    \caption{A high-level overview of a system with TrustZone.}
    \label{fig:trustzone}
\end{figure}

\subsection{Secure Monitor}

Underneath any system with TrustZone is the \textit{secure monitor}. This is a small piece of software which acts as the aforementioned Core Root of Trust Measurement (CRTM), and mediates the context switches between the normal and secure world.

Communication with the secure monitor (and thus context switches between the normal and secure world) are achieved using the \texttt{smc} instruction. This follows a particular calling convention, in which parameters to calls to the normal or secure world are placed in the general purpose registers (\texttt{x0}---\texttt{x7} by default).

One caveat of the \texttt{smc} instruction is that it can only be executed in \textit{privileged mode}. This is a design issue for microkernels, as it means that the equivalent of a driver for TrustZone cannot be written fully in userspace. The only option is to somehow move the \texttt{smc} instruction into the kernel. Since the secure world can access and change normal world memory, if the secure world is not trusted, the \texttt{smc} instruction also cannot be trusted.

\subsection{Secure World Operating System}

On top of the secure monitor, the secure world has analogues of an operating system and processes. The secure world operating system is designed to act as an operating system for secure world services (processes), mediating their access to hardware and providing simple abstractions for them to use. These secure world services provide a service which takes advantage of the isolation provided by the secure world.

The secure world operating system should be as minimal as possible, this makes seL4 a prime candidate. However, the current most well-supported secure world operating system is \textit{OP-TEE}. To ensure a minimal trusted computing base, OP-TEE is supported in the normal world by a \textit{supplicant}. This supplicant is used to co-ordinate shared memory between the normal and secure worlds, and to offload any functionality onto the normal world which can be offloaded. For example, access to the secure storage.

\section{Secure Storage}

\textit{Multi-Media Card} (MMC) is a storage standard which is aimed at embedded systems. It covers both removable cards (SD/microSD) and embedded cards, which are present as chips on the device. Some embedded chips will implement a \textit{Replay-Protected Memory Block} (RPMB), which can be used to provide a means of secure storage only accessible to the secure world.

The RPMB is available as a special partition with one logical block on the MMC device. RPMB \textit{commands} can be issued by writing to this block, and responses received by reading from this block, much like a special device file on UNIX. The RPMB is equipped with a key during manufacturing or provisioning, with the idea that this key is only accessible to the RPMB and to the secure world. This key allows the secure world to read and write to the replay-protected memory via the normal world without the normal world being able to intercept the requests. Programming this key is a one-time operation.

The key can be restricted to the secure world by a number of means. The simplest is to use re-write the secure world system to use a proprietary method of generating the key and restrict the source code for the secure world. While simple, this method relies on security by obscurity. A more secure way is to take advantage of devices restricted to the secure world and program the RPMB key into an electronic fuse only accessible to the secure world.

\unchapter{3}{Related Work}

Now we can explore some existing work which could make our approach easier. In particular, we look at \textit{fTPM} --- an implementation of a firmware TPM using ARM's TrustZone \cite{RajFTPM}; \textit{HYDRA} --- an implementation of a ``hybrid'' TPM using seL4 and a small amount of secure hardware \cite{EldefrawyHYDRA}; and \textit{SABLE} --- a formally verified bootloader which provides secure boot and local attestation using a TPM \cite{ConstableSABLE}.

SABLE and HYDRA are both solutions for securely booting and attesting seL4-based systems, with different characteristics. \autoref{tab:sablehydracompare} compares SABLE and HYDRA on a number of key points, which we will use later to discuss our own approach. fTPM is a different kind of existing work in that it could help us to design our solution, but is not necessarily a solution by itself.

\begin{table}[h]
    \centering
    \begin{tabular}{lll}
        \toprule
                                      & SABLE          & HYDRA           \\
        \midrule
            Platform Support          & x86            & ARM             \\
            Hardware Requirements     & Discrete TPM   & None            \\
            Secure Boot Support       & Yes            & Yes             \\
            Attestation Support       & Local only     & Local or remote \\
            Attestation Scope         & Whole platform & Userspace       \\
            Root of Trust Measurement & Dynamic        & Static          \\
            Verification              & Yes            & Planned         \\
        \bottomrule
    \end{tabular}
    \caption{Comparison of SABLE and HYDRA.}
    \label{tab:sablehydracompare}
\end{table}

\section{Microsoft's Firmware TPM} \label{sec:ftpm}

As we mentioned before, ARM platforms do not necessarily support secure boot or attestation by hardware or firmware out of the box. Instead, modern ARM SoCs will support ARM TrustZone --- usually with some extra secure hardware to increase the SoC's security capabilities. In order to securely boot and support Windows 10 systems on ARM devices Microsoft has developed \textit{fTPM} --- a TPM fully implemented in software inside ARM TrustZone's secure world.

\subsection{Design Overview}

Recall that TrustZone separates the system into a normal and secure world, separated in firmware by a coarse context switch. Microsoft's fTPM has two components: a driver that runs in the normal world and allows the operating system to interface with the fTPM, and the fTPM itself running in the secure world and implementing the TPM.

The fTPM places three extra hardware requirements on the system outside of ARM's TrustZone: a secure entropy source (that is, an entropy source only available to TrustZone), secure storage, and a number of \textit{hardware fuses} --- small portions of write-once storage that are written with secure keys during manufacturing. The secure storage comes in the form of an \textit{embedded Multi-Media Card} (eMMC) that is equipped with an RPMB.

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \draw [dotted] (3.5,-0.5) -- (3.5,2.25);
        \draw [dotted] (6.5,-0.5) -- (6.5,2.25);
        \node at (1.5,-0.25) {\footnotesize{}Normal World};
        \node at (5,-0.25) {\footnotesize{}Secure World};
        \node at (8,-0.25) {\footnotesize{}Hardware};
        
        \draw (0,0) rectangle (3,1);
        \node at (1.5,0.5) {\footnotesize{}OS};
        
        \draw (0,1.25) rectangle (1.375,2.25);
        \node at (0.6875,1.75) {\footnotesize{}Apps};
        
        \draw (1.625,1.25) rectangle (3,2.25);
        \node at (2.3125,1.75) {\footnotesize{}\begin{tabular}{c}fTPM\\Driver\end{tabular}};
        
        \draw (4,0) rectangle (6,2.25);
        \node at (5,1.125) {\footnotesize{}fTPM};
        
        \draw (7,0) rectangle (9,2.25);
        \node at (8,1.125) {\footnotesize{}\begin{tabular}{c}Secure\\Hardware\end{tabular}};
        
        \draw [<->] (3,1.75) -- (4,1.75);
        \draw [<->] (6,1.75) -- (7,1.75);
        \draw [<->] (1.375,1.75) -- (1.625,1.75);
        \draw [<->] (2.3125,1) -- (2.3125,1.25);
    \end{tikzpicture}
    \caption{Overview of fTPM's Architecture.}
\end{figure}

\subsection{Limitations}

The biggest limitation of Microsoft's fTPM is the availability. Primarily, it depends on ARM TrustZone not only being present on the SoC, but also available for use. Although all modern ARM SoCs do contain TrustZone by specification, this is usually restricted by the manufacturer for various reasons. In particular, they may offer their own bespoke security services on top of TrustZone and may not allow these to be easily modified.

fTPM also makes some small modifications to the semantics of some TPM commands. However, these commands are still largely the same, and these commands are not ones which are important for attestation or secure boot.

\section{HYDRA}

\textit{Hybrid Design for Remote Attestation} or \textit{HYDRA} is a system which implements a kind of ``hybrid'' TPM using seL4 and some secure hardware, intended for platforms which do not have the full support for a hardware or firmware TPM. These would be older or smaller ARM systems, or systems with more obscure architectures. The hybrid TPM takes advantage of the isolation capabilities of seL4 and provides a software TPM as a separate seL4 task, which can then be used by remote verifiers or other seL4 tasks such as a virtualised commodity operating system.

This is not quite what we are trying to achieve, but it does demonstrate a unique architecture for a TPM that is only possible with a microkernel with strong isolation properties such as seL4. In particular, this is an architecture that was initially proposed by NICTA when seL4 was first released \cite{HeiserTrust}.

\subsection{Design Overview}

This is a system targeted specifically at remote attestation of a system running on seL4. It makes use of a higher priority attestation task running alongside the system, and a platform-supported secure boot to ensure the integrity of seL4 and the attestation task itself. In particular there are no requirements on the platform outside of this secure boot support.

By running the attestation task with a higher priority than the virtualised system, the virtualised system can be interrupted and attested to at any time, which is more flexible than normal TPM attestation. It also places a minimal amount of trust in hardware and firmware solutions, relying on software to provide isolation and security. This means it cannot defend against some hardware and firmware level attacks, but also means it is less susceptible to vulnerabilities as it can rely on formally verified software which can be updated and patched easily.

\subsection{Limitations}

The main limitation of HYDRA is the dependence of platform-level secure boot and the reliance on this to attest any firmware or the seL4 system itself. The entire attestation program \textit{including the private key} is stored un-encrypted on regular storage. If the platform-level secure boot is compromised or disabled, then an attacker can simply read this storage and leak the private key, allowing them to fake attestation messages. In this way, the system is only secure and trustworthy if seL4 is securely loaded by the platform in the first place and can control access to storage. This means it cannot truly replace a TPM or TPM attestation, although it can provide similar functionality for the userspace system.

\section{SABLE}

The \textit{Syracuse Assured Boot Loader Executive} or \textit{SABLE} is a formally-verified secure bootloader, supporting secure boot and local TPM attestation. It was originally intended for seL4/Genode systems, but is theoretically capable of booting any system.

\subsection{Details}

SABLE works in much the same way as a normal bootloader with security features added (e.g. the \textit{Grand Unified Bootloader} (GRUB)) in that it takes advantage of the platform's support for secure boot and whatever hardware or firmware TPM exists. However, it is targeted specifically for x86 platforms and as such relies on whatever firmware TPMs are provided by the processor, as opposed to using fTPM or some other third-party firmware TPM.

SABLE is unique in that it specifically makes use of a \textit{Dynamic Root of Trust Measurement} (DRTM) as opposed to a \textit{Static Root of Trust Measurement} (SRTM) as is typical of TPM attestation. For attestation using SRTM, the entire platform initialisation starts at the secure Core Root of Trust Measurement (CRTM) which measures the next stage and establishes a chain of trust across the entire boot process. For attestation using DRTM, once the platform is fully initialised a special CPU instruction can be issued (\texttt{skinit} for AMD platforms and \texttt{SENTER} for Intel platforms) which effectively clears all CPU state and starts a new secure loader from which new measurements are taken.

This DRTM means that the rest of platform before the secure loader can be ignored and excluded from the \textit{Trusted Computing Base} (TCB). Minimising the TCB is a well-established security practice as it makes it easier to secure what \textit{is} inside the TCB. However, this relies on the CPU and the platform securely and reliably clearing its state.

\subsection{Limitations}

The main limitation of SABLE is the amount of platform dependence. Firstly, by relying on hardware or native firmware TPMs, it restricts itself to platforms which have these. Most importantly however, the reliance on a DRTM and the platform-specific DRTM instructions means it can only work on platforms which support these instructions. Currently both of these restrictions limit SABLE to modern commodity x86 platforms.

It also specifically targets the TPM 1.2 standard as opposed to the TPM 2.0 standard. The TPM 2.0 standard offers improved security guarantees in a number of areas, but is \textit{not} backwards compatible with TPM 1.2, and a non-trivial porting effort would be required to make SABLE support TPM 2.0.

Finally, the use of local attestation over remote attestation means that SABLE can only be used to provide assurance if a human verifier is present. However with the right userspace tools SABLE could be configured to also provide remote attestation, as it still produces the required TPM measurements.

\unchapter{4}{Approach}

The initial problem statement of introducing secure boot and attestation to seL4-based systems is quite broad, and the required design will depend highly on the chosen platform and chosen secure boot and attestation implementations. In particular, it would be impossible to have one general solution for all platforms.

To start with, before choosing a particular platform or implementation, we will lay out the desired requirements and design goals for an ideal solution. We then lay out a proposed approach for the implementation.

\section{Requirements}

\subsection{Design Goals}

We begin by choosing some over-arching design goals. These are based heavily on the design goals of seL4 \cite{HeiserPrinciples}, to ensure the best integration into an seL4-based system.

\begin{requirement}[Security]
\label{req:security}
The design should follow the current state of the art in security practices, using as many of the available security mechanisms as possible in the correct way.
\end{requirement}

\begin{requirement}[Performance]
\label{req:performance}
The implemented solution should not cause a significant overhead in the boot process and should not impede the operation of the system after the boot process unless specifically invoked.
\end{requirement}

\begin{requirement}[Policy Freedom]
\label{req:policyfreedom}
The design should not require the system running on top of seL4 to adhere to a particular security policy. Designers of the `end user' system should be able to freely use the TPM and attestation facilities in whatever way they see fit.
\end{requirement}

\begin{requirement}[Verification]
\label{req:verification}
While full verification is outside the scope of this thesis, the design and implemented solution should at least be amenable to verification, with a strong specification and a relatively small codebase.
\end{requirement}

We can now lay out some concrete, high-level requirements for the implementation. These are directly drawn from the thesis statement, and are independent of the chosen platform (as long as the platform supports some form of TPM).

\begin{requirement}[Secure Boot]
\label{req:secureboot}
The design should leverage some hardware or firmware functionality to attempt to certify a cryptographic signature for seL4 and the initial task, and should fail to boot if it cannot certify those signatures.
\end{requirement}

\begin{requirement}[TPM Attestation]
\label{req:attestation}
The design should leverage a hardware or firmware TPM to provide \textit{remote} attestation to a trusted remote verifier, through the use of a CAmkES module.
\end{requirement}

\subsection{Targeted Platform}

The exact nature of the solution depends on the platform chosen, since each platform has varying levels of support for secure boot and attestation and different implementations of each.

Since RISC-V does not yet have good support for these technologies, and the problem already seems solved on x86 platforms by SABLE, we will specifically be targeting \textit{ARM} platforms. This would be a good target, as ARM is a popular choice for embedded systems, which is the largest use case for seL4.

\begin{requirement}[Chosen Platform]
\label{req:platform}
The implementation should work on any ARM platform which supports some level of secure boot on the firmware and fTPM via. TrustZone.
\end{requirement}

As we have seen, the choice of ARM introduces a number of challenges. We cannot rely on DRTM as ARM lacks the appropriate instructions, we need access to TrustZone on whichever SoC is chosen along with the appropriate secure hardware, and we need some level of support for secure boot from the underlying firmware.

\section{Design}

We will start by looking at how the existing work relates to the requirements listed above. \autoref{tab:reqeval} lists how each of the existing solutions matches each requirement.

\begin{table}[h]
    \centering
    \begin{tabular}{lll}
        \toprule
            Requirement                                  & SABLE           & HYDRA               \\
        \midrule
            \hyperref[req:security]{Security}            & Yes             & No (unsuitable TCB) \\
            \hyperref[req:performance]{Performance}      & Unknown         & Unknown             \\
            \hyperref[req:policyfreedom]{Policy Freedom} & No              & Yes                 \\
            \hyperref[req:verification]{Verification}    & Yes             & Planned             \\
            \hyperref[req:secureboot]{Secure Boot}       & Yes             & Yes                 \\
            \hyperref[req:attestation]{Attestation}      & No (local only) & Yes                 \\
            \hyperref[req:platform]{Platform}            & No (x86 only)   & Yes                 \\
        \bottomrule
    \end{tabular}
    \caption{Evaluation of SABLE and HYDRA against the stated requirements.}
    \label{tab:reqeval}
\end{table}

As we can see from \autoref{tab:reqeval}, neither solution exactly meets our requirements. However, by leveraging fTPM and looking into platform-specific features for secure boot, we may be close to meeting our requirements. fTPM will require some effort to port to seL4, and secure boot will be somewhat platform-dependent, but this will fit better into the time constraints of this thesis than adapting any of the other existing work.

The proposed solution consists of the following stages:

\begin{itemize}
    \item Investigating support for fTPM, TrustZone and secure boot on the chosen platform.
    \item Writing drivers to support the secure world operating system and fTPM from within seL4.
    \item Implementing any userspace software and other utilities to support attestation.
\end{itemize}

The new boot and attestation process will work like so:

\begin{enumerate}
    \item The platform's secure monitor starts in the secure world, initialises fTPM, and measures U-Boot.
    \item The secure monitor switches to the normal world and starts U-Boot.
    \item U-Boot measures the seL4 image (including the kernel and root server), and boots into seL4.
    \item The seL4 root server uses fTPM to generate an attestation to provide to the remote verifier.
\end{enumerate}

This also assumes some provisioning and external utilities, which are also in the scope of this thesis:

\begin{itemize}
    \item Provisioning the chosen platform with the necessary keys.
    \item Userspace utilities (e.g., a root server library) to use TPM commands to generate an attestation.
    \item An external verifier program which is able to verify a generated attestation.
\end{itemize}

\unchapter{5}{Implementation}

Due to time constraints and unforseen roadblocks, it was only possible to implement most of the TPM attestation aspect of this thesis. The implementation can be considered from the `bottom-up' with regards to TPM attestation:

\begin{enumerate}
    \item Choosing a suitable platform.
    \item Accessing the secure monitor from within seL4.
    \item Installing and accessing a secure world operating system (OP-TEE).
    \item Implementing the required normal world supplicant for OP-TEE in seL4.
    \item Installing and accessing fTPM as a secure world service from within seL4.
    \item Provisioning fTPM with the required keys for attestation.
    \item Implementing the standard attestation workflow commands within seL4.
    \item Implementing an external application for verification.
\end{enumerate}

Many pieces of this implementation exist in some form on some other platform, usually embedded Linux. Therefore, most of the implementation phase involved understanding and porting these onto seL4, with some adaptations where necessary. Some cases where documentation is missing or difficult to find (such as OP-TEE and fTPM) required some imagination and reverse engineering.

\section{The Platform}

The chosen platform was the \textit{i.MX8 MQ Evaluation Kit} (henceforth referred to as ``the i.MX8''), a development board based on the i.MX8 MQ applications processor shown in \autoref{fig:imx8photo}. This is a platform well supported by seL4. Importantly for this thesis, it also has a somewhat well-documented boot process, and support for open source configurations of OP-TEE and fTPM. It also has the secure storage support required for fTPM, through the embedded MMC card.

\begin{figure}[h]
    \centering
    \includegraphics[width=0.5\textwidth]{imx8-photo}
    \caption{A marketing photo of the i.MX8 MQ Evaluation Kit, with the heatsink removed. The SoC is in the centre of the board, and the eMMC containing the Replay-Protected Memory Block (RPMB) is located to the top-left of the board. Image by NXP. Source: \url{https://www.nxp.com/design/development-boards/i-mx-evaluation-and-development-boards/evaluation-kit-for-the-i-mx-8m-applications-processor:MCIMX8M-EVK}}
    \label{fig:imx8photo}
\end{figure}

\section{\texttt{smc} Instruction}

On any ARM system that supports TrustZone, the \texttt{smc} instruction can be used to access the secure world. Therefore, this is a natural prerequisite for the rest of the system.

As mentioned in the background section, the \texttt{smc} instruction can only be called from kernel mode. This means that seL4 has to be modified with an extra capability to allow \texttt{smc} calls.

To implement this thesis, we introduce an extra architecture-specific capability for Aarch64 called \texttt{seL4\_ARM\_SMC}. The capability has only one kind of call, \texttt{seL4\_ARM\_SMC\_SMC}. This takes the input registers for the \texttt{smc} call, makes the \texttt{smc} call, and returns the output registers for the \texttt{smc} call. The input and output registers are marshalled and unmarshalled into structures by \texttt{libsel4}.

On Aarch64 systems, this capability is placed into the root tasks's CSpace and the BootInfo structure. The capability holds no information on the kernel side, and simply represents the ability of a thread to make an \texttt{smc} call through the kernel. The intended design is that only one or two threads acting as servers actually have the capability, and that clients wishing to interact with the secure world should have endpoints to these servers.

\texttt{smc} calls are dangerous, and in a secure system will require some kind of access control. One way to do this would be to have these access controls implemented somehow in seL4, this would provide better security guarantees and adhere to the principle of least privilege by only giving userspace threads just enough access to the secure world \cite{SMCRFC}.

However, the arguments to \texttt{smc} calls can be complicated, and may vary in structure depending on the platform and what is running in the secure world.

For instance, the calling convention specifies that the function ID being called in the secure world should be placed in \texttt{x0}. In that case, seL4 may choose to filter calls based on the function ID. However, in the case of OP-TEE, most function calls use the \textit{same} function ID (\texttt{OPTEE\_SMC\_CALL\_WITH\_ARG} (\texttt{0x32000004})). The secure world function being called is stored in the shared memory.

To minimise the complexity of the kernel and provide true policy freedom, it is better to have an all-powerful capability restricted to a minimal amount of threads, and to implement the access controls in userspace.

One potential issue left to be addressed is long-running operations in the secure world. Some secure world operations are considered atomic and do not enable interrupts. Others are considered to be interruptable and can be paused and resumed, during which time the system may return to the normal world.

It is currently not clear to me how this would interact with the seL4 scheduling requirements, particularly MCS scheduling budgets. In particular, operations in the seL4 kernel are assumed to be short, which results in a kernel-wide lock. Since these \texttt{smc} calls take place in the kernel, this may cause system-wide pauses whenever a long-running secure world operation is started.

\section{OP-TEE and OP-TEE Supplicant}

Before accessing OP-TEE from within seL4, OP-TEE needs to be present on the system. For the i.MX8, OP-TEE is not installed out of the box, only the secure monitor. The open source OP-TEE repository \cite{OPTEERepo} includes a manifest and Makefile for the i.MX8, this builds OP-TEE, U-Boot, TF-A (the open source reference secure monitor) and Linux.

The Makefile then produces an image which can be flashed onto a microSD card, which can be booted from directly on the i.MX8 by selecting the microSD on a hardware switch. This image will boot Linux by default, however we can modify the included boot script to boot an seL4 image over the network, or copy an seL4 image onto the microSD itself. The image also ensures that OP-TEE boots first as a secure world operating system.

Recall that OP-TEE is paired with a supplicant which acts on behalf of OP-TEE in the normal world. This supplicant is responsible for managing shared memory and for storage requests. For the supplicant, the Linux drivers are slightly more complex, as the supplicant is in userspace and the driver itself is in the kernel. For seL4 this can be simplified, as both are in userspace.

From there, drivers are required from within seL4 to access OP-TEE. For the driver for OP-TEE and its supplicant, these were derived from the Linux drivers. Secure storage requires MMC drivers, which I ported from U-Boot. These required some modification to work properly within seL4.

\subsection{OP-TEE Messages}

OP-TEE messages are sent through the \texttt{smc} instruction. These only use a limited number of the available registers for the \texttt{smc} calling convention, and pass more information through shared memory objects. These shared memory objects are allocated in the normal world, and are sent by physical address to the secure world.

OP-TEE shared memory comes in a number of different forms, all of which require slightly different handling:

\begin{itemize}
    \item Shared memory can span multiple pages. In this case, the physical address passed to OP-TEE points to a page containing a list of physical addresses of other pages. This is also to allow support for non-contiguous memory mappings.
    \item Shared memory can be allocated on request by OP-TEE, or allocated in advance by the normal world. For memory allocated in advance --- except for memory used to hold arguments --- it must be \textit{registered} with OP-TEE. This involves making another \texttt{smc} call to OP-TEE which contains the physical address of the shared memory object.
\end{itemize}

For all of these shared memory objects, the cache must be invalidated and flushed before and after using as for any DMA operations. This is because the secure world and normal world share different mappings.

Currently, these shared memory objects are allocated using a bump pointer for testing purposes. However, since shared memory is always allocated as whole pages, this could be changed to use a separate frame allocation library with a proper free list.

The responses are delivered in the same shared memory objects. These responses may indicate success or an error, and contain some payload. However, in some cases, these responses may be a \textit{Remote Procedure Call} (RPC) response. This is a way of OP-TEE indicating to the normal world that some action from the supplicant (e.g. allocation of shared memory, secure storage access) is required before the message can be addressed. \autoref{fig:opteemsg} is a sequence diagram showing how RPC responses work. Multiple RPC responses may need to be handled before OP-TEE can handle the original request.

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
		\draw (0,0) -- (0,6);
		\node at (0,6.5) {\footnotesize{}MMC Driver};

		\draw (3,0) -- (3,6);
		\node at (3,6.5) {\footnotesize{}Supplicant};

		\draw (6,0) -- (6,6);
		\node at (6,6.5) {\footnotesize{}OP-TEE Driver};

		\draw (9,0) -- (9,6);
		\node at (9,6.5) {\footnotesize{}OP-TEE};

		\draw [dotted,draw=Thesis] (8.25,6.75) -- (8.25,0);

		\node at (9.5,3) {\tiny\color{Thesis}\begin{tabular}{c}Secure\\World\end{tabular}};
		\node at (-0.5,3) {\tiny\color{Thesis}\begin{tabular}{c}Normal\\World\end{tabular}};

		\draw [->] (6,5.5) -- (9,5.5);
		\node at (7.15,5.65) {\tiny{}Request};

		\draw [->] (9,5) -- (6,5);
		\node at (7.15,5.15) {\tiny{}Allocate Memory};

		\draw [->] (6,5) -- (3,5);
		\node at (4.5,5.15) {\tiny{}Allocate Memory};

		\draw [->] (3,4.5) -- (6,4.5);
		\node at (4.5,4.65) {\tiny{}Memory Object};

		\draw [->] (6,4.5) -- (9,4.5);
		\node at (7.15,4.65) {\tiny{}Memory Object};

		\draw [->] (9,4) -- (6,4);
		\node at (7.15,4.15) {\tiny{}RPMB Request};

		\draw [->] (6,4) -- (3,4);
		\node at (4.5,4.15) {\tiny{}RPMB Request};

		\draw [->] (3,4) -- (0,4);
		\node at (1.5,4.15) {\tiny{}RPMB Frames};

		\draw [->] (0,3.5) -- (3,3.5);
		\node at (1.5,3.65) {\tiny{}Response Frames};

		\draw [->] (3,3.5) -- (6,3.5);
		\node at (4.5,3.65) {\tiny{}RPMB Response};

		\draw [->] (6,3.5) -- (9,3.5);
		\node at (7.15,3.65) {\tiny{}RPMB Response};

		\node at (4.5,2.5) {\footnotesize{}(Repeats...)};

		\draw [->] (9,1.5) -- (6,1.5);
		\node at (7.15,1.65) {\tiny{}Free Memory};

		\draw [->] (6,1.5) -- (3,1.5);
		\node at (4.5,1.65) {\tiny{}Free Memory};

		\draw [->] (3,1) -- (6,1);
		\node at (4.5,1.15) {\tiny{}Okay};

		\draw [->] (6,1) -- (9,1);
		\node at (7.15,1.15) {\tiny{}Okay};

		\draw [->] (9,0.5) -- (6,0.5);
		\node at (7.15,0.65) {\tiny{}Response};
	\end{tikzpicture}
    \caption{The full process for sending an OP-TEE message, including any intermediate RPC responses.}
    \label{fig:opteemsg}
\end{figure}

OP-TEE messages that are sent to a secure application are associated with a \textit{session}. These sessions are opened using OP-TEE messages themselves, and use a TA's \textit{Universally Unique Identifier} (UUID) to select the TA associated with the session.

\autoref{fig:opteesnip1} shows how the fTPM library initialises itself, by opening an OP-TEE session using fTPM's UUID. \autoref{fig:opteesnip2} and \autoref{fig:opteesnip3} show how the fTPM library can send TPM commands, using OP-TEE messages.

\begin{figure}[h]
    \centering
    \begin{tabular}{c}
        \lstinputlisting[language=C]{files/opteesnip.c}
    \end{tabular}
    \caption{A simplified version of the code used to open an fTPM session with OP-TEE.}
    \label{fig:opteesnip1}
\end{figure}

\begin{figure}[h]
    \centering
    \begin{tabular}{c}
        \lstinputlisting[language=C,lastline=47]{files/opteesnip2.c}
    \end{tabular}
    \caption{A simplified version of the code used to send TPM commands as OP-TEE messages to fTPM.}
    \label{fig:opteesnip2}
\end{figure}

\begin{figure}[h]
    \centering
    \begin{tabular}{c}
        \lstinputlisting[language=C,firstline=49]{files/opteesnip2.c}
    \end{tabular}
    \caption{A simplified version of the code used to send TPM commands as OP-TEE messages to fTPM \textit{(Continued from \autoref{fig:opteesnip2})}.}
    \label{fig:opteesnip3}
\end{figure}

\subsection{Secure Storage}

Access to secure storage is highly platform dependent and is likely to be a problem for a small trusted computing base. Instead, OP-TEE forms platform indepenent Replay-Protected Memory Block (RPMB) commands in the secure world, and routes these through to the normal world in RPC responses. The normal world then needs an MMC driver to service these RPMB requests.

In the case of the i.MX8, the seL4 ecosystem already has a similar driver (for the i.MX6). However, U-Boot already has a driver specifically for the i.MX8, which is more suitable \cite{UBootRepo}. I also ported the clock driver from U-Boot, as this is required for the MMC driver to work.

Before sending the RPMB requests, some initialisation is required from the MMC driver:

\begin{enumerate}
    \item The eMMC device itself is re-initialised, to clear any settings left behind by U-Boot. I found that the device was only partially cleared at the end of the boot process.
    \item Some information is requested from the eMMC device. In particular, the Card ID, reliable sector count, and RPMB partition size. These may be requested by OP-TEE at any time, usually during initialisation.
    \item The eMMC device should be switched to the RPMB partition. If the eMMC is being used for storage purposes, this will need to happen every time the RPMB is needed.
\end{enumerate}

With this initialisation complete, RPMB requests can be sent and received by reading and writing to logical blocks on the eMMC device.

\section{fTPM}

fTPM exists as a \textit{trusted application} (TA) running on top of OP-TEE. Generally, OP-TEE loads a trusted application from the file system on request from the normal world. However, in the case of fTPM, we need it to be available before the normal world has loaded and before a file system is available. We can do this by building OP-TEE with fTPM included as an \textit{early TA}. These TAs are linked directly into the OP-TEE image and are available as soon as the system starts, and more importantly do not require a file system to be used.

With fTPM linked as an early TA and with OP-TEE messages available in seL4, we have everything we need to use TPM2 commands. We start in seL4 by opening a session with fTPM. For normal trusted applications this would load the application into memory, but in the case of fTPM this simply establishes some state within OP-TEE. Then we can send TPM commands and receive TPM responses wrapped within OP-TEE messages. \autoref{fig:ftpmsnippet} shows a snippet of code which interfaces with fTPM from within seL4.

\begin{figure}[h]
    \centering
    \begin{tabular}{c}
        \lstinputlisting[language=C]{files/ftpmsnip.c}
    \end{tabular}
    \caption{Using fTPM from within seL4 as a userspace library. This implements a function which initialises fTPM and OP-TEE, then uses \texttt{TPM2\_GetRandom} to fetch 32 random bytes.}
    \label{fig:ftpmsnippet}
\end{figure}

The code that the fTPM library uses itself to communicate with OP-TEE (in \autoref{fig:opteesnip1}, \autoref{fig:opteesnip2} and \autoref{fig:opteesnip3}) is also adapted from U-Boot, with some adjustments for my implementation of the OP-TEE driver.

\section{Key Provisioning}

For attestation to work, the system needs to be provisioned with an RPMB key and an attestation key, as well as any primary seeds required by the TPM. The RPMB key can be configured to be written by OP-TEE automatically if it has not been programmed yet, and fTPM will initialise the primary seeds if those have not been initialised yet. Provisioning the attestation key must be done manually using the \texttt{TPM2\_Create} command.

Since U-Boot has file system support and all the relevant drivers, we can extend U-Boot's command system to include a command for creating an attestation key. This will place the public and private components in memory, and these can be written to a file on the microSD card for transfer to a remote computer.

\section{Example Setup}

For the thesis demonstration, and to evaluate this prototype, we have a small example of attestation in action. This consists of:

\begin{itemize}
    \item A U-Boot script that pulls a complete seL4 + root server image off TFTP and measures it into PCR 0.
    \item An seL4-power serial console diary, which provides the value of PCR 0 as well as a signed quote of the value in PCR 0.
    \item A remote verifier, implemented as a web application on a separate computer.
\end{itemize}

The verifier checks, in order:

\begin{enumerate}
    \item That the attestation structure is valid and contains a TPM quote.
    \item That the PCR digests provided match those in the attestation structure.
    \item That the signature is a valid signature for that attestation structure (using an OpenSSL command).
    \item That the attestation structure has a safe clock value.
    \item That no previous valid attestation attempts have the same or higher clock values. This means checking the clock, reset and restart values.
\end{enumerate}

If these checks pass, the verifier adds this attestation attempt to the history of valid attestation attempts.

If an attacker manages to hack the TFTP server, they can replace the seL4 image. However, U-Boot and OP-TEE are both written on the microSD card, so these are not compromised. For the example, we consider three different situations:

\begin{enumerate}
    \item The diary image is not compromised. (\autoref{fig:examplegood})
    \item An attacker replaces seL4 with `eL4' --- a version of seL4 with worse security guarantees than seL4. The root server image is unchanged. (\autoref{fig:examplebad})
    \item As above, but the attacker replaces the root server image with one that returns a hardcoded, known good PCR value and quote. (\autoref{fig:examplereplay})
\end{enumerate}

In the first case, the verifier application will in fact successfully verify the attestation. However, the PCR value is clearly different. This presents a practical drawback of TPM attestation. If a PCR value changes, it can be difficult to know if this is from an attack, or simply a system update (for example). For this example setup, we place the responsibility of checking the PCR on the end user.

In the second case, there are two possibilities. If the verifier application has seen a quote previously with a \textit{later} clock value than the hard-coded quote, the hard-coded quote fails to verify as the clock values are considered to be in the past. If the verifier application has not seen a quote previously with a later clock value than the hard-coded quote, the diary application is configured to re-generate the quote on pressing \texttt{@}. If the quote is hard-coded, the same quote will be produced, and the verifier application will detect that the same clock value has been used twice.

\begin{figure}[h]
    \centering
    \includegraphics[width=0.75\textwidth]{diary-good}

    \vspace{1cm}

    \includegraphics[width=0.95\textwidth]{site-good}
    \caption{The known good version of the diary, and the result of entering the details into the verification application.}
    \label{fig:examplegood}
\end{figure}

\begin{figure}[h]
    \centering
    \includegraphics[width=0.75\textwidth]{diary-bad}

    \vspace{1cm}

    \includegraphics[width=0.95\textwidth]{site-bad}
    \caption{The compromised version of the diary. Note that the PCR digest has changed.}
    \label{fig:examplebad}
\end{figure}

\begin{figure}[h]
    \centering
    \includegraphics[width=0.75\textwidth]{diary-replay}

    \vspace{1cm}

    \includegraphics[width=0.95\textwidth]{site-replay}
    \caption{A version of the diary implementing a replay attack. The PCR digest looks good, but the verification application realises it has seen newer clock values.}
    \label{fig:examplereplay}
\end{figure}

\unchapter{6}{Evaluation}

With a system using fTPM on top of seL4, as well as the example use case from the thesis demonstration, we can now compare the solution against the requirements detailed earlier.

\section{\hyperref[req:security]{Security}}

The security requirement is stated as: \textit{The design should follow the current state of the art in security practices, using as many of the available security mechanisms as possible in the correct way.}

For the parts of the design which have been implemented, this has been followed. The latest open source versions of fTPM and OP-TEE are used, fTPM implements as closely as possible the TPM 2.0 standard which is at the time of writing the most recent. The full access to the TPM means that the user can choose the algorithms being used in their TPM command parameters, however in the example setup only secure algorithms are being used (SHA256, 2048-bit RSA).

The only place where the current setup falls short is that there is no way to program the RPMB key into a secure fuse, instead the default derived OP-TEE key is used, which can be calculated from information read from the eMMC's manufacturing registers.

\section{\hyperref[req:performance]{Performance}}

The performance requirement is stated as: \textit{The implemented solution should not cause a significant overhead in the boot process and should not impede the operation of the system after the boot process unless specifically invoked.}

The overhead in the boot process was never measured, although we know from fTPM's paper that a firmware TPM is generally faster than a discrete TPM, since it ultimately runs on the main CPU \cite{RajFTPM}. More importantly however, since fTPM and the secure world can only be passively invoked from the \texttt{smc} instruction (when only using fTPM) this solution should not impede the operation of the system after the boot process unless specifically invoked, and thus the latter half of this requirement is met.

However, we cannot make any serious claims about performance without doing a proper benchmark. Since there are no benchmarks of this particular solution, this requirement can only be considered partially met.

\section{\hyperref[req:policyfreedom]{Policy Freedom}}

The policy freedom requirement is stated as: \textit{The design should not require the system running on top of seL4 to adhere to a particular security policy. Designers of the `end user' system should be able to freely use the TPM and attestation facilities in whatever way they see fit.}

Since fTPM support is fully implemented, the root server (and any other server with the \texttt{smc} capability) is free to use whichever TPM commands they like. This can be used to implement other security systems, or to make variations on the standard attestation process. Thus as far as the TPM is concerned, this requirement is met.

\section{\hyperref[req:verification]{Verification}}

The verification requirement is stated as: \textit{While full verification is outside the scope of this thesis, the design and implemented solution should at least be amenable to verification, with a strong specification and relatively small codebase.}

The nature of this solution makes this difficult to achieve. The largest targets for verification here are OP-TEE and fTPM. OP-TEE can in theory be replaced with seL4 in the long run, removing the need to verify it. However, the TPM specification is quite large and complicated, although it includes a full reference implementation.

The \texttt{smc} kernel object is difficult to verify without making strict assumptions about the secure world and any services running on top of it, and thus this solution may never be suitable for verification.

\section{\hyperref[req:secureboot]{Secure Boot}}

The secure boot requirement is stated as: \textit{The design should leverage some hardware or firmware functionality to attempt to certify a cryptographic signature for seL4 and the initial task, and should fail to boot if it cannot certify those signatures.}

As secure boot was not part of the final implementation nor part of the example system, this requirement is not met.

\section{\hyperref[req:attestation]{Attestation}}

The attestation requirement is stated as: \textit{The design should leverage a hardware or firmware TPM to provide remote attestation to a trusted remote verifier, through the use of a CAmkES module.}

Besides not using a CAmkES module, the example system demonstrates this requirement exactly, with an attestation being verified remotely over a serial connection.

\section{\hyperref[req:platform]{Platform}}

The platform requirement is stated as: \textit{The implementation should work on any ARM platform which supports some level of secure boot on the firmware and fTPM via. TrustZone}.

Most of the drivers used for the implementation would be platform independent. The exception is the MMC driver, however this follows a standard interface (the RPMB commands). Thus, to port this implementation to another system, one would only need to check for support for fTPM and provide an MMC driver capable of issuing MMC commands. This requirement is met.

\section{Summary}

\begin{table}[h]
    \centering
    \begin{tabular}{ll}
        \toprule
        Requirement                                  & Met? \\
        \midrule
        \hyperref[req:security]{Security}            & Mostly \\
        \hyperref[req:performance]{Performance}      & Somewhat \\
        \hyperref[req:policyfreedom]{Policy Freedom} & Yes \\
        \hyperref[req:verification]{Verification}    & No \\
        \hyperref[req:secureboot]{Secure Boot}       & No \\
        \hyperref[req:attestation]{Attestation}      & Mostly \\
        \hyperref[req:platform]{Platform}            & Yes \\
        \bottomrule
    \end{tabular}
    \caption{Summary of requirements met.}
    \label{tab:reqsummary}
\end{table}

\autoref{tab:reqsummary} summarises the degree to which each requirement is met. Four out of seven requirements are at least mostly met, and with some future work it should be possible to meet all requirements by building off this design. Only verification would not be possible to achieve with this design, due to fundamental problems with the \texttt{smc} instruction.

\unchapter{7}{Future Work}

We will now look at some work for the future: what work would be needed to consider this thesis truly complete, and with the benefit of hindsight some interesting alternative designs.

\section{Near Future}

For the near future, there are some small usability changes to be made to the source code. This includes packaging the libraries as CAmkES modules, and de-coupling the MMC driver, memory allocation, etc. However, the main aspect missing from the solution is secure boot support.

\subsection{Secure Boot}

Although attestation provides similar functionality to secure boot, an ideal system would support some combination of both. Although each stage of the boot process has some support for secure boot, this was never fully looked into. The only difference secure boot should have for seL4 is the quirk that the seL4 image has to be verified in two separate pieces: the kernel and ELF loader, and the root server image. This is because the root server image would likely be signed with a different key (or not at all) to the kernel and ELF loader. Since the way the image is generated depends on the platform, this could require some modifications to U-Boot such as a custom command.

To truly get secure boot working on ARM in the spirit of seL4 and verified software, it would be ideal to port a verified bootloader such as SABLE, however this would require complex changes to the way that SABLE works.

\section{Far Future}

For the far future, during this thesis we have identified some fundamental problems with the approach. These are some different approaches tailored to seL4 which can help address these problems, although they would require relatively more work.

\subsection{seL4 as a Trusted OS}

An ideal secure world operating system should be small enough to fit into secure memory, have strong security guarantees, and a small trusted computing base. This makes seL4 an ideal choice for running as a trusted operating system, and doing so has been proposed before in the seL4 community.

This means that, with a number of other secure world services, seL4 could be configured to replace OP-TEE as the underlying secure world operating system for fTPM as shown in \autoref{fig:futuresel4trusted}. This could even evolve into a multikernel-style solution, in which the normal world and secure world kernel are aware of each other's protections, and there are some guarantees that secure world applications cannot interfere with the normal world in unwanted ways.

Such a system is the only real way to make the \texttt{smc} instruction compatible with verification, assuming that the secure monitor is trusted that seL4 is in fact being used in both the normal and secure world.

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \draw (0,0) rectangle (5,1);
        \node at (2.5,0.5) {\footnotesize{}Secure Monitor};

        \draw (0,1.25) rectangle (2.375,2.25);
        \node at (1.1875,1.75) {\footnotesize{}seL4};

        \draw [fill=Thesis2] (2.625,1.25) rectangle (5,2.25);
        \node at (3.8125,1.75) {\footnotesize{}seL4};

        \draw (0,2.5) rectangle (1.0625,3.5);
        \node at (0.53125,3) {\footnotesize{}Apps};

        \draw (1.3125,2.5) rectangle (2.375,3.5);
        \node at (1.84375,3) {\footnotesize{}Suppl.};

        \draw (2.625,2.5) rectangle (3.6875,3.5);
        \node at (3.15625,3) {\footnotesize{}fTPM};

        \draw [fill=Thesis2] (3.9375,2.5) rectangle (5,3.5);
        \node at (4.46875,3) {\footnotesize{}Utils.};
    \end{tikzpicture}
    \caption{How seL4 can work as both a normal-world OS and a secure-world OS, in this case running fTPM in the secure world.}
    \label{fig:futuresel4trusted}
\end{figure}

\subsection{seL4 as a Bootloader}

The main motivation behind using TrustZone at all for attestation is that, in a normal system, TrustZone boots before seL4 and can provide isolation before seL4. However, if seL4 was used as a bootloader, seL4 would be able to provide it's own isolation early in the platform initialisation process. This would significantly reduce the reliance on TrustZone. Such a system could also help reduce the security issues faced by bootloaders, by offloading some parts of the boot process into isolated userspace processes.

This would require some modification of seL4, to support a `boot capability' granted to the root server, as shown in \autoref{fig:futuresel4bootloader}. This boot capability, when invoked by a thread, would:

\begin{enumerate}
    \item Unmap all pages except for the pages owned by this thread. Boot images, etc. would need to be copied into this `booting thread'.
    \item Jump to a given address in kernel mode, this address must be mapped in this thread.
\end{enumerate}

\begin{figure}[h]
    \centering
    \begin{tikzpicture}
        \draw (0,3) rectangle (3,4);
        \node at (1.5,3.5) {\footnotesize{}seL4};

        \draw (0,4.25) rectangle (1.375,5.25);
        \node at (0.6875,4.75) {\footnotesize{}Utils.};

        \draw (1.625,4.25) rectangle (3,5.25);
        \node at (2.3125,4.75) {\footnotesize{}Boot};

        \draw [fill=BG] (1.75,5.125) rectangle (2.875,5.625);
        \node at (2.3125,5.375) {\tiny{}Boot Cap.};

        \draw [dotted] (-0.25,2.75) -- (3.25,2.75);

        \draw (0,1.5) rectangle (3,2.5);
        \node at (1.5,2) {\footnotesize{}Main OS};

        \draw [->] (3.125,5.375) to [bend left] (3.125,3.75);
        \draw [->] (3.125,3.25) to [bend left] (3.125,2);
    \end{tikzpicture}
    \caption{How seL4 can be reconfigured to support a bootloader.}
    \label{fig:futuresel4bootloader}
\end{figure}

\unchapter{8}{Conclusion}

To conclude, we have designed and implemented a system which supports attestation on ARM systems using fTPM. While not implementing it in the design, we also speculate that secure boot is compatible with this design. There are however some fundamental issues with the design, and some other areas that could be improved.

When it comes to seL4, while secure boot and TPM attestation are viable means of providing platform security, it could be the case that a fundamentally different approach is better suited. This is particularly evident with fTPM and TrustZone, where it is difficult to justify having an isolated `secure' environment running on an operating system with \textit{less} security guarantees than seL4. Additionally, we are left wondering why we cannot bring seL4 into the boot process earlier, and rely on software-based isolation earlier in the boot process as opposed to hardware or firmware isolation.

\begin{thebibliography}{99}

\bibitem[Ars Technica 2011]{ArsTechAlureon}
Ars Technica.
2011.
4 million strong Alureon P2P botnet ``practically indestructible''. (July 2011).
Retrieved from \url{https://arstechnica.com/information-technology/2011/07/4-million-strong-alureon-botnet-practically-indestructable/}.

\bibitem[Goodin 2010]{RegisterAlureon}
Dan Goodin.
The Register.
2010.
World's most advanced rootkit penetrates 64-bit Windows. (November 2010).
Retrieved from \url{https://www.theregister.com/2010/11/16/tdl_rootkit_does_64_bit_windows/}.

\bibitem[Rutkowska 2009]{RutkowskaBitLocker}
Joanna Rutkowska.
2009.
Why do I miss Microsoft BitLocker?. (January 2009).
Retrieved from \url{http://theinvisiblethings.blogspot.com/2009/01/why-do-i-miss-microsoft-bitlocker.html}.

\bibitem[UEFI 2020]{UEFISpec}
UEFI Forum Inc.
2020.
Unified Extensible Firmware Interface (UEFI) Specification Version 2.8 (Errata B).

\bibitem[TCG 2019]{TPMSpec}
Trusted Computing Group.
2019.
Trusted Platform Module Library Specification, Family ``2.0'', Level 00, Revision 01.59.

\bibitem[Klein et. al. 2009]{KleinseL4}
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Endelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood.
2009.
seL4: Formal verification of an OS kernel.
\textit{ACM SOSP '09}, (January 2009), 207--220.

\bibitem[Heiser 2020]{HeiserPrinciples}
Gernot Heiser.
2020.
seL4 Design Principles. (March 2020).
Retrieved from \url{https://microkerneldude.wordpress.com/2020/03/11/sel4-design-principles/}.

\bibitem[Shkatov and Michael 2020]{NVDBoothole}
Mickey Shkatov and Jesse Michael.
2020.
There's a Hole in the Boot. (July 2020).
Retrieved from \url{https://eclypsium.com/2020/07/29/theres-a-hole-in-the-boot/}.

\bibitem[Constable et. al. 2018]{ConstableSABLE}
Scott Constable, Rob Sutton, Arash Sahebolamri and Steve Chapin.
2018.
\textit{Formal Verification of a Modern Boot Loader}.
Electrical Engineering and Computer Science Technical Reports.
Syracuse University, Syracuse, NY.

\bibitem[Raj et. al. 2016]{RajFTPM}
Himanshu Raj, Stefan Saroiu, Alec Wolman, Ronald Aigner, Jeremiah Cox, Paul England, Chris Fenner, Kinshuman Kinshumann, Jork Loeser, Dennis Mattoon, Magnus Nystrom, David Robinson, Rob Spiger, Stefan Thom, and David Wooten.
2016.
fTPM: A Software-Only Implementation of a TPM Chip.
\textit{USENIX Security 16}, (August 2016), 841--856.

\bibitem[Eldefrawy et. al. 2017]{EldefrawyHYDRA}
Karim Eldefrawy, Norrathep Rattanavipanon and Gene Tsudik.
2017.
HYDRA: Hybrid Design for Remote Attestation (Using a Formally Verified Microkernel).
\textit{ACM WiSec '17}, (July 2017), 99--110.

\bibitem[Heiser et. al. 2011]{HeiserTrust}
Gernot Heiser, Leonid Ryzhykm Michael von Tessin, and Aleksander Budzynowski.
2011.
What If You Could Actually Trust Your Kernel?
\textit{USENIX HotOS 13}, (May 2011).

\bibitem[Tremblay 2021]{MicrosoftSigning}
Kevin Tremblay.
2021.
UEFI Signing Requirements. (January 2021).
Retrieved from \url{https://techcommunity.microsoft.com/t5/hardware-dev-center/updated-uefi-signing-requirements/ba-p/1062916}.

\bibitem[Debian 2021]{DebianShim}
Debian Wiki.
2021.
Secure Boot. (February 2021).
Retrieved from \url{https://wiki.debian.org/SecureBoot#Shim}.

\bibitem[Garrett 2019]{GarrettRemote}
Matthew Garrett.
2019.
What does remote attestation buy you?.
\textit{Linux Plumbers Conference 2019}, (September 2019).

\bibitem[Garret 2017]{GarrettFragility}
Matthew Garrett.
2017.
Avoiding TPM PCR Fragility Using Secure Boot. (July 2017).
Retrieved from \url{https://mjg59.dreamwidth.org/48897.html}.

\bibitem[Arthur et. al. 2015]{SpringerPCRs}
Will Arthur, David Challener and Kenneth Goldman.
2015.
\textit{A Practical Guide to TPM 2.0}.
Apress, Berkeley, CA.

\bibitem[Chiang 2021]{ChiangKeys}
Eric Chiang.
2021.
The Trusted Platform Module Key Hierarchy. (January 2021).
Retrieved from \url{https://ericchiang.github.io/post/tpm-keys/}.

\bibitem[Trustworthy Systems 2020]{seL4Manual}
Trustworthy Systems Team.
2020.
\textit{seL4 Reference Manual}. Version 12.0.0.

\bibitem[VanVossen 2021]{SMCRFC}
Robbie VanVossen.
2021.
seL4 RFC-9: Add new capability for seL4 SMC Forwarding. (November 2021).
Retrieved from \url{https://sel4.atlassian.net/browse/RFC-9}.

\bibitem[OP-TEE 2021]{OPTEERepo}
OP-TEE Core Maintainers.
2021.
OP-TEE build.git.
Retrieved from \url{https://github.com/OP-TEE/build}.

\bibitem[Denk 2021]{UBootRepo}
Wolfgang Denk, DENX Software Engineering and U-Boot Maintainers.
2021.
Das U-Boot Source Tree.
Retrieved from \url{https://github.com/U-Boot/u-boot}.

\end{thebibliography}

\end{document}
