6 ms·

The key is that it’s proven within the formal method system used. For example, you can prove that you don’t have an out of bounds write, but not that a hardware

The key is that it’s proven within the formal method system used. For example, you can prove that you don’t have an out of bounds write, but not that a hardware bug doesn’t exist. There was a proof of SSL or TLS (can’t remember which) as a protocol was secure, but later was exploited. This was because the exploit was something the spec didn’t cover

MaxBarraclough 7y ago
> For example, you can prove that you don’t have an out of bounds write, but not that a hardware bug doesn’t exist. Also, a bug in the compiler could introduce such a bug. To my knowledge, the major Ada compilers have a very good reputation for correctness, but none are formally verified, and there's no such compiler on the horizon. > There was a proof of SSL or TLS (can’t remember which) as a protocol was secure, but later was exploited. This was because the exploit was something the spec didn’t cover Typically we'd expect the only vulnerabilities in such an implementation would be side-channel attacks, such as timing attacks. Do you have any more details on this? I couldn't find anything with a quick google.
- albntomat0 7y ago
  Top of the second page: https://link.springer.com/article/10.1007/s00165-012-0269-9 https://link.springer.com/article/10.1007/s00165-012-0269-9 My understanding is that both Needham–Schroeder and SSL had formal verification prior to the breaks, but the breaks relied on properties outside of what was proven (which was thought to be complete at the time).
  - MaxBarraclough 7y ago
    Great, thanks. I found a freely available pre-print at http://alfredo.pironti.eu/research/sites/default/files/cf11.pdf http://alfredo.pironti.eu/research/sites/default/files/cf11.... The relevant content is mostly on page 2. They seem to be saying that when it comes to crypto, both the requirements work and the implementation work are both challenging and error-prone, even for expert practitioners. I don't think they're exactly saying anything against formal methods, though: > It is significant, for example, that the above mentioned flaw affecting the Needham-Schroeder public-key protocol could be found by applying formal methods Later, under Motivation, regarding what are essentially integration bugs: > in OpenSSL an error condition returned by a cryptographic function was incorrectly interpreted by the function caller, making the application accept corrupted data; such a fault cannot be found if a formal model that has no relation with the implementation code is analyzed Not exactly a demonstration of a weakness of formal methods. Instead, an instance of a bug (a normal one, not a side-channel vulnerability) occurring in a system which was only partially formally verified. > a large gap still exists between these models and a real-world protocol implementation and its execution. A problem with real-world implementation, not with formal methods. I wonder what they would have made of 'SPARKSkein', released around the time that paper was published. [0] I suppose it wouldn't have been anything all that new - integration bugs could still occur. [0] https://www.adacore.com/papers/sparkskein https://www.adacore.com/papers/sparkskein
    - albntomat0 7y ago
      My takeaway is that using formal methods is difficult to turn into any sort of actual security guarantee, due to the difficulty of connecting them to a real world system in a meaningful way. While formal methods could produce something meaningful with proper "inputs", getting that done is hard.
      - MaxBarraclough 7y ago
        I'm more optimistic. There's real value in building ultra-low-defect crypto code, and as far as I can tell, formal methods have a good track-record there. We already knew that integration into non-verified code isn't guaranteed to be free of defects - that's out of scope by definition. That's somewhere safe languages can help though. What the paper describes as corrupted data might well be the kind of bug that often happens in C, but rarely happens in a safe language. The other question is vulnerability to side-channel attacks. Today's formal methods aren't much use against them.
- vfclists 7y ago
  >> For example, you can prove that you don’t have an out of bounds write, but not that a hardware bug doesn’t exist. > Also, a bug in the compiler could introduce such a bug. > To my knowledge, the major Ada compilers have a very good reputation for correctness, but none are formally verified, and there's no such compiler on the horizon. No, a bug in the compiler does not introduce such a bug. A bug in the compiler is a bug in the implementation and does not equate to a bug in the formal spec. It is rather like a fault in a machine or a building arising from a dodgy supplier using below spec materials, or a fault in the manufacturing or assembly process.
  - MaxBarraclough 7y ago
    > No, a bug in the compiler does not introduce such a bug. > A bug in the compiler is a bug in the implementation and does not equate to a bug in the formal spec. We weren't discussing the challenges of creating a correct formal specification. I presume you meant a bug in the formally verified implementation, rather than a bug in the formal spec, in which case: More precisely then: a compiler bug could introduce a defect into the final system, which was not present in the formally verified implementation source code. (This assumes that the scope of the formal verification stops at Ada source code.) > It is rather like a fault in a machine or a building arising from a dodgy supplier using below spec materials, or a fault in the manufacturing or assembly process. Those are all risks that mechanical engineers need to deal with carefully. If it's your job to deliver a defect-free avionics software binary, then dealing with the risk of compiler bugs is part of that. A company like Airbus isn't going to treat compiler bugs as Eh, not our problem. Presumably they're going to be careful in their choice of compiler, and back it up with testing. My point was that a bug in the compiler is similar to a bug in hardware, in that it opens the door to defects which are formally assured to be absent from the verified implementation's source code. It's possible to use formal verification to guarantee against issues arising from compiler bugs, it's just that I don't think this can currently be done with SPARK. There are two formal approaches to protect against compiler bugs: either use a formally-verified compiler (like the CompCert C compiler), or use a non-verified compiler and then verify the correspondence between the input source and the generated machine-code (the approach used by Sel4).

