It is a difficult process to prove it at this level. Model checkers, design-level proofs, design-by-contract, static analysis... these are all techniques with good tooling available that will get you 80-90% the way there. The other 10-20% can be difficult or impossible. That's what projects like seL4 aim at.
The advice I give on this stuff is to use tech such as this (or above list) on the most critical portions. For instance, the underlying kernel, the key middleware (eg TCP, Protocol Buffers), the type system of the language, the compiler, long-term software like SSL, and so on. Effort is made once that continues to pay off in numerous uses while being incrementally extended. Modularity, careful API design, and layering make modifications easier as proven in Orange Book B3/A1 systems.
So, you build it then keep reusing it. Older, security kernels were used in VPN's, firewalls, databases, messaging systems (esp mail guards), primitive desktops (esp console), thin clients, and so on. New one's can be used similarly... are by Green Hills and Sirrix IIRC. Middleware part is extremely important, though, as even MILS kernel vendors admit (and develop). Best route is to combine: kernels like this; components written in safe subsets amenable to static analysis; middleware synthesized w/ security checks from specs and constraints; CPU or board support packages whose implementation details are hidden behind interfaces w/ their own verification done. Pieces of that are already deployed or verified. Just need an integrated version that's also OSS.
Then, the rest of the developers can use Rust, Ada, Eiffel, whatever on top of these. If there's runtimes, they should be similarly verified.
Sorry for late reply. Don't take the number literally: it was a play on something Dr Schell used to say (example in [1]). He pointed out the reason GEMSOS and A1 class included formal verification was to get the last bit of assurance done. The tests proved the presence of specific issues. The model checkers and provers were meant to prove absence of issues. Model checkers often did a search through a number of states checking for invariants but were often limited due to state explosion. So, provers had to be used to show a given design implemented given policy or invariants in all situations. Additionally, show that a refinement to more concrete form preserved equivalence.
This is hard work. The lessons learned in 70's and 80's showed you could only do it once you had good mathematical formulations of certain concepts. That explains why the effort vs defects found varied considerably among projects. The other aspect that all of them discovered was the design or code had to be built with verification in mind. As in, certain implementation details were easy to modify, translate, etc while others were either difficult or impossible. You could use model checkers, traditional methods, etc to get pretty far in your assurance argument, maybe even 90-99%. That last bit that fell out of range of tools due to their problems or your implementation choice might be impossible gap to close.
So, the highest assurance argument took a combination of strong specs/models, proofs of invariants on all use-cases, minimization of state/complexity in general, and easy-to-analyse implementations. You can actually see this in action if you look at the layering/composition of GEMSOS [1], PSOS [2], KSOS [3], and VAX security Kernels [4]. CompCert's compiler passes applied [5] same rules of thumb.
I still say use lighter methods if you have to or can get away with it. There's been a number of software that used model-checking with success at finding flaws and a decent assurance argument. The problem was that they often require you to extrapolate what happens with small amount of states, data, or time to potentially huge amounts. Experience shows many things break down as load intensifies. So, I'd rather know it works in all states. And that's the last piece of assurance case that might be impossible to reach if you didn't design for it from the start. Hope this helps.
The advice I give on this stuff is to use tech such as this (or above list) on the most critical portions. For instance, the underlying kernel, the key middleware (eg TCP, Protocol Buffers), the type system of the language, the compiler, long-term software like SSL, and so on. Effort is made once that continues to pay off in numerous uses while being incrementally extended. Modularity, careful API design, and layering make modifications easier as proven in Orange Book B3/A1 systems.
So, you build it then keep reusing it. Older, security kernels were used in VPN's, firewalls, databases, messaging systems (esp mail guards), primitive desktops (esp console), thin clients, and so on. New one's can be used similarly... are by Green Hills and Sirrix IIRC. Middleware part is extremely important, though, as even MILS kernel vendors admit (and develop). Best route is to combine: kernels like this; components written in safe subsets amenable to static analysis; middleware synthesized w/ security checks from specs and constraints; CPU or board support packages whose implementation details are hidden behind interfaces w/ their own verification done. Pieces of that are already deployed or verified. Just need an integrated version that's also OSS.
Then, the rest of the developers can use Rust, Ada, Eiffel, whatever on top of these. If there's runtimes, they should be similarly verified.