"Common Criteria certification (say EAL4) is not cheap and takes years to achieve."
Oh yeah. The original criteria got watered down to point that it's mostly expensive paperwork and takes years to achieve. The only ones that are even meaningful are EAL5-7. That's when the assurance activities that benefit security kick in plus you get pentesting of source. Contrary to pjc, I think certification is meaningful if it's a continuous or regular thing against meaningful criteria. The EAL's are meaningful given each requirement has proven to improve security in the past. Protection profiles often have sensible requirements mixed with BS. So, process needs to be subsetted and in a way that focuses on active evaluation rather than just paperwork with sensible requirements and only higher EAL's.
I wrote on revamping the evaluation process here:
https://www.schneier.com/blog/archives/2014/04/friday_squid_...
Far as specifics, the original systems secured to A1-class are still mostly secure today. I could shoot holes in them with what we've learned. Yet, the techniques they used left them in really good shape after all this time and still easier to apply modern stuff to than modern software. Imagine that. It's as if the certification criteria on design & assurance side were fundamental principles that geniuses figured out through many military & academic experiments that still work better than what most developers guess at or throw together. ;)
Examples:
http://www.cse.psu.edu/~trj1/cse544-s10/slides/cse544-lec9-1...
Note: Started with SCOMP and GEMSOS. SCOMP had minimal TCB, IOMMU, totally compartmentalized OS, trusted path, and (as XTS-300) ran UNIX apps in user-mode.
http://www.cse.psu.edu/~trj1/cse543-f06/papers/vax_vmm.pdf
Note: I keep citing this, mainly layered design and assurance sections, because it's still more secure at software level than most virtualization. Just look at level of precision, testing, configuration management, safer coding, and so on. They also, per criteria, did a covert channel analysis that would've helped all these clouds with their so-called "side channels." ;)
https://www.cis.upenn.edu/~KeyKOS/NanoKernel/NanoKernel.html
Note: A B3-class OS (w/ KeySAFE) from capability-security field. NanoKernel, protected IPC, and regular checkpointing for integrity/availability after a crash.
http://www.cyberdefenseagency.com/publications/LOCK-An_Histo...
Notes: LOCK was interesting as it was a hardware/software system with Type 1 cryptoprocessor & UNIX layer. They invented Type Enforcement for this product then implemented it with capability mechanisms. After it was canceled, "features over assurance," NSA had Utah reimplement that tech in a microkernel. They later added it to Linux as SELinux. LOCK was original model, though, with the UNIX section confirming prior experiments that UNIX calls are inherently insecure to point you can have compatibility or security. It's why separation kernels that came later all just virtualized it as a whole with security-critical apps running right on separation kernel.
So, there's four systems that illustrate some design requirements and especially assurance activities. The assurance activities worked. Real flaws were found. A few did great in pentesting and/or the field. Definitely worth copying even if one avoids a CC evaluation: private certification against the criteria with plenty of source code focus instead. Preferably an ongoing process that starts at beginning of the project with third parties auditing feeding right back into development, esp catching flaws.