4 ms·

Possibly more interesting is a machine checked implementation. http://www.mitls.org/wsgi http://www.mitls.org/wsgi

by johnbender 13y ago

dyoder 13y ago
Very interesting. I was thinking something similar could be done in Haskell.
- quchen 12y ago
  Haskell is not a theorem prover, and I doubt it can be made one. You can encode some properties of data via the type system, but it's still a general purpose language. Agda on the other hand is a theorem prover, but much less general purpose.
jude- 13y ago
From the website, it seems that they proved that their implementation is correct with respect to their formalization of the interfaces in the RFCs. That is, their implementation is logically correct. However, this says nothing about whether or not the implementation is secure. They admit that they don't model time in their proofs, so I doubt their implementation is free of timing attacks. Moreover, its written in F#, so you have to trust your CLI implementation to be bug-free as well.
- ketralnis 12y ago
  > its written in F#, so you have to trust your CLI implementation to be bug-free as well Is that any different to an implementation in C relying on the processor being bug-free?
  - reidrac 12y ago
    The CLI is running in a processor, isn't it? I guess your argument is that the software using CLI is potentially affected by more bugs ;)
  - jude- 12y ago
    If you count up all of the possible states a processor can be in, as well as the number of transitions between them, you'll come up with a very big number of possible execution paths you'll need to verify work correctly. However, if you do the same for the CLI (or any non-trivial piece of software), you'll come up with a much, much, MUCH bigger number. As in, each additional state the CLI can enter potentially doubles the number of possible execution paths you'll need to check. The number of states and transitions for a processor today is large, but not so large that engineers can't formally and automatically verify that the processor will behave correctly under all inputs. Also, the structure of the processor and the way it is specified (i.e. Verilog) make it amenable to formal verification. This is not true for most software, not even things written in Haskell. You can cover a lot of cases with automated software testing, but you'll find that it's very, very, VERY hard to prove that you've covered every possible case. Even if you can, modeling multiple instances of the system as they evolve in time (i.e. any networked system or interactive system) means you have to consider all possible combinations of states they can be in. To put into perspective how hard formal verification of software is, I have a story. A friend of mine did his masters thesis on modifying TCP to allow for host mobility, and formally proving the correctness of his new TCP protocol. Despite having a 100-node cluster of beefy (48GB RAM) compute nodes at his disposal, it simply didn't have enough total RAM to verify the correctness of his protocol beyond five rounds of communication between one client and one server. Unless the CLI developers add machine-checked but hand-crafted proofs of correctness for each and every method, I trust the processor to be bug-free far more than any piece of software it runs. Now of course, if the NSA tampers with either, then all bets are off :P

Possibly more interesting is a machine checked implementation. http://www.mitls.org/wsgi http://www.mitls.org/wsgi

dyoder 13y ago

Very interesting. I was thinking something similar could be done in Haskell.

quchen 12y ago
Haskell is not a theorem prover, and I doubt it can be made one. You can encode some properties of data via the type system, but it's still a general purpose language. Agda on the other hand is a theorem prover, but much less general purpose.

jude- 13y ago

From the website, it seems that they proved that their implementation is correct with respect to their formalization of the interfaces in the RFCs. That is, their implementation is logically correct. However, this says nothing about whether or not the implementation is secure. They admit that they don't model time in their proofs, so I doubt their implementation is free of timing attacks. Moreover, its written in F#, so you have to trust your CLI implementation to be bug-free as well.

ketralnis 12y ago
> its written in F#, so you have to trust your CLI implementation to be bug-free as well Is that any different to an implementation in C relying on the processor being bug-free?
- reidrac 12y ago
  The CLI is running in a processor, isn't it? I guess your argument is that the software using CLI is potentially affected by more bugs ;)
- jude- 12y ago
  If you count up all of the possible states a processor can be in, as well as the number of transitions between them, you'll come up with a very big number of possible execution paths you'll need to verify work correctly. However, if you do the same for the CLI (or any non-trivial piece of software), you'll come up with a much, much, MUCH bigger number. As in, each additional state the CLI can enter potentially doubles the number of possible execution paths you'll need to check. The number of states and transitions for a processor today is large, but not so large that engineers can't formally and automatically verify that the processor will behave correctly under all inputs. Also, the structure of the processor and the way it is specified (i.e. Verilog) make it amenable to formal verification. This is not true for most software, not even things written in Haskell. You can cover a lot of cases with automated software testing, but you'll find that it's very, very, VERY hard to prove that you've covered every possible case. Even if you can, modeling multiple instances of the system as they evolve in time (i.e. any networked system or interactive system) means you have to consider all possible combinations of states they can be in. To put into perspective how hard formal verification of software is, I have a story. A friend of mine did his masters thesis on modifying TCP to allow for host mobility, and formally proving the correctness of his new TCP protocol. Despite having a 100-node cluster of beefy (48GB RAM) compute nodes at his disposal, it simply didn't have enough total RAM to verify the correctness of his protocol beyond five rounds of communication between one client and one server. Unless the CLI developers add machine-checked but hand-crafted proofs of correctness for each and every method, I trust the processor to be bug-free far more than any piece of software it runs. Now of course, if the NSA tampers with either, then all bets are off :P