Post #1546534

@regehr @dpiponi The team next to mine in my last job was adopting EverCrypt. EverCrypt is a formally verified set of crypto libraries. They were proven to be memory safe. The temporal safety proof obligation was expressed as ‘no memory is accessed after it is freed’. This was proven to hold. Running it in an SGX enclave with 32 MiB of total available RAM rapidly showed how it had been achieved: no memory was ever freed. Fixing the code was fairly simple, fixing the proofs was much harder.