UFMRG Interim meeting

Logistics:

Agenda:

Attendees

Meeting notes

Note takers: Felix Linker, Carsten Bormann

intro/agenda-bash (chairs, 5 mins)

SF: This interim after Yokohama to try and get work started
SF: -> main item is "getting people to start doing things"

FL: What kind(s) of output artefacts might be produced?
SF: People produce papers, we may want to produce I-Ds/RFCs; think
whether some of the work might go to ANRW
JGH: We don't have intermediate training examples -- trivial ones and
extremely complicated only. -> increasing path of difficulty

SSPVerif (Jan Winkelmann, 15 mins)

JW presenting
https://datatracker.ietf.org/meeting/interim-2023-ufmrg-01/materials/slides-interim-2023-ufmrg-01-sessa-sspverif-verifying-state-separating-proofs-00

SF: Does HPKE in these slides mean (exactly) RFC 9180?
JW: Intended meaning here is more generic than that and not precisely
9180

Slide (7) tried to inline everything -- is a pain

Slide (8) Working in Rust, used to very good error reporting, can't
claim to have that here yet

Slide (9) For loops: Have approach, not exercised yet
Easycrypt is about smaller systems, at a finer level of granularity --
we are looking at high level

JGH: Tamarin background, TLS 1.3: hard to prove with bigger things, how
parts fit together and the state flows between them
Is there a nice way to show how you pass state?
JW: Tamarin is symbolic; here, for all possible states, before an oracle
invocation, certain invariants hold; target state also matches
invariant; more like an invariant based thing instead of tracking
individual states
JGH: In TLS, don't get guarantee until Finished message.
ChBr: Not modelled these in SSP yet; privacy may be more of a match to
SSP

BS: Code?
JW: Not yet.
BS: Could you imagine making an Easycrypt backend?
JW: Could be an avenue, not yet explored
BS: Both of the tools (easycrypt, coq) would give you better way to
connect to running code
BS: Could you prove anything about Rust code?
JW: Hacspec, didn't get into this level of detail

FL: Proving things about what exactly? What is your domain?
JW: Not sure I get the question. Core thing we need SMTlib for:
input-output equivalence between two different things
FL: Code verification?
JW: Not sure what that is
FL: What is in these boxes?
JW: pieces of the game, composition is the game

KB: Pseudocode?
JW: Language we made up
KB: Would be nice to link up with CFRG specs
Please send links on mailing list

Fun with Rosette (Bob Halley, 15 mins)

BH presenting
https://datatracker.ietf.org/meeting/interim-2023-ufmrg-01/materials/slides-interim-2023-ufmrg-01-sessa-fun-with-rosette/

Rosette:
Scheme/Racket, Z3 SMT solver

BH presents as target audience ("engineer", but surrouned with formal
methods people)
(3) Looking for an example: fullcompare() from dnspython
(4) complicated enough to be interesting
(5) simplifying problem for Rosette; rewrote Python into tail-recursive
Racket
(8) feeling much better about algorithm -- even if you only do small
critical fragments, found bugs in at least the initial translation --
with concrete enough counterexamples to know where they are

WH: How easy to spin this up in Lisp (Scheme, Racket)?
Unit testing here; functional testing?
BH: Higher-level testing is possible (saw this at SRI), I didn't do it
First had to translate into Scheme (learned in College); what was nice
about Rosette is the overlay on top of Scheme -- I write my normal
program, but now have symbolic values, design by contract wasn't weird
for me. Verify on an assertion checks that there are no
counterexamples...
Felt very programmy, did not have to learn about SMT or what the
translation to that was (300 terms it was checking)...

KB: I'm coming from the other side -- valuable you shared this.
Small, clear spec, self-contained -- rare...
Corpus of small interesting examples?
BH: I'm sure you can come up with that
(My other example was even more valuable to me as an exploration
tool...)
Good tool in an architecture phase, learn the space better
I don't mind working on large systems, I wanted to show that anything is
better already

(Chat: Talia Ringer 17:51
Agreed there's too much emphasis on end-to-end formal verification, but
starting from unit tests and just getting stronger guarantees for
important or commonly used parts of a program is huge and such a good
starting point
Talia Ringer: like, given most people are writing unit tests, starting
from that and saying "well you can get something stronger than your unit
tests for those same parts of your program" is going to be a good
selling point
Talia Ringer: esp. given that once you have a formal spec, you can also
use it to generate more tests...so you can get free, quick returns
coupled with longer-term returns with more investment)

SF: two quick questions:
(1) how much effort
(2) how to document this in a way that others can learn from
BH: a couple of days; documentation was good;

Sample problem (Stephen Farrell, 15 mins)

SF presenting
https://datatracker.ietf.org/meeting/interim-2023-ufmrg-01/materials/slides-interim-2023-ufmrg-01-sessa-sample-problem-01

SF: BH has just given a sample problem
Look for non-crypto problem because crypto scares away some people
IMAP SEARCH results have state, results can be referred to from future
SEARCHes

KB: Are you suggesting analyzing the RFC, or something more abstract?
SF: Suggesting to document a subset of IMAP SEARCH

FL: What kind of things would you like to investigate?
SF: Combinations of searches might produce interesting results, e.g.,
where UIDs change

MP: What property we want to show/prove here
Related: Interested in usability as an engineer
Usability is in the eye of the beholder
Nobody can convince me something is usable
Would encourage rosettacode approach: one problem, multiple languages
Would be good to have something where we already know it's wrong
Something akin to Rosetta Code

KB: IMAP RFC scares a lot of people
Look for a more minimal thing
SF: First thing would be to extract subset and document that in an
accessible form
Preferably with that subset containing a problem we are already aware
of.

KB to advertise this to students when we have a well documented form.

MP: Another sample problem possibility: RFC 3261 SIP -- we already know
what is wrong (fix is documented in RFC 6026)

FL: What is the goal of using FM?
Once you know what to look for, the tool tends to work remarkably well
Favoring IMAP
Tamarin: Formal methods for security
vs. formal methods for correctness
Usable Security section for formal modellers
Student analyzed some protocol; half of the work was to find the
security objectives.
Figuring out why people do not (cannot?) write those sections.

SF: hard to know what security consideration sections do.
JGH: second that.
Aside: BCP how to write a security section. (SF notes we're an IRTF RG
so not our job and attempting to improving RFC 3552 is non-trivial)

Poll "should the RG spend time trying to idenfity/document a sample
problem"? -> 21:0 (of 33)

CP: Classes of problem? Give thought to different types of things you
can prove
SF: Good point

Action on chairs: send mail to list starting that discussion so people
have more time to consider their suggestions/opinions

Usability issues in formal methods (Jonathan Hoyland, 15 mins)

JGH presenting
https://datatracker.ietf.org/meeting/interim-2023-ufmrg-01/materials/slides-interim-2023-ufmrg-01-sessa-usability-issues-00

JGH: The issues we have currently that make FM less useful

getting people to start doing things (chairs, #arm-twisting mins)

back to
https://datatracker.ietf.org/meeting/interim-2023-ufmrg-01/materials/slides-interim-2023-ufmrg-01-sessa-chair-slides-01
slide 6

CP: Keep list of protocols where people want input
SF: Wiki - yes, we should update that

if time permits: Delegated Credentials (Jonathan Hoyland, 15 mins)

https://datatracker.ietf.org/meeting/interim-2023-ufmrg-01/materials/slides-interim-2023-ufmrg-01-sessa-delegated-credentials-00

Time did not permit.