diff options
Diffstat (limited to 'thesis.bib')
| -rw-r--r-- | thesis.bib | 93 |
1 files changed, 93 insertions, 0 deletions
@@ -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} +} |