3 ms·

Frankly, those are just box ticking exercises. Same with SOC certifications. Security is not a state of being, it is a process.

Veserv 3y ago
In what world are formal proofs of correctness “box ticking exercises”? You are wrongly extrapolating that the lowest levels of certification, that were literally designed to allow people incapable of more than box ticking to be rated on a unified scale, somehow applies to the levels that were designed to evaluate actual security. That is like saying the Richter scale is useless because you can not even feel a 1.0 earthquake. That is the entire point. The scale can measure from very low to very high. You are complaining that the scale is useless because the lowest ratings are easy to get, yeah, duh, that is why they are low ratings. However, you are correct for SOC. That is because the highest ratings are easy to get and are mere box ticking exercises. If the highest rating is easy, then the standard is useless for evaluating anything beyond that. This logic does not apply when a low rating is easy to get; that just means anything which can only get a low rating sucks.
- astrange 3y ago
  Adding the word "formal" to something doesn't mean it can do the impossible. It's not realistic to prove things correct, since it's both an impossible amount of work and you'll end up finding that your definition of "correct" was incorrect. (CompCert, a "formally correct C compiler", has had bugs found in it.)
  - Veserv 3y ago
    I do not see how that is relevant to my statement that formal methods, as required by the higher Common Criteria levels, do not constitute “box-ticking exercises”. Or are you arguing that these standards which require proofs of correctness are useless because proofs of correctness are much less impressive than box ticking?
    - astrange 3y ago
      They are extremely expensive box ticking exercises. Furthermore, I don't think anything except box ticking exercises exists or could ever exist. You can only write down ways to make a process worse, not better.
      - Veserv 3y ago
        I know that I have more confidence in a proven compiler that is thoroughly tested over a random compiler Joe the intern slammed out, but you do not seem to think that way. That is fine, you do you.
    - EVa5I7bHFq9mnYK 3y ago
      Nothing realistically complex can be proven "correct". There is even a mathematical theorem about it - given a program's code, one can't even prove that it ever stops. One can, of course, apply proof of correctness to simple curcuits, where all possible inputs and outputs can be enumerated.
      - Veserv 3y ago
        That is a complete misunderstanding of consequences of Rice’s theorem which generalizes the halting problem. You can not prove non-trivial properties about all programs that could could ever exist with no false positives or false negatives. You can prove non-trivial properties about almost every program. For instance, if I want to disallow programs that will not halt, I can just reject any program with a unbounded loop. I may also reject programs with a unbounded loop that will halt, a false negative, but I do not care. I just want to be certain that I will never run a program that will not halt. I just decided: “will definitely halt for my purposes” even though the halting problem is unsolvable in general. This is generically true and is why formal methods work at all.

Veserv 3y ago

In what world are formal proofs of correctness “box ticking exercises”? You are wrongly extrapolating that the lowest levels of certification, that were literally designed to allow people incapable of more than box ticking to be rated on a unified scale, somehow applies to the levels that were designed to evaluate actual security. That is like saying the Richter scale is useless because you can not even feel a 1.0 earthquake. That is the entire point. The scale can measure from very low to very high. You are complaining that the scale is useless because the lowest ratings are easy to get, yeah, duh, that is why they are low ratings. However, you are correct for SOC. That is because the highest ratings are easy to get and are mere box ticking exercises. If the highest rating is easy, then the standard is useless for evaluating anything beyond that. This logic does not apply when a low rating is easy to get; that just means anything which can only get a low rating sucks.

astrange 3y ago
Adding the word "formal" to something doesn't mean it can do the impossible. It's not realistic to prove things correct, since it's both an impossible amount of work and you'll end up finding that your definition of "correct" was incorrect. (CompCert, a "formally correct C compiler", has had bugs found in it.)
- Veserv 3y ago
  I do not see how that is relevant to my statement that formal methods, as required by the higher Common Criteria levels, do not constitute “box-ticking exercises”. Or are you arguing that these standards which require proofs of correctness are useless because proofs of correctness are much less impressive than box ticking?
  - astrange 3y ago
    They are extremely expensive box ticking exercises. Furthermore, I don't think anything except box ticking exercises exists or could ever exist. You can only write down ways to make a process worse, not better.
    - Veserv 3y ago
      I know that I have more confidence in a proven compiler that is thoroughly tested over a random compiler Joe the intern slammed out, but you do not seem to think that way. That is fine, you do you.
  - EVa5I7bHFq9mnYK 3y ago
    Nothing realistically complex can be proven "correct". There is even a mathematical theorem about it - given a program's code, one can't even prove that it ever stops. One can, of course, apply proof of correctness to simple curcuits, where all possible inputs and outputs can be enumerated.
    - Veserv 3y ago
      That is a complete misunderstanding of consequences of Rice’s theorem which generalizes the halting problem. You can not prove non-trivial properties about all programs that could could ever exist with no false positives or false negatives. You can prove non-trivial properties about almost every program. For instance, if I want to disallow programs that will not halt, I can just reject any program with a unbounded loop. I may also reject programs with a unbounded loop that will halt, a false negative, but I do not care. I just want to be certain that I will never run a program that will not halt. I just decided: “will definitely halt for my purposes” even though the halting problem is unsolvable in general. This is generically true and is why formal methods work at all.