Internet Engineering Task Force Interim Meetings, 24 May 2023

Previous Meeting Next Meeting

⏯

youtube image

►

From YouTube: IETF-UFMRG-20230524-1500

Description

UFMRG meeting session at IETF
2023/05/24 1500

https://datatracker.ietf.org/meeting//proceedings/

A

A

Your video popped up there that's good.

B

A

Again, if anybody else wants to do an audio or video chat, now's a good time.

C

A

I think I heard you just there again, yep.

A

So we'll give people a few minutes, including my co-chair, to get joined.

A

Here Comes Jonathan.

A

Thank you Carson, so Kirsten is willing to give occasional help. Anybody can jump in and help with. No taking as well. That's a it's a tool. Everybody can edit once you've authenticated to it.

A

Jonathan there you are, and.

A

Do you want to send some audio of Jonathan as well yeah.

D

I was just trying to get that video I wasn't happy with me. Hi everyone.

D

A

We'll get uh started about four pass like this or five past. Let's say just give people a chance. I have one email from somebody asking how to join.

A

All right so Jonathan I I'm, not sure we got slides from Jan uh I, don't know if you saw that. But those are now open, ready and yeah and is in the room.

E

A

And Carson is willing to help out with occasional help for note-taking, which is great. If any, is anybody else willing to try and help us keep some notes? We don't need detailed notes, just basically it's good if somebody volunteers, to do something that we get their name, so we can hassle them later.

A

And Felix, you don't need to send video throughout the meeting. It's it's okay, to uh mute, your video and just have presenters kind of as we need them.

A

Okay, so Karsten is volunteer to help it, though it's on Jonathan, I guess you and I can also try and keep up with uh people volunteering as they do.

D

Oh yeah, don't worry. I'll definitely make a note to any volunteers.

A

And I think we are being recorded according to what it says on my browser, which is good I. That was when we were using WebEx for these meetings. I would always forget to hit the button so.

A

uh So this is the usable, formal methods, research group, information, uh we're kind of just getting started. Still um we agreed and we had a meeting in uh Yokohama we agreed we'd have an interim I guess. The main goal I would have for this interim is to try and tee up people starting to work on things um and kind of, let's see if we can get groups of people going and stuff. My name is Stephen Farrell by the way I'm one of the co-chairs and Jonathan is the other, so Jonathan just going to say hi.

D

Hi everyone I'm Jonathan I'm, one of the I'm, the other co-chair um and uh yeah so I- think we're gonna have some very useful information uh this uh session and hopefully we'll start getting some real directions for what we're gonna do and detect where we can take. This group.

A

I think we have some boilerplate stuff first, this is an irtf meeting. The internet research task force also follows the ietfs handling of intellectual property rights and so on. uh So if you're uncomfortable any of that, then that's probably you know it's probably not a good thing. uh I'm assuming people are, we are being recorded, um so those recordings are available later uh yeah.

A

So, basically, if you're sending audio and video You're consenting to be in the recording and again like all kind of IDF and RTF groups, uh you know we'd like people to behave and I, don't expect misbehavior to be a common thing in this research group.

A

um So that should be all good and again, there's a bunch of links on those slides that are the real meat of uh whatever is is meant, so those node well slides are really pointers to the uh the policies um again just to say the Clear Internet research task force uh basically is false, focusing on what it says, their longer term research issues, we're not a standards, development organization. We don't develop standards, we don't we don't get to tell the ITF what to do, etc, etc.

A

If anybody has questions about any of that kind of stuff, then drop them in the chat or uh jump up and down in audio, if need be okay. So today, uh this is our agenda, which will ask people to bash the agenda if they wish in a second.

A

um This is the intro part we have Jan is going to talk to us about SSP verif, a colleague of Jonathan's Bob uh is has done some work related to DNS. uh We have some ideas about sample problems. Jonathan has some uh information about usability issues um and I. Think I would encourage unless the speakers, otherwise I'd, encourage people to jump in with any questions as we go, I don't think, there's a need to wait.

A

We're not pressed for time today, as far as I can see uh to do that, there is a hand raising tool at the top left of your screen just below your name where you can join the queue I. Just did it to show you this and you pop in the queue and we'll ask you to send audio uh and our video as need be.

A

If you have a question or comments again, if any of the speakers prefer to wait till the end, they should say that otherwise, please just jump on the queue, as you feel the need to say something, um and then, if we, the I, think for me the main kind of part of the the meeting which doesn't have to be an individual agenda item but can be distributed, is the getting people to start doing things, but um where we want to try and see who who's.

A

You know, a bunch of people clearly are interested in this topic. uh We want to start to see who's interested in actually doing what, um initially, with a view to kind of leading up to a possible meeting at the July ITF, uh but obviously for ongoing things as well, and then, if time permits we should probably will Jonathan has some slides on delegated credentials that he did not cover in Yokohama, because we didn't have time there.

A

That's our agenda, Jonathan I, don't know, did I skip, did I forget something or missed anything or okay.

E

A

Anybody have a comment to the agenda things they want to change, add feel free to suggest changes or editions. That's that's entirely fine, Felix you're in the queue so.

B

Yeah, it's maybe a minor thing and we can discuss it later, but I would what I would be particularly interested in in the bullet point for getting people to start doing things.

B

um I lack a bit of an imagination with possible deliverables or artifacts could be that come out of this research group and I'd like to maybe discuss that as a possible. More concrete thing to discuss then start doing things. Sure.

A

That's a very fair question or a comment: um I guess you know. Typically irtf research groups uh uh can produce. You know people produce papers um in a normal kind of publishing kind of Arena.

A

um It can be the case that we may want to produce some internet drafts or rfcs that doesn't have to be the case, um I think for This research group in particular. We one of the things we should think about is whether some of the work might be nicely published in the context of the anrw workshop.

A

um um But yes, I think that's a good point and probably one that we should think about as we you know as we go through the agenda as to what kind of artifacts might this produce and how might we handle them? Jonathan.

D

So um I am in my uh usability issues in formal methods. Slides I do have some concrete suggestions, but just to give a quick preview.

D

um I think one of the really key things that we don't have uh at the moment are intermediate training examples for a lot of the tools, a lot of the tools that I've used at least have one trivial example and then go straight on to incredibly complex, uh very hard to replicate without many years, training example, um and so something that this group could work on and Stephen will talk on later, is a sample problem or maybe even you know, eventually a suite of problems, and you would then say: I have this new tool.

D

Here is each of those problems solved in my new tool or whichever one to apply um so that there's a sort of increasing path of difficulty, so that people can learn how to use these tools. So one thing might be training materials.

A

Indeed, again, thanks Felix for that comment, uh anybody else have a comment or agenda bashing type thing or something they would like to interject now.

A

If not Jan um I can present the slides I can do the button clicking on the slides for you or I can actually hand you control if you prefer. So let me just switch to your slide deck.

A

So Jan, if you want to start yeah there, you go and would you like to control the slides or would you like me to hit the buttons for you.

C

Yeah I think it's easier if I control them thanks.

A

Okay, so I'm passing the control. You should see the um you should see the slide number thing at the bottom of your screen.

C

A

C

Again, yeah we're not.

A

Hugely pressed for time today, I, don't think so, uh don't feel the need to rush, but I think we budgeted like 15 minutes or something like that. So uh I have to stop only.

F

A

And uh over to you yeah, thank you.

C

Yeah thanks for having me um hi I'm, Jan I'm, working with Kristen Kristoff on SSP virif, um which is about verifying State separating proofs, and a lot of you may be wondering what state separating proofs are and um State separating proofs are a method for modularizing com, computational, cryptographic, security, proofs in cryptographic, security, proofs in the computational model. You usually say: okay, we have an adversary and they're like computationally bounded and if we set them into this game into into a cryptographic game where they interact with um with cryptographic Primitives they have to tell apart.

C

Is this like the real primitive? Or is it just like the the ideal primitive that just actually gives them random numbers all the time? And uh then we say: okay, there's a they have a certain bound on on their success.

C

Probability and um State separate, improves, um take this concept and try to modularize this to make um a lot of the proof steps specifically the reductions, a lot more simpler, a lot more simple and um for the purpose of this talk, I like to use hybrid encryption from chem and Dem as a motivating example, um hybrid public encryption, basically, is you have a public key from a receiver, and you want to send them a message and then use the public key encrypt the message with the public key and give them the ciphertext, and then they can decrypt it um in hybrid encryption.

C

You use um two steps. First, the asymmetrics, where you just like, get a key that you can then use a symmetric encryption algorithm for which is called them like key encapsulation and data encapsulation, and if you just use Cam and Dem in in like a modularized way and modularized in a way that makes sense for State separating proofs. You would end up with something like this. Where, on the left, you see basically the oracle, the oracles that the adversary can call like invoke on the on the individual pieces called packages in SSP lingo.

