Popular Media Coverage of Software and Formal Methods

Popular Media Coverage of Software and Formal Methods

Matt Konda No Comment
Application Security

It is interesting … in the wake of Equifax and other recent news, The Atlantic has published several articles about software:

I say it is interesting because I am completely torn about both of them.  On the one hand, they are correct.  The Equifax Breach should not really be a surprise and the fact that there are coding errors in any system of significant size is something that most software developers or security professionals would accept without argument.

On the other hand, complacency or acceptance is the last thing that I would advocate for developers, consumers or companies after the Equifax breach.  I’ve already written about that here.

Furthermore, while formal methods present an interesting direction for software verification, in practice they are limited to very specific use cases.  I’ve never seen them employed professionally for any widely used application.  That doesn’t mean they aren’t or couldn’t be, but if I haven’t seen it – probably its not real or accessible for common developers yet.

An interesting side effect of these articles being in The Atlantic is that people who wouldn’t usually ask about these things are asking.  I’ve heard about each of these articles from numerous people at clients and partners.  I suppose that is a benefit of having the discussion – provided people have the attention span to continue the discussion.

The “Saving the World From Code” article also included a general quote which I think probably should have been attributed to Marc Andreesen in the Wall St. Journal in 2011:

It’s been said that software is “eating the world.”

The fact that it is not, makes me wonder just a bit about the context the article is written from.  One thing I can’t argue with is the substance of that quote, which again was from 2011.  I would perhaps add to it that software is flawed everywhere.  I just don’t buy that formal systems or rigorous modeling are a realistic near term solution for that.  Many of our clients are adopting new languages or technology – sometimes with more security issues – even as we work to secure their systems.  The idea of a 4GL language, which has been an idea for almost my whole professional career, where we can assemble a program in an increasingly sophisticated IDE with visual blocks like the hacking scene in the movie Swordfish seems unachievable in practice.  If anything, I prefer simpler text editors than ever before.

Ultimately, there is a lot that we can do to secure our systems.  Things like threat modeling to identify and then isolate scope, actively working on architecture, building common reliable blocks, teaching developers, building cultures that value security, using tools and smarts to think about scenarios, teaching practices that encourage security to be a first class part of the SDLC … all of these are real things people in the real world are doing to make software safer.  I doubt there is a silver bullet that somehow avoids the people understanding the problem – we have to accept that as a cost or accept the insecurity of the software we use.  I guess that’s why people hire us to help them secure their software.

Leave a Reply