Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use formal methods to prove security properties #271

Open
Eh2406 opened this issue Feb 17, 2023 · 7 comments
Open

Use formal methods to prove security properties #271

Eh2406 opened this issue Feb 17, 2023 · 7 comments

Comments

@Eh2406
Copy link

Eh2406 commented Feb 17, 2023

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
Copy link
Author

Eh2406 commented Feb 17, 2023

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

@JustinCappos
Copy link
Member

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
Copy link
Member

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
Copy link
Member

joshuagl commented Apr 6, 2023

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
Copy link

Alloy may be relevant here:

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
Copy link

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
Copy link
Member

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 🙂

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

6 participants