Note Takers: Chris, Joe
Agenda Bashed
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
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.
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.