MaxBarraclough 7y ago

> For example, you can prove that you don’t have an out of bounds write, but not that a hardware bug doesn’t exist. Also, a bug in the compiler could introduce such a bug. To my knowledge, the major Ada compilers have a very good reputation for correctness, but none are formally verified, and there's no such compiler on the horizon. > There was a proof of SSL or TLS (can’t remember which) as a protocol was secure, but later was exploited. This was because the exploit was something the spec didn’t cover Typically we'd expect the only vulnerabilities in such an implementation would be side-channel attacks, such as timing attacks. Do you have any more details on this? I couldn't find anything with a quick google.

albntomat0 7y ago
Top of the second page: https://link.springer.com/article/10.1007/s00165-012-0269-9 https://link.springer.com/article/10.1007/s00165-012-0269-9 My understanding is that both Needham–Schroeder and SSL had formal verification prior to the breaks, but the breaks relied on properties outside of what was proven (which was thought to be complete at the time).
- MaxBarraclough 7y ago
  Great, thanks. I found a freely available pre-print at http://alfredo.pironti.eu/research/sites/default/files/cf11.pdf http://alfredo.pironti.eu/research/sites/default/files/cf11.... The relevant content is mostly on page 2. They seem to be saying that when it comes to crypto, both the requirements work and the implementation work are both challenging and error-prone, even for expert practitioners. I don't think they're exactly saying anything against formal methods, though: > It is significant, for example, that the above mentioned flaw affecting the Needham-Schroeder public-key protocol could be found by applying formal methods Later, under Motivation, regarding what are essentially integration bugs: > in OpenSSL an error condition returned by a cryptographic function was incorrectly interpreted by the function caller, making the application accept corrupted data; such a fault cannot be found if a formal model that has no relation with the implementation code is analyzed Not exactly a demonstration of a weakness of formal methods. Instead, an instance of a bug (a normal one, not a side-channel vulnerability) occurring in a system which was only partially formally verified. > a large gap still exists between these models and a real-world protocol implementation and its execution. A problem with real-world implementation, not with formal methods. I wonder what they would have made of 'SPARKSkein', released around the time that paper was published. [0] I suppose it wouldn't have been anything all that new - integration bugs could still occur. [0] https://www.adacore.com/papers/sparkskein https://www.adacore.com/papers/sparkskein
  - albntomat0 7y ago
    My takeaway is that using formal methods is difficult to turn into any sort of actual security guarantee, due to the difficulty of connecting them to a real world system in a meaningful way. While formal methods could produce something meaningful with proper "inputs", getting that done is hard.
    - MaxBarraclough 7y ago
      I'm more optimistic. There's real value in building ultra-low-defect crypto code, and as far as I can tell, formal methods have a good track-record there. We already knew that integration into non-verified code isn't guaranteed to be free of defects - that's out of scope by definition. That's somewhere safe languages can help though. What the paper describes as corrupted data might well be the kind of bug that often happens in C, but rarely happens in a safe language. The other question is vulnerability to side-channel attacks. Today's formal methods aren't much use against them.
vfclists 7y ago
>> For example, you can prove that you don’t have an out of bounds write, but not that a hardware bug doesn’t exist. > Also, a bug in the compiler could introduce such a bug. > To my knowledge, the major Ada compilers have a very good reputation for correctness, but none are formally verified, and there's no such compiler on the horizon. No, a bug in the compiler does not introduce such a bug. A bug in the compiler is a bug in the implementation and does not equate to a bug in the formal spec. It is rather like a fault in a machine or a building arising from a dodgy supplier using below spec materials, or a fault in the manufacturing or assembly process.
- MaxBarraclough 7y ago
  > No, a bug in the compiler does not introduce such a bug. > A bug in the compiler is a bug in the implementation and does not equate to a bug in the formal spec. We weren't discussing the challenges of creating a correct formal specification. I presume you meant a bug in the formally verified implementation, rather than a bug in the formal spec, in which case: More precisely then: a compiler bug could introduce a defect into the final system, which was not present in the formally verified implementation source code. (This assumes that the scope of the formal verification stops at Ada source code.) > It is rather like a fault in a machine or a building arising from a dodgy supplier using below spec materials, or a fault in the manufacturing or assembly process. Those are all risks that mechanical engineers need to deal with carefully. If it's your job to deliver a defect-free avionics software binary, then dealing with the risk of compiler bugs is part of that. A company like Airbus isn't going to treat compiler bugs as Eh, not our problem. Presumably they're going to be careful in their choice of compiler, and back it up with testing. My point was that a bug in the compiler is similar to a bug in hardware, in that it opens the door to defects which are formally assured to be absent from the verified implementation's source code. It's possible to use formal verification to guarantee against issues arising from compiler bugs, it's just that I don't think this can currently be done with SPARK. There are two formal approaches to protect against compiler bugs: either use a formally-verified compiler (like the CompCert C compiler), or use a non-verified compiler and then verify the correspondence between the input source and the generated machine-code (the approach used by Sel4).