links.html

---
layout: default
title: HACS – Projects & Links
date: 2019-06-04
---

<p>
Please find below a non-comprehensive list of links to projects,
tools, and libraries that are relevant to HACS. Many of these projects
are with involvement of HACS participants; some grew out of
collaborations that started through the HACS workshop.
<p>
<!-- Please email us if you would like your project to be listed here.-->

<h3>Formally verified crypto</h3>

<ul>
  <li>
    <a href="https://github.com/bshvass/by-inversion">by-inversion</a>:
    Formalization of a prime field inversion algorithm by Bernstein and Yang
  </li>

  <li>
    <a href="https://github.com/mit-plv/fiat-crypto/">Fiat-Crypto</a>: 
    automatic derivation of fast field arithmatic code from specifications in Coq
  </li>

  <li>
    <a href="https://github.com/project-everest/hacl-star">HACL&ast;</a>: 
    a verified cryptographic library in F&ast; including verified assembly code from Vale
  </li>

  <li>
    <a href="https://github.com/GaloisInc/hacrypto">hacrypto</a>: 
    verified crypto primitives using SAW/Cryptol
  </li>

  <li>
    <a href="https://jasmin-lang.github.io/">Jasmin</a>: 
    verified assembly implementations of crypto primitives
  </li>

  <li>
    <a href="https://medium.com/blockstream/a-formal-proof-of-safegcd-bounds-695e1735a348">
      A Formal Proof of safegcd Bounds</a>
  </li>

  <li>
    <a href="https://github.com/project-everest/hacl-star/tree/master/vale">ValeCrypto</a>: 
    formally verified high-performance cryptographic code in assembly language
  </li
>
<!--
  <li>
    <a href="https://github.com/benlaurie/openssl/tree/saw/proof">WIP: applying SAW to OpenSSL</a>
  </li>
-->
</ul>

<h3>Other verification projects</h3>
<ul>
  <li>
    <a href="http://flint.cs.yale.edu/certikos/">CertiKOS</a>: 
    kernel with clean-slate design with end-to-end guarantees on extensibility, security, and resilience
  </li>
  <li>
    <a href="http://compcert.inria.fr/">CompCert</a> A verified C compiler, written in Coq 
  </li>
  <li>
    <a href="https://sel4.systems/">seL4</a>: 
    an L4 kernel verified with Isabelle/HOL
  </li>
  <li>
    <a href="https://mitls.org/">miTLS</a>: 
    a verified reference implementation of TLS
  </li>

  <li>
    <a href="http://deepspec.org/">DeepSpec</a>:
    specification and verification of full functional correctness of software and hardware
  </li>

  <li>
    <a href="https://project-everest.github.io/">Project Everest</a>:
    verified end-to-end secure transport
  </li>

  <li>
    <a href="https://plv.mpi-sws.org/rustbelt/">RustBelt</a>:
    Logical Foundations for the Future of Safe Systems Programming
  </li>
</ul>


<h3>Tools for verification</h3>

