Solutions

These techniques go back decades and have been given various names: Formal Methods, High Assurance Software, Evaluation Assurance Levels, et. al.

Those who want really reliable software will find that they must find means of avoiding the majority of bugs to start with, and as a result the programming process will become cheaper.

Techniques and Technologies

• Language-theoretic Security
• Make invalid states unrepresentable (2023)
• You Need More Constraints

Static Analysis

Analysis Tools and Linters to Improve Code Quality and Avoid Bugs

Formal Verification of Systems

awesome-formal-verification: Welcome to the ultimate list of resources for formal verification techniques and tools. This repository aims to provide an organized collection of high-quality resources to help professionals, researchers, and enthusiasts stay updated and advance their knowledge in the field.

Secure Operating systems

Today’s operating systems tend to fall into one of several categories.

• Monolithic Kernels (Linux, macOS, Windows): Poorly Structured and Insecure
• RTOSs (RealTime Operating System): Rigorously designed to keep system time in sync with the real world
  • Soft RealTime
  • Hard RealTime
• Formally Verified Microkernels
• Security Kernel Operating System (GEMSOS, P)

More info on the Secure OSes page.

Does it Work

• Making Software ‘Correct by Construction’ - Professor Martyn Thomas CBE (YouTube)
• Tokeneer | AdaCore

HACMS

• DARPA High-Assurance Cyber Military Systems (HACMS)
• The HACMS program: using formal methods to eliminate exploitable bugs - PMC
• HACMS MH-6 Little Bird helicopter - YouTube