20 ms·

I can't help but pick a couple of general points from area standards-arguer man. One is 'problems of standardization in high-development-velocity fields': htt

by pvg 3y ago

I can't help but pick a couple of general points from area standards-arguer man. One is 'problems of standardization in high-development-velocity fields': https://news.ycombinator.com/item?id=3577837 https://news.ycombinator.com/item?id=3577837 The other is "this is worse in security engineering broadly and outright catastrophic in cryptography engineering specifically" https://news.ycombinator.com/item?id=25451351 https://news.ycombinator.com/item?id=25451351 There's probably better/longer, I just looked at the first page of "standards" search. The points are strong, like messageboard-argument-winning bear, though.

tptacek 3y ago
What'd I do here? You have me worried. Did I manage to back into an argument that standards processes are good? Really I'm just trying to say two things here: * The Common Criteria process is a farce, and things that are secure by dint of being EAL5+ are really secure because they're so small you can almost prove them with formal methods (which is not to say that everything EAL5+ has usefully applied formal methods). * The meaning of the word "operating system" is different when we're talking about EAL5+ stuff; seL4 is an "operating system" that has been proven secure with formal methods, and it is secure, but it's secure in large part because it does almost nothing; it isn't comparable to Windows, macOS, or Linux. You couldn't build an iPhone experience on top of it (you could --- and people do --- host Unix kernels on top of L4 OS's, but when you do that you keep many/most of the security issues of that Unix kernel).
- pvg 3y ago
  No no, sorry, it wasn't intended as backhanded snark. You've had a running critique of standards stuff here for years and it's good and the other person should read it. A bit of an unsuppressed "well, maybe if they looked at the principles, then they'll see the light" nerd-response on my part. You're not going to make an iPhone out of seL4, you're also not going to come up with a Secure Enclave or an IOMMU or an encrypted serial bus or whatever by reading standards/meeting certification reqs either because, generally, that's not how standards and certifications work. For multiple developed versions of this argument, see 'tptacek! I'm sure you're right about the details of Jor-EAL5+ and the bottle city CRYSTALS-Kandor, just saying "also right in this other way but with less lore". Not that there is anything wrong with lore.
  - tptacek 3y ago
    Well, you'll make the iPhone fingerprint reader out of seL4. :)
- Veserv 3y ago
  So what you are saying is that EAL >=5 does not imply secure, it is the formal methods that imply secure? Well good news, that is not a mistake. EAL >=5 implies formal methods of various degrees. The standard demands the thing that works, amazing. It might be too hard for consumer companies to achieve, but that does not make the process a farce as long as there are companies that can certify useful functionality according to the process. And, although you seem to think the functionality that can be certified is limited, I doubt you consider secure cryptographic co-processors useless or unimportant.
  - tptacek 3y ago
    In that paragraph, the words "of various degrees" is load-bearing. I don't think you're making a coherent case for the security or insecurity of an iPhone with any of this stuff. Real security in complex products simply has nothing to do with the CCTL process. Which, I'm sorry to say again, is farcical. If it's not clear: I've had the displeasure of working with this process in my career, most of which I've spent in vulnerability research.
    - Veserv 3y ago
      Yes, various degrees; we are discussing three distinct levels. Why on earth would they all demand the same degree of formal methods? Up to EAL4 all you need is a informal specification; what is basically useless paperwork. It is only at EAL5 that you are required to supply a semi-formal design, ADV_TDS.4, and interface specification, ADV_FSP.5. At EAL6 you must also supply a formal model of the security policy, ADV_SPM.1, and a complete mapping between design and implementation, ADV_IMP.2. By EAL7 you are required to supply a complete formal design, ADV_TDS.6, and specification, ADV_FSP.6. You then have a formal model of the security policy, the interface enforcing that policy, the design backing the interface, and a mapping from the formal design to the implementation. That is pretty dang exhaustive. I guess you could go further and demand a formal, machine-checkable correspondence between the implementation and the design? Since you bring up that you have worked with the process, what products at EAL5 or higher have you had the displeasure of working on?
      - 3y ago

by pvg 3y ago

tptacek 3y ago

What'd I do here? You have me worried. Did I manage to back into an argument that standards processes are good? Really I'm just trying to say two things here: * The Common Criteria process is a farce, and things that are secure by dint of being EAL5+ are really secure because they're so small you can almost prove them with formal methods (which is not to say that everything EAL5+ has usefully applied formal methods). * The meaning of the word "operating system" is different when we're talking about EAL5+ stuff; seL4 is an "operating system" that has been proven secure with formal methods, and it is secure, but it's secure in large part because it does almost nothing; it isn't comparable to Windows, macOS, or Linux. You couldn't build an iPhone experience on top of it (you could --- and people do --- host Unix kernels on top of L4 OS's, but when you do that you keep many/most of the security issues of that Unix kernel).

pvg 3y ago
No no, sorry, it wasn't intended as backhanded snark. You've had a running critique of standards stuff here for years and it's good and the other person should read it. A bit of an unsuppressed "well, maybe if they looked at the principles, then they'll see the light" nerd-response on my part. You're not going to make an iPhone out of seL4, you're also not going to come up with a Secure Enclave or an IOMMU or an encrypted serial bus or whatever by reading standards/meeting certification reqs either because, generally, that's not how standards and certifications work. For multiple developed versions of this argument, see 'tptacek! I'm sure you're right about the details of Jor-EAL5+ and the bottle city CRYSTALS-Kandor, just saying "also right in this other way but with less lore". Not that there is anything wrong with lore.
- tptacek 3y ago
  Well, you'll make the iPhone fingerprint reader out of seL4. :)
Veserv 3y ago
So what you are saying is that EAL >=5 does not imply secure, it is the formal methods that imply secure? Well good news, that is not a mistake. EAL >=5 implies formal methods of various degrees. The standard demands the thing that works, amazing. It might be too hard for consumer companies to achieve, but that does not make the process a farce as long as there are companies that can certify useful functionality according to the process. And, although you seem to think the functionality that can be certified is limited, I doubt you consider secure cryptographic co-processors useless or unimportant.
- tptacek 3y ago
  In that paragraph, the words "of various degrees" is load-bearing. I don't think you're making a coherent case for the security or insecurity of an iPhone with any of this stuff. Real security in complex products simply has nothing to do with the CCTL process. Which, I'm sorry to say again, is farcical. If it's not clear: I've had the displeasure of working with this process in my career, most of which I've spent in vulnerability research.
  - Veserv 3y ago
    Yes, various degrees; we are discussing three distinct levels. Why on earth would they all demand the same degree of formal methods? Up to EAL4 all you need is a informal specification; what is basically useless paperwork. It is only at EAL5 that you are required to supply a semi-formal design, ADV_TDS.4, and interface specification, ADV_FSP.5. At EAL6 you must also supply a formal model of the security policy, ADV_SPM.1, and a complete mapping between design and implementation, ADV_IMP.2. By EAL7 you are required to supply a complete formal design, ADV_TDS.6, and specification, ADV_FSP.6. You then have a formal model of the security policy, the interface enforcing that policy, the design backing the interface, and a mapping from the formal design to the implementation. That is pretty dang exhaustive. I guess you could go further and demand a formal, machine-checkable correspondence between the implementation and the design? Since you bring up that you have worked with the process, what products at EAL5 or higher have you had the displeasure of working on?
    - 3y ago