sangel
Joined 10 years ago
Joined 10 years ago
They use TLA+ with TLC which model checks the write ahead log (a component of the system). But that only models the WAL protocol, not the actual Rust code and not the other 99% of the system.
Any formal verification is of course awesome to see though.
This is why tools like formal verification and symbolic analyses can help you establish that for all possible integers X, your function does the right thing (for some definition of “right”). You get this assurance without having to actually enumerate all X.
There are no obvious ways to improve on this work, so it is not a matter of engineering. We really do need another breakthrough result to get us closer to practicality.
We never built it into a product because we couldn't figure out a way to monetize it to pay for the servers.
But yes, you make less as a professor than you do in industry.
Key idea is the client issues a query that is independent of what they really want. This is the “offline” query. This query is linear (unavoidable) and the client gets some hints as a result
Then later, the client can issue one or more queries for elements they want and those queries can be sublinear in terms of computation. The client uses hints to make that happen.
Some papers on this are:
https://eprint.iacr.org/2019/1075.pdf
That said, yeah this hashing example is not zero knowledge because, among other things, the hash is not hiding.
I don’t see how you can call that good temperature.