Stream: Coq users

Topic: using VST to verify commercial code


view this post on Zulip Quinn (Jan 10 2022 at 15:03):

has anyone used vst in production? any tips about navigating the compcert licensing in order to do so?

view this post on Zulip Théo Zimmermann (Jan 10 2022 at 15:12):

Not me, but from what I understood, beyond learning, there isn't much that you can do in production without buying a CompCert license.

view this post on Zulip Alix Trieu (Jan 10 2022 at 15:14):

Footnote 2 of this paper says that there seems to be industrial users of VST https://www.cs.princeton.edu/~appel/papers/ecosystem.pdf I don't know anything apart from that.

view this post on Zulip Karl Palmskog (Jan 10 2022 at 15:14):

some caveats here, in particular regarding clightgen: https://github.com/palmskog/coq-program-verification-template#generating-clight-for-coq

view this post on Zulip Michael Soegtrop (Jan 10 2022 at 16:33):

You need to buy a license for Clightgen from AbsInt, but not for CompCert. Clightgen is typically licensed on a per project basis and these project based are not expensive (< 1 engineer man month).

For evaluating purposes - that is for checking if you actually can do what you want - you can use Clightgen based on the evaluation terms. As far as I can tell use for code which is intended for production but not yet used in production is fine, but I would recommend to discuss with AbsInt what they deem to be evaluation.

view this post on Zulip Karl Palmskog (Jan 10 2022 at 16:39):

on the other hand, if you license clightgen and not ccomp, then you will have a "trust gap" between the code you verify and the code you compile

view this post on Zulip Karl Palmskog (Jan 10 2022 at 16:40):

@Michael Soegtrop is there actually any realistic workflow right now where one can compile the code generated by clightgen using CompCert, and not the pre-clightgen code?

view this post on Zulip Michael Soegtrop (Jan 10 2022 at 16:40):

Well yes, but IMHO clightgen + VST is the first step and CompCert the second. I think if you can prove to your management that you can wrangle VST, they will give you the money for CompCert as well.

view this post on Zulip Karl Palmskog (Jan 10 2022 at 16:43):

yeah a clightgen license should allow one to do anything with VST without worry (since VST is not compiling anything)

view this post on Zulip Michael Soegtrop (Jan 10 2022 at 16:43):

@Karl Palmskog : as far as I know not. IMHO it would also make sense to not use extracted OCaml CompCert, but to run it in Coq - it should be fast enough for "final builds".

view this post on Zulip Karl Palmskog (Jan 10 2022 at 16:45):

sure, then you avoid trusting the runtime system and linking and so on, but the CakeML experience shows that ITP-hosted compilation tends to be really slow (CakeML bootstrapping takes a full day!). Maybe if it could be run with native compilation inside Coq

view this post on Zulip Michael Soegtrop (Jan 10 2022 at 16:45):

Well native compilation also uses the OCaml system, doesn't it?

view this post on Zulip Karl Palmskog (Jan 10 2022 at 16:46):

well, at least in a more predictable way than ccomp, right?

view this post on Zulip Michael Soegtrop (Jan 10 2022 at 16:48):

But I would think VM compute might be fast enough - I am usually more impressed by what it can do rather than the other way around. And for final production builds it doesn't matter much if it takes a few hours and ccomp now supports separate compilation.

view this post on Zulip Michael Soegtrop (Jan 10 2022 at 16:49):

It might be faster than checking the VST proofs ...

view this post on Zulip Karl Palmskog (Jan 10 2022 at 16:49):

one might say: we have practically no hope of verifying OCaml and its runtime system anytime soon, but vm_compute and native_compute might become within reach (compare CertiCoq)

view this post on Zulip Michael Soegtrop (Jan 10 2022 at 16:50):

yes, this is true.

view this post on Zulip Karl Palmskog (Jan 10 2022 at 16:52):

but anyway, getting code into VST and specifying it and verifying it is such a large part of obtaining the verified program, that the final compilation is arguably a minor quibble

view this post on Zulip Karl Palmskog (Jan 10 2022 at 17:01):

to verify native_compute, one could probably go for translation validation...

view this post on Zulip Bas Spitters (Jan 11 2022 at 17:17):

There's a nice overview paper on using compcert in a nuclear powerplant. Hopefully shouldn't be too hard to find.

view this post on Zulip Alexander Gryzlov (Jan 11 2022 at 18:28):

I guess this one https://www.absint.com/mtu_fh.htm ?


Last updated: Jan 27 2023 at 01:03 UTC