C

um So they can generate new public keys and then they can encrypt both the keys and the data, and um this is all neat. uh The problem is that, like this, isn't really compatible with the um hpke interface, which just has like a single encryption, a single decryption Oracle, so we can do is we can just like put an adapter in between and then um yeah? That's just a single function. It just calls them both both sequentially in a way that makes sense for hpke now um in in state suffering proofs.

C

The the neat thing is like I said: the reductions are supposed to be very simple and in the way that the assumptions are formulated, um we can now just actually go and say: okay, we know that this is basically the set like the the real uh can. The game in which the cam is real is basically the same or yeah indistinguishable from the chem in which the game, the cam, the game in which the chem is ideal, which means it just returns, random ciphertext and produces random keys, and in such a setting.

C

um Now the Dem consumes random Keys, the uh yeah that one also matches the the Assumption, and now the Dem can also be idealized, which means it will just produce random ciphertexts, uh but still decrypt fine. So this is. um This is all neat and a very, very practical and a very handy thing for for working proofs.

C

But the problem is what we're actually dealing with is the hbka security definition and that lives in a single package, um and it's not modularized at all, and we still have to like somehow show that it that it that we actually talking about the same kind of security like we have to show that the security definition where working with in the modularized version is the same as the monolithic um yeah Stephen. Do you want to go now or after.

A

Oh it after it's fine, but I just had a clarifying question so hpk here you are referring to RFC 918.

C

um um I think it used to be called like integrated encryption scheme as well um or ice ecis as well for elliptic curves. It's just like the the general I think HP I'm using the term, because I ietf uses to use that term, but I think it basically is that um I I would have only looked at like that RFC briefly, but I think it basically is that yeah, okay.

A

C

um Right, okay, so this um we we tried like. um There were like several approaches to to do this before SSP um one approach I did in my Master's thesis was that I tried to inline all of the code and then show that basically, it's the same in the monolithic and the modular version.

C

um That was a pain and um so then more formal methods, but on paper were also used by other researchers um such as Chris and Kristoff um and yeah. So now it just it just turns out again and again that this was a very annoying proof step and what I wanted is something that is easily verifiable and we don't have to manually, write and keep consistent between changes, a whole lot of code across a whole lot of pages.

C

um So we started working on SSP verif um as the use of the tool. You would write, something that looks somewhat close to pseudocode.

C

um That stuff is then parsed and you would generate smt lip code, um including the the smt lab versions of the the package code that you've written in pseudocode as well as some helpers and the user then writes invariants um that are all consumed as well consumed by by the tool.

C

um Where is the pvrf that people then invokes the s p solver in a certain way to, in order to like show that the two things are equivalent. So this is like the the most complicated I would say part of the of the whole thing of the tool. What we also do is we type check the code. Well, maybe this is the most complicated one and also um we.

C

We also show that the the compositions um are like are also type checked, such that, like yeah, basically check all the all. The packages are connected in a sensible Manner and um we not only support equivalent steps but also reduction proof steps. So, basically, the the goal is to to have like a start to end proof encoded in SSP varif.

C

um One thing we're working on is better error, reporting um we're working in Rust, so as developers, we're used to very good error reporting, uh which is not something we currently can claim for to provide our users.

C

Luckily, we are the only users we currently so um and yeah we're also working on tools to give better insights into proofs and why the proof doesn't occur in pass, currently does or doesn't pass um yeah current challenges um is that the users have to be really fluent in smt lib for several um for all over the code base. Basically they're dealing with it and dealing with for Loops also is a bit tricky, um but I think we have.

C

We have a good approach and we are, we haven't been able to like really use it, but we're we're on it and, um as a case study, we're formalizing the proof of your scaffolding scheme provided by postcard, excellent on paper, we're now making formalizing this in the tool, and we also want to do something with key exchange.

C

um Finally, the hopes for the future we have is that we can verify ssps for very large protocols.

C

um I think this is something that also sets It Off from easycrypt, which um is it's more about like smaller systems, but in a more fine detail like it, it seems to capture time it's like side channel to timing and stuff, like this I think stuff about C code. Even and this is not something that we're really dealing with we're like looking at the high level at the moment, yeah I think uh that was it from me and looking forward to questions yeah Jonathan.

D

So uh this is super interesting to me. I I came from a Tamarind background, so I looked at um yeah, that's one of three um and one thing: that's really hard to prove when you're doing bigger size, things is how all of the different pieces linked together and how the state you're guaranteed whatever you're guaranteed from you know. This key derives this key, which means that this message must be tied to that thing um and your your proofs look all very separate. Is there?

D

uh Is there a nice way of showing how you pass State between each part of them.

C

um So basically, we say: semi Tamarin works very different right, I'm, a symbolic model, and if we, if we, if you look at the picture here, basically what we do is we say before, like for all for all possible states where, before an oracle invocation, the state satisfies the certain invariant. Then we we invoke the Oracle and then the response to the user like to the adversary is the same, and we also have like a relation between the real this, the state of the system in the the real game and the ideal game.

C

And if that it's like an equality sort of equivalent sort of relation, and um if, if that is the same, then then the output is the same and then the target state of the system is also uh also matches the invariant and also again will in for both systems fulfilled that equivalence relation. So so, basically, it's more like an invariant based thing, so we don't really keep track of of States individually. It's more.

D

Yeah, so you you can't or well can, can you can you say in tls13 just because that's what I'm familiar with uh you don't get certain authentication guarantees until you've received the final finished message.

D

um So can you say Cascade back up the stack say uh we know we have this authentication guarantee at this point because later on we know the finished message was accurate.

G

But so, okay, so so so so, firstly,.

H

That's a that's.

G

A good point, kind of like um adaptive properties, are kind of annoying to um to you know like pass the information across several packages. That's a that's a that's! An absolutely good good catch. I haven't model these authentication properties in states of writing proofs yet but I think for authentication properties. It's usually fine, the the you you!

G

You should be able to do that, um but you would you would somehow need to to pass the state from you know what one point to another, um but um I think authentication is also not necessarily what this tool is best at more about protocol flow and protocol logic, where tamarine is amazing um and I, think kind of privacy, properties and domain separation. This kind of things as maybe more strings of um this kind of techniques. But question is like how to compose them nicely.

D

Very cool, thank you. um Are there other questions.

E

E

I had a quick look at your GitHub. Is the code available somewhere.

C

C

um We can work on that.

E

I'm curious when it comes out and the second one is you say: I mean the last slide of your last line of your slide. You say it's a complimenter uh complementary to to easy script, but could you imagine making easy crypto, backend and and I guess the same question holds for S is proof.

C

This is something that we discussed. um I think it should maybe be an Avenue, but so far um we haven't exploded in depth because we were still had so many things to do. um I think I, don't know, I think it would definitely I think it would be an option. um I think the the question that would need to be answered is: what are the specific benefits of using these tools?

C

um Maybe just being able to generate code in the language might be yeah I think what would happen is that we generate instead of generating smt code, we would generate um SS proof, I, think it's in Haskell, right and.

E

Ss publishing cop and Asia cup is right.

C

Yeah yeah, like I, was just like some ml language. Okay and- and these Crypt is completely different, yeah I think that would would be something that's possible. um Yeah I think I think one. The question is like: what do you want to gain from this um and I think.

E

Yeah I mean, if you go to Egypt, you could verify well. I mean both of these tools would give you much more possibilities to to connect the running code. For example, it's one of the things I I presented last time.

E

um uh Both these equipped and and um um Hancock would allow you to to generate um Jasmine code, for example,.

E

And you would I mean other questions about our properties of the the computational model. You could do there and I, don't think you have them in in SSP there to you.

C

Well, the the properties of the computational model arise from SSP right, and we we only use symbolic things for for showing equivalence and the reductions are are done by just showing okay yeah that basically the assumptions match, and then you can rewrite the graph.

E

But could you prove anything about um rust code, for example,.

C

Oh, no, um we were looking into hexback I, think, which is like the the subset of rust, which is, but this is something that that seems for for our purposes way too deep. In the the details of like okay. Now we have a byte array like an array of units. That is this long, and this was not at all what we were getting at, because we were like modeling Global protocol State and not like looking at individual implementations.

E

But but in the end you would like to have a complete proof about uh I mean running code at some point.

C

Yeah I mean like this is an interesting feature, but it hasn't been one. That's been guiding the development of this tool at this point.

E

Yep and I understand it's just some something that might be interesting in the future.

A

I'll just drop you off the queue. If you need, if you had a different question, you can rejoin if you Felix.

B

A

B

Keep doing right? Yes, um thanks for the succinct talk, my connection connects and my question connects a bit to what bus just said, I wonder what exactly you are approving things of. Like you say we prove things about code.

B

um What's the what's your domain.

C

