Re: [irtf-discuss] [115attendees] Usable formal methods side meeting at IETF 115

[Sampo Syreeni <[e-mail]>]

On 2022-11-08, Jonathan Hoyland wrote:

> A common method for formally analysing protocols is to express them in 
> some kind of rewriting system, and then check that the system has some 
> LTL property.

That doesn't really answer the question, though. Because *anything* at 
*all*, *any* computation can be expressed as a rewritng system. Just 
look at lambda calculus and the Church-Turing thesis.

It's not about what is *possible* or how it's mathematically expressed. 
It's about how it's *structured* for *human* consumpition.

> For example Tamarin is a software tool that uses multi-set rewriting 
> to express protocols, [...]

You said it yourself, just now. It's about how to structure your logic. 
In this case using multilsets.

> [...] and a fragment of first order logic to analyse them. It was used 
> to analyse, for example, TLS 1.3, and find mistakes in some of the 
> drafts.

"A fragment", yes. Because the whole deal might be intractable.

Also, if you want to formalize and analyze protocols, you most likely 
need to apply temporal/modal logics. Quite beyond the kinds of logics 
uhnderpinning e.g. free or even tagged-tree or heaven forbid attribute 
grammars. (Which, by the way, under their most general semantics, 
approach in their generality the Church-Turing bound.)

> Formal verification looks at code and checks that it implements some 
> spec.

So it it's spec, duh. So the sages of the field defined it, from the 
beginning.

> One technique for formally verifying protocols is to write the code in 
> some restricted programming language, and then use tools to check that 
> that code has some property.

It doesn't matter which language the code is written in. The only thing 
which matters is whether we know what the code *means*, *logically*, 
and so whether we can ascertain its validity.


> For example you can use EasyCrypt and Jasmin to write low-level crypto 
> code, and verify its security properties, including checking for 
> things like side channel safety. Alternatively you can use F# with F7 
> to analyse code. There are formally verified implementations of things 
> from ChaChaPoly to TLS 1.3. Formally verified code is deployed in 
> projects such as Chrome and Firefox.

True, but we could do even better. Why not just write preconditions and 
invariants everywhere? All over the code? So that theorem provers could 
make sure our code is correct throughout? Notify the coder if something 
was amiss?

That's not too difficult to do, and would definitely cut a bug or two 
every here and then.

> The idea of generating prose from a specification is interesting, but 
> not something I have seen any work on so far.

I've seen some work around these parts already. Even GPT-3 has been 
applied to this problem. However, that work only solves the problem of 
generating prose from a specification, somehow intuitionistically. It 
does not solve the problem of generating a proper, valid and sound 
logical document, from a description. "You can't be sure about what 
you're reading."
-- 
Sampo Syreeni, aka decoy - [e-mail], http://decoy.iki.fi/front
[phone], 025E D175 ABE5 027C 9494 EEB0 E090 8BA9 0509 85C2