5 ms·

But how do you verify the formal verification?

by rcme 3y ago

mejutoco 3y ago
Proving in Math that the building blocks have certain properties.
- tialaramex 3y ago
  While this is worthwhile, there is an opportunity for the math to violate your assumptions in a way you didn't understand. Let's talk briefly about TLS 1.3 Selfie attacks. TLS 1.3 is the first TLS in which experts built a formally verified model of the protocol before they shipped the standard. There are models of earlier TLS versions, but nothing learned from them could be incorporated into the corresponding standard because they were an afterthought - like writing unit tests after shipping version 1.0 TLS 1.3 has a mode intended for applications where some nodes which have a pre-existing relationship communicate, in this case we don't need the Web PKI ("SSL certificates") instead we use Pre-shared Keys (PSKs) - that is all the parties know the keys anyway, which clearly couldn't work for the open web but is fine for my boiler and its remote thermostat since duh, I don't want some random other person's thermostat talking to my boiler. PSKs are also used when you connect to the same server again later, but that doesn't matter here. The mathematical proof seemed to say exactly what the designers wanted, and it passed. So TLS 1.3 is exactly what we wanted... right? Well, almost. Designers were thinking of symmetries like "Alice talks to Bob" and "Bob talks to Alice" as one conversation, but the proof thinks that's two conversations. So the proof thinks Alice and Bob need two keys, the Alice->Bob key and the Bob->Alice key, while humans assumed they only need a single key, an Alice-x-Bob key. And so the RFC documents (prior to errata) the human assumption but the protocol actually requires the machine assumption. The result is the Selfie Attack. In our scenario Alice, and Bob have a Cat. The Cat, like many cats, would like more food, but Alice and Bob use a secure protocol to ensure they only feed the cat once. Bob has fed the cat and left. The cat is sat by an empty food bowl looking plaintive. Alice sends Bob an encrypted message, "Did you feed the cat?". The Cat intercepts the message, it doesn't have the Alice-x-Bob key so it can't decrypt this message nor directly answer it, but it doesn't need to. The Cat simply sends Alice's own message back to her. Receiving a message encrypted with the Alice-x-Bob key, Alice concludes it's from Bob. "Did you feed the cat?". So she replies "No, I did not feed the cat". The cat receives this message too, and directs it back to Alice as well, now Alice has what appears to be a reply to her first question, "No, I did not feed the cat" encrypted with the Alice-x-Bob key. So, Alice feeds the cat again because the cat was able to trick her into answering her own question.
  - pritambaral 3y ago
    I like your simplified example, but it does miss an important nuance: Alice has to act as both a client and a server, must use the same PSK for both roles, and must not (or not be able to) check the sender or intended recipient of any message. TLS handshakes were never designed to be symmetric. Every TLS connection is clearly between a client and a server. Alice and Bob, both running a client and a server, where both servers use the same PSK, is not a TLS setup. It's two (2) separate TLS setups. The math was never intended to verify if sharing PSKs across independent unrelated servers is safe. In fact, the Selfie attack is not really a "selfie" attack; it works even if Alice hosts only a client and no server, as long as there exists an Eve that hosts a server (but not necessarily a client). > Designers were thinking of symmetries like "Alice talks to Bob" and "Bob talks to Alice" as one conversation ... I strongly doubt that. A TLS connection, once established, is symmetric, sure, but a TLS handshake isn't. The failure mode in Selfie isn't in the post-handshake domain. It's not like Selfie allows you to take packets from an already established connection and play it against an unsuspecting server that has no connections, and thus making it think it has a connection. The failure is literally this: Alice says "Hey I wanna talk to you" intended for Bob but doesn't specify who, exactly, are "I" and "you". The Cat records Alice's speech and replays it to her, making her believe someone is trying to initiate a new, separate conversation. The verifiers writing the proofs would be acutely aware of the asymmetrical nature of TLS handshakes. In fact, I strongly doubt they even considered any case where the same entity hosts both a TLS client and a TLS server for a shared purpose.
    - tialaramex 3y ago
      > I strongly doubt that. That's nice, but I'm reporting historical fact. https://eprint.iacr.org/2019/347 https://eprint.iacr.org/2019/347 This is Hacker News, where people who know nothing about a topic come to tell each other about their expertise. You believe no-one would make this type of mistake, I know they did and I have just provided you a link to the paper at the time. Alas some people will believe you, and they will assume that they too are infallible and the rest is inevitable. What did Dorothy Parker say about Horticulture ?
      - 3y ago
szundi 3y ago
You know having some bugs in there is not that problematic as even if they stay in the shadows, most product bugs are catched anyway. Also these make false alerts, then instead of fixing the nonexistent bug, they fix the test suite.
tzs 3y ago
In the case of formal verification done with proof assistants or similar, I believe the way it works is something like this. The people who develop such software start out writing a verifier for a much system of logic or programming than what the final system will handle. This first system is sufficiently simple that the verifier that can verify programs in that system is very small and straightforward, so that if several humans look at it and can't see any bugs it is almost certainly correct. Then they write a verifier for a more expressive system. This verify isn't as small or straightforward and so even if humans don't see any bugs we can't be confident that there none. They then use the first verifier to verify the second verifier. The formal proof of correctness might be long and difficult to develop because it can only use the reduced logic of the first verifier, but once they manage that and the first verifier verifies it, they can be confident that the second verifier is correct. If the system the second verifier still isn't expressive enough to verify the things they ultimately want to handle they write an even more expressive system, and use the second verifier to verify that. Repeat until you've got the system you wanted in the first place.

