Can a software application / OS get past EAL4 if no source code is available
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?
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.