2

The EAL for Common Criteria are described briefly as:

EAL1: Functionally Tested. ...
EAL2: Structurally Tested. ...
EAL3: Methodically Tested and Checked. ...
EAL4: Methodically Designed, Tested, and Reviewed. ...
EAL5: Semi-Formally Designed and Tested. ...
EAL6: Semi-Formally Verified Design and Tested. ...
EAL7: Formally Verified Design and Tested.

Does "Formally Verified Design" refer to the source code undergoing static code analysis? Thus meaning that the source code would have to be disclosed to gain EAL > 4?

I'm Root James
  • 131
  • 7

2 Answers2

2

From my understanding formally verified is much more difficult than just providing the source code. It is more or less proving that the source code does what it is supposed to do and that what it is supposed to do is also the right thing. Just providing the code to prove this is not sufficient but proving it without providing the code is probably not possible. And at least in my experience it is normal to provide source code with EAL4 already.

Also, disclosing the source code does not mean to open source it. It only means that the agency doing the evaluation has access to it, typically with some non-disclosure agreements.

Steffen Ullrich
  • 184,332
  • 29
  • 363
  • 424
  • This is an older document from CISCO available on the CC website that describes using tools for source code analysis: http://www.commoncriteriaportal.org/iccc/9iccc/pdf/A2412.pdf. Your answer helps to better understand how CC internals work. – I'm Root James Jun 10 '21 at 05:11
0

EAL4 includes explicit code review evaluation activity, if you don't have access to the source code you can't complete it, preventing you from completing entire evaluation.

Kirill Sinitski
  • 989
  • 6
  • 12