But how do you verify the formal verification?

by rcme 3y ago

But how do you verify the formal verification?

mejutoco 3y ago

Proving in Math that the building blocks have certain properties.

tialaramex 3y ago
While this is worthwhile, there is an opportunity for the math to violate your assumptions in a way you didn't understand. Let's talk briefly about TLS 1.3 Selfie attacks. TLS 1.3 is the first TLS in which experts built a formally verified model of the protocol before they shipped the standard. There are models of earlier TLS versions, but nothing learned from them could be incorporated into the corresponding standard because they were an afterthought - like writing unit tests after shipping version 1.0 TLS 1.3 has a mode intended for applications where some nodes which have a pre-existing relationship communicate, in this case we don't need the Web PKI ("SSL certificates") instead we use Pre-shared Keys (PSKs) - that is all the parties know the keys anyway, which clearly couldn't work for the open web but is fine for my boiler and its remote thermostat since duh, I don't want some random other person's thermostat talking to my boiler. PSKs are also used when you connect to the same server again later, but that doesn't matter here. The mathematical proof seemed to say exactly what the designers wanted, and it passed. So TLS 1.3 is exactly what we wanted... right? Well, almost. Designers were thinking of symmetries like "Alice talks to Bob" and "Bob talks to Alice" as one conversation, but the proof thinks that's two conversations. So the proof thinks Alice and Bob need two keys, the Alice->Bob key and the Bob->Alice key, while humans assumed they only need a single key, an Alice-x-Bob key. And so the RFC documents (prior to errata) the human assumption but the protocol actually requires the machine assumption. The result is the Selfie Attack. In our scenario Alice, and Bob have a Cat. The Cat, like many cats, would like more food, but Alice and Bob use a secure protocol to ensure they only feed the cat once. Bob has fed the cat and left. The cat is sat by an empty food bowl looking plaintive. Alice sends Bob an encrypted message, "Did you feed the cat?". The Cat intercepts the message, it doesn't have the Alice-x-Bob key so it can't decrypt this message nor directly answer it, but it doesn't need to. The Cat simply sends Alice's own message back to her. Receiving a message encrypted with the Alice-x-Bob key, Alice concludes it's from Bob. "Did you feed the cat?". So she replies "No, I did not feed the cat". The cat receives this message too, and directs it back to Alice as well, now Alice has what appears to be a reply to her first question, "No, I did not feed the cat" encrypted with the Alice-x-Bob key. So, Alice feeds the cat again because the cat was able to trick her into answering her own question.
- pritambaral 3y ago
  I like your simplified example, but it does miss an important nuance: Alice has to act as both a client and a server, must use the same PSK for both roles, and must not (or not be able to) check the sender or intended recipient of any message. TLS handshakes were never designed to be symmetric. Every TLS connection is clearly between a client and a server. Alice and Bob, both running a client and a server, where both servers use the same PSK, is not a TLS setup. It's two (2) separate TLS setups. The math was never intended to verify if sharing PSKs across independent unrelated servers is safe. In fact, the Selfie attack is not really a "selfie" attack; it works even if Alice hosts only a client and no server, as long as there exists an Eve that hosts a server (but not necessarily a client). > Designers were thinking of symmetries like "Alice talks to Bob" and "Bob talks to Alice" as one conversation ... I strongly doubt that. A TLS connection, once established, is symmetric, sure, but a TLS handshake isn't. The failure mode in Selfie isn't in the post-handshake domain. It's not like Selfie allows you to take packets from an already established connection and play it against an unsuspecting server that has no connections, and thus making it think it has a connection. The failure is literally this: Alice says "Hey I wanna talk to you" intended for Bob but doesn't specify who, exactly, are "I" and "you". The Cat records Alice's speech and replays it to her, making her believe someone is trying to initiate a new, separate conversation. The verifiers writing the proofs would be acutely aware of the asymmetrical nature of TLS handshakes. In fact, I strongly doubt they even considered any case where the same entity hosts both a TLS client and a TLS server for a shared purpose.
  - tialaramex 3y ago
    > I strongly doubt that. That's nice, but I'm reporting historical fact. https://eprint.iacr.org/2019/347 https://eprint.iacr.org/2019/347 This is Hacker News, where people who know nothing about a topic come to tell each other about their expertise. You believe no-one would make this type of mistake, I know they did and I have just provided you a link to the paper at the time. Alas some people will believe you, and they will assume that they too are infallible and the rest is inevitable. What did Dorothy Parker say about Horticulture ?
    - 3y ago

szundi 3y ago

You know having some bugs in there is not that problematic as even if they stay in the shadows, most product bugs are catched anyway. Also these make false alerts, then instead of fixing the nonexistent bug, they fix the test suite.

tzs 3y ago

In the case of formal verification done with proof assistants or similar, I believe the way it works is something like this. The people who develop such software start out writing a verifier for a much system of logic or programming than what the final system will handle. This first system is sufficiently simple that the verifier that can verify programs in that system is very small and straightforward, so that if several humans look at it and can't see any bugs it is almost certainly correct. Then they write a verifier for a more expressive system. This verify isn't as small or straightforward and so even if humans don't see any bugs we can't be confident that there none. They then use the first verifier to verify the second verifier. The formal proof of correctness might be long and difficult to develop because it can only use the reduced logic of the first verifier, but once they manage that and the first verifier verifies it, they can be confident that the second verifier is correct. If the system the second verifier still isn't expressive enough to verify the things they ultimately want to handle they write an even more expressive system, and use the second verifier to verify that. Repeat until you've got the system you wanted in the first place.