Open jumaffre opened 4 years ago
@protz this is about the non-null annotation on the memcpy
arguments, which clang reported some time ago. I thought you fixed this, but something about it doesn't seem to be working. A simple example is
let hash_copy #_ s src dst =
B.blit src 0ul dst 0ul s
in MerkleTree.Low.Datastructures.fst
, which extracts to
static void hash_copy(uint32_t s, uint8_t *src, uint8_t *dst)
{
memcpy(dst, src, s * sizeof (uint8_t));
}
where src/dst are allowed to be NULL
because of the definition of the hash
type:
type hash (#hsz:hash_size_t) = b:B.buffer uint8 { B.len b = hsz \/ B.g_is_null b }
So, I think this memcpy
needs to be guarded by a NULL
-check. Without the sanitizer, clang just calls memcpy, which happens to do the right thing even when the arguments are NULL
, but that's unspecified behaviour.
Hi Christoph,
There is a massive rewrite underway that fixes this. However, it's very labor-intensive, and many algorithms need to be rewritten to avoid the insertion of null-checks. Do you have time? We could use some help porting the EverCrypt layers and the hash/hmac/hkdf algorithms to avoid ugly C code.
Relevant Slack thread: https://everestexpedition.slack.com/archives/C4237009M/p1596467100365000
Thanks,
Jonathan
That's great, thanks for the pointer! I don't have a lot of time, but I'll definitely look at the Merkle tree code.
Same as hacl-star/hacl-star#327 (cross-referencing the two issues)
We recently turned on more sanitizer checks for CCF (i.e.
-fsanitize=undefined,address -fno-omit-frame-pointer -fno-sanitize-recover=all -fno-sanitize=function
). We've observed a runtime error after deserialising a Merkle tree and appending two hashes to it:A minimal repro is (using CCF's thin C++ wrapper around EverCrypt hash library):
Backtrace is:
At this point:
Please let me know if you need any additional detail on this. For now, we've added
MerkleTree.c
to our sanitizer blacklist.