It's better to read the papers where they attempt provable security and then those published years later reviewing that work or those methods. Certain methods worked well, some failed over time, and so on. The lessons learned and looking back papers are where I find the most wisdom in this field. Naturally.
The papers on Orange Book-era B3 and A1 class systems along with the Common Criteria EAL6/EAL7 works taught me the most. They all required a clear, security policy and a strong argument the design/implementation embody it. The systems are modular, layered, internally simple, use structured programming style, use safer subsets of programming languages, often are state-machines, account for failure modes for everything, and trace each potential execution flow of the system. They also add, where possible, static analysis and covert channel analysis. Some did formal proofs but the above gets you 90-99% of the way.
So, the idea is that you design the system or algorithm in such a way that you can easily demonstrate it has certain properties. It was hard work. However, LOCK project even with proofs only cost around 30-40% extra on top of solid, development process. Another lesson is the specs, implementation, and proofs/arguments should always evolve side-by-side with plenty of communication between team members. This spots problems early. Analysis of various phases showed above methods caught all kinds of reliability and security flaws in actual systems with many doing excellent during years of pentesting. Proof themselves, on other hand, should only be used if the property is easy to model mathematically. Otherwise, you use a lot of effort with little gained. Final lesson came from TCB concept: focus all your provable security on mechanisms that are flexible and simple so the cost is spread over all projects benefiting from it. Security & separation kernels did this to a degree but I think CompCert compiler is best, modern example of ROI on high-assurance development.
Most of the best papers are behind paywalls, unfortunately. I do have a small sampling on-hand from there and now that illustrate some of the high-assurance methods.
http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
Modern effort (seL4) to exceed EAL7 by bringing verification to code itself. Note that some A1 projects had close to 1-to-1 spec to implementation mapping. So, full formal might be replaced by low-level, verified specs and matching code verified by inspection, etc.
http://www.crash-safe.org/assets/verified-ifc-long-draft-201...
Previous work proved kernels supported MLS or MILS models. This is better given it's proving a hardware mechanism both enforces a security requirement and meets functional requirements. Significant given SAFE (see crash-safe.org) makes inherently secure apps easier to write.
http://goto.ucsd.edu/quark/usenix12.pdf
Proving security properties of a web browser. Typically, you know the work is legit if it spends time talking about the flaws formal verification caught. I don't see so much of that in this but they might have omitted that to publish what worked instead.
http://pastebin.com/y3PufJ0V
My framework compliments that and reminds that it must be applied to every layer down to the gates.
So, although my sharing is limited by paywalls, I hope you find these interesting and can see the different perspectives of highly assured security. There have been numerous successes in independent testing, pen-testing, and field use. Also remember that this is only provable security rather than verification of properties in general. The field of verification and correctness assurance has progressed quite a bit (see CompCert, SPARK, Esterel, etc). Have fun.
Very interesting reading. The whole notion of the AAMP7G processor is fascinating. Made solely for government in tiny quantities, in tightly controlled facilities, probably rad hard, resistant to power analysis, etc.
Fine to learn for personal use but other stuff is better if you're job hunting. If you want to learn, then skip Esterel (big $$$) to learn Ada with AdaCore's free GNAT IDE. Helps to understand why it does certain things (eg foundations). Get that here:
AdaCore's "Gems" and other resources will help you plenty. SPARK is a variant of Ada designed to be easy to analyze with mathematical techniques with goal of automatically proving absence of certain bugs in over 95% of code. The article below has links to many resources and demonstrations. Tokeneer further demo's Praxis's Correct by Construction process, which is also cool.
I'll end with a few other goodies. Adam Chlipala does great work in teaching and making formal methods lightweight. His book below describes such methods. More links in comments.
Sandia's Secure Processor (SSP), also called Score, utilizes a highly assured design and implementation that results in a Java processor immune to obvious code injection techniques or radiation-related issues. Their SEED architecture is really nice. Modern stuff is paywalled but this old paper tells plenty. Thing it leaves out, IIRC, is they use an ML-based hardware model to do equivalence checking between executable specification, hardware spec (in ML), and actual hardware HDL. Already in ASIC's on rad-hard processes. Availability of ASSET tools or SSP/Score unknown.
The papers on Orange Book-era B3 and A1 class systems along with the Common Criteria EAL6/EAL7 works taught me the most. They all required a clear, security policy and a strong argument the design/implementation embody it. The systems are modular, layered, internally simple, use structured programming style, use safer subsets of programming languages, often are state-machines, account for failure modes for everything, and trace each potential execution flow of the system. They also add, where possible, static analysis and covert channel analysis. Some did formal proofs but the above gets you 90-99% of the way.
So, the idea is that you design the system or algorithm in such a way that you can easily demonstrate it has certain properties. It was hard work. However, LOCK project even with proofs only cost around 30-40% extra on top of solid, development process. Another lesson is the specs, implementation, and proofs/arguments should always evolve side-by-side with plenty of communication between team members. This spots problems early. Analysis of various phases showed above methods caught all kinds of reliability and security flaws in actual systems with many doing excellent during years of pentesting. Proof themselves, on other hand, should only be used if the property is easy to model mathematically. Otherwise, you use a lot of effort with little gained. Final lesson came from TCB concept: focus all your provable security on mechanisms that are flexible and simple so the cost is spread over all projects benefiting from it. Security & separation kernels did this to a degree but I think CompCert compiler is best, modern example of ROI on high-assurance development.