UFMRG Interim meeting

Logistics:

• time: 2023-05-24 1500-1700 UTC
• meeting via the meetecho below (you need to login to datatracker)
  • https://meetings.conf.meetecho.com/interim/?short=0d06afcd-6c3f-469a-b16b-3ddcdd10b477

Agenda:

• intro/agenda-bash (chairs, 5 mins)
• SSPVerif (Jan Winkelmann, 15 mins)
• Sample problem (Stephen Farrell, 15 mins)
• Usability issues in formal methods (Jonathan Hoyland, 15 mins)
• getting people to start doing things (chairs, #arm-twisting mins)
• if time permits: Delegated Credentials (Jonathan Hoyland, 15 mins)

Attendees

• Stephen Farrell

  • add your name here please, because Stephen likes us to do that

• Carsten Bormann

• Jan Winkelmann
• Cory Myers
• Marc Petit-Huguenin
• Felix Linker

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

• Tooling: UX/UI issues

• Pen-and-Paper Proofs: stop doing this

  • nobody has time to check an 80-page pen-and-paper proof
  • SF: How would that manifest in this RG?
  • JGH: make tools so good that people want to do it naturally in
    the tool
  • Goal for this RG: See people not doing Pen-and-Paper Proofs any
    more
  • ChP: Pen-and-Paper Proofs can be good.
  • JGH: I start with a sketch on paper (whiteboard) -- I don't
    think as this as a proof
  • GB: documentation/training materials...
  • ChBr: SSPs on paper -- code of KE protocols is so huge,
    maintaining a paper proof is absurdly painful. Can't keep
    objects of proof in your head.
  • JGH: With Pen-and-Paper Proofs I need to understand both what we
    have proven and the proof mechanics
  • FL: Why is X the tool you are looking for
  • JGH: I use Tamarin, bad UI/UX, would Tamarin much more if I
    could fix those issues
  • ChBr: Tamarin is one of the good examples! I saw people learn
    Tamarin from the docs and model complicated security properties
  • JGH: It is the best, that doesn't mean it's good. Pretty state
    diagrams, boxes with different colors -- different shades of
    green -- could not even see that they are supposed to be
    different... (and there is a dozen more: when you get to a big
    proof, several minutes to repaint a one-line change...)

• Publishability

  • can't publish affirmative results
  • sneaking formal analysis into deployment or system papers, which
    means I don't get the right reviewers
  • FL: high barrier for publishing security-critical designs (e.g,
    protocols) without formal proofs
  • JGH: Yes, if you are publishing the design as well
  • JGH: So need to publish results ourselves

• Training

  • nowhere to go for intermediate level training
  • SF: What kind of timeline for the RG to work in that?
  • JGH: One instinct to me would be: We could do a hackathon
    training session cheaply at IETF 117
  • SF: Anybody interested to run that?
  • FL: This would be a Prague (IETF118) thing; won't come to SFO
  • CP: Find people in the region to do a tutorial?
  • YS: I'd like to try idea behind SF's presentation; successful
    training could lead to better examples, more likely to lead to
    [YS disappeared]
  • ChBr: too early for us to make commitment -- tool not yet
    published

• Verifiability

  • TLS 1.3 takes lots of beefy CPU
  • Zero-Knowledge, Probabilistically checkable proofs, check very
    cheaply -> kick off research project
  • FL: I share your concerns; not sure it is the biggest problem we
    have -- most proofs terminate, malicious authors could cheat in
    other ways (It's not hard to make a proof terminate -- it is
    hard to make a meaningful proof terminate). Real issue:
    assumptions clearly documented, details of mapping to real world
  • JGH: TLS 1.3: > $500 for a review. I'd bet noone did this.
  • JW: When I dealt with Tamarin, it allowed me to generate proofs
    that were easily verifiable, not sure this still works.
  • SMTlib can give you unsat proofs.
  • (Chat: Jan Winkelmann 18:52
    yeah, groth16 and plonk and friends)

• Reusability, Composability, Understandability, Mathematical limits,
  …

  • FL: mind-yoga needed to map subject to the minimal math
    available in the tools

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.