# Usable Formal Methods Proposed Research Group   {#usable-formal-methods-proposed-research-group}

Note Takers: Chris, Joe

*   Agenda Bash (chairs, 5)

Agenda Bashed

*   Using Formal Methods at Google (Thyla van der Merwe, 10+5)

Yaron Sheffer: Complaints about non-backward compatible changes to
theorem tools, does that impact production code too?  
Thyla: yes, and I'll cover that shortly

Chris Patton: Is Google honing in on a small number of tools that they
will use? Or will it be many tools?  
Thyla: We're a small team, so will likely be a small set, but we want to
udnerstand limitations and choose appropriate tools  
Chris: So then in 10 years it will be that small set of tools  
Thyla: No, I don't know what tools or how large the group will be

Alexander: Can you explain the 20% speed up  
thyla: Yes, we had gnarly assembler, but the process of using the
verified tool chain made clean more optimized assembler

*   OWL (Joshua Gancher, 10+5)

Felix Linker: 1) Users don't specify security properties  
Joshua 1) It falls out of the type system  
Felix: 2) do you assume separate client and server? How do you handle
network layer?  
Joshua: 2) Specify the entire protocol in 1 file, a global definition;
then you can use the client and server separately. Owl assumes full
adversary control of network in its model  
Message reorder is built in

Chris Patton: THis seems like everything I want. As a cryptographer how
do I express N-CPA in OWL  
Joshua: Owl takes a different approach to computational complexity
compared to other systems; its baked into the type system. Owl comes
with crypto assumptions in its type system and you can extend that. It
generates properties like N-CPA.  
Orie Steele: How is computational security achieved, assumes type system
achieves properites? For what type system does htis work for Rust, Type
Script?   
Joshua: A very specific type system that doesn't exist in Rust or
Typescript. It's a very expressive type system that allows properties
that don't exist in regular languages. They inductive over Owl's type
system. You cannot replace Owl's type system.

*   H2 Reset (Lucas Pardue, 10+5)

PHB: I believe that you could model this with CSP, and what you would
look for is to see the traces were bounded in certain ways. What you
need here is to have better backend feedback. But its a system error,
not an error in the protocol.

Lucas: yes, feedback is very important. THis isn't a problem until it is
a problem. Depends upon resource limits of real things  
PHB: the problem there is getting into timed models.

Johnathan Hoyland: Glad you said CSP, because that was what he would
say; Tony Hoare, late 60s early 70s.  
CSP = Communicating sequential processes

*   Sample Problems, TEEP (Cory Francis Myers, 5)

*   Next steps/actions (chairs, 5)

*   Evaluation of IETF 118 training

Chria Inacio: Training was excellent, not sure the recording would have
value. Need to be to get the value

Chris P: I agree with CHris. Let's do it at the next IETF. Maybe
PRoverif next time

Jonathan: would you like other tools Coq and something else  
Chris P: no, Coq is too general

Gergley: more hands on training

Chair: Security tool focused training, or something more general?  
from the room, would like a more general tool  
Cory: Appreciated the training on Isabelle @ 117

Felix: Interacting throerem Provers are intimidating, maybe not the best
for introduction. to difficult

Orie: Proverif can be taught in a short time.   
Verifying structure of data formats. Is there interested if there is
alagous of schema alidation for protocols?

Muhannad Sardar:  
Should target intermediate training instead of initial training. But the
training seemed to have a lot of beginnners in the room on Sunday. Teep
found something during the Hackathon (maybe with Coq) but it was still
relatively basic use of the tool.