package eqaf
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=67d1369c57c4d2d14a10d02632d45e355224abeb98aec08979c0bae5843092ee
sha512=7f75b5d5667e3605f8d95e2d6fda40953129033e6a342ee2c98ee4135c2428e1db87547971868605ab989374757c47c21c5397d4c3da578952d716826a156979
Description
This package provides an equal function on string in constanttime to avoid timingattack with crypto stuff.
Published: 26 Jun 2024
README
Eq(af)  Constant time equal function
This library implements various constant time algorithms, first and foremost the Eqaf.equal
equality testing function for string
.
While the test suite has a number of external dependencies, the library itself does not have any dependencies besides the OCaml standard library. This should make eqaf
small, selfcontained, and easy to integrate in your code.
The "constant time" provided by this library is constant in the sense that the time required to execute the functions does not depend on the values of the operands. The purpose is to help programmer shield their code from timingbased sidechannel attacks where an adversary tries to measure execution time to learn about the contents of the operands. They are not necessarily "constant time" in the sense that each invocation takes exactly the same amount of microseconds.
Constant time implementations are beneficial in many different applications; cryptographic libraries like digestif, but also practial code that deal with sensitive information (like passwords) benefit from constant time execution in select situations. A practical example of where this matters is the Lucky Thirteen attack against the TLS protocol, where a shortcircuiting comparison compromised the message encryption layer in many vulnerable implementations.
You can generate and view the documentation in a browser with:
dune build @doc
xdgopen ./_build/default/_doc/_html/index.html
Contents
We found that we often had to duplicate the constant time equal
function, and to avoid replication of code and ensure maintainability of the implementation, we decided to provide a little package which implements the equal
function on string
. Since then, we have added a number of other useful constant time implementations:
compare_be
andcompare_le
: can be used to compare integers (or actual strings) of any size in either bigendian or littleendian representation. Regular string comparison (e.g.String.compare
) is usually shortcircuiting, which results in an adversary being able to learn the contents of compared strings by timing repeated executions. If the lengths do not match, the semantics forcompare_be
follow those ofString.compare
, andcompare_le
those ofString.compare (reverse str)
.The
compare_be_with_len
andcompare_le_with_len
are similar, but does a constant time comparison of the lengths of the two strings and the~len
parameter. If the lengths do not match, an exception is thrown (which leaks the fact that the lengths did not match, but not the lengths or the contents of the input operands).
exists_uint8 : ?off > f:(int > bool) > string > bool
: implements the equivalent ofList.exists
onstring
, but executing in constant time with respect to the contents of the string and?off
. The user provides a callback function that is given each byte as an integer, and is responsible for ensuring this function also operates in constant time.find_uint8
: similar toexists_uint8
, but implementing the functionality ofList.find
: It returns the string index of the first match.divmod
: constant time division and modulo operations. The execution time of both operations in normal implementations are notoriously dependent on the operands. Theeqaf
implementation uses an algorithm ported fromSUPERCOP
.ascii_of_int32 : digits:int > int32 > string
: Turns theint32
argument into a fixedwidth (of length= digits
) leftpadded string containing the decimal representation, ex:ascii_of_int32 ~digits:4 123l
is"0123"
. Usually programming languages provide similar functionality (ex:Int32.to_string
), but are vulnerable to timing attacks since they rely on division. This implementation is similar, but usesEqaf.divmod
to mitigate side channels.lowercase_ascii
anduppercase_ascii
implement functionality equivalent to the identically named functions inStdlib.String
module, but without introducing a timing side channel.hex_of_string
: constanttime hex encoding. Normally hex encoding is implemented with either a table lookup or processor branches, both of which introduce side channels for an adversary to learn about the contents of the string being encoded. That can be a problem if an adversary can repeatedly trigger encoding of sensitive values in your application and measure the response time.string_of_hex
: constanttime hex decoding. Inverse ofhex_of_string
, but with support for decoding uppercase and lowercase letters alike.
This package, if cstruct
or basebigarray
is available, will make this equal
function for them too (as eqaf.cstruct
and eqaf.bigarray
).
A number of lowlevel primitives used by Eqaf
are also exposed to enable you to construct your own constant time implementations:
zero_if_not_zero : int > int
:(if n <> 0 then 0 else 1)
, or!n
in the C programming language.one_if_not_zero : int > int
:(if n <> 0 then 1 else 0)
, or!!n
in the C programming language.bool_of_int : int > bool
, likeone_if_not_zero
but cast tobool
int_of_bool : bool > int
, inverse ofbool_of_int
select_int : int > int > int > int
:select_int choose_b a b
is a constant time utility for branching, but always executing all the branches (to ensure constant time operation):let select_int choose_b a b = if choose_b = 0 then a else b
select_a_if_in_range : ~low:int > ~high:int > n:int > int > int > int
Similar toselect_int
, but checking for inclusion in a range rather than testing for zero  a CT version of:let select_a_if_in_range ~low ~high ~n a b = if low <= n && n <= high then a else b
Check tool
To ensure correctness, eqaf
ships with a test suite to measure the functions and comparing results both to the Stdlib
implementations and to executions of the same function with similar length/size input. The goal is to try to spot implementation weaknesses that rely on the values of the function operands.
The check tool will first attempt to calculate how many executions are required to get statistically sound numbers (sorting out random jitter from external factors like other programs executing on the computer).
Then, using linear regression, we compare the results and verify that we did not spot differences: the regression coefficient should be close to 0.0
.
You can test eqaf
with this:
$ dune exec check/check.exe
Q/A
Q How to update eqaf
implementation?
A eqaf
is fragile where the most important assumption is times needed to compute equal
. So eqaf
provides the check
tool but results from it can be disturb by sidechannel (like hypervisor). In a baremetal environment, check
strictly works and should return 0
.
Q eqaf
is slower than String.compare
, it's possible to optimize it?
A The final goal of eqaf
is to provide a safe equal function. Speed is clearly not what we want where we prefer to provide an implementation which does not leak informations like: where is the first byte which differs between a
and b
.
Q Which attack eqaf
prevents?
A eqaf
provide an equal function to avoid a timing attack. Most of equal or compare functions (like String.compare
) leave at the first byte which differs. A possible attack is to see how long we need to compare two values, like an user input and a password.
Logically, the longer this time is, the more user input is the password. So when we need to compare sensible values (like hashes), we should use something like eqaf
. The distribution provides an example of this attack:
$ dune exec attack/attack.exe
Random: [218;243;59;121;8;57;151;218;212;91;181;41;].
471cd8bc03992a31f8f0f0c55e9e477d
471cd8bc03992a31f8f0f0c55e9e477d
The first value is the hash, the second is what we found just by an introspection of time needed by our equal
function.
Q eqaf
provides only equal function on string
?
A The first implementation use string
, then, we copy/paste the code with bigarray
and provide it only if basebigarray
is available. Finally, we provide an equal
function for cstruct
only if this package is available.
So, it's not only about string
but for some others datastructures.
Q Why we need to do a linear regression to check assumptions on eqaf
?
A As we said, times are noisy by several sidecomputation (hypervisor, kernel, butterfly...). So, if we record two times how long we spend to compute equal
, we will have 2 different values  close each others but different.
So we need to have a bunch of samples and do an analyze on them to get an approximation. From that, we do 2 analyzes:
get the approximation where we compare 2 same values
get the approximation where we compare 2 different values
From these results, we need to do an other analyze on these approximations to see if they are close each others or not. In the case of eqaf
, it should be the case (and if it is, that means eqaf
does not leak a time information according inputs). In the case of String.compare
, we should have a big difference  and confirm expected behaviors.
Dev Dependencies (5)
Used by (13)

awa
>= "0.0.5"

callipyge
>= "0.2"

digestif
>= "0.7"
 eqafcstruct
 hacl_x25519

jose
>= "0.5.0"
 mec

miragecrypto
>= "1.0.0"
 miragecryptoec

miragecryptopk
>= "0.8.1"
 noise
 octezlibs
 octezmec
Conflicts
None