Use formal methods to prove security properties

[Eh2406]

This is to start a conversation. I am hoping to nerd snipe someone who has the relevant knowledge into doing something I don't know how to do.

I think it would be very helpful to have a Formal Model of TUF. A mathematical model of the server and the client so that proofs can be generated of the security properties. I've seen a lot of questions about "if I just skip this step what security properties do I break", to which the answer is often "more than you realize" because this is a hard complicated problem, but is sometimes "just this one thing, if you don't care about it go ahead". It feels like a formal model would allow people to answer those questions on their own.

I have heard of https://p-org.github.io/P/ which allows modeling entities as state machines, which I think would map really well to the descriptions in the current specification. But I don't think it allows for proofs. I have had TLA+ recommended to me for doing proofs, but it has a far more flexible modeling language. I know that there are many other options available.

[Eh2406]

P now has support for certain kinds of exhaustivenest checking. https://dafny.org/ was also recommend as was https://tamarin-prover.github.io/.

[JustinCappos]

I also don't have expertise in this area, but would be happy to help others who have the right skill set with the process.

[trishankatdatadog]

Something to note is that even if you had a provable specification of TUF, that would not necessarily translate to the correctness of any implementation 😕

[joshuagl]

I don't have expertise in this area but am increasingly interested in playing around with using formal methods with TUF. To add to the list of possible tools, I recently learned of Alloy.

[tarcieri]

Alloy may be relevant here:

• paper: https://cacm.acm.org/magazines/2019/9/238969-alloy/fulltext
• latest release: https://alloytools.org/alloy6.html

It's a model checking language for software systems which can be used to automatically find software vulnerabilities.

It also has a visualizer, which could be useful for generating diagrams for the specification.

[znewman01]

I think this plays really nicely with another idea that's been floated: porting the TUF spec into a logic programming language like Datalog. Then, I think we could more easily reason about the correctness of an implementation using that language directly.

I'm planning on playing with TUF+Datalog over the next couple months; will keep the community posted.

[trishankatdatadog]

I'm planning on playing with TUF+Datalog over the next couple months; will keep the community posted.

Please include me on your experiments? Would like to work on this together 🙂