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

[Jonathan Hoyland <[e-mail]>]

Hi All,

These are problems that have been discussed and worked on at length in both
academia and in the Security Area at the IETF.

You can break formal methods into two broad fields, formal analysis and
formal verification.

Formal analysis lets us look at a protocol design and check it has some
property we want.
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.
For example Tamarin <https://tamarin-prover.github.io/> is a software tool
that uses multi-set rewriting to express protocols, and a fragment of first
order logic to analyse them.
It was used to analyse, for example, *TLS 1.3*
<https://github.com/tls13tamarin/TLS13Tamarin>, and find mistakes in some
of the drafts <https://ieeexplore.ieee.org/abstract/document/7546518>.

Formal verification looks at code and checks that it implements some spec.
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.
For example you can use EasyCrypt <https://github.com/EasyCrypt/easycrypt/>
and Jasmin <https://github.com/jasmin-lang/jasmin/wiki> 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
<https://www.microsoft.com/en-us/research/project/f7-refinement-types-for-f/>
to analyse code.
There are formally verified implementations of things from ChaChaPoly
<https://github.com/EasyCrypt/easycrypt/tree/main/examples/ChaChaPoly> to TLS
1.3 <https://mitls.org/>.
Formally verified code is deployed in projects such as Chrome
<https://boringssl.googlesource.com/boringssl/+/refs/heads/master/third_party/fiat/>
and Firefox
<https://blog.mozilla.org/security/2020/07/06/performance-improvements-via-formally-verified-cryptography-in-firefox/>
.

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

Regards,

Jonathan

On Tue, 8 Nov 2022 at 07:18, Buday Gergely <buday.gergely.istvan=
[e-mail]> wrote:

> Hi Sampo,
>
> you wrote:
>
> 11/7/2022 10:06 PM keltezéssel, Sampo Syreeni írta:
> > I think English should augment formal specifications as it could
> > ignite debate whether the formalisation is correct and unambigous.
> >
> > Here I'd go more with the literal programming idea, and coloring your
> > statements with comments. Because if you really formalized your
> > protocol fully, so that the formal description really is whole and
> > binding, there is no need for debate. It just is or isn't valid.
>
> Formal verification can check whether a system conforms a specification.
> But there's always a question whether the specification conforms reality.
>
> You can prove theorems about your definitions with a theorem prover, but
> are your definitions right? This is another type of code review that
> protocol experts should do.
>
> >
> > As such English (why not other languages) simply serve to explain to a
> > human, what the intended semantics of the protocol and its data
> > formats are meant to be.
>
> Formal logic does not stand in itself, there are always thoughts about
> the protocol, system etc. that should be expressed in plain English to
> ease understanding. At all, for many formal methods practitioners, the
> main goal of formal verification is to better understand our designs,
> let the computer do the "trivial" stuff.
>
> - Gergely
>
> --
> 115attendees mailing list
> [e-mail]
> https://www.ietf.org/mailman/listinfo/115attendees
>