Hacker News Reader

Comment by nickpsecurity | Hacker News Reader

High-assurance software and security field have been doing real engineering for decades. Here's a nice presentation with a tie-in to another high-assurance discipline:

http://web.cecs.pdx.edu/~hook/cs491sp08/AssuranceSp08.ppt

Here's an old method, Cleanroom, that was cost-effective for business with low, defect rate even on first use:

http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=E10....

Altran[-Praxis] is a modern company engineering solutions with their Correct by Construction methodology:

http://www.sis.pitt.edu/jjoshi/Devsec/CorrectnessByConstruct....

They warranty their code like Cleanroom teams used to. Still in business so the method works. ;) Their SPARK tool is now GPL with lots of learning resources available. So, those are a few examples of engineering software vs just developing it. The results in terms of predictability, reliability and low defects speak for themselves.

View on HN

About Cleanroom, the prohibition on unit testing is insane; CPU and compiler bug exists, so do subtleties in languages, and even good quality models in formalized forms have some defects that probably prevent to get a mathematical proof of correctness even if the CPU/Compiler would be defect free (ex: C++11 memory model - and I think the formal Java memory model also has some issues). They should do as if they are forbidden to do unit testing, but then once they are "sure" all their code is correct do it anyway. Having a separate team do some level of testing is fine, but there is value in also having some done by authors, because conveying all the intents and caveats and things taken into account when writing it but also things NOT done and the reason for that, about a piece of source code, even very small, is incredibly hard.

Oh I agree with you entirely. Not running code and no unit testing were critiques I had with it. I used it as an example of engineering software. Cleanroom certainly isnt the last word in that.

Personally, as it's function-oriented, I'd combine it with a subset of Haskell that was easy to translate into imperative code. Build the app with Haskell, use QuickCheck/QuickSpec, test every execution path, covert channels via Flow Caml-like setup, and certified compilation to target with pre-verified runtime. Now, we can use that directly or use it as an executable spec for an imperative implementation.

So, that's how I see applying Cleanroom today for most benefit. Maybe drop the statistical stuff, too.

Here's the two truncated links:

http://pastebin.com/e5sgFpjx

The 2nd and 3rd links are truncated and do not seem to go where they are supposed to go.

Didnt know this forum did that and Im already at work. Ill reply to that comment with new links soon if possible on mobile. Otherwise Ill add it when Im home after 10p.

Edit: added them in a reply via pastebin.

Reply on news.ycombinator.com