search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
928 stars 81 forks source link

Floating point determinism #753

Open sorear opened 3 years ago

sorear commented 3 years ago

Currently, the floating point semantics of all CakeML ILs just delegates to machine_ieee, which uses a @ term to select a NaN to return in cases where that is the result. This makes the behavior of basic floating point operations dependent on the HOL model. While it is philosophically unsatisfactory for a physical value which is subjectable to experiment to not be model-theoretically absolute, it's not problematic for program verification: any statement you can prove about fp64 math is true for all models, including the model which agrees with ARM VFP semantics.

If native floats are added for any other architecture, this breaks down, as different architectures have different rules for NaN propagation, invalid float-to-int conversions, and probably other things. It would also be unsuitable for hardware verification, as hardware cannot simultaneously match all HOL models.

I believe we need to either pick a deterministic semantics for floating point and commit to emulating it on all platforms, or somehow make the semantics explicitly nondeterministic.

michael-roe commented 2 years ago

This might also be an issue for some security proofs.

Some people like to do confidentiality proofs that show the program doesn't learn any information it isn't supposed to have access to.

personally, I believe the integrity proofs about what a program can write to, but think the confidentiality proofs are nonsense. Real implementations are full of covert channels (say hello to Spectre and Meltdown) that mean the implementation lacks the confidentiality property even if you can prove it in the model. Note that CHERI does not rely on confidentiality - contents of capabilities are not required to be kept secret. This is by design.

Anyhow, the ways these confidentiality proofs work is that the cpu needs to be deterministic (and this can lead you to using a special build of the cpu hardware that has been specially designed to avoid potential covert channels).

unfortunately, as far as these proofs go, non-deterministic bits in nans look like a covert channel. How do you know that there isn't a Meltdown like cpu bug that relies on the attacker looking at payload bits in nans?

So, ok, you can make the hardware deterministic. RISC-V defines the payload bits, so you're good to go there, without needing to have a special CPU core with different Nan behaviour for high security environments. But to do the proofs, you need to reflect this in the model.

Summary: we may need to fix hol's ieee float model to be able to do security proofs of CPU's with floating poInt.

mn200 commented 1 year ago

The CakeML semantics could be made explicitly deterministic, without relying on weird properties of the HOL model, by having it use just one canonical NaN at the top level of the semantics. We'd then implement that design by making compiled code notice NaNs arising and then picking its one canonical NaN at the last possible point. (You might avoid excessive checks by letting internal, un-canonicalised NaNs propagate within nested computations.)