Digging into the F* source code¶
Most users will only ever want to obtain the C or assembly implementations of various crypto algorithms, but expert users may want to look at or modify the F* sources.
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.
It is almost always a good idea to look at F* interface files (
than implementations (
.fst). These typically have the most up-to-date
comments, as well as a wealth of information regarding preconditions, such as
length of arrays, disjointness, etc. that C clients MUST obey.
There are some general rules for mapping a
.h file to an
- Files that start with
Hacl_are found in the
code/subdirectory; for instance,
.hfiles may combine multiple source F* files (known as “bundling”); for instance,
Hacl_Hash.hcombines all files from
- Files that start with
Lib_are found in the
lib/cdirectory; 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
In case finding a particular declaration is important: if a function is named
Foo_Bar_baz, then you want to find
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
definition lists all the properties that must hold for a call to
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.lengthdenotes the length of a C array; we see that
iv_lenmust be the length of the pointer
iv, and that this length must be strictly positive
B.disjointstate that memory chunks shall not overlap; we see that no overlap is tolerated between
tag, but that
ciphermust be either the same pointer, or non-overlapping memory allocations
all_livemeans 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
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.