Introduction first draft.

1 files changed, 93 insertions, 0 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}
+}