2 ms·
This is an insightful example because it's kind of "wrong at the higher level". It follows the spec. Every formal verification method will confirm that. It's t
by praptak 3y ago
This is an insightful example because it's kind of "wrong at the higher level". It follows the spec. Every formal verification method will confirm that.
It's the spec that is wrong. Obviously I mean the "replaces digits with zeros" spec, which does not follow the "doesn't leak data" spec.
The root problem is that "doesn't leak data" is hard to define in a way that can be formally verified. This is a fundamental problem, not an incidental one.
- tgv 3y agoIndeed. It looks as if it could have been written in Rust and Spark. > doesn't leak data This requirement was translated into "zero a rectangle" without considering every format. Careful analysis is clearly possible, it was done by the author of that code, but understanding the full implications of code is hard.