um I'm I'm, not I'm, not unsure, I, completely, understand question um like so I. Think, there's like several steps. um One thing like the core thing that we need smt Loop for is proving that the code of that that, in basically input output, equivalence in a way between two different implementations of supposedly the same functionality are actually the same.

B

Okay, so you're doing code, verification of a crypto Library.

C

um I'm not sure what like code verification I mean if that is a technical term, I'm, not I'm, not really deep, in like formal methods, yeah and just like winged it in a way yeah.

B

Yeah what I want is, you know there are people who come up with cryptographic, Primitives and then they do game based proofs about the cryptographic, people uh or The Primitives. Then you have people implementing these Primitives. You might want to prove something about those I I didn't quite like I, wonder what is in these boxes that I see on the.

C

Slide right, um these are games. These are cryptographic game. This is like like pieces of a cryptographic game and the composition is the game like like the top thing? Is a game and the bottom thing is a game, and we want to show that these games are actually equivalent. Okay,.

B

So in the in the end, you have a theoretical result. Yes, okay, great thanks.

I

Hi so I'm up next I guess uh this is fun uh again, I think I'm, just gonna go a bit further from the previous question. You said that the source is a bit like pseudocode and that's interesting a lot. uh What does it look like? uh What is this.

C

Okay, let me let me try to find an example. It's a language that we made up um and then heck together. The parser.

C

Yeah, that would have been a good bonus slide. I agree.

I

You don't have to search for it right now,.

H

But that does indeed to.

I

See because it's also the way to see how the connection is between the kinds of standards that are being standards at the cfrg, how you would link it to something like this, so maybe it would be nice to have such a kind of semi-formal serial chord language which people couldn't use directly in the standards or in their papers or whatever, which could then fit into your your tool right. So that would be an interesting thing to look at.

C

I

The moment this is yeah, maybe maybe, when you're ready to uh kind of meet public some of the results. You could send an email on the on the mailing list with with a link to stuffing, uh and that would be quite nice for us to look at it.

C

Yeah sure definitely.

E

Okay, we appear to have.

D

uh um Any last questions, or shall we move on to the next talk.

D

Okay, the queue's staying empty. uh Thank you very much. uh This is really interesting and uh we're going to have uh Bob presenting hi Bob.

D

Do you have control of the slides?

D

H

F

H

Oh I do excellent. Okay, I've never used this uh presentation program before so I'm going to talk a little bit about some experiments. I was doing with Rosette.

H

Rosette is uh augmentation to scheme, slash, Racket and uh uses the was using the Z3 smt solver.

H

So uh I wanted to say something about background here, because uh I'm kind of more a representative of your target audience than I am uh someone creating the tools.

H

um I've been an engineer for a long time, although I'm currently in research, I, don't have any training, informal methods, but I do have some awareness of them. I was at SRI CSL before I, went to Cloud fire research and was surrounded by formal methods. People so I saw some of what they did, but I never kind of understood. What could I do with it in day-to-day engineering kind of things, as opposed to you know, trying to do something exotic like prove the correctness of an entire DNS server.

H

That seems hard to me still, but um any kind of proving of anything is is oftentimes better than nothing.

H

um You know, I did I, have used formally proven things in the past that other people did proofs of, but at any rate, as a part of my current research, I wanted to be able to have proofs in a completely different area and I decided I needed to learn more about this topic and I realized that things have changed a lot since the last time. I, even you know, considered what it could do and I remember.

H

We had an intern last year who said that rosette was really pretty and well documented and high level, so I decided to just try it and make some problems for myself. uh That I thought were substantive problems that I could see what it could be done with it.

H

So that's sort of where I'm coming from and I mentioned, DNS python here, just because I'm using part of it as an example, not because it's super important.

H

So the thing that I was looking at is a method in the name object called Full compare and its job is to compare two different names and return, some relation information on them and there's a quite a bit of relationship. Information there's sort of where they are in the tree super domain subdomain.

H

Maybe they have a common ancestor, but are not direct parent and children or maybe they don't have any relation at all and they're kind of complicated, because DNS pythons, let you have both fully qualified names, that is names ending in the root label and also partially qualified names that are relative to some unspecified origin.

H

In addition to the tree relationship, there's also an ordering within the dnssec ordering, and it's also useful to find out how many common labels you have for other operations. So this is what I'm looking at and why did I look at this particular thing it as I understand the subject area. This particular method is important in the context of DNS Python's Library.

H

It's not important in the world, but uh this name comparison thing is, is used by a lot of stuff and it's very important that it's right, I'm not worried about it being wrong, but I thought it would be a good problem, and it's also complicated enough to be interesting to me and I. Just didn't see going into this, how it was going to work and it has good test coverage, but you know I'm never really happy with unit tests, because I never really know what I missed in a unit test right.

H

uh So how did I approach this? Well, the DNS space seemed too complicated, still right. A DNS name is kind of a a sequence of labels and it can be up to 255 bytes and the labels are strings and there's case insensitive comparisons. But none of this was really super important, for is the actual algorithm in full.

H

Compare right, so I simplified things into something that was much happier for rosette, which is I'm modeling DNS labels just as integers, because all I really care is that they have an order um and I simplified a domain name. Instead of being much longer and complicated list of labels.

H

I just said it's going to be between zero and three labels, and then I took the full, compare function from DNS Python and rewrote it into a tail recursive function in Rosette and I I did it as tail recursive just because it always makes progress that way, and it felt better as a mathematical argument, right that if, if I can get this step to be proven, then that would generalize better to the full problem uh of longer more complicated names, and so the the sample problem I have was to check for consistency which is like.

H

If a is a subdomain of B, will it say that b is a super domain of a if a equals B? Well, let's say, b equals a those sort of things. So it's a simple test right. This is like an exercise for me not not uh anything or shattering here, um and this will be too small to read, but I just put it here, uh you can see.

H

This is basically doing the kinds of check that I was talking about for each of the cases and I'll say a little bit more about what this meant uh rosette wise later.

H

But let me just get to the important bit um so here these new name, things are just basically generating any name from the space of names between zero and three labels, and it's going to exhaustively check that this assertion that the names are consistent is true for, for this, entire space and I run it and it returns unset- and this is really an epiphany for somebody like me, because this is much stronger than a unit chest right, like I I've, just shot it, the the smt Checker, it just shown, there's no way to make check false and so in the in that entire space.

H

So this was. This was really exciting for me and the takeaways from this. Although this problem was overly simplified, perhaps I still learned a lot about the algorithm um and there are, and it will generalize to the larger problem so I leave this even though I haven't necessarily proven the full original program.

H

Correct I still leave this feeling much better about the algorithm um and I think that this could really make a big difference in day-to-day engineering and to the extent that I I think that this should be added to people's toolboxes, because even if you only do small critical fragments of things you're still creating a really meaningfully better experience than what we have without it. uh And it was really easy to use.

H

um Rosette basically exposes uh this notion of a symbolic variable and verify and solve and verify and solve, are kind of the same thing. Just one is looking for exceptions to the thing and others looking for a solution, but it's, but um it was really handy because I actually made bugs in my first uh translation and so I confidently check in verify, and it says.

J

H

Here's the model of where you made a mistake and now I know exactly what's wrong and can plug that in and see and then fix it and uh in another example that I'm not describing here I did a much more in-depth kind of explorations of the space and that really worked for me as a developer.

H

In that um the way I work I like to explore things and do a lot of hand, testing just to sort of learn what the the space that I'm working in is and having something that can come up with examples or proof that there are no examples. Just it's it's. It was a real power, lift I thought and a productivity enhancement.

H

So anyway, that's that's uh I! Guess: I have one more slide uh where that was it. That was it so I'm happy to take questions as you're possible target audience.

A

So where's I think.

K

Gear, first, all right, thanks um sort of two questions are somewhat related. um You know one I I found this. You know a presentation fascinating thanks for the information. I now need to go, read a whole lot of documentation on rosette, because I didn't know anything about it, but uh I'm curious about the usability level right.

K

It's clearly a programming language is clearly you know, list oriented things like that, and so what I'm wondering is how easy you know was it for you to spin up and be able to do this, and let me tie that to more concrete example of you talked about it. You know being better than and then unit testing, because it can verify that that you couldn't have done anything wrong right.

K

It's not just that you're testing, one scenario, you're testing them all almost seems Quantum like um what I'm curious about is how much effort does it take to produce a set of things that make. You feel confident that you haven't missed anything so unit testing is very small and microscopic in terms of the types of things that you're testing, whereas you know what I think we really want to do is test functional testing, that is, more user oriented end-to-end.

K

You know high-level kind of Concepts and it doesn't seem like that's entirely possible and sorry for the long-winded question.

H

