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

@InProceedings{10.1007/3-540-47721-7_24,
author="Barrett, Paul",
editor="Odlyzko, Andrew M.",
title="Implementing the Rivest Shamir and Adleman Public Key Encryption Algorithm on a Standard Digital Signal Processor",
booktitle="Advances in Cryptology --- CRYPTO' 86",
date="1987",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="311--323",
abstract="A description of the techniques employed at Oxford University to obtain a high speed implementation of the RSA encryption algorithm on an ``off-the-shelf'' digital signal processing chip. Using these techniques a two and a half second (average) encrypt time (for 512 bit exponent and modulus) was achieved on a first generation DSP (The Texas Instruments TMS 32010) and times below one second are achievable on second generation parts. Furthermore the techniques of algorithm development employed lead to a provably correct implementation.",
isbn="978-3-540-47721-1",
doi = {10.1007/3-540-47721-7_24}
}

@online{agda.readthedocs.io,
author = "Agda",
title = "Agda's Documentation",
date = "2021-12-08T07:15:24+00:00",
url = "https://agda.readthedocs.io/en/v2.6.2.1/",
version = "59c7944b",
urldate = "2022-05-18T16:39:44+01:00"
}

@article{10.1145/3290384,
author = {Armstrong, Alasdair and Bauereiss, Thomas and Campbell, Brian and Reid, Alastair and Gray, Kathryn E. and Norton, Robert M. and Mundkur, Prashanth and Wassell, Mark and French, Jon and Pulte, Christopher and Flur, Shaked and Stark, Ian and Krishnaswami, Neel and Sewell, Peter},
title = {ISA Semantics for ARMv8-a, RISC-v, and CHERI-MIPS},
issue_date = {January 2019},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {3},
number = {POPL},
url = {https://doi.org/10.1145/3290384},
doi = {10.1145/3290384},
abstract = { Architecture specifications notionally define the fundamental interface between hardware and software: the envelope of allowed behaviour for processor implementations, and the basic assumptions for software development and verification. But in practice, they are typically prose and pseudocode documents, not rigorous or executable artifacts, leaving software and verification on shaky ground.  In this paper, we present rigorous semantic models for the sequential behaviour of large parts of the mainstream ARMv8-A, RISC-V, and MIPS architectures, and the research CHERI-MIPS architecture, that are complete enough to boot operating systems, variously Linux, FreeBSD, or seL4. Our ARMv8-A models are automatically translated from authoritative ARM-internal definitions, and (in one variant) tested against the ARM Architecture Validation Suite.  We do this using a custom language for ISA semantics, Sail, with a lightweight dependent type system, that supports automatic generation of emulator code in C and OCaml, and automatic generation of proof-assistant definitions for Isabelle, HOL4, and (currently only for MIPS) Coq. We use the former for validation, and to assess specification coverage. To demonstrate the usability of the latter, we prove (in Isabelle) correctness of a purely functional characterisation of ARMv8-A address translation. We moreover integrate the RISC-V model into the RMEM tool for (user-mode) relaxed-memory concurrency exploration. We prove (on paper) the soundness of the core Sail type system.  We thereby take a big step towards making the architectural abstraction actually well-defined, establishing foundations for verification and reasoning. },
journal = {Proc. ACM Program. Lang.},
date = {2019-01},
articleno = {71},
numpages = {31},
keywords = {Theorem Proving, Instruction Set Architectures, Semantics}
}

@manual{riscv/spec-20191213,
title = {The RISC-V Instruction Set Manual},
subtitle = {Volume I: Unprivileged ISA},
author = {{The RISC-V Foundation}},
shortauthor = {RISC-V},
editor = {Waterman, Andrew and Asanović, Krste},
date = {2019-12-13},
version = {20191213},
organsization = {The RISC-V Foundation},
url = {https://github.com/riscv/riscv-isa-manual/releases/download/Ratified-IMAFDQC/riscv-spec-20191213.pdf},
}

@article{10.46586/tches.v2022.i1.211-244,
title={Neon NTT: Faster Dilithium, Kyber, and Saber on Cortex-A72 and Apple M1},
author={Becker, Hanno and Hwang, Vincent and Kannwischer, Matthias J. and Yang, Bo-Yin and Yang, Shang-Yi},
volume={2022},
abstract={We present new speed records on the Armv8-A architecture for the latticebased schemes Dilithium, Kyber, and Saber. The core novelty in this paper is the combination of Montgomery multiplication and Barrett reduction resulting in “Barrett multiplication” which allows particularly efficient modular one-known-factor multiplication using the Armv8-A Neon vector instructions. These novel techniques combined with fast two-unknown-factor Montgomery multiplication, Barrett reduction sequences, and interleaved multi-stage butterflies result in significantly faster code. We also introduce “asymmetric multiplication” which is an improved technique for caching the results of the incomplete NTT, used e.g. for matrix-to-vector polynomial multiplication. Our implementations target the Arm Cortex-A72 CPU, on which our speed is 1.7× that of the state-of-the-art matrix-to-vector polynomial multiplication in kyber768 [Nguyen–Gaj 2021]. For Saber, NTTs are far superior to Toom–Cook multiplication on the Armv8-A architecture, outrunning the matrix-to-vector polynomial multiplication by 2.0×. On the Apple M1, our matrix-vector products run 2.1× and 1.9× faster for Kyber and Saber respectively.},
number={1},
journal={IACR Transactions on Cryptographic Hardware and Embedded Systems},
date={2021-11-19},
pages={221–244},
doi={10.46586/tches.v2022.i1.221-244}
}