NDSS

\documentclass[conference]{IEEEtran}
\IEEEoverridecommandlockouts

\usepackage{times}
\usepackage{graphicx}
\usepackage{amsmath,amssymb}
\usepackage{booktabs}
\usepackage{url}
\usepackage{cite}
\usepackage[hidelinks]{hyperref}

\hyphenation{op-tical net-works semi-conduc-tor}

% NDSS-mandated footer block. Update year/DOI/ISBN for the target instance.
\makeatletter
\def\ps@headings{%
\def\@oddhead{\mbox{}\hfill
\hspace*{1em}\thepage}%
\def\@oddfoot{\hfill\scriptsize\parbox{0.9\textwidth}{\centering
Network and Distributed System Security (NDSS) Symposium 2026\\
24--28 February 2026, City, Country\\
ISBN 1-891562-XX-X\\
https://dx.doi.org/10.14722/ndss.2026.XXXXX\\
www.ndss-symposium.org}\hfill}}
\makeatother
\pagestyle{headings}

\begin{document}

\title{EnclaveX: Verified Confidential Computing for\\
       Memory-Constrained Embedded Devices}

\author{\IEEEauthorblockN{First Last, Jane Doe, John Smith}
\IEEEauthorblockA{University of Example \\
Example Research Labs\\
\{you, jane, john\}@example.com}}

\maketitle

\begin{abstract}
Trusted execution environments (TEEs) on embedded devices offer strong
isolation but lack formal verification of their runtime. We present
EnclaveX, a verified micro-runtime for ARM TrustZone that fits in 18KB
of ROM and formally guarantees memory isolation and secure boot
integrity via Coq proofs. EnclaveX has been deployed on three
commercial device families across 14 months of evaluation and has
passed independent penetration testing by two external teams.
\end{abstract}

\section{Introduction}
Billions of devices now run TEEs. Few are formally verified; most have
had non-trivial bugs discovered in their runtimes. The embedded segment
in particular is under-served by verification work, which has focused
on server-class SGX implementations.

\paragraph{Contributions.}
\begin{itemize}
\item A verified TrustZone micro-runtime in 18KB ROM with formal Coq
  proofs of memory isolation and boot integrity.
\item A Rust-to-Coq pipeline that makes verification tractable for
  system programmers who are not proof engineers.
\item Deployment on three commercial device families covering 14 months
  of production use without observed vulnerabilities.
\end{itemize}

\section{Background}
ARM TrustZone, seL4, Komodo, HACL*, and the TEE ecosystem.

\section{Threat Model}
We assume an attacker with arbitrary code execution in the non-secure
world, network adversarial control, and physical access up to (but not
including) decapsulation. The hardware root of trust is assumed intact.

\section{Design}
EnclaveX's micro-runtime provides minimal syscalls: memory allocation,
secure storage, attestation. Each is accompanied by a Coq-verified
contract.

\subsection{Memory-Safety Proof}
We prove that no secure-world pointer ever escapes to the non-secure
world via a single invariant over the syscall interface.

\subsection{Attestation}
The runtime measures itself during boot and produces a signed
attestation. The measurement chain covers ROM, stack initialization,
and the initial syscall dispatch table.

\section{Implementation}
The implementation is 5{,}100 LOC of Rust, verified via the
Rust-to-Coq pipeline described in Section IV. The corresponding Coq
development is 18{,}300 lines.

\section{Evaluation}
\begin{table}[t]
\centering
\small
\begin{tabular}{lc}
\toprule
Benchmark & Overhead (\%) \\
\midrule
Crypto throughput     & 1.8 \\
Storage access        & 4.2 \\
Remote attestation    & 6.1 \\
\bottomrule
\end{tabular}
\caption{Measured overhead vs.\ vendor TEE runtime.}
\end{table}

\subsection{External Evaluation}
Two independent penetration-testing teams spent four person-weeks
probing EnclaveX for vulnerabilities. None were found.

\section{Related Work}
seL4-on-ARM, Komodo, Sanctum, Keystone.

\section{Conclusion}
Verified TEEs are feasible at the scale required for consumer embedded
devices. EnclaveX provides a foundation for higher-assurance systems
across the embedded TEE ecosystem.

\section*{Ethics Considerations}
This work involved no human subjects. All third-party device firmware
used for testing was obtained through legitimate channels.

\bibliographystyle{IEEEtran}
\bibliography{refs}

\end{document}