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 🙂

[domodwyer]

Hi there,

I have recently been working with a TUF-based system, and as part of that work I have produced a model using TLA+ that reflects my specific area of interest in the system.

The model is used to describe and verify a number of security and liveness properties with respect to the communication between a TUF client, and the TUF repo in the presence of a MITM attacker.

Specifically, even if the network connection is under attacker control, the clients:

• Only ever install attested files, or
• Are aware of DoS based on client-visible state.
• Never accept any metadata manipulated by the attacker.
• Are not vulnerable to mix-and-match attacks.
• Reject attempts to roll-back state.
• Support secure key rotation and revocation, even in hostile environments.
• Eventually get updates (liveness).

I'm happy to open a PR and share the model if it is of interest - if so, where would be best to PR to?

Dom

[JustinCappos]

Wow, this is very exciting! I can see a few options. If this is something you'd like to maintain in the (very infrequent) scenarios where we change the specification through the TAP process, we could make a new repo in our org to host this and make you a maintainer. The other option would be to treat this as a "finished product" and then accept this into an existing repo which has other maintainers. (In this case, we'll need to chat quickly to decide where to put it.) What are your thoughts about these two options? Regardless, I'd love to take a look at this, as may others @patrick Zielinski ***@***.***>. Does your verification exist in a location where we can check it out?

…

On Thu, Apr 3, 2025 at 6:34 AM Dom ***@***.***> wrote: Hi there, I have recently been working with a TUF-based system, and as part of that work I have produced a model using TLA+ <https://lamport.azurewebsites.net/tla/tla.html> that reflects my specific area of interest in the system. The model is used to describe and verify a number of security and liveness properties with respect to the communication between a TUF client, and the TUF repo in the presence of a MITM attacker. Specifically, even if the network connection is under attacker control, the clients: - Only ever install attested files, or - Are aware of DoS based on client-visible state. - Never accept any metadata manipulated by the attacker. - Are not vulnerable to mix-and-match attacks. - Reject attempts to roll-back state. - Support secure key rotation and revocation, even in hostile environments. - Eventually get updates (liveness). I'm happy to open a PR and share the model if it is of interest - if so, where would be best to PR to? Dom — Reply to this email directly, view it on GitHub <#271 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAGRODZWTM2HHVDWCQFRRIT2XUFDVAVCNFSM6AAAAAB2L2VOIGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDONZVGI4DIOJRGU> . You are receiving this because you commented.Message ID: ***@***.***> [image: domodwyer]*domodwyer* left a comment (theupdateframework/specification#271) <#271 (comment)> Hi there, I have recently been working with a TUF-based system, and as part of that work I have produced a model using TLA+ <https://lamport.azurewebsites.net/tla/tla.html> that reflects my specific area of interest in the system. The model is used to describe and verify a number of security and liveness properties with respect to the communication between a TUF client, and the TUF repo in the presence of a MITM attacker. Specifically, even if the network connection is under attacker control, the clients: - Only ever install attested files, or - Are aware of DoS based on client-visible state. - Never accept any metadata manipulated by the attacker. - Are not vulnerable to mix-and-match attacks. - Reject attempts to roll-back state. - Support secure key rotation and revocation, even in hostile environments. - Eventually get updates (liveness). I'm happy to open a PR and share the model if it is of interest - if so, where would be best to PR to? Dom — Reply to this email directly, view it on GitHub <#271 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAGRODZWTM2HHVDWCQFRRIT2XUFDVAVCNFSM6AAAAAB2L2VOIGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDONZVGI4DIOJRGU> . You are receiving this because you commented.Message ID: ***@***.***>

[domodwyer]

Hey @JustinCappos!

Either works for me - I'd be happy to maintain the spec if / when the relevant portions of the spec change.

Just to reiterate, it's not a model of the full TUF spec, but rather a "zoomed in" view of the client / server protocol (with signatures & concurrent key rotations). I am a fan of using a number of small, quick-to-run, focused models (as opposed to one giant model) so maybe having >1 spec over time (or even using other formal methods entirely) influences your decision.

Does your verification exist in a location where we can check it out?

Currently it lives in a private repo owned by Datadog - I can make a copy public on my personal repo shortly though if that helps.

Dom

[patzielinski]

Hi @domodwyer! Justin pointed me to this and it would certainly be interesting to take a look at as someone who's interested in formal verification of software. The others on this thread will know how to best integrate this into the TUF spec, but having a public copy we could take a look for now at would be great! (even if it's just a small portion of the entire TUF spec).

[domodwyer]

Hey @patzielinski - I've pushed a copy here: https://github.com/domodwyer/tuf-tla

[trishankatdatadog]

Having read this thread, I think it makes sense to place it inside the specification repo, provided that we always have someone who can correctly update the model every time we update the spec. What do y'all think?