<ul>
  <li>
    <a href="https://autognp.github.io">AutoG&amp;P</a>: tool for performing highly automated game-hopping proofs for
    pairing-based cryptographic primitives
  </li>

  <li>
    <a href="https://github.com/binsec/haunted">Binsec/Haunted</a>: 
    A binary-level analyzer to detect Spectre attacks.
  </li>

  <li>
    <a href="https://people.cs.rutgers.edu/~sn349/papers/casm-verify-cgo-2019.pdf">CASM-verify</a>:
    Automatic Equivalence Checking for AssemblyImplementations of Cryptography Libraries
  </li>

  <li>
    <a href="https://github.com/diffblue/cbmc">CBMC</a>: a bounded model checker for C and Java
  </li>

  <li>
    <a href="http://compcert.inria.fr/">CompCert</a> A verified C compiler, written in Coq 
  </li>

  <li>
    The <a href="https://coq.inria.fr/">Coq</a> Proof Assistant<br>
  </li>

  <li>
    <a href="https://github.com/GaloisInc/crucible">Crucible</a>: 
    a language-agnostic library for performing forward symbolic execution of imperative progams
  </li>

  <li>
    <a href="https://www.isa-afp.org/entries/CryptHOL.html">CryptHOL</a>:
    A framework for formalising cryptographic arguments in Isabelle/HOL;
    see also <a href="https://eprint.iacr.org/2018/941">ePrint 2018/941</a>
  </li>

  <li>
    <a href="http://cryptol.net/">Cryptol</a>: 
    a domain-specific language for specifying cryptographic algorithms
  </li>

  <li>
    <a href="https://github.com/fmlab-iis/cryptoline">Cryptoline</a>: 
    verification of low-level implementations of mathematical constructs
  </li>

  <li>
    <a href="http://cryptoverif.inria.fr">CryptoVerif</a>:
    cryptographic protocol verifier in the computational model
  </li>

  <li>
    <a href="https://www.easycrypt.info/trac/">EasyCrypt</a>: 
    a toolset for reasoning about relational properties of
    probabilistic computations with adversarial code
  </li>

  <li>
    <a href="https://github.com/easyuc/EasyUC">EasyUC</a>:
    Experiments with Universal Composability in EasyCrypt
  </li>

  <li>
    <a href="http://entroposcope.verifythis.org">Entroposcope</a>: 
    a tool for finding entropy loss bugs in PRNGs
  </li>

  <li>
    <a href="https://www.fstar-lang.org/">F&ast;</a>: 
    an ML-like language with a type system for program verification
  </li>

  <li>
    <a href="https://github.com/mit-plv/fiat-crypto/">Fiat Crypto</a>: 
    automatic derivation of fast crypto-primitive code (for now just ECC) from specifications in Coq, 
    generating proofs along the way 
  </li>

  <li>
    <a href="http://frama-c.com/">Frama-C</a>: 
    an extensible and collaborative platform dedicated to source-code analysis of C software
  </li>

  <li>
    <a href="http://gfverif.cryptojedi.org">gfverif</a>: 
    fast and easy verification of finite-field arithmetic
  </li>

  <li>
    <a href="https://github.com/HACS-workshop/hacspec">hacspec</a>: 
    a language for specifying crypto
  </li>

  <li>
    <a href="http://ivorylang.org/">Ivory</a>: 
    an eDSL for safe systems programming. You can think of Ivory as a safer C, embedded in Haskell
  </li>

  <li>
    <a href="https://jasmin-lang.github.io/">Jasmin</a>: 
    high-speed and high-assurance cryptographic software in assembly
  </li>

  <li>
    <a href="http://plv.csail.mit.edu/kami/">Kami</a>: 
    tool for verified hardware design (ISA-&gt;RTL)
  </li>

  <li>
    <a href="http://www.key-project.org/">KeY</a>: 
    a deductive verifier of functional correctness of Java programs (wrt properties annotated in JML)
  </li>

  <li>
    <a href="https://github.com/FStarLang/kremlin">Kremlin</a>: 
    translate a subset of F&ast; to C
  </li>

  <li>
  <a href="https://ranjitjhala.github.io/static/fact_dsl.pdf">FaCT</a>:
    A DSL for timing-sensitive computation
  </li>

  <li>
    <a href="https://secpriv.wien/horst/">HoRSt</a>:
     Horn clause based sound static analysis
  </li>

  <li>
    <a href="http://proverif.inria.fr">ProVerif</a>:
    automatic cryptographic protocol verifier in the formal (Dolev-Yao) model
  </li>

  <li>
    <a href="https://github.com/dominique-unruh/qrhl-tool">qrhl-tool</a>: 
    Proof assistant for qRHL</a>
  </li>

  <li>
    <a href="https://plv.mpi-sws.org/refinedc/">RefinedC</a>:
    Automating the Foundational Verification of C Code with Refined Ownership Types
  </li>

  <li>
    <a href="https://medium.com/blockstream/a-formal-proof-of-safegcd-bounds-695e1735a348">
      Rust verification tools</a>
  </li>

  <li>
    <a href="https://saw.galois.com/">Software Analysis Workbench (SAW)</a>
  </li>

  <li>
    <a href="https://tamarin-prover.github.io/">Tamarin</a>:
    security protocol verification tool that supports both falsification and unbounded verification in the symbolic model.
  </li>

  <li>
    <a href="https://github.com/easyuc/EasyUC/tree/master/uc-dsl">UC-DSL</a>:
    UC Domain Specific Language
  </li>

  <li>
    <a href="https://github.com/project-everest/vale">Vale</a>: 
    Verified Assembly Language for Everest
  </li>

  <li>
    <a href="https://github.com/verifast/verifast/">VeriFast</a>: 
    a verifier for single-threaded and multithreaded C and Java programs 
    annotated with preconditions and postconditions written in separation logic
  </li>

  <li>
    <a href="https://verifpal.com/">Verifpal</a>:
     a protocol analyzer and verifier with a focus on real-world protocols and ease of use
  </li>

  <li>
    <a href="http://deepspec.org/research/VST/">Verified Software Toolchain (VST)</a>: 
    software toolchain that uses static analyzers and proof assistants to verify software
  </li>

  <li>
    <a href="https://www.easycrypt.info/trac/wiki/ZooCrypt">ZooCrypt</a>: 
    fully automated analysis of padding-based encryption
  </li>
