$\mathcal{P}\text{ARseL}$: Towards a Verified Root-of-Trust Over seL4

Widespread adoption and growing popularity of embedded/IoT/CPS devices make them attractive attack targets. On low-to-mid-range devices, security features are typically few or none due to various constraints. Such devices are thus subject to malware-based compromise. One popular defensive measure is Remote Attestation $(\mathcal{R}\mathrm{A})$ which allows a trusted entity to determine the current software integrity of an untrusted remote device. For higher-end devices, $\mathcal{R}\mathrm{A}$ is achievable via secure hardware components. For low-end (bare metal) devices, minimalistic hybrid (hardware/-software) $\mathcal{R}\mathrm{A}$ is effective, which incurs some hardware modifications. That leaves certain mid-range devices (e.g., ARM Cortex-A family) equipped with standard hardware components, e.g., a memory management unit (MMU) and perhaps a secure boot facility. In this space, seL4 (a verified microkernel with guaranteed process isolation) is a promising platform for attaining $\mathcal{R}\mathrm{A}$ . HYDRA [1] made a first step towards this, albeit without achieving any verifiability or provable guarantees. This paper picks up where HYDRA left off by constructing a $\mathcal{P}\text{ARseL}$ architecture, that separates all user-dependent components from the TCB. This leads to much stronger isolation guarantees, based on seL4 alone, and facilitates formal verification. In $\mathcal{P}\text{ARseL}$ , We use formal verification to obtain several security properties for the isolated $\mathcal{R}\mathrm{A}$ TCB, including: memory safety, functional correctness, and secret independence. We implement $\mathcal{P}\text{ARseL}$ in $F^{\ast}$ and specify/prove expected properties using Hoare logic. Next, we automatically translate the $F^{\ast}$ implementation to C using KaRaM eL, which preserves verified properties of $\mathcal{P}\text{ARseL}$ , C implementation (atop seL4). Finally, we instantiate and evaluate $\mathcal{P}\text{ARseL}$ on a commodity platform - a SabreLite embedded device.