Yeah I, don't I, can't I, don't think I can say about the high level thing. um I I will say that that higher level testing is possible. I saw this at SRI, although I wasn't writing it, but I I saw a more complicated end-to-end orchestration of something so I think that there is some possibilities in there um so back to I, guess how it was for me with the coding.

H

um Well. First of all, you know: I did have to translate into scheme which didn't bother me because I learned scheme at the very start of my education in in college long ago now um and I always liked it and remembered it. So that didn't bother me I, think that if this was going to go for a bigger audience, it would be nice if you didn't have to do that translation.

H

But the thing that was really nice about rosette is that it's basically an overlay on top of scheme, and you can imagine doing this kind of overlay. On top of another language, I mean the the interface to me as a programmer was I write, my normal program, except that I can now use these symbolic variables as well as regular variables. I can now encode some assumptions, which was also familiar to me, because I've done design by contract type programming for decades.

H

You know so you assume assume assume a certain assert, and so so writing that wasn't weird for me and then the nice thing is. You just call verify on an assertion and it checks that you know there are no counter examples to that statement. Whatever that function is doing based on whatever assumptions that you've limited it to so you know, I would have assumptions like assume that Elizabeth that the lisp is between zero.

H

The list is between zero and three uh that kind of stuff, but it still felt very programming like I, never had to learn about how smt solvers work I never had to learn I, never made any translation in I mean I'm aware of what this smt lib thing is because I I poked around a bit but I didn't have to think about what the translation was into that uh and gosh. The translation was pretty complicated. I looked at a couple of them.

H

You know it wrote like I think it had like 300 variables and one thing after it enrolled everything 300 terms that it was checking. But I didn't worry about all that I'm just sort of living in this augmented programming space, where uh I now have these tools to go simulate the entire space of inputs and outputs.

H

um You know I still think knowing how to limit things so that you don't run into limitations of the solver is probably going to be relevant and uh I don't know. Does that answer some of your question yeah.

K

Yeah I did think so that was definitely helpful and it certainly sounds like it was helpful. You had a lot of background too, but I'll. Let others go for I.

H

Could talk to you for a half an hour.

I

K

I

Oh, this is a gem of a talk. I really enjoyed that thanks so much for this uh I'm coming from the other side of this working group, every building tools, and uh so this is very valuable for us to to hear this kind of thing, I think uh and one of the nice things about your example.

I

Although you picked it as a startup example in some sense is the fact that it's small, it has a clear uh spec and it's self-contained, and this is rare actually for us, you know, because at the end for pre-published papers, you end up publishing things about large, huge protocols with lots of dependencies and stuff and and it's not clear that it's actually accessible or usable, because you're always focusing on the big thing.

I

um So do you think from your experience as engineer for these years? Do you think there is a it's possible to build a corpus of small, interesting examples that would be good to verify and the things as things exist, I mean full. Compare is one of them, but is there other things like this, which you.

H

Could point out I'm sure, I'm sure that you can come up with that because, uh like I say this was only one of a couple examples and my other examples were in a completely different domain and it was a domain that I didn't know as much about so they were actually more valuable to me as an exploration tool like I went in and purposely made some mistakes uh in order to discover them right to see how the tools worked, but I also discovered that I'd made a whole bunch of other mistakes that I didn't mean to make, and so because uh this so I think it'd be a really good tool in an architecture phase.

H

If you're designing things that that you can learn the space better and learn what your assumptions are, and that kind of stuff and and one of the things I'm definitely trying to say today is while I don't have anything against proving full large complex systems. I'd love it. If you had a completely provably correct name, server, um I just wanted to say that it's one of these things that it's not an either or- and you don't have to do everything and the state of being for a lot of things- is so low.

H

That anything is better. You know like to get to to get from I hope that my unit case covered everything to knowing that my tests covered.

H

Everything is Big, because not all parts of my program have the same sensitivity, but you know like if I was doing network security code or something I would really want that to be as nailed down as possible and I would be happy just to have it proven, even if nothing else could be proven and I believe that these tools are sufficiently mature now and maybe getting to the point of sufficiently high level that they could be accessible to more people.

I

Yeah that makes complete sense, I think one of the big challenges, even from the from the from the application tool application point of view, is even to extract out a piece of code like he was saying about: network security or or whatever and say we want to verify just this piece, it's quite hard, often because yeah, but anyway thanks so much. This is very useful.

A

Hi Bob thanks again.

H

I think yeah I think this.

A

Is really useful to say, can just two quick questions, uh one is: can you kind of give a sense of how much effort it was to kind of do this work and second question is uh assuming somebody was willing to kind of try and document this in a way that others could learn from?

A

What way would that be best done? Would you say, and would you be willing to do it and and send the results to the list if you're, if you're going crazy but I'm.

H

Kind of interested how much.

A

Effort and like how would you, how would you kind of write this down, so other people could reproduce the same kind of thing somewhere else.

H

Yeah, let's see as far as effort I think I spent a couple days, but no more on the actual on all the modeling. That I did um it.

H

You know took a little while to get going because the the you know, the the learning curve is pretty steep at the start, and and I didn't even have the tools set up right so like I, had to get bracket installed and it's IDE and then install the package and then had to read all the documentation to learn about symbolic variables and things, but the documentation was really good and and in particular it uh it gave me a really great tool.

H

This notion of I mentioned it in the talk of picking a list between zero and three things long. You know the those that list type is not a solvable type itself within uh rackets or rosettes terminology, but you can build up. You know you can build up a list of things like that by sort of parameterizing it by things which are solvable like integers, and it was smart enough to do all the translation for it.

H

For that, provided that you didn't make things you know infinitely long, and um so so it wasn't too bad a learning curve, but you know I I, guess I'm! Maybe was ready to hear it too we're ready to do it for some for some reason, but uh and I would be willing to write up. You know my experience.

H

A

Be great yeah. Thank you.

A

um Nikita forehead.

A

A

Are you in the queue or having audio difficulties or you can? If you are having audio difficulties, you can use the chaff feature to okay there. You are now no audio.

A

Okay, so Nikita said she's having trouble with microphone and we'll ask offline uh any other questions about Bob did I hear you actually just promise to say that you probably would write something like this up and send it to the list. At some point.

H

A

H

Think I did say that on.

A

Wednesday, that's great and I hope our note takers caught that.

H

Jonathan won't, let me forget good good.

A

Any other questions or comments for Bob.

A

If not thanks Bob, that's that's pretty interesting and I. Think it's me next.

A

So this is a kind of a similar thing, except obviously that's well done and more kind of flaky. uh But we had you know, as we were chartering This research group. We had you know the idea of possibly having sample problems, and maybe Bob has just kind of given one particular one right to DNS.

A

uh But if we had one or a few sample problems that we we could document that were attractable and where people could as well just described, try and make use of the kind of formal methods and see how they work and be able to explain to people how to use them. I think that might be useful, so uh I had an idea for this or what might be interesting.

A

Perhaps it's a crazy idea, but the the basic concept of the sample problem is, you know, to try and have something: that's ietf, oriented, relatively simple, not cryptographic, because I think that scares away a bunch of people.

A

We should there's a lot of good work being done, informal methods to do cryptography and that's great, but maybe we need something- that's not um and again, for these kind of purposes here to basically help people to understand how to apply the methods- uh and you know perhaps, to help people who are developing those methods, improve usability and maybe even find out something about the problem itself.

A

So the one that occurred to me. That might be interesting. If you know, as a you know, perhaps some kind of subset or simplified version of IMAP search, um so IMAP we're all familiar with, but probably we're all familiar with having mail and mail messages in the message store and using IMAP clients uh to do searches and apparently, a whole bunch of mobile clients, actually make extensive use of search and to save battery and local storage and so on, and there is a definition of uh in RC.

A

1951 defines it's the most modern IMAP RFC in this section, but, along with some other a b and F defines the search and I guess we're kind of familiar with the type of things you can do with search.

A

um You know search on various attributes of the message, one of the things that I I wasn't aware of beforehand, but that's uh I'm, a people I'm sure are, is that you can have some state in the search in that the the search results can be then referred to in preview and subsequent instructions from the IMAP client to the server um and obviously, of course also, you can have multiple user agents uh that you know belonging to the same user.

A

Let's say not necessarily different user agents or different users, but the same different user agents for the same user might be doing things at the same time. uh It's a relatively Rich syntax, but not particularly um complex I. Don't think in some ways it has the state- and we also I, guess have probably a bunch of people who have implementation and deployment experience that might help kind of Point.

A

Some of the people, developing formal Methods at uh interesting aspects of this to think about are things that would be nice if we could prove something about them. So if we were to choose that, then what would we want to do?

A

um And again you know this. This could be something that we do on this problem or some other problem. But if we, if we picked some problem, we might want to get some people who are kind of familiar with, in this case IMAP and somebody familiar with some of the formalisms uh try and figure out how to document some subset of IMAP search. That's interesting perhaps write that down in an internet draft or some other format, but an IDE could kind of be sensible here and try and you know, discuss it in the research group.