</ul>


<h3>Fuzzing and testing tools</h3>

<ul>
  <li>
    <a href="https://github.com/google/AFL">AFL</a>: 
    american fuzzy lop
  </li>

  <li>
    <a href="https://github.com/guidovranken/cryptofuzz">Cryptofuzz</a>: 
    Differential cryptography fuzzing
  </li>

  <li>
    <a href="http://libfuzzer.info">libFuzzer</a>: 
    a fuzzer
  </li>

  <li>
    <a href="https://github.com/google/oss-fuzz">OSS-Fuzz</a>: 
    fuzzing service for open-source software
  </li>

  <li>
    <a href="https://github.com/google/wycheproof">Wycheproof</a>: 
    testing crypto libraries against known attacks
  </li>
</ul>

<h3>Other HACS-related projects</h3>

<ul>
  <li>
    <a href="https://opentitan.org/">OpenTitan</a>:
    Open source project building a transparent, high-quality reference design and integration guidelines for silicon root of trust (RoT) chips
  </li>

  <li>
    <a href="https://www.scarv.org/">SCARV</a>:
    Side-channel security for RISC-V
  </li>

  <li>
    <a href="https://github.com/ElementsProject/simplicity">Simplicity</a>: 
    A blockchain programming language designed as an alternative to Bitcoin script
  </li>
</ul>

<!--
<h3>Reading material</h3>

<ul>
  <li>
    <a href="http://formal.iti.kit.edu/~klebanov/pubs/libgcrypt-cve-2016-6313.pdf">
      Entropy Loss and Output Predictability in the Libgcrypt PRNG</a>
  </li>

  <li>
    <a href="https://blog.fuzzing-project.org/51-Fun-with-Bignums-Crashing-MatrixSSL-and-more.html">
      Fun with Bignums: Crashing MatrixSSL and more</a>
  </li>

  <li>
    <a href="http://www.cs.princeton.edu/~appel/papers/modsec.pdf">
      Modular Verification for Computer Security</a>
  </li>

  <li>
    <a href="http://formal.iti.kit.edu/~klebanov/pubs/ccs2016.pdf">
      Practical Detection of Entropy Loss in Pseudo-Random Number Generators</a>
  </li>

  <li>
    <a href="http://www.cs.princeton.edu/~appel/papers/verif-sha-2.pdf">
      Second Edition: Verification of a Cryptographic Primitive: SHA-256</a>
  </li>

  <li><a href="http://www.cs.princeton.edu/~appel/papers/verified-hmac.pdf">Verified Correctness and Security of OpenSSL HMAC</a>, 
    by Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. In 24th USENIX Security Symposium, 
    pages 207&ndash;221, August 2015
  </li>

  <li>
    <a href="https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/">Verifying s2n HMAC with SAW</a>
  </li>

  <li>
    <a href="https://www.cis.upenn.edu/~bcpierce/sf/current/index.html">Software Foundations</a>, 
    by Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm
    Sjöberg, Brent Yorgey
  </li>

  <li>
    <a href="http://adam.chlipala.net/cpdt/">Certified Programming with Dependent Types</a> by Adam Chlipala
  </li>
</ul>

-->