\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\usepackage{eurosym}
  %for \<euro>

%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd}
  %for \<Sqinter>, \<Parallel>, \<Zsemi>, \<Parallel>, \<sslash>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}


\begin{document}

\title{A Formal CHERI-C Memory Model}
\author{Seung Hoon Park}
\maketitle

\begin{abstract}
%CHERI-C extends the C programming language by adding \textit{hardware
%capabilities}, ensuring a certain degree of memory safety while remaining efficient.
%Capabilities can also be employed for higher-level security measures, such as
%software compartmentalization, that have to be used correctly to achieve the
%desired security guarantees. As the extension changes the semantics of C,
%new theories and tooling are required to reason about CHERI-C code
%and verify correctness.
%
In this work, we present a formal memory model that provides a memory
semantics for CHERI-C programs with uncompressed capabilities in a `purecap'
environment. We present a CHERI-C memory model theory with
properties suitable for verification and potentially other types of
analyses. Our theory generates an OCaml executable instance of the memory model,
which is then used to instantiate the parametric \textit{Gillian}
program analysis framework, enabling concrete execution of
CHERI-C programs. The tool can run a CHERI-C test suite, demonstrating the
correctness of our tool, and catch a good class of safety violations that the
CHERI hardware might miss.

The proof is accompanied by a paper~\cite{park_2022} that explains the Gillian
framework instantiation that uses the OCaml code generated by this work.
\end{abstract}

\tableofcontents
\subsubsection*{Acknowledgements}
The author was funded by the UKRI programme on Digital Security by Design 
(Ref. EP/V000225/1, \href{https://scorch-project.github.io/}{SCorCH}).
\newpage

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
