3 ms·
> and some of them do indeed require mathematical proof of correctness > (EAL6+ being a key standard) Nitpick: EAL6 is still semi-formal, EAL7 is formally veri
by yaantc 7y ago
> and some of them do indeed require mathematical proof of correctness
> (EAL6+ being a key standard)
Nitpick: EAL6 is still semi-formal, EAL7 is formally verified design and tested. EAL7 is very rare, on the CC certified products page [1] there are only 2 EAL7 certified products: a hardware diode, and a virtual machine OS.
[1] https://www.commoncriteriaportal.org/products/ https://www.commoncriteriaportal.org/products/
- speedplane 7y ago> Nitpick: EAL6 is still semi-formal, EAL7 is formally verified design and tested. EAL7 is very rare, on the CC certified products page [1] there are only 2 EAL7 certified products: a hardware diode, and a virtual machine OS. You are definitely correct. Also, disclosure... I worked on that EAL7 Virtual OS. When I left it was only EAL6+, likely leading to my bias towards it.