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. .. note:: It is almost always a good idea to look at F* interface files (``.fsti``) rather 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 ``.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-preconditions: 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. .. literalinclude:: ../providers/evercrypt/EverCrypt.AEAD.fsti :start-after: SNIPPET_START: encrypt_pre :end-before: SNIPPET_END: encrypt_pre 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.