1. 10

  2. 3

    In high-assurance systems, certification usually mandates that many forms of verification are used since one might catch problems others missed. Sometimes, the problems are in the verification tools themselves. The authors review tools that seem to have only used formal verification on select aspects of their distributed systems. The added techniques of code/doc review, observing things in debugger, component-based testing, and network/file fuzzing caught a bunch of problems.

    Interestingly, the verified code did exactly what the spec said it would. Like with CompCert, the formal verification made the implementation flawless in terms of conforming to the spec. The spec errors were mostly at interfaces as the founders of software engineering found in the 1960’s. I always say to bulletproof those by throwing everything you can afford to at them. That numerous components didn’t work the way the authors guessed reinforces why high-assurance software always lists everything in the Trusted Computing Base (TCB) along with what was verified and how. If you don’t fully understand a 3rd-party component, then there’s no way you can say your own component correctly uses the other one. This is also why projects such as deepspec.org are going from hypervisor code all the way down to the hardware. An example of a lightweight method is to build monitors for 3rd-party components that watch traces of its execution to spot inconsistencies with specifications that reflect user’s expectations. This has been used in both embedded (Copilot) and enterprise (NonStop) systems.