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

@phdthesis{cs.cmu.edu/girard-72-thesis,
author={Girard, Jean-Yves},
title={Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur},
institution={University of Paris VII},
date={1972-06-26},
language={french},
pagetotal={230}
}

@article{10.1145/360933.360975,
author = {Dijkstra, Edsger W.},
title = {Guarded Commands, Nondeterminacy and Formal Derivation of Programs},
issue_date = {Aug. 1975},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {18},
number = {8},
issn = {0001-0782},
doi = {10.1145/360933.360975},
abstract = {So-called “guarded commands” are introduced as a building block for alternative and repetitive constructs that allow nondeterministic program components for which at least the activity evoked, but possibly even the final state, is not necessarily uniquely determined by the initial state. For the formal derivation of programs expressed in terms of these constructs, a calculus will be be shown.},
journal = {Commun. ACM},
date = {1975-08},
pages = {453–457},
numpages = {5},
keywords = {termination, program semantics, case-construction, programming methodology, repetition, programming language semantics, correctness proof, nondeterminancy, sequencing primitives, programming languages, derivation of programs}
}

@INPROCEEDINGS{10.1109/SP.2019.00005,
author={Erbsen, Andres and Philipoom, Jade and Gross, Jason and Sloan, Robert and Chlipala, Adam},
booktitle={2019 IEEE Symposium on Security and Privacy (SP)},
title={Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises},
year={2019},
volume={},
number={},
pages={1202-1219},
doi={10.1109/SP.2019.00005}
}

@inproceedings{10.1145/3319535.3354199,
author = {Fu, Yu-Fu and Liu, Jiaxiang and Shi, Xiaomu and Tsai, Ming-Hsien and Wang, Bow-Yaw and Yang, Bo-Yin},
title = {Signed Cryptographic Program Verification with Typed CryptoLine},
year = {2019},
isbn = {9781450367479},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
doi = {10.1145/3319535.3354199},
abstract = {We develop an automated formal technique to specify and verify signed computation in cryptographic programs. In addition to new instructions, we introduce a type system to detect type errors in programs. A type inference algorithm is also provided to deduce types and instruction variants in cryptographic programs. In order to verify signed cryptographic C programs, we develop a translator from the GCC intermediate representation to our language. Using our technique, we have verified 82 C functions in cryptography libraries including NaCl, wolfSSL, bitcoin, OpenSSL, and BoringSSL.},
booktitle = {Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security},
pages = {1591–1606},
numpages = {16},
keywords = {formal verification, cryptographic programs, model checking},
location = {London, United Kingdom},
series = {CCS '19}
}

@article{10.1007/s00165-014-0326-7,
author={Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and Signoles, Julien and Yakobowski, Boris},
title = {Frama-C: A software analysis perspective},
date = {2015-01-09},
pages = {573-609},
numpages = {37},
journal = {Formal Aspects of Computing},
abstract = {Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements.},
doi = {10.1007/s00165-014-0326-7},
number = {3},
volume = {27}
}

@InProceedings{10.1007/978-3-642-19718-5_1,
author="Appel, Andrew W.",
editor="Barthe, Gilles",
title="Verified Software Toolchain",
booktitle="Programming Languages and Systems",
year="2011",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="1--17",
abstract="The software toolchain includes static analyzers to check assertions about programs; optimizing compilers to translate programs to machine language; operating systems and libraries to supply context for programs. Our Verified Software Toolchain verifies with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context, on a weakly-consistent-shared-memory machine.",
isbn="978-3-642-19718-5",
doi={10.1007/978-3-642-19718-5_1}
}

@article{10.1145/3290376,
author = {Fromherz, Aymeric and Giannarakis, Nick and Hawblitzel, Chris and Parno, Bryan and Rastogi, Aseem and Swamy, Nikhil},
title = {A Verified, Efficient Embedding of a Verifiable Assembly Language},
year = {2019},
issue_date = {January 2019},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {3},
number = {POPL},
url = {https://doi.org/10.1145/3290376},
doi = {10.1145/3290376},
abstract = {High-performance cryptographic libraries often mix code written in a high-level language with code written in assembly. To support formally verifying the correctness and security of such hybrid programs, this paper presents an embedding of a subset of x64 assembly language in F* that allows efficient verification of both assembly and its interoperation with C code generated from F*. The key idea is to use the computational power of a dependent type system's type checker to run a verified verification-condition generator during type checking. This allows the embedding to customize the verification condition sent by the type checker to an SMT solver. By combining our proof-by-reflection style with SMT solving, we demonstrate improved automation for proving the correctness of assembly-language code. This approach has allowed us to complete the first-ever proof of correctness of an optimized implementation of AES-GCM, a cryptographic routine used by 90\% of secure Internet traffic.},
journal = {Proc. ACM Program. Lang.},
month = {jan},
articleno = {63},
numpages = {30},
keywords = {Assembly language, domain-specific languages, cryptography}
}

@article{10.1145/3391900,
author = {Lukyanov, Georgy and Mokhov, Andrey and Lechner, Jakob},
title = {Formal Verification of Spacecraft Control Programs},
year = {2020},
issue_date = {September 2020},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {19},
number = {5},
issn = {1539-9087},
url = {https://doi.org/10.1145/3391900},
doi = {10.1145/3391900},
abstract = {Verification of correctness of control programs is an essential task in the development of space electronics; it is difficult and typically outweighs design and programming tasks in terms of development hours. This article presents a verification approach designed to help spacecraft engineers reduce the effort required for formal verification of low-level control programs executed on custom hardware.The verification approach is demonstrated on an industrial case study. We present a REDuced instruction set for Fixed-point and INteger arithmetic (REDFIN), a processing core used in space missions, and its formal semantics expressed using the proposed metalanguage for state transformers, followed by examples of verification of simple control programs.},
journal = {ACM Trans. Embed. Comput. Syst.},
month = {oct},
articleno = {37},
numpages = {18},
keywords = {instruction set architecture, Formal verification, domain-specific languages, functional programming}
}