path: root/thesis.bib

@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}
}

@article{10.1145/363235.363259,
author = {Hoare, C. A. R.},
title = {An Axiomatic Basis for Computer Programming},
issue_date = {Oct. 1969},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {12},
number = {10},
issn = {0001-0782},
doi = {10.1145/363235.363259},
abstract = {In this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics. This involves the elucidation of sets of axioms and rules of inference which can be used in proofs of the properties of computer programs. Examples are given of such axioms and rules, and a formal proof of a simple theorem is displayed. Finally, it is argued that important advantage, both theoretical and practical, may follow from a pursuance of these topics.},
journal = {Commun. ACM},
date = {1969-10},
pages = {576–580},
numpages = {5},
keywords = {machine-independent programming, theory of programming' proofs of programs, program documentation, axiomatic method, programming language design, formal language definition}
}

@article{10.1007/s001650050057,
author = {Kleymann, Thomas},
title = {Hoare Logic and Auxiliary Variables},
issue_date = {Dec 1999},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
volume = {11},
number = {5},
issn = {0934-5043},
doi = {10.1007/s001650050057},
abstract = {Auxiliary variables are essential for specifying programs in Hoare Logic. They are required to relate the value of variables in different states. However, the axioms and rules of Hoare Logic turn a blind eye to the role of auxiliary variables. We stipulate a new structural rule for adjusting auxiliary variables when strengthening preconditions and weakening postconditions. Courtesy of this new rule, Hoare Logic is adaptation complete, which benefits software re-use. This property is responsible for a number of improvements. Relative completeness follows uniformly from the Most General Formula property. Moreover, one can show that Hoare Logic subsumes Vienna Development Method's (VDM) operation decomposition rules in that every derivation in VDM can be naturally embedded in Hoare Logic. Furthermore, the new treatment leads to a significant simplification in the presentation for verification calculi dealing with more interesting features such as recursion.},
journal = {Formal Aspects of Computing},
date = {1999-12},
pages = {541–566},
numpages = {26},
keywords = {Keywords: Hoare Logic; Auxiliary variables; Adaptation Completeness; Most General Formula; VDM}
}

@article{10.1007/s00165-019-00501-3,
author = {Apt, Krzysztof R. and Olderog, Ernst-R\"{u}diger},
title = {Fifty Years of Hoare’s Logic},
issue_date = {Dec 2019},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
volume = {31},
number = {6},
issn = {0934-5043},
doi = {10.1007/s00165-019-00501-3},
abstract = {We present a history of Hoare’s logic.},
journal = {Formal Aspects of Computing},
date = {2019-12},
pages = {751–807},
numpages = {57}
}