To add to it, in browsers we have things like Illinois Browser OS, ExpressOS for mobile example, and just running instances on a separation kernel in safer language or with mitigations like INTEGRITY-178B, GenodeOS, etc.

https://www.usenix.org/legacy/event/osdi10/tech/full_papers/...

http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=9D1...

On the language side, there's things like SVA-OS for automating it if they don't want to do rewrites in safer language.

http://safecode.cs.illinois.edu/sva.html

Capability-security used to combine usability with higher security esp if they got rid of the Java crap underneath E. I can't recall if this niche made any recent improvements on effortless software security with reasonable overhead.

http://www.combex.com/tech/darpaBrowser.html

On hardware, we have tagged CPU's like SAFE, even better a C-compatible one w/ capability security running FreeBSD called CHERI, those designed for safe languages like jHISC, and those that protect software + fight malicious peripherals with confidentiality & integrity at the page level within the memory subsystem.

https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/

All of these have at least prototypes with a subset deployed commercially by interested parties. Separation kernel approach having most suppliers with CodeSEAL being one processor + compiler approach that saw some adoption outside small stuff for smartcards. CodeSEAL was confidentiality + integrity of pages + control flow enforcement w/ access controls for execution paths. Quite a few companies are also building stuff using tools like Astree & SPARK that prove absence of critical errors in code done in a restricted style. One just commercialized a combination of QuickCheck with C programs. Always happens if a small company with decent funds is willing to do it.

Lots of shit going on. I haven't even got into formal methods as applied to software (down to machine instructions) or hardware (down to gates). I haven't mentioned all the advances in automated or spec-driven testing with tools backing them. Hell, there's so much to draw on now for anyone studying high-assurance security a long time that my current problem is where to start on tackling future problems. I have to filter rather than find ways to knock out classes of vulnerabilities or show correctness. I about need to stop learning most of this shit to properly sort out all the newest findings but improvements are coming at phenomenal pace compared to 90's or early 2000's. :)

Note: This is all possibly part of a larger theory I have about how knowledge gets siloed and/or forgotten in IT due to different cultures with different teachings passed on. My idea was a curated resources collecting as many things that got results as possible with open discussions from people in the many groups. Can't build it right now but mention it for feedback periodically.

Note 2: One of the best ways I find real (aha HA) security versus mainstream when looking for new papers or tech is to put this in quotes: "TCB" All high-assurance engineers or researchers care about the TCB with its LOC usually listed. They also tend to list their assumptions (aka possible screwups). This filter plus words browser and security took me to Gazella, OP2, and IBOS last run. To be clear, Gazelle didn't have TCB in document but described it & was in another's related work. All it took given most efforts at hardening browsers apparently don't know what a TCB is or don't care. Works well with other things, too. Sadly.