Reference. Galápagos: Developing Verified Low Level Cryptography on Heterogeneous Hardwares

Cite

Cite as @zhou-2023-galapagos (helia, typst) · \cite{zhou-2023-galapagos} (LaTeX)
BibTeX
bibtex · 1 line
@inproceedings{zhou-2023-galapagos, series={CCS ’23}, title={Galápagos: Developing Verified Low Level Cryptography on Heterogeneous Hardwares}, url={http://dx.doi.org/10.1145/3576915.3616603}, DOI={10.1145/3576915.3616603}, booktitle={Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security}, publisher={ACM}, author={Zhou, Yi and Gibson, Sydney and Cai, Sarah and Winchell, Menucha and Parno, Bryan}, year={2023}, month=Nov, pages={2113–2127}, collection={CCS ’23} }
hayagriva YAML (typst)
yaml · 21 lines
zhou-2023-galapagos:
  type: article
  title: 'Galápagos: Developing Verified Low Level Cryptography on Heterogeneous Hardwares'
  author:
  - Zhou, Yi
  - Gibson, Sydney
  - Cai, Sarah
  - Winchell, Menucha
  - Parno, Bryan
  date: 2023-11
  page-range: 2113-2127
  url: http://dx.doi.org/10.1145/3576915.3616603
  serial-number:
    doi: 10.1145/3576915.3616603
  parent:
    type: proceedings
    title: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
    publisher: ACM
    parent:
      type: proceedings
      title: CCS ’23
Cited by (1)

Verus: A Practical Foundation for Systems Verification lattuada-2024-verus

DOI
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.
PDF · DOI · pldb

IronFleet: proving practical distributed systems correct hawblitzel-2015-ironfleet

DOI

Verified Software Toolchain appel_vst_2011

Bootstrapping Trust in Modern Computers parno-2011-bootstrapping

DOI

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.
PDF · DOI · pldb
External (60)
zhou-2023-galapagos reference entries/refs/zhou-2023-galapagos/zhou-2023-galapagos.hel