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

[Jonathan Hoyland <[e-mail]>]

Hi Sampo,

I don't think we disagree on what is possible, but I'd like to emphasise
the value and importance of tooling.
Whilst it is totally possible to apply formal methods by hand there are two
huge issues.

First, humans are really bad at applying a set of rules with perfect
consistency thousands and thousands of times.
Our formal analysis of TLS 1.3 comes out to ~750,000 steps.
Is that doable by hand? Maybe
Is it doable without a single error? Probably not

Second, humans are really bad at checking that a set of rules has been
applied with perfect consistency thousands and thousands of times.
Manual proofs are basically uncheckable in the peer review system.
I once took two weeks to go through a 40 page proof someone had submitted.
I found 19 mistakes.
Other reviewers who didn't have time (or perhaps the inclination) to take
two weeks to validate someone else's proof would have had to simply accept
the proof at face value.

When I write about formal analysis (and in particular Tamarin) I'm talking
about tool-assisted formal analysis.
Specifically, it's not just about writing down a specification and some
properties, or even manually proving the spec has the properties, it's
about coming up with a machine checkable proof where it is easy for a human
to understand the proof's claim, and we can then rely on the machine to
check that the claim is true.

As you pointed out, FA is very complex in the general case, and so I think
it's unlikely that we will ever want to use one language to describe every
IETF protocol.
Something expressive enough to capture all possible protocols would likely
be so expressive that the problem is undecidable (as it is in the general
case).
Tamarin is one of the most powerful tools available, and even though there
are some things it can't capture efficiently, it's already only
semi-decidable.
My goal would be to come up with a small stable of domain specific
languages with good tooling that can efficiently make and check proofs for
the protocols we care most about.
Trying to get to one-language-to-rule-them-all seems like a very arbitrary
and not especially useful goal.

With respect to the language the code is written in, unfortunately it
matters a lot, even if in theory it doesn't need to.
Only a tiny handful of languages have the tooling for proving functional
correctness, let alone the tooling necessary to prove things like
side-channel resistance.
Whilst in theory you can prove code is correct entirely manually it's both
hugely difficult and highly error prone.
With F# in particular you can write preconditions and invariants everywhere
if you have a mind to; I was including correctness as a key property for
proof of security.

Knowing what code means logically, and ascertaining its validity are again,
possible by hand, but even if you can check the code is correct, you can't
easily convince someone else of that.
They effectively have to know and trust that you did the proof with
sufficient care and attention, and that you didn't miss some edge case, etc.
With good tooling they only have to trust the tool, and it's much easier to
check a tool for bugs than a person's brain.

Regards,

Jonathan



On Mon, 5 Dec 2022 at 04:18, Sampo Syreeni <[e-mail]> wrote:

> 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] <http://decoy.iki.fi/front+358-40-3751464>, 025E D175
> ABE5 027C 9494 EEB0 E090 8BA9 0509 85C2
>