Introduction first draft.

2 files changed, 192 insertions, 6 deletions

diff --git a/thesis.bib b/thesis.bib
index e69de29..54b8b70 100644
--- a/thesis.bib
+++ b/thesis.bib
@@ -0,0 +1,93 @@
+@inproceedings{10.1145/3133956.3134078,
+author = {Almeida, Jos\'{e} Bacelar and Barbosa, Manuel and Barthe, Gilles and Blot, Arthur and Gr\'{e}goire, Benjamin and Laporte, Vincent and Oliveira, Tiago and Pacheco, Hugo and Schmidt, Benedikt and Strub, Pierre-Yves},
+title = {Jasmin: High-Assurance and High-Speed Cryptography},
+year = {2017},
+isbn = {9781450349468},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+doi = {10.1145/3133956.3134078},
+abstract = {Jasmin is a framework for developing high-speed and high-assurance cryptographic software.
+The framework is structured around the Jasmin programming language and its compiler.
+The language is designed for enhancing portability of programs and for simplifying
+verification tasks. The compiler is designed to achieve predictability and efficiency
+of the output code (currently limited to x64 platforms), and is formally verified
+in the Coq proof assistant. Using the supercop framework, we evaluate the Jasmin compiler
+on representative cryptographic routines and conclude that the code generated by the
+compiler is as efficient as fast, hand-crafted, implementations. Moreover, the framework
+includes highly automated tools for proving memory safety and constant-time security
+(for protecting against cache-based timing attacks). We also demonstrate the effectiveness
+of the verification tools on a large set of cryptographic routines.},
+booktitle = {Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security},
+pages = {1807–1823},
+numpages = {17},
+keywords = {constant-time security, safety, cryptographic implementations, verified compiler},
+location = {Dallas, Texas, USA},
+series = {CCS '17}
+}
+
+
+@inproceedings{hal/01238879,
+  author = {Leroy, Xavier and Blazy, Sandrine and K\"astner, Daniel
+            and Schommer, Bernhard and Pister, Markus and Ferdinand, Christian},
+  title = {CompCert -- A Formally Verified Optimizing Compiler},
+  booktitle = {ERTS 2016: Embedded Real Time Software and Systems},
+  publisher = {SEE},
+  year = 2016,
+  url = {https://hal.inria.fr/hal-01238879},
+  xtopic = {compcert},
+  abstract = {CompCert is the first commercially available
+optimizing compiler that is formally verified, using machine-assisted
+mathematical proofs, to be exempt from mis-compilation.
+The executable code it produces is proved
+to behave exactly as specified by the semantics of the
+source C program. This article gives an overview of
+the design of CompCert and its proof concept and then
+focuses on aspects relevant for industrial application.
+We briefly summarize practical experience and give an
+overview of recent CompCert development aiming at industrial usage.
+CompCert’s intended use is the compilation of life-critical
+and mission-critical software meeting high levels of assurance.
+In this context tool qualification is of paramount importance. We
+summarize the confidence argument of CompCert and give an overview of
+relevant qualification strategies.}
+}
+
+@article{10.46586/tches.v2022.i1.482-505,
+author={Becker, Hanno and Bermudo Mera, Jose Maria and Karmakar, Angshuman and Yiu, Joseph and Verbauwhede, Ingrid},
+title={Polynomial multiplication on embedded vector architectures},
+journal={IACR Transactions on Cryptographic Hardware and Embedded Systems},
+publisher={Ruhr-Universität Bochum},
+volume={2022, Issue 1},
+pages={482-505},
+doi={10.46586/tches.v2022.i1.482-505},
+year=2021
+}
+
+@manual{arm/DDI0553B.s,
+title = {Armv8-M Architecture Reference Manual},
+author = {{Arm Limited}},
+shortauthor = {Arm},
+date = {2022-04-01},
+version = {B.s},
+organsization = {Arm Limited},
+url = {https://developer.arm.com/documentation/ddi0553/bs/},
+}
+
+@InProceedings{10.1007/978-3-642-03359-9_6,
+author="Bove, Ana
+and Dybjer, Peter
+and Norell, Ulf",
+editor="Berghofer, Stefan
+and Nipkow, Tobias
+and Urban, Christian
+and Wenzel, Makarius",
+title="A Brief Overview of Agda -- A Functional Language with Dependent Types",
+booktitle="Theorem Proving in Higher Order Logics",
+date="2009",
+publisher="Springer Berlin Heidelberg",
+address="Berlin, Heidelberg",
+pages="73--78",
+abstract="We give an overview of Agda, the latest in a series of dependently typed programming languages developed in Gothenburg. Agda is based on Martin-L{\"o}f's intuitionistic type theory but extends it with numerous programming language features. It supports a wide range of inductive data types, including inductive families and inductive-recursive types, with associated flexible pattern-matching. Unlike other proof assistants, Agda is not tactic-based. Instead it has an Emacs-based interface which allows programming by gradual refinement of incomplete type-correct terms.",
+isbn="978-3-642-03359-9",
+doi={10.1007/978-3-642-03359-9_6}
+}
diff --git a/thesis.org b/thesis.org
index 21a5125..e08bd45 100644
--- a/thesis.org
+++ b/thesis.org
@@ -1,7 +1,7 @@
 #+options: ':t *:t -:t ::t <:t H:3 \n:nil ^:t arch:headline author:t
 #+options: broken-links:nil c:nil creator:nil d:(not "LOGBOOK") date:t e:t
 #+options: email:nil f:t inline:t num:t p:nil pri:nil prop:nil stat:t tags:t
-#+options: tasks:t tex:t timestamp:t title:t toc:t todo:t |:t
+#+options: tasks:t tex:t timestamp:t title:t toc:nil todo:t |:t
 #+title: Semantics of an embedded vector architecture for formal verification of software
 #+date: \today
 #+author: Greg Brown
@@ -13,7 +13,7 @@
 #+cite_export: biblatex
 #+bibliography: ./thesis.bib
 #+latex_class: article
-#+latex_class_options: [twocolumn,a4paper]
+#+latex_class_options: [twoside,a4paper]
 #+latex_header: \usepackage[hyperref=true,url=true,backend=biber,natbib=true]{biblatex}
 #+latex_header: \usepackage{savetrees}
 #+latex_compiler: pdflatex
@@ -32,14 +32,107 @@ applications.
 
 * Introduction
 
-* Arm Pseudocode
+In nearly all cases, the best implementation of an algorithm for a particular
+purpose is both correct and fast. If the implementation is not correct, then it
+does not implement the algorithm. If the implementation is slow, then resources are
+wasted executing this algorithm over performing other useful work. Ensuring
+implementations are both performant and correct is typically difficult.
 
-* Denotational Semantics
+One case that proves particularly tricky is writing assembly code. Most modern
+handwritten assembly is for cryptographic algorithms, where it is vital that
+compilers do not introduce timing attacks or other side channels. Hand written
+assembly can also take advantage of microarchitectural differences to gain a
+slight performance benefit.
 
-* Hoare Semantics
+Another domain that frequently deals with assembly code is the output of
+compilers. Optimising compilers take the semantic operations described by
+high-level code and attempt to produce the optimal machine code to perform those
+actions.
 
-* Mathematical Proofs
+In both of these cases, either humans or machines shuffle around instructions in
+an attempt to eek out the best performance from hardware. The resulting code
+warps the original algorithms in ways that make it difficult to determine
+whether the actions performed actually have the same result. The correctness of
+the assembly code comes into question.
+
+It is only possible to prove the assembly code is correct if there is a model
+describing how it should behave. Suitable mathematical models of the behaviour
+allow for the construction of formal proofs certifying the assembly code has the
+correct behaviour. Due to the size and complexity of different instruction set
+architectures (ISAs), formal verification of software in this manner makes use
+of a number of software tools.
+
+Formal verification software is well-developed for the x86-64 and Arm A-profile
+ISAs. For instance, Jasmin [cite:@10.1145/3133956.3134078] is a programming
+language which verifies that compiling to x86-64 preserves a set of user-defined
+safety properties. Another similar tool is CompCert [cite:@hal/01238879] which
+is a verified C compiler, ensuring that the program semantics are preserved
+during compilation.
+
+Unfortunately, little work has been done to formally verify software written for
+the Arm M-profile architecture. This architecture is designed for low-power and
+low-latency microcontrollers, which operate in resource-constrained
+environments.
+
+The goal of this project is to formally verify an assembly function for the Arm
+M-profile architecture. The specific algorithm
+[cite:@10.46586/tches.v2022.i1.482-505] is a hand-written highly-optimised
+assembly-code implementation of the number-theoretic transform, which is an
+important procedure for post-quantum cryptography.
+
+This work has made progress on two fronts. Most work has been spent developing
+an embedding and semantic model of the Armv8.1-M pseudocode specification
+language for the Agda programming language [cite:@10.1007/978-3-642-03359-9_6].
+All instructions in the Armv8.1-M architecture are given a "precise description"
+[cite:@arm/DDI0553B.s § \(\texttt{I}_\texttt{RTDZ}\)] using the pseudocode, and
+by developing an embedding within Agda, it is possible to use its powerful type
+system to construct formal proofs of correctness.
+
+Progress has also been made on the formal algebraic verification of Barrett
+reduction, a subroutine of the NTT.  Whilst there exists a paper proof of the
+correctness of Barrett reduction, a proof of Barrett reduction within Agda is
+necessary to be able to prove the correctness of the given implementation of the
+NTT.
+
+Structure of the paper:
+- [[Armv8.1-M Pseudocode Specification Language]] describes the Armv8.1-M pseudocode
+  specification language. This is an imperative programming language used by the
+  Armv8.1-M manual to describe the operation of the instructions.
+- A simple recap of Hoare logic is given in [[Hoare Logic]]. This is the backbone of
+  one of the formal verification techniques used in this work.
+- [[Formal Definition of MSL]] contains a description of MSL. This is a language
+  similar to the Armv8.1-M pseudocode embedded within the Agda programming
+  language.
+- The denotational semantics and a Hoare logic semantics of MSL are detailed in
+  [[Semantics of MSL]]. Due to Agda's nature of being a dependently-typed language,
+  these are both given using Agda code.
+- [[Application to Proofs]] describes the experience of using the Hoare logic and
+  denotational semantics of MSL to prove the correctness of some simple
+  routines, given in [[Proofs using Hoare Semantics]] and [[Proofs using Denotational
+  Semantics]] respectively.
+- Formal verification of Barrett reduction, an important subroutine in the NTT,
+  is given in [[Proofs of Barrett Reduction]]. In particular, it proves that Barrett
+  reduction performs a modulo reduction and gives bounds on the size of the
+  result.
+- Finally, [[Future Work]] describes the steps necessary to complete the formal
+  verification of the NTT, as well as listing some other directions this work
+  can be taken.
+
+* Background
+** Armv8.1-M Pseudocode Specification Language
+** Hoare Logic
+
+* Implementation
+** Formal Definition of MSL
+** Semantics of MSL
+
+* Application to Proofs
+** General Observations
+** Proofs using Hoare Semantics
+** Proofs using Denotational Semantics
+** Proofs of Barrett Reduction
 
 * Conclusions
+** Future Work
 
 #+print_bibliography: