Stream: Miscellaneous

Topic: IETF formal methods

Karl Palmskog (Dec 13 2022 at 09:17):

The IETF community has long used natural language to describe and specify protocols [...] In many ways this is clearly a successful approach. After all, the Internet exists as an interoperable, global, multi-vendor, network in large part due to the protocol standards the IETF develops.

https://csperkins.org/research/protocol-standards/2022-11-30-usable-formal-methods/

I guess since natural language specs didn't lead to complete disaster all the time, we'll have to keep doing them...

Bas Spitters (Dec 13 2022 at 12:45):

That's why we've been working on hacspec. It now has both a Coq and an SSProve backend.

Karl Palmskog (Dec 13 2022 at 13:53):

yeah I hope you can sell hacspec to IETF, but it's still a bit backwards to me (subset of unspecified language that outputs something well-specified)

Karl Palmskog (Dec 13 2022 at 13:56):

but I think they could have at least investigated: how much did all the ambiguity and misunderstandings due to natural lang specs actually cost? It seems like a low bar that they actually made some infrastructure work with it.

Bas Spitters (Dec 13 2022 at 15:42):

Hacspec has an independent operational semantics.

Karl Palmskog (Dec 13 2022 at 16:19):

but as I think we discussed before, the evolution of the semantics is likely going to be constrained, if not outright dictated, by whatever people check in to the Rust compiler repository on GitHub...

Karl Palmskog (Dec 13 2022 at 16:20):

or has anyone said: "Hacspec compatibility with Rust is not a high priority anymore"?

Paolo Giarrusso (Dec 13 2022 at 18:27):

Didn't IETF require multiple interoperable implementations, or was that another standard? That doesn't seem a plain "natural language" spec.
Also the link seems about the opposite of that quote since they are exploring more formal methods :grinning:

Karl Palmskog (Dec 13 2022 at 18:36):

from the minutes:

What are formal methods and why should IETFers care?

why should we care then if it’s all difficult?

Karl Palmskog (Dec 13 2022 at 18:39):

I think the chances of losing this game are overwhelming: whatever FM techniques you introduce or push for, they need to ensure positive ROI up front compared to whatever old methods you were using, that never had any cost/benefit analysis

Karl Palmskog (Dec 13 2022 at 18:49):

so essentially I believe they are setting up this whole "exploration" of FM to fail, and it will be a net negative for ITP and friends

Andres Erbsen (Dec 13 2022 at 19:39):

I have the same sense; I further think the skepticism we are reading here is a well-deserved consequence of the PL tradition of zealously pushing for design choices that are better seen as academic simplifications.

Karl Palmskog (Dec 13 2022 at 19:46):

for what it's worth I think the RISC-V formal specification competition/process was more of a step in the right direction for real-world formal methods (if we assume an ISA is a protocol, which it sort of is). At least, it ensured almost every popular ITP has a RISC-V ISA spec.

Karl Palmskog (Dec 13 2022 at 19:51):

and seemingly few unwilling people were subjected to PL design choices along the way

Karl Palmskog (Apr 16 2023 at 15:19):

saw this in the latest IETF formal methods research working group agenda/minutes from March 2023, regarding FM in general:

Why aren't these things already usable?

In my view, completely counterproductive adverse signaling to FM research community.

Paolo Giarrusso (Apr 17 2023 at 00:51):

Looking at the linked talk:

Verifying a mechanical proof is correct can take many hours and cost hundreds or even thousands of dollars.

Uhm?

A successful analysis may find no issues, i.e. that the protocol meets its goals.
Such results are very hard to get published because they are not “novel”, even though they may be valuable to the community.

What community is that?

Paolo Giarrusso (Apr 17 2023 at 00:57):

Naively, I'd also have expected at least lightweight formal methods like model checkers/TLA+ to be already relatively practical here?

Karl Palmskog (Apr 17 2023 at 07:50):

I think we have plenty of workshops/conferences that welcome FM case studies that "find no issues". Of course, the workshops are not tier 1, maybe not even tier 2, but it gets added to the scholarly record. Was surprised when even TACAS (1.5 tier?) "allowed" this.

Bas Spitters (Apr 18 2023 at 07:04):

I gave a presentation there, https://datatracker.ietf.org/meeting/116/materials/slides-116-ufmrg-foundational-end-to-end-verification-of-high-speed-cryptography-00
which I believe was well received. These people will not be writing Coq code, but they there's some adoption of hacspec.

Last updated: Jun 05 2023 at 09:01 UTC