Reference. Galápagos: Developing Verified Low Level Cryptography on Heterogeneous Hardwares
Cite
Cited by (1)
Verus: A Practical Foundation for Systems Verification lattuada-2024-verus
Cites 65 works (5 here)
With notes (5)
Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility lorch-2022-armada
Safely writing high-performance concurrent programs is notoriously difficult. To aid developers, we introduce Armada, a language and tool designed to formally verify such programs with relatively little effort. Via a C-like language and a small-step, state-machine-based semantics, Armadagives developers the flexibility to choose arbitrary memory layout and synchronization primitives so that they are never constrained in their pursuit of performance. To reduce developer effort, Armadaleverages SMT-powered automation and a library of powerful reasoning techniques, including rely-guarantee, TSO elimination, reduction, and pointer analysis. All of these techniques are proven sound, and Armadacan be soundly extended with additional strategies over time. Using Armada, we verify five concurrent case studies and show that we can achieve performance equivalent to that of unverified code.
IronFleet: proving practical distributed systems correct hawblitzel-2015-ironfleet
Verified Software Toolchain appel_vst_2011
Bootstrapping Trust in Modern Computers parno-2011-bootstrapping
Finding and Understanding Bugs in C Compilers yangFindingUnderstandingBugs
Compilers should be correct. To improve the quality of C compilers, we created Csmith, a randomized test-case generation tool, and spent three years using it to find compiler bugs. During this period we reported more than 325 previously unknown bugs to compiler developers. Every compiler we tested was found to crash and also to silently generate wrong code when presented with valid input. In this paper we present our compiler-testing tool and the results of our bug-hunting study. Our first contribution is to advance the state of the art in compiler testing. Unlike previous tools, Csmith generates programs that cover a large subset of C while avoiding the undefined and unspecified behaviors that would destroy its ability to automatically find wrong-code bugs. Our second contribution is a collection of qualitative and quantitative results about the bugs we have found in open-source C compilers.
External (60)
- Generating Programs for Polynomial Multiplication with Correctness Assurance (2023)
- veri-titan source code (software) (2023)
- Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU (2022)
- Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code (2022)
- NEON (Arm architecture documentation) (2022)
- Singular 4-3-0 - A computer algebra system for polynomial computations (2022)
- SoK: Computer-Aided Cryptography (2021)
- GoJournal: A verified, concurrent, crash-safe journaling system (2021)
- The Last Mile: High-Assurance and High-Speed Cryptographic Implementations (2020)
- Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language (2020)
- Verification of an Optimized NTT Algorithm (2020)
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs (2020)
- EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider (2020)
- Storage Systems are Distributed Systems (So Verify Them That Way!) (2020)
- HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms) (2020)
- ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS (2019)
- A complete formal semantics of x86-64 user-level instruction set architecture (2019)
- A verified, efficient embedding of a verifiable assembly language (2019)
- MobiSR: Efficient On-Device Super-Resolution through Heterogeneous Mobile Processors (2019)
- Post-Quantum Lattice-Based Cryptography Implementations (2019)
- Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises (2019)
- Verifying Arithmetic Assembly Programs in Cryptographic Primitives (2018)
- Jasmin: High-Assurance and High-Speed Cryptography (2017)
- Komodo: Using verification to disentangle secure-enclave hardware from software (2017)
- Falcon: Fast-Fourier Lattice-based Compact Signatures over NTRU (2017)
- In-Datacenter Performance Analysis of a Tensor Processing Unit (2017)
- DeepEye: Resource Efficient Local Execution of Multiple Deep Vision Models using Wearable Commodity Hardware (2017)
- The RISC-V Instruction Set Manual, Volume I: User-Level ISA, Document Version 2.2 (2017)
- Certified Verification of Algebraic Properties on Low-Level Mathematical Constructs in Cryptographic Programs (2017)
- HACL*: A Verified Modern Cryptographic Library (2017)
- Vale: Verifying High-Performance Cryptographic Assembly Code (2017)
- Verified Correctness and Security of mbedTLS HMAC-DRBG (2017)
- Constructing Semantic Models of Programs with the Software Analysis Workbench (2016)
- DeepX: A Software Accelerator for Low-Power Deep Learning Inference on Mobile Devices (2016)
- Speeding up the Number Theoretic Transform for Faster Ideal Lattice-Based Cryptography (2016)
- Trustworthy specifications of ARM® v8-A and v8-M system level architecture (2016)
- Automated Verification of Real-World Cryptographic Implementations (2016)
- Design of the RISC-V Instruction Set Architecture (2016)
- A Verified Extensible Library of Elliptic Curves (2016)
- Verification of a Cryptographic Primitive (2015)
- Efficient Ring-LWE Encryption on 8-Bit AVR Processors (2015)
- Verified Correctness and Security of OpenSSL HMAC (2015)
- Verifying Curve25519 Software (2014)
- Ironclad Apps: End-to-End Security via Automated Full-System Verification (2014)
- Verifying security invariants in ExpressOS (2013)
- Undefined behavior: what happened to my code? (2012)
- Intel Advanced Encryption Standard (AES) New Instructions Set (2012)
- Trusted Platform Module Main Specification, Version 1.2 Revision 116 (2011)
- Z3: An Efficient SMT Solver (2008)
- Automating Elementary Number-Theoretic Proofs Using Gröbner Bases (2007)
- Understanding and Evolving the ML Module System (2005)
- The Elliptic Curve Digital Signature Algorithm (ECDSA) (2001)
- MSP430 Family Mixed-signal Microcontroller Application Reports (2000)
- Generating Hard Instances of Lattice Problems (1996)
- Hilbert's Tenth Problem (1993)
- The Digital Distributed System Security Architecture (1989)
- Modular multiplication without trial division (1985)
- An algorithm for the machine calculation of complex Fourier series (1965)
- OTBN simulator (OpenTitan)
- The OpenTitan Project