At the beginning of this century, aerospace and nuclear engineers began looking toward formal methods. They spoke with researchers in the field. Their biggest question: “Could you help us guarantee the behavior of our code?”
Formal methods use mathematical techniques to “solve” the logic of computer programs or other systems (integrated circuits, for example) to answer questions about their behavior. For example, if you want to know if there is any way a buffer overflow could occur in your program, formal methods can be used to determine that. What’s more, a state-of-the-art formal methods tool can answer those questions for you automatically.
Formal methods are ideal for validating code that needs to be perfect. A sound formal methods tool will report every defect in your code. That may not sound so useful if you’re not worried about users finding bugs that can be fixed in a future release. But it’s highly useful if you’re developing a TEE that needs to be 100% reliable and impervious to cyberattacks.
Sound formal methods tools do more than just find bugs. When you do traditional testing, you can never be certain you didn’t forget an important test case. Formal methods, as we’ll see later, can guarantee you have exhaustive test coverage of your requirements.
Formal methods can also be used to guarantee your program exactly matches its specification. That doesn’t guarantee your application will work perfectly; there may be errors in the requirements. But your task then becomes reviewing the specification. That’s far easier than reviewing the full source code, as those poor aerospace-and-nuclear-sector software engineers used to do.