search

project-everest / mitls-fstar

Verified implementation of TLS 1.3 in F*
https://www.mitls.org
Other
173 stars 16 forks source link

EXT vs ML effect mismatch in Platform.Tcp.recv #92

Open BarryBo opened 8 years ago

BarryBo commented 8 years ago

See .fstar/ucontrib/Platform/fst/Platform.Tcp.fst: "assume val recv: networkStream -> max:nat -> EXT (optResult string (b:bytes {length b <= max}))"

The underlying ML implementation does not actually meet the EXT effect requirements, as it does a string substring operation, and that may throw an exception. By code inspection, the substring operation cannot be passed incorrect arguments in this case, so the exception should never be thrown, but there is no ability to prove that through the ML code.

I caught this when re-implementing TCP in F* instead of ML. The issue is non-blocking, as I have a workaround, but I feel it should be tracked, in case a proof or general correctness depends on an ML call being truly EXT.

BarryBo commented 6 years ago

Is this still an issue? If so, it probably makes sense to move into the F* issue tracker, and be prioritized appropriately.

nikswamy commented 6 years ago

The result type is an optResult. I would have expected the implementation to do a dynamic test on the length of the substring and return the Error case of optResult if the test fails.

But maybe that dynamic test is not possible in this context?

BarryBo commented 6 years ago

I think this problem is that the effect declared is EXT, but the actual implementation has ML effect (it can throw). I hit this long ago, when I was writing an alternative API to Platform.Tcp for miTLS, in F, and couldn't use the EXT effect in my code because I got caught by the F compiler.