Digging into the F* source code¶

Finding the F* source¶

Looking at the original F* files allows the user to identify any preconditions or remarks that may have been left in there (work is in progress to forward source-level comments to the generated C code). Indeed, our C code is generated; as such, some information is lost in the translation process.

There are some general rules for mapping a .h file to an .fsti file.

• Files that start with Hacl_ are found in the code/ subdirectory; for instance, Hacl_HKDF.h comes from code/hkdf/Hacl.HKDF.fsti. Some .h files may combine multiple source F* files (known as “bundling”); for instance, Hacl_Hash.h combines all files from code/hash along with code/sha3.
• Files that start with Lib_ are found in the lib/c directory; they are hand-written and are assumed to faithfully implement a given F* signature; these should be carefully reviewed before any integration. In particular, for zero-ing out memory and randomness, we only have basic implementations; pull requests welcome.
• Files that start with EverCrypt_ are found in the providers/evercrypt directory.

In case finding a particular declaration is important: if a function is named Foo_Bar_baz, then you want to find Foo.Bar.fst{,i}.

Reading F* preconditions¶

It is important to be able to read some amount of F* code in order to successfully use an API. For instance, looking at AEAD encryption, there are various pre-conditions that client must satisfy, related to liveness, disjointness and array lengths. We expect unverified C clients to abide by these preconditions; otherwise, none of our verification guarantees hold! As such, it is up to the user to read the preconditions and make sure they are satisfied.

As an example, consider EverCrypt_AEAD_encrypt. Per the section above, we look up providers/evercrypt/EverCrypt.AEAD.fsti. The encrypt_pre definition lists all the properties that must hold for a call to encrypt to be valid.

let encrypt_gen_pre (a: supported_alg)
  (iv:iv_p a)
  (iv_len: UInt32.t)
  (ad:ad_p a)
  (ad_len: UInt32.t)
  (plain: plain_p a)
  (plain_len: UInt32.t)
  (cipher: B.buffer uint8)
  (tag: B.buffer uint8)
  (h0: HS.mem)
=
  v iv_len = B.length iv /\ v iv_len > 0 /\
  v ad_len = B.length ad /\ v ad_len <= pow2 31 /\
  v plain_len = B.length plain /\ v plain_len <= max_length a /\
  B.length cipher = B.length plain /\
  B.length tag = tag_length a

let encrypt_live_disjoint_pre (a: supported_alg)
  (iv:iv_p a)
  (iv_len: UInt32.t)
  (ad:ad_p a)
  (ad_len: UInt32.t)
  (plain: plain_p a)
  (plain_len: UInt32.t)
  (cipher: B.buffer uint8)
  (tag: B.buffer uint8)
  (h0: HS.mem)
=
  MB.(all_live h0 [ buf iv; buf ad; buf plain; buf cipher; buf tag ]) /\
  (B.disjoint plain cipher \/ plain == cipher) /\
  B.disjoint cipher tag /\
  B.disjoint iv cipher /\ B.disjoint iv tag /\
  B.disjoint plain tag /\
  B.disjoint plain ad /\
  B.disjoint ad cipher /\ B.disjoint ad tag

let encrypt_pre (a: supported_alg)
  (s:B.pointer_or_null (state_s a))
  (iv:iv_p a)
  (iv_len: UInt32.t)
  (ad:ad_p a)
  (ad_len: UInt32.t)
  (plain: plain_p a)
  (plain_len: UInt32.t)
  (cipher: B.buffer uint8)
  (tag: B.buffer uint8)
  (h0: HS.mem)
=
  encrypt_gen_pre a iv iv_len ad ad_len plain plain_len cipher tag h0 /\ (
  not (B.g_is_null s) ==>
    invariant h0 s /\
    B.(loc_disjoint (footprint h0 s) (loc_buffer iv)) /\
    B.(loc_disjoint (footprint h0 s) (loc_buffer ad)) /\
    B.(loc_disjoint (footprint h0 s) (loc_buffer tag)) /\
    B.(loc_disjoint (footprint h0 s) (loc_buffer plain)) /\
    B.(loc_disjoint (footprint h0 s) (loc_buffer cipher)) /\
    encrypt_live_disjoint_pre a iv iv_len ad ad_len plain plain_len cipher tag h0)

Here are some examples:

• B.length denotes the length of a C array; we see that iv_len must be the length of the pointer iv, and that this length must be strictly positive
• loc_disjoint or B.disjoint state that memory chunks shall not overlap; we see that no overlap is tolerated between cipher and tag, but that plain and cipher must be either the same pointer, or non-overlapping memory allocations
• all_live means that all of the pointers in the list must be valid allocations that have not yet been freed

A few lines below, we see from the signature of encrypt that the only two possible errors are Success and InvalidKey.

Static vs. run-time checks¶

We sometimes perform additional run-time checks for violations of the API that are ruled out for verified clients; for instance, continuing with the encrypt example, we do perform a check at run-time for zero-length IVs, even though no F* client would be allowed to do that.

C clients should not rely on those details, since i) this is best-effort and we do not offer any guarantee as to which preconditions we check for and ii) the error that is returned is not captured in the post-condition, since it cannot happen for verified clients.