I mostly agree with his write-up. I’ll just modify one part, that about marginal investment, to say a significant amount of resources went into formal methods. From companies in safety-critical to academia, it was tens of millions at the least. The market noticed the results were failure in both adoption and profit.
Another angle is regulation. Companies on their own either refused to do QA or security, or faked it. It wasn’t until the Orange Book regulations forced them to do specific things, like formal methods and side-channel analysis, that they did that. Later, Common Criteria and DO-178B incentivized higher levels of quality. The market rarely invests in real security on their own.
Why do they not invest in real security? What could hamper formal methods adoption? Two reasons.
In the VAX VMM Security Kernel, they noticed that formally-verified, rigorous designs took two to three quarters for a significant change to the product. Competitors not using these things could slap together and sell what worked well enough. Project leader Steve Lipner, who made SDL for Microsoft from these lessons, said his take away was the market prioritizes shipping useful stuff to customers above all else. Others point out any cost or effort not generating revenue is a liability to management.
Roger Schell, one of the founders of INFOSEC, talked to executives about secure kernels long ago. He said they were interested but believed they’d never be sold. The reason? They believed companies intentionally made shoddy software to sell them the fixes as updates over time, thereby assuring long-term revenue. SaaS has only increased tactics like this for most companies. So, this incentive works against us still.
Lightweight, push-button analyzers are about the only worthwhile use of formal methods in the general market. They need to have low, false positives with a low price with integration with existing pipelines. Also, some companies want extra assurance for specific things, like financial protocols or secure updates, that justify some formal methods.
Outside that, I wouldn’t recommend formal methods today since I’ve seen 20 years of people loose uphill battles. Both in formal methods and just trying to spend more onboarding QA tools that slow development velocity. Whatever it is must clearly support, not hamper, management’s goals for the software from their viewpoint on priorities.
Another angle is regulation. Companies on their own either refused to do QA or security, or faked it. It wasn’t until the Orange Book regulations forced them to do specific things, like formal methods and side-channel analysis, that they did that. Later, Common Criteria and DO-178B incentivized higher levels of quality. The market rarely invests in real security on their own.
Why do they not invest in real security? What could hamper formal methods adoption? Two reasons.
In the VAX VMM Security Kernel, they noticed that formally-verified, rigorous designs took two to three quarters for a significant change to the product. Competitors not using these things could slap together and sell what worked well enough. Project leader Steve Lipner, who made SDL for Microsoft from these lessons, said his take away was the market prioritizes shipping useful stuff to customers above all else. Others point out any cost or effort not generating revenue is a liability to management.
Roger Schell, one of the founders of INFOSEC, talked to executives about secure kernels long ago. He said they were interested but believed they’d never be sold. The reason? They believed companies intentionally made shoddy software to sell them the fixes as updates over time, thereby assuring long-term revenue. SaaS has only increased tactics like this for most companies. So, this incentive works against us still.
Lightweight, push-button analyzers are about the only worthwhile use of formal methods in the general market. They need to have low, false positives with a low price with integration with existing pipelines. Also, some companies want extra assurance for specific things, like financial protocols or secure updates, that justify some formal methods.
Outside that, I wouldn’t recommend formal methods today since I’ve seen 20 years of people loose uphill battles. Both in formal methods and just trying to spend more onboarding QA tools that slow development velocity. Whatever it is must clearly support, not hamper, management’s goals for the software from their viewpoint on priorities.