A

Maybe do some kind of last call type thing to stabilize it, but not necessarily publish as an rrc and then try and encourage people to try and apply formalisms to that sample problem show us how they did it, how much effort it was, how you know what are the results and so on, and then again the publication question that I think Felix asked at the beginning is how you know: how would you get those artifacts published and anrw might be one of those uh one.

A

You know a suitable place for publishing such kind of uh applications or particular formalisms to the sample problem or.

E

A

Know you talk about an RC so that doesn't have to be the open, so uh I guess I'd be interested in in feedback from the group as to like you know, is this perhaps a useful problem to try and look at and if so, anybody want to work on it? Are there other problems that might have good attributes that we could try and encourage people to work on?

A

You know if people want to start a bunch of these things, that'll be fine, not everything will kind of finish, um but uh I think the idea of having some sample problems I think it seems attractive.

A

um So my question is: do people does anybody like this particular problem or want to suggest a different one, and in particular, is anybody willing to do some work on either this problem or some other one and that's all I had so I'm hoping people will join the queue to to say this? Is crazy or enough or I'd be happily work on it or whatever Karthik.

I

um Hi so just to understand, are you suggesting analyzing the RFC or something something more abstract or.

A

Well sure what I'm suggesting is trying to document a subset of the IMAP search operation as a problem and that's you know, that's extracting text from The Roc and perhaps simplifying it to some extent if needed uh and then sort of asking people to far ahead and try and Tackle. This problem.

I

And what would be like a I mean? Is that a easy enough spec to understand that it's it should return? Director is also something I mean. What is the expected.

A

I

Basically, iMac.

A

Is when your male client is talking to the message store and where you can select some messages? uh You know the message is from Karthik or the messages from last February um and you can do some combinations of that and then you can also have other operations done on the results. So there's a stateful element to the results as well.

I

Okay, all right thanks.

A

I didn't hear Karthik volunteers do anything, that's a Pity, but maybe we'll get them in a minute. Felix.

B

Yeah, my questions may be a bit connected to correct, so I wanna. What kind of things you would like to investigate here- and this is actually like my earliest question about the kind of artifacts was not about publication um and by you, suggesting this I'm a problem to tackle. Actually, you answered my question already, so would you like to verify the correctness of this API because, like I want for the most part apis? Don't have a correctness notion in in themselves right.

A

So what I would again what I'm I can imagine that it's possible that various combinations of IMAP instructions using the search commands could produce interesting the odd results. So, for example, apparently, if you do a search, one of a message is part of the results and in parallel, a different user agent, move that message to another folder and back.

A

You end up with different uids for the message, and so the results are no longer correct um and, and there could be a whole bunch of other Corner cases that people who Implement mail servers probably know about, and there are clients I'm not aware that anybody has tried to prove anything about it and it's a relatively simple problem to understand, I, think and if people could apply their formalisms to it to this and then demonstrate how you do it I think we might have a good bit of learning.

B

A

L

Hello, um so uh yeah, so one of my comments was like the produced you speaker or was that we need to know exactly what property we want to uh to show to prove here, but I wanted to talk about something uh slightly uh highlighted. So um as an engineer, I am interested in the usability of things right. I am interested in that.

L

What are the white formal media I should do that are usable for me as a as an engineer, all right, the problem of usability is that this is in the eye of the Builder right. We, okay, sorry.

L

Is that what is usable for me is not what is available for another engineer or for another researcher of offers. Someone else right and the problem with usability is that nobody can convince me that something is used as the devil right. I have I, don't know what this thing is continuously flipping.

L

So the only way for me can you hear me.

A

L

Yeah, okay, so the the.

L

Sorry, I am interrupted by stupid Bowser, which is uh doing wrong things um yeah. So the only way for me to be convinced that something usable is to see it right is to see a use of a formal, specific or reformal method for a specific things right, and this is something that we do all the time with programming right. The advantage of programming language is that there is a lot of resources with chip books and so on. This is not true for formal method.

L

uh In any books you want to buy on formal method is really expensive. There is very few resources for that.

L

So I think that this exercise is a very interesting one, because it would bring me where to judge the usability of something on the problem that I know about which is, in this case uh IMAP right, so I think that uh what would be really interesting is to have this this one or another, I will say a little bit about this uh after is to have um this uh thing with the property proven in many many different, formal wizard right with the source of the variable.

L

Well, one of the problem also is that a lot of papers that are used with Tamarind and all is that you don't have access to the source. You don't see how this thing from your eyes. You don't see the proof and some few exception you have nowhere to judge if this formalism is easy to use or or honor, so I would really uh encourage to to choose one to um to put somewhere I put uh it's like Rosetta could, if you know Jose Taco. This is exactly the same.

L

They have one problem and it's Elementary with all the possible programming language. So, in my opinion, it would be very useful to have that to show to let people decide if it's usable or not for them about the example of IMAP. Personally I would have a slight preference for uh the protocol, which we already know. That is wrong. That is incorrect for some property, because in this case we don't have to do the formalism and searching if it's true or not at the same time, I think it would simplify a little bit. Thank you.

L

A

I

All right put my setup uh I'm still hurtful and getting ready to do something, but uh I would say that I think this is a IMAP. Has a nice feature that it's clearly something a lot of people care about? It's like real world, but if I were to get a student to do something like this I mean if I just ask them to go. Look at the IMR part of C. It just scares the hell out of people and we.

H

I

This before it's uh just to understand the context around this search is already too much. So if, in such a problem description, we could also like offer from the engineering or the ATF side all right, you know what we'll just frame for you, this minimal thing in even in text or we'll just extract out the relevant bits of the rlcs. This is all you really need to know and formalize and.

F

I

It then you get to say that oh I actually formalized a chunk of the IMAP as extracted by experts of the internet. So it's not like completely a fake thing that I analyze, but I, don't actually have to go and learn everything so I mean making things a bit more self-contained would I, think attract would be, would make it possible to put a intern or a student, or something like this on a project like this I think, which is the way I see this going forward.

A

Yeah yeah I absolutely agree, that's why um you know if, if we did proceed with this problem, I think the first thing to do uh would be to kind of figure out a sensible subset of not even IMAP, but just a sensible subset of IMAP search and document that, in a way that's consumable for the you know a student you might ask to try and Tackle this person um and I I think the point that Mark just made also was probably a good one, is trying to include something that's problematic in the subset you document that we know about that would be.

A

That would be a good thing and I don't know if there is such a thing or not associated with IMF search, uh so Karthik did I hear you promised to put a student on this if we can produce a crisp definition, that's useful for a student.

I

A

Will certainly advertise.

I

It to the groups of students, I supervise, who often are looking for a project which will have real world impact, but just don't know how to get started. So, okay,.

A

So a possible promise for the future. That's that's probably as much as we can ask so. I just want to check. Also are there other problems that people have in mind that we might be worthwhile? Having trying to encourage the research group participants to investigate.

A

You know again this it's it's entirely fine to have top of the head answers here, and especially if people are willing to have a look at something between now and the kind of next ietf meeting time frame, so Mark yeah.

L

uh Yeah so uh one protocol that I one thing that I propose to uh formalize was RFC 3261., which is super, and the reason for that is that there is a lot of bugs that were discovered in RFC 3261 and that were fixed right. So there is at least two figs that were done, and this is uh in the state machine. uh There is one set machine which was absolutely wrong: well, actually wrong, so it could be a good place.

L

I I am yes, obviously, because I work for the last 20 years with a ship, so I know the Fig there's a thing very well, but it could be an example of something to formalize. That we already know is wrong. We know exactly what is wrong and we know that was fixed and there is multiple papers that that you can think with people all finding the same error on explaining the seminal.

L

So, as I said, if we go to the with the ideas that we can have, multiple different formalism to formalization is to be able to compare them. This could be a simple things, because now we don't have to search if it's wrong. It's wrong. It's! It's obviously,.

A

Great thanks, Mark Felix.

B

Yeah first before I make my extra remark um I'd like to comment on Woodmark just set so I think it's I mean it always depends on what the goal is of. Why are we looking at something with formal methods and uh especially with with existing problems? I think you know it's.

M

B

You often run into the problem of knowing what you look for and then all of a sudden, the tool Works remarkably well um so I think it's better to go to explore something that we can sell to other people uh and for that reason, I'd like to support the IMAP idea a bit more and secondly, um no, my my actual common food to erased my hand you're asking for of the top of my head ideas about uh about.

M

B

Things to work on so what I work with the Tamara improva, so I use former methods for security and what I found very interesting and I I knew about it. But it wasn't on my mind. Anymore, is former methods for correctness right and I guess this is much more.

B

