Skip to content
This repository has been archived by the owner on Jun 17, 2024. It is now read-only.

Cédric's notes

Jump to bottom
Jonathan Protzenko edited this page Oct 7, 2016 · 7 revisions

@channel Summary of our discussion on file names and code restructuring for low-level crypto (for now on the ⁠⁠⁠⁠fournet_aead⁠⁠⁠⁠ branch of F*). ⁠⁠⁠⁠FStar.Buffer⁠⁠⁠⁠ to be improved a bit, and extended with common type aliases:

type uint8_s = Seq.seq Uint8.t
type uint8_p = Buffer.buffer Uint8.t
type uint8_sl (l:nat) = s:uint8_s {Seq.length s = l}
type uint8_pl (l:nat) = b:uint8_p {Buffer.length b = l}

and similarly for uint32.t

⁠⁠⁠⁠Fstar.Buffer.Utils⁠⁠⁠⁠ to subsume ⁠⁠⁠⁠Crypto.Symmetric.Bytes⁠⁠⁠⁠, meant to include useful coding on top of buffers, such as conversion with various integers.

⁠⁠⁠⁠FStar.Buffer.Alloc⁠⁠⁠⁠ to isolate any Stack code that may implicitly allocate immutable stuff on the back-end heap, thereby escaping the Low*/Kremlin discipline. We need it for idealization, for testing, for ocaml apps such as miTLS. But we need to exclude it from concrete HACL*.

⁠⁠⁠⁠Crypto.Symmetric.Cipher⁠⁠⁠⁠ to replace ⁠⁠⁠⁠Crypto.Symmetric.BlockCipher⁠⁠⁠⁠ and multiplex between Chacha and 3 flavors or AES.

⁠⁠⁠⁠Crypto.Symmetric.PRF⁠⁠⁠⁠ to idealize it.

⁠⁠⁠⁠Crypto.Symmetric.MAC⁠⁠⁠⁠ to idealize and encode and multiplex between POLY1305 and GF128 (we may split it e.g. into ⁠⁠⁠⁠MAC⁠⁠⁠⁠ and ⁠⁠⁠⁠INT1CMA⁠⁠⁠⁠)

⁠⁠⁠⁠Crypto.AEAD⁠⁠⁠⁠ to replace ⁠⁠⁠⁠Crypto.AEAD.ChachaPoly1305.Ideal⁠⁠⁠⁠ and multiplex between Chacha20Poly1305, AES256_GCM, and possibly other combinations.

⁠⁠⁠⁠Crypto.AEAD.Test⁠⁠⁠⁠ to replace ⁠⁠⁠⁠Test⁠⁠⁠⁠ and do functionality testing (and similarly for the other files, moving test code from ML to F*)

We'll atomically implement those changes by the end of this week, unless someone objects. The plan is then to integrate those files into HACL* and adapt it accordingly, so that it can entirely replace ⁠⁠⁠⁠low-level/crypto⁠⁠⁠⁠. (edited)

Naming convention (to be implemented in both projects):

  • we have a ⁠⁠⁠⁠Flag.fsti⁠⁠⁠⁠ with e.g. an ⁠⁠⁠⁠assume val aes_prf: bool⁠⁠⁠⁠ for every game-based each crypto assumption we use in the whole development. That file also records constraints, reflecting the order of games. For instance ⁠⁠⁠⁠assume val poly1305_mac1 : b:bool { poly1305_mac1 => aes_prf }⁠⁠⁠⁠.
  • we typecheck once the whole development, hence guaranteeing that every valid combination of flags yields a well-type program. This justify that, as we switch a flag in accordance to a game-based assumption, the whole program is a valid adversary for that game.
  • we have a directory "real" that contains ⁠⁠⁠⁠Flag.fst⁠⁠⁠⁠ setting every boolean to false ⁠⁠⁠⁠inline let aes_prf = false⁠⁠⁠⁠. We use ⁠⁠⁠⁠--include real⁠⁠⁠⁠ whenever we extract the real implementation, either in kremlin or ocaml.
  • we could have others, although typing without revealing the flags seems good enough the (meta) game-based proof. TODO: write up relationship to ⁠⁠⁠⁠strong⁠⁠⁠⁠ booleans. Roughly, they are a way to document and aggregate crypto assumptions in the development.

protz [3:40 PM]
to make sure we can extract code and only dump the ideal case; either:

  • write ⁠⁠⁠⁠if ideal && authId i then⁠⁠⁠⁠ everywhere; manual inspection of ⁠⁠⁠⁠normalize.fs⁠⁠⁠⁠ revealed that boolean operators are indeed normalized (line 485 and after); or,
  • ⁠⁠⁠⁠assume val authId': id -> bool⁠⁠⁠⁠ followed by ⁠⁠⁠⁠inline let authId = ideal && authId'⁠⁠⁠⁠ @fournet mentioned he'd like to have a manual ⁠⁠⁠⁠normalize⁠⁠⁠⁠ operator to force normalizing a given term; also, a specification of what the normalizer normalizes would be helpful (edited)

fournet [11:43 AM]
@taramana, @adl @karthik @jk @santiago: @protz and I discussed how to represent immutable sequences of UInt8.t (and probably other machine integers) in F*, an important step to reconcile crypto and mitls. Some requirements:

  • replace bytes in miTLS
  • be coded/verified mostly in F*. For now this is a lot of unverified ocaml-specific code
  • provide at least their functionality; possibly with a major rewriting of miTLS once we figure out what the best API is.
  • replace seq UInt8.t in low-level/crypto
  • with a more efficient implementation (not just for specs)
  • with the same lemmas etc, ideally the same interface as seqs coded as lists.
  • be compatible with low*:
  • allocate flat arrays, not lists
  • take advantage of pointer arithmetic for splitting buffers, at least with Kremlin. (We may keep something like for buffers in ocaml.)
  • be refcounting-friendly (is it compatible with a value semantics in the front-end?)
  • be stack-allocable (tough, possibly only as a kremlin optimization).
  • provide conversions between mutable buffers and immutable array values. Possibly by using a frame to prepare a buffer, then turning it into a value in a variation of pop_frame.
    For now the ocaml implementation uses lists of strings (to defer concatenations), but I am not sure it is a good idea for low*. But we could use it for experiments, if it is a easy hack, implementing both the lists and strings of ocaml as leaky mallocs in kremlin. (edited)
Clone this wiki locally