This is one of best articles on high-assurance, security engineering Ive seen. It explains things in detail without a pile of math.
One thing to notice is how they did the networking stack. High-assurance security tries to make as much of system as possible be outside trusted base while proving smallest number of components. Given high-assurance separation and crypto guard, they could ignore the risk of the entire networking stack. Note I recommended using guards on separation kernels many times here for same reason.
Now, on bad note, the article is heavy on formal verification since that’s what people in project are about. That’s not how it was done under TCSEC. They knew different methods catch different problems. So, they mandated formal methods, thorough testing, and human inspection of all artifacts. Currently, the safety-critical segment (esp DO-178C) is favoring full-coverage testing using automated, test generation on top of statis analysis and tons lf review.
Given current capabilities, it’s my opinion that software should use and pass all of those methods to get label of high-assurance. Additionally, they should do test generation, static analysis, and human review before proof since those catch problems fastest. That also allows for cheaper, QA people which allows more QA people on some projects. Or more profit in commercial endeavors.