What you'd go for uh with the IMF example in the for security um part I recently was wondering how little protocols, actually uh like specifications, actually have a usable um security section for former modelers, so I think all the specifications need to be a bit more usable for people who want to investigate the security we recently.

H

B

A master thesis presentation where the student analyzed some protocols and the the security goals were just you couldn't understand it and hope. Half of the work of that student was to actually come up with sensible security definitions.

B

I talked to a colleague about this already and they pointed out to me that there is an RFC already on how to write security uh sections in in rfcs something along those lines, and it is okay but I, wonder I, wonder where the Gap is. You know, especially because often oftentimes, when you, when you look through ifcs, I yeah I, still will not. Okay,.

F

B

Are they actually doing and figuring out why people cannot write these sections would be or or do not write.

E

This section- maybe they can but like.

B

Yeah why people don't do not write? These sections would be something interesting too. This is a much less actionable proposal, um I think you're, so much concrete, but it is.

E

B

A

Yeah sure, yeah and I I totally agree that uh aiming to figure out what the hell is, the meaning of security consideration, sections of rocs. That's a very much a variable thing, so um uh Jonathan you're thecube.

D

Yeah yeah I wanted to uh absolutely second that most uh rfcs that I've ended up analyzing. The uh security considerations do not appear anywhere in the security consideration section, um and you know you mostly find smeared across in large document.

D

um I I do things like maybe further down. The road we could think about. Is writing something like a BCP on how to write a security sections but I think before we can do that. We'd first have to uh have something sensible to say um like I, we we we definitely know when they're good, and we definitely know when they're bad, but there are a lot that are sort of in between.

D

So uh when we've got something useful to say, I think that might be worth trying.

A

Sure and bear in mind, of course, that pcps are things for the ietf and not the irtf as well. Etc, um okay, cool uh uh any other. Take some of this. uh So let I I think, and there is a tool called the show of hands tool.

A

um I'm going to ask a question using that, because to see, if I can elicit more input.

A

uh And let's see if I've done this right because I haven't done it for a while, so the question here that there's a show of hands tool that you can click on and the question is: should the research group spend time trying to identify and document the sample problem, whether IMAP or something else, um and if you click the raise hand button?

A

If you think spending that time would be useful that and if you think that spending that time would not be useful, then click the do not raise hand button and in the nature of these things, uh it's common to try and ask at the end, if somebody is in the contrarian kind of side of the poll, uh if they're willing to say why, but actually we have zero at the moment so that doesn't Supply.

A

So we need to stay that running for a second more and we can just so. We can document the results it looks like we have about 33 people in the meeting and about 21 people seem to agree that trying to spend time identifying and documenting a sample problem is worthwhile. So that's good.

A

I think probably yeah well I'm open to people making other suggestions, um but a question might be well I, don't know Jonathan I'm, not sure. If you have any thoughts. Maybe the best thing to persuade proceed to this is to just bring that up on the mailing list um and see if people you know with a bit more consideration, have other ideas for um what kinds of uh sample problem to work on Etc.

D

A

I think bringing.

D

It up on sorry, I think bringing it up on the mailing list is probably going to give people enough time to uh think about uh other sample problems, but I am quite a big fan of the IMAP search. One I think that's quite a if we can scope it well. I think that's quite a good choice.

D

J

Oh yeah I can figure out how to work. This eventually um I mean there were a couple of comments earlier about some of the different classes of uh problem. You know, you know proof of correctness versus a security proof, for example, uh I'm wondering if, if um we should maybe give thought to the different types of things, you can prove and try and identify a couple of a couple of different classes of problem. You know maybe a straightforward security thing versus a straightforward correctness: Thing versus whatever else there might be.

A

Yeah, okay, good points, so I guess, as we yeah as we um I mean I guess with you know as chair as we can take an action to try and craft a mail to the list. Saying uh you'll be kicking off this discussion and I think that's a that's, a very fair aspect that we should include as people think about what to do.

A

Okay, I, don't see anybody else in the queue Colin I think you're able to drop from the queue where I can boot. You um um in that case, I think we've covered this topic unless somebody else wants to Jump On, In and I. Think the next one is Jonathan.

N

If I'm correct.

A

It's always very.

D

A

D

You sure am I sharing the slides or are you um I was going to, but you look like you've already done it. So, okay.

A

So that I can give you control, so uh there you go now. You got control all.

D

Right, thank you, okay. So this is basically a talk. That's going to say these are the issues I think we have currently in formal methods that make them not less usable, and the goal of this is for people to first uh say no I, don't think that's an issue or to say oh, you've missed out this other big issue and then second for people to say this is a thing we could work on, that we could actually achieve so this slide.

D

This uh deck has eight slides in it, uh but about 15 words, so, hopefully, I'm gonna get lots of uh audience participation.

D

um There we go so I would say the currently biggest issues are issues with tooling uh pen and paper proofs issues with publishability issues, with training and issues with verifiability uh and I'm going to quickly go through all of those and then hopefully, I will have a cue.

D

um So when I say tooling, I think one of the biggest issues is a lot of the tools have uh UI ux issues that make it very difficult to achieve a proof that you want um and that's not related to the functionality of the tools. We have lots of tools with amazing functionality, but there are a lot of issues with UI ux that make it incredibly difficult to actually use them. You know even things like color palette choices, making it impossible to see what the tool is.

D

Trying to tell you um the next one that I think is really uh important and I think the only solution is to stop doing. This is uh pen and paper proofs, um pen and paper proofs are much easier to write down, but as they become longer, they basically stop being proofs and just become proofs by assertion.

D

um When I uh I recently saw a paper which had an 80-page algebraic proof in it and the when the authors uh send that for peer review, uh no reviewer has the time to go through and actually check an 80-page security proof by hand, and so I think. The one of the things we need to do is make it so that the tools are so good that nobody would choose to do. A pen and paper proof Stephen.

A

uh Just another question: did you want questions as you go or or I.

D

Don't know that would be ideal. Yes, uh okay,.

A

In that case, I even have a question, uh so I can I. You know what you say is clearly something with which it would be hard to disagree um in this in the context of This research, you know how would how would improving the situation with better and paper proofs? How would that manifest itself in the research group? What might happen so.

D

Let's encourage.

A

Other people to jump in and and interact on on this as we go.

D

For sure, um so the thing I really think uh I mean to sort of put my cards on the table. Obviously, what I think is no one should do pen and paper proofs um in practice. What I think that means is the onus is on uh tool developers and the users of these tools to make the tools so good and so usable that people would choose not to do a pen and paper proof.

D

um You can't force somebody to not do it. uh The only thing you can do is say here is a tool that is so good that you would just do it naturally in the tool um and like has good training, materials and so on, um and so I think this sort of is a goal. Maybe for This research group is we where we know we've achieved usability when we see people using the tools, and we see people not doing pattern paper proofs anymore.

D

um uh uh Any other comments.

D

uh Crispy uh Chris Patton, sorry.

O

Yeah, sorry I just uh oops, sorry I, just clicked all the buttons uh trying to get myself to talk. um I just wanted to say in defense of pen and paper proofs. um They are uh a good way of doing just your own security analysis of your protocol. If you can do it, if you can convince yourself, a reduction can be done, then your increased confidence but I I mean I.

O

Think the end goal should be a uh a a machine, checkable proof for sure, um but I think along the way people are still going to write them. um I I, wouldn't ever I I can't imagine, starting with the mecca trying to do a mechanized proof.

O

um That's said: I have I I lack any experience with these tools.

D

Yeah, so I I completely agree that, like doing a proof sketch is 100 necessary. uh Certainly if I'm trying to do a proof in Tamron or anything, obviously, I start on paper uh or on a whiteboard actually, but that that I totally think of as a sketch and not as this is actually uh something a product that I could show to other people, because I don't think it's actually a proof. I think it's a shape.

D

I'm not getting any sound.

E

F

Is uh that uh the training material should be part of the user experience, because, most of the time, documentation is not a learning material, so they just write down all the features, but that's not how so they don't tell you how to carry out what you said amid the size proof.

F

Okay, that's it yeah.

D

I I think that's very true. I think uh documentation and training materials are both important and are definitely different. um Chris.

G

Yeah, yes, so um when, when working with ssps on paper, so one reason I wanted to work with ssps was that code of key exchange protocols was so huge, so so that you know like if you want to come even close to the real protocol. I'm, not even talking about an actual implementation, but just like have all the protocol features it. Just it's just too much and um maintaining a huge code base on paper on a paper proof! It's it's! It's! It's absolutely absurd.

G

Like you, you change your article here in your latex document and then you need to change it and all the like. You know 15.

H

G

Where it shows up in your proof, so whenever you have a huge like code base of a huge protocol to to deal with it's it's, it's it's absolutely painful on on paper, so so I think that um when the objects that we prove things about are so huge that we cannot keep them in memory, I think this is really a point. When um you know this tooling really really makes things easier, and- and you know it hits this point where doing a pen and paper proof is just it's just no fun.

G

Of course you still use pen and paper and developing the proof, but um I think for for really large objects. um You you, you will want to to use this kind of tooling. So that's yeah! That's.

H

Just where we come.

G

From from this frustration of of saying no, you cannot do this with pen and paper, so um just just to say that uh I don't know.

D

Yeah um with pen and paper um I I'm, this is just my feeling with pen and paper. What I have to keep in memory is the formalism and the whole proof set with a machine checkable proof all I need to understand is the formalism and then the computer says yes, is sufficient right. I! Don't need to understand how the mechanics of the proof behind the scenes work? That's not even interesting to me! Well it! Actually.

D

It is interesting to me in a completely different sphere, but the um I I care very much that this is what we have proven and I think that's the the key thing pen and paper proofs require too much memory space to understand.

D

um Are there any more comments on pen and paper proofs or should I move on Felix.

B

Maybe not really.

I

A common opinion.

B

Paper, but why is Isabel the tool you're looking for.

D

Isabelle Hall.

B

D

um I I have to admit I've, never particularly tried it as well, um but the tool I use is is tamarind um and um it has some really bad UI ux issues and I would use Tamron a lot more and for a much broader range of things. If I could fix those issues, um and so there I think one reason: a lot of people don't use machine checkable proofs is the tools can't handle it and not. For reasons of like this is unprovable or they don't have the feature.

D

But because of the tools have you know, issues bugs whatever uh Chris.

G

um I was, can you hear me all right? I was actually thinking that um kind of Tamarind is is.

G

Is one of these good examples like I I thought that you know like I, saw multiple people with minimal support and background um learn tamarine, essentially by themselves from the documentation, uh analyze and model very complicated security properties, etc, etc. So so um I like I and- and you know like make sense of these graphs Etc, so I thought tamarine was actually one of these very good examples in terms of usability and user experience,.

D

So I well as much as I like to hate on Tamarind. um It is the best tool in my opinion, um that doesn't mean it's good. It just means it's the best.

D

um You know it's it's things like you know it produces those very pretty uh like State diagrams of where you are on your proof uh and the boxes you might not have noticed. This have different colors and they're.

D

All very different, slightly different shades of green I was using Tamarind for three years before I even knew that those colors were supposed to be different and they're supposed to be providing with semantic information to me that information was just not there, because I cannot see right that I couldn't even see that they were supposed to be different right, like that's I and like that was a choice in the design easily fixable that there actually is like a branch that has a way that lets you change the colors, but, like that's a usability issue that has nothing to do with the technical tool.

G

Right, sorry, is that the like, so that that's oh.

D

I can keep going, there's like a dozen of them, but okay, but uh but you know, as an example like um or you know, the another one is uh when you get to a big proof: um it reload repaints the entire screen for every step you do and um the when you're doing the TLs proof. When you get to step 749 9999, it takes several minutes to render a one-line change on a machine with a decent GPU.

D

It takes several minutes to render a one-line change like you, don't need to change, reload, re-render, the entire proof right by definition, it's not changing anyway. So issues like that which are nothing technical they're, just like UI issues, right thanks, um okay, any any more pen and paper proof comments. No, in which case I have a few more slides.

D

um Oh yeah. This is another one that annoys me immensely um publishability, um quite a lot of formal analyzes and then yes, this is fine or we didn't find any major bugs, um and even if you go to journals that say, oh yes, we accept negative results.

D

You'll be told, your proof is not novel, and it is very, very hard to get your proof that this is okay published, um even though that would be very useful for the community to say here is a demonstration that this tool is that this protocol is secure um and we can use it, um and so what I've taken to doing is sneaking formal analysis into papers, deployment papers or systems papers, um which means they don't really get checks by somebody who's an expert in formal analysis, but it is basically very difficult, if not impossible, to publish results that are not.

D

uh We broke this protocol, um any comments on these publishability or actually, let's just come back to the end of Felix sure.

B

Yeah I I know what you mean, and you definitely have a point, but I still would like to argue against that point. A bit um from my experience, my limited experience in publishing you have a quite High barrier for a security, critical designs in publishing that you could publish as a design and that get often rejected. If you don't come with formal proofs I think even non-formal people start to get a better feeling of kind of which designs are in the ballpark of being provable right like if.

N

B

A brand new OS OS thing right, usually people don't say: oh, you should get a proof right, but if you design a new protocol, I think you could get rejected for not having a form of proof um which just means we have a problem of verifying the things that are already around because in that space there definitely is an issue in publishing positive results.

D

Yeah um so I I agree. Yes, if you are also publishing the design, but quite often a design has been published and someone says: oh, can you do an analysis of that and I'll check it I'll, say yeah. It looks great, never gets published, like the the DC paper, which I'll talk about the DC presentation that I'll talk about at the end.

D

um I I did that analysis. Like three years ago, I tried to get it published for a year and then gave up.

D

um Okay, next slide there we go um I think this is one that we really can work on um training.

D

um Oh on the previous slide. uh The thing we could do is we could publish these artifacts ourselves uh uh training. uh A lot of people have told me: oh I tried to do a formal analysis, but I couldn't get the tool to work or I. Couldn't I I got a state space explosion and I didn't know how to fix it um and there's sort of nowhere to go between.

D

uh This is a really trivial example and This Is Us, using all kinds of weird hacks, to trick the tool into working that you wouldn't necessarily know how to use um and I think one thing that would be really worthwhile for us to work on is say here are some like intermediate difficulty examples and we sort of just host them on the wiki or some kind of articles um there we go yes, uh another one is verifiability and I. Think oh Steve, so.

A

Back on uh Jonathan on training, yeah.

A

I'm just trying to form a question, probably yeah. What kind of timeline would make sense for the research group to try and make progress on? That is this something that we could try and encourage people to produce some training materials in the near future. Or is this something where it's kind of gonna have to happen down the line? Some.

D

um I mean one interesting to me would, and this is me uh postulating standing on one foot, but you know we could do a hackathon training session right fairly cheaply uh at itf117, for example, or we could do something more. uh You know just the producing the uh very simple example with multiple implementations in different languages.

D

um I think we could get started with that fairly easily, um because hopefully an intermediate example would only be a couple of days. Work to produce sign experts, um but yeah, so I I think we could definitely start seeing some kind of output before ATF 117. If we can find people who are interested and.

A

So I guess then the question is, um is anyone interested so is.

H

There anybody who.

A

Would volunteer I guess to try and put together some training materials that could be presented either at the the hackathon weekend before the ietf 117 or uh in some other way around that time frame, which is the end of July.

A

Does anybody want to jump up and say, hey I would be willing to do that.

D

E

Are you planning.

D

To go to the ITF in SF in San, Francisco.

B

Yeah, that was my I was about to write it. um This would be a Prague thing.

A

Okay, so that's the Prague is November this year. Is it I think so.

B

Yes, I I, don't know whether I can come, but I will definitely not come to San Francisco right.

A

Okay, so then, and so then modify my question and in the context of uh July or November this year, does anybody feel the that they'd be happy to do a bit of work to present some training on some of these formalisms that some people at an ietf meeting might find valuable.

D

F

D

I mean I just to make sure we'll have something: I'll try and put things together for rosette for November as well. If we're gonna aim for November.

B

I I wanted to volunteer with my with my last message.

A

um Fantastic physics, thank you.

D

uh Colin and then yaron.

J

Hi, so I I certainly don't have the expertise to volunteer anything. um uh It's it's strictly as well as sort of things like hacker funds. We might be able to find people who are at universities near some of the meeting venues and invite them to give you a tutorial.

J

You know if, if we have a have a meeting in France- and uh you know find someone at one of the relevant groups that didn't really invite them, for example,.

D

uh That's certainly an option. I mean Prague is relatively near France.

C

Yeah, it's pretty close.

D

Although annoying to get to by train um okay, I I think we'll take that to the list and see if we can uh arrange some kind of training.

A

M

Thank you so I'd like to try this idea into Steven's presentation and the idea of an example and IMAP um I think that successful training with people from across the ITF could lead to ideas that are more relevant, more more modern and more likely to produce actual failures than IMAP. And so.

M

A

D

A

Disappeared for me.

D

Yeah I I think you got to cut off your one.

A

But I I I I I. He can correct me but I think the point he's making was that if we had some such training that might help to identify better sample problems than the IMF thing suggested so far, that's a fair point.

D

Yeah um we could uh send an email to some mailing list somewhere I'm, not sure what it would be um and just say. uh Would people be interested in form methods, training, um bring your own problem along.

D

You know we'll just try and get some experts to hopefully be there and uh try and help them along okay.

A

I think the takeaway there is is try and try and aim for something for November.

D

Sounds good, uh okay, verifiability and then I only have one more slide um verifying uh these proofs once you're, given a mechanized proof uh can actually take quite a long time. The tls13 proof takes a couple of days to run on a fairly beefy uh gcp box or a cloud compute box, um and it can cost quite a lot of money to actually rent a box for that much time um and I.

D

Think for pen and paper proofs I've already mentioned, like actually checking on 80 page proof would take months, um and so these are sort of beyond the capabilities of peer review and I I. Think one problem with a lot of formal methods is no one ever actually checks that the proof is correct um in terms of things that we could do in this space uh uh they're. All this work from the uh zero knowledge crowd and all of the work into uh probabilistically, checkable proofs, um it might be worth thinking about.

D

Is there a way that we can produce an artifact that lets you check that a proof is correct, uh very, very cheaply um without having to uh rebuild the proof from scratch, um and so, if that inspires, anyone to I know kick off a research project that would be very cool um and I. Think I'm almost like yes, one more slide last slide.

D

um Does anyone else think something else is important or uh vital for reusability for usability um some suggestions at the bottom uh but yeah this is this is open floor? Is there something else that you think is making formal methods unusable or difficult to use.

D

B

Yeah I have two thoughts before I answer. Your question I'd like to comment your last Point regarding verifiability, so I completely share your concerns that former proofs are often not looked at enough, um but I I'm, not sure. If this is the biggest problem we have because, like the you, throw the model and proof at a machine and it returns true or false, I I.

B

Don't think that this is the the problems that um I think many proofs terminate, because most authors, I, hope and I believe are actually honest enough to to make them terminate and uh malicious or like a malicious author, they could cheat in other ways, which is like.

E

B

Tiny details of their model, so I think the problem is rather like. Are your assumptions are well documented and are they like? Is your model actually matching the real world? I think this is a much bigger problem and there you just need to put in the time um I.

D

Don't think so, I I think with TLS 1.3.

D

That's a quite a good example in point, um our proof, um you you, we published our proof uh any of the reviewers could have put that into a you know an AWS box and run it, um but it would probably have cost them at the time more than five hundred dollars and so I would I would bet money that none of our peer reviewers for that paper actually did that and I think that's actually quite a significant failing right like we're supposed to have been peer-reviewed, but actually no one, and it's not that we were being dishonest or that our proof doesn't terminate it's that.

D

Actually, it's just a really long proof.

B

Yeah yeah I know, but you know, even if you were dishonest and you're proof wouldn't terminate, and you knew that your peer reviewers would check it. You just cheat in your model so that you approve just terminates right. It's not hard to make a proof, terminate it's hard to make a meaningful proof, Terminator, um that's what I'm, what I mean and now I to your question about other things so and again, a very high level thought, but I think uh it.

B

Maybe this connects a bit to understandability, but I think a lot of formal methods tools suffer from their low levelness of their input languages right. um They are more often more. The you're often very close to the mathematical Concepts that underpin these tools and so to know to know, for example, how to implement a loop in Tamarin right. It takes some. It takes some mind, yoga um and I.

B

Think it's super tough to to make this better, but in an Ideal, World I think many formal methods tools would provide more abstractions out of the box that match the intuitions that Engineers have of the systems.

D

Yeah, that's that's interesting, um although how you would achieve that without building some kind of transpiler I, don't know like that. That sounds like a very difficult challenge.

D

um Any further comments, thoughts, ideas.

D

um Anyone think anyone have any suggestions for how we can tackle any of these uh topics or others or things that we can actually contribute here.

A

So so I guess we have one concrete thing on the training. Is that a few people who are interested in doing something in the November time frame? That's good.

A

And I think that was yeah yeah.

C

Okay, um I think in so when I dealt with Tamarin. It allowed me to I think really generate proofs um that were supposed to be easily and quickly verifiable, but I think when I try to do it on a later version. A few months later, it didn't verify anymore. So maybe this is not worth it, but I think that also was like four years ago or something um another thing I think smt lib is, can give you onset, unsatisfiability proofs, um so yeah I think to some degree, like the foundations, already provide the features.

C

So maybe it is just a question just in in quotation marks a question of like developing the features and the.

J

D

Yeah um the particular thing about verifiability was I was just uh very inspired by uh some of the zero knowledge proof systems where you literally just send three um elliptic curve points, and suddenly you have a you can be sure that every step of this huge proof was run correctly and so I can verify. The proof was run correctly and, like you know,.

H

D

Rather than days of expensive computer time exactly and like recursive snarks and all of that, like fabulous Magic.

D

um Any any further comments on things we could actually do. Chris.

G

I

G

That we're potentially interested in contributing to training, but not at the point where we can commit to anything, because this is a major time commitment to produce a reasonable teaching material.

D

Well, yeah I mean: would you be willing to show up in November and uh just like help out with people who come up? Who show up.

G

Well, if we have a tool that is published by then I mean.

G

So I think it's too early to make a commitment that it's it's a. Is it possible to jump in later for sure, okay,.

D

um Okay, I think that's everything.

D

um Are we gonna go with the Earth time permits.

A

I, especially maybe at the time where time doesn't promise.

A

I just wanted to go back to the chair, slides, uh very good one. Second, um so we look at our agenda. I think we've covered the the first bunch of things.

A

uh I I I think we're going to have to delegate uh to the next time for delegated credentials, um but what I did want to just check is that uh are there things people want to work on in the research group and would be interested in trying to collaborate with people or just do it yourself, but especially if they haven't been mentioned, um you know I. Think we'd, like to kind of start, uh as the research groups get going see the level of activity kind of bump up a little bit doesn't have to be.

A

You know, going at 100 miles an hour but uh be nice to see things happening, so in particular, if there's things that didn't come up already today um that you would be Keen to work on, um especially if you're looking for people to work with um it'd be really good to hear about that now. So if you, if anybody wants to join the queue and go to the mic and to say you know, I I want to work on this and we haven't mentioned it. Yet. uh This is the time to do that.

A

We have a few minutes so.

A

So I don't believe that we've mentioned everything that people might think of working on um some. Perhaps that indicates that people are after nearly two hours in the meeting or a bit kind of tired of it. But.

A

You know there's the opportunity to to kind of speak to the group of 29 of us still here saying uh that you think such and such a thing is worth working on.

A

That, with crickets.

F

J

um So any particular thing that I want to mention now, but, but maybe one of the uh the things the group could be doing, is helping to um so capture a list of protocols where people want input um as well as a list of techniques and things where people can can. You know, be trading out particular techniques.

A

Yeah fair point and I mean so I mean we could probably try and address that by trying to organize to do another pass on the wiki I know, I. Think Chris Wood did a bit of work on the wiki previously.

E

A

And so you know that uh we could, we could probably try and arm twist there Abyss. uh Is he still at the meeting or is gone? Maybe Chris is gone.

J

N

J

Mean you put collecting the stuff on the wiki. Wiki is really important, but also just highlighting in in meetings and various ATF venues. You know if people have protocols where they need to need input. This might be a good way of connecting protocol designers to people with formal methods, expertise, sure.

A

Drop thanks, Colin, um good points and so I don't see a pile of people jumping to the microphone I, don't I I, don't think we have time to do justice to your delegated credentials. Presentations doesn't I.

D

Yeah I think perhaps not.

A

So I guess that brings us to the uh any other business kind of part of the agenda that wasn't there, but it is now um so do we have any other business that people would like to bring up complaints? Things are you know things you hated, uh you want. The chairs replaced already nothing at all like that. No.

A

E

A

Think we have a couple of actions: uh I just wanted to check. um As far as I know, Felix and Karsten were helping. Take the the excellent notes um if I'm missing somebody there. Please tell me your name or add your name to the note takers, because it's always good to credit people for doing that, um and otherwise I think we are not uh Customs. Yes,.

N

Yeah I just wanted to say that many of the notes are from a person who knows nothing about formal verification. So you may want to read those notes uh before I completely misrepresent what you were trying to say.

A

Okay, Carson I'm, I'm I'm highly confident in the capability of your note-taking, so I'm sure it'll be perfect, but we will certainly uh give them a good look over before we hit the publish button on them.

A

um Okay, so we're giving the number two minutes to the error and I don't see anybody else in the mic line. I guess I'd like to thank everybody for joining, um especially the people who've made presentations, uh we'll kind of stroll through those notes, look for the couple of actions as chairs and try and bring stuff to the list uh with a view to meeting I guess sorry. I should check we're we're planning to request a session for July ITF.

A

um If anybody thinks that's a bad plan, then just say so, um but our default is is the request a session, um but with that I think Jonathan anything else or are we.

D

A

M

A

Taking part uh look forward to doing more stuff on the list and in future meetings. So thank you and goodbye.

D

Thanks everyone.

A

All right so oh Jonathan's gone all right. Oh Jonathan he's gone. Yes all right, never mind.