You're selective again. I named all kinds of existing products and solutions that do a better job at solving real-world problems in a safe/secure way than mainstream alternatives. You ignored that to focus on the EAL7 thing, claimed high assurance hasn't done anything beyond smart cards (lol), and kind of stopped there.

Ok, let's get back to foundations since you didn't read my framework. The methods are more important than the certs themselves. The old stuff (Orange Book) called for strong specifications of requirements, design, each thing a system did, failure modes and so on. The implementation had to be done in safest known way, be modular, have well-defined interfaces with input checks, and provably correspond to that spec. Testing, covert channel analysis, configuration management, pentesting, trusted distribution... many requirements on top of it. Later, static analysis, rigorously evaluated code generators, and so on added to the mix. Early projects, which you claim have no practical value, built secure email, VPN's, databases, object storage, thin clients, web servers, logistics systems, and so on. The empirical assessments (eg "lessons learned from...") showed the various methods caught all kinds of problems albeit with different payoff rates in different situations.

Following NSA's finishing off high assurance market, the mainstream stuff and all the hacks one could desire prevaled for years. Eventually, DOD/NSA demanded high assurance again with their separation kernel concept which academia and private companies built. Academia had also been doing strong verification, from math to clever testing, for all kinds of things up to this moment. A common theme from old days repeated in that they focused EAL6-7 type of effort on critical mechanisms that could be easily leveraged for safety/security benefit since we couldn't do everything like that (good guess on your part). The mechanism could be isolation, analysis, transformation, and so on. More flexible the better.

MILS and Nizza architectures split systems between isolated apps and VM's with eg Linux running on top of strong kernels (eg EAL6+). Results of some did well against NSA pentesters. For others, tiny amount of trusted code by itself shows it could never have the number of problems of... whatever you wrote that post with. Others focused on compilers, language type systems, processor enhancements, code generators, DSL's, and so on. Are you saying a fully-documented, predictable, rigorously tested C compiler isn't practical? Or the finished WCET analysis during compilation or pluggable optimizations other groups are working on now?

Meanwhile, there were plenty of medium assurance offerings. Software such as qmail, Secure64, and HYDRA used architecture that greatly reduced risk. GenodeOS took it quite further by making their architecture plug and play with your choice of assured components. Tools such as Astree and SPARK knocked out all kinds of errors in embedded systems plus components of larger systems. Ada, the ML's, Eiffel (esp Design by Contract & Scoop concurrency) did the same in regular ones. Cornell's SWIFT, Ur/Web, Opa, and SPECTRE all made web applications immune to certain types of attacks in different ways without much effort by developers. We saw the formation of all kinds of secure storage, networking, backup, synchronization, virtualization, recovery, etc in academia with a subset rigorously analyzed and some also integrated with production software in prototypes. We saw hypervisor and paravirtualization work that made the OS itself untrusted. We saw CPU designs such as SAFE, CHERI, DIFT stuff, and those leveraging crypto beat vast majority of attacks down to CPU level with one proving properties down to the gates.

Tons and tons of work. Best stuff being things where effort is expended once to pay off many times. Tagged/capability CPU's, better architectures for OS's, compilers that automatically enforce strong safety/security, static analysis tools that prove absence of common bugs, type systems for high level languages easy to code in... the list goes on. These are all very practical with many used in real projects or products. The thing they all have in common is they (a) believably do their job and (b) result in drastic reduction of risk and attack surface at every layer of our systems. Widespread adoption and investment in such methods that work rather than mainstream one's that don't will have a direct impact on "the market for zero-day vulnerabilities." Given pervasive deployment, that market would mostly disappear outside subversions and interdictions.

And I encourage naysayers such as yourself to put effort into such strong methods to get those that aren't at mainstream readiness to mainstream readiness. Your own mind would be very beneficial to academics designing secure filesystems and messaging systems that rely on necessarily complex protocols and crypto. You might knock out problems they didn't see. There might be many other people on HN with similar things to offer and great results to show for it in future. It's why I respond to these misleading comments of yours in detail. One day, someone reading them might be inspired to do better than any project I referenced or simply put effort into those proven to already get plenty results. It is worth it even if the troll or failure-to-get-it rate of those reading it is 99%. That 1% might make one of these real and everything I cited started with one of them that decided to build on proven theory and practice in contrast to mainstream.

So, I'll stay at it even if you think highly secure processors, kernels, compilers, type systems, web apps, databases, middleware, and so on has... "no applicibility to the real world." Not the majority of it, I'll agree. They prefer their IT assets served to their opponents on a silver platter. I write for the others.