[trustable-software] So how do we get there from here?

Gerald Harris gerald.harris at t-online.de
Fri Jul 29 13:36:08 UTC 2016


Hello,

I would like to start by providing my own very personal statement of what I would expect of trustworthy software (with a short bow to Paul and Colin re. the difference between “trustable” and “trustworthy”).
Trustworthy software must fulfill the purpose for which it was intended.

It must always behave as expected without any surprises.

It may only fail as a result of external conditions having changed such that the intended behaviour is no longer safely possible.

If it fails, it must do so in a fashion that precludes danger or damage and which does not obscure the cause of the failure.

In some of the discussions so far, specific development processes have been suggested as a way to achieve trustworthy software. The implication seems to be that if these processes are followed the resulting software will be more trustworthy than software that was produced without these processes. I must confess to a deep distrust of processes. I freely acknowledge the need for and the potential benefit of processes. This ties in with the fact that software development as a whole is all too seldom treated as an engineering discipline - there are far too many artists amongst us yet. On the other hand, I am sure that we all have had extensive experience with processes in which the quality of the documentation seems be equated to its weight as hardcopy. IMHO the purpose of a formal process should be to support and guide the developer in his work, to ensure that essential considerations are not neglected. A certain degree of pragmatism and freedom must be preserved. All too often in the concrete day to day practice, poorly implemented and overly strict processes are imposed by a technologically analphabetic, misguided management, serving largely to provide them with an illusion of understanding and control.

Rather than trusting to process alone, I would desire to make use of software to make software more trustworthy. Where are the commercial tools that can usefully analyse source code and detect architectural anti-patterns? At this time I am only aware of Gamma [1] despite a wealth of research and scholarly articles.[2][3] Most of the tools with which I have been confronted over the years are either too limited in their targeted scope (PClint, Coverity, etc), are too strongly focussed on some subset of the problem (e.g. Veracode as an AST tool) or simply don’t scale to modern large systems containing many millions of lines of code.

Model driven engineering shows promise, opening the door to formal model verification. Indeed, formal verification would seem to be the holy grail. However, modelling always involves simplification, glossing over those aspects of the problem and solution domains which would otherwise make the model overly complex and/or unmanageable. How do we verify those hand-written parts of the solution which must be added to the model to provide a complete solution?
Moving beyond model driven engineering, one might consider the general issue of formal verification. Quoting from the Wikepedia article for “formal verification”:
Formal verification is the act of proving <https://en.wikipedia.org/wiki/Mathematical_proof> or disproving the correctness <https://en.wikipedia.org/wiki/Correctness_%28computer_science%29> of intended algorithms <https://en.wikipedia.org/wiki/Algorithms> underlying a system with respect to a certain formal specification <https://en.wikipedia.org/wiki/Formal_specification> or property, using formal methods <https://en.wikipedia.org/wiki/Formal_methods> of mathematics <https://en.wikipedia.org/wiki/Mathematics>.
If software can be proven mathematically to be correct, this should be sufficient to be able to consider it to be trustworthy. However, one must also remember that every proof is based on assumptions. Violation of any assumption will invalidate the proof. Formal correctness is a fragile achievement and the path of formal proof is difficult.

Another fascinating quote (at least in my mind) can be found towards the end of the same article.

At present, formal verification is used by most or all leading hardware companies, but its use in the software industry <https://en.wikipedia.org/wiki/Software_industry> is still languishing.
In short, I am trying to make two points with this post. We should not limit ourselves in this discussion by focusing on security, safety, reliability or any other individual attribute which we would expect of trustworthy code. These issues are essential and valid, but no one of them should be used to define the context of our discussions. The second point is that we need to devote some serious thought to the question of how to get there from here.

I would be very interested in positive and negative experiences that others may have had in trying to address the question of trustworthy software. What lessons have you learned and how has this influenced you?

best regards,
Gerald Harris

[1] http://www.acellere.com/ <http://www.acellere.com/>
[2] Knowledge-based Software Engineering: Proceedings… <https://books.google.de/books?id=F-pFOkejbK4C&pg=PA161&lpg=PA161&dq=%22anti-patterns%22+static+source+code+analysis&source=bl&ots=5W0H0O-WZk&sig=qQxsxE0S1Qq7Pf4V5W-SF7inGyM&hl=en&sa=X&ved=0ahUKEwj3_PiZ25jOAhXCOBQKHY-QBTcQ6AEITjAD>
[3] Mining the Relationship between Anti-patterns Dependencies and ... <https://www.google.de/url?sa=t&rct=j&q=&esrc=s&source=web&cd=5&cad=rja&uact=8&ved=0ahUKEwj3_PiZ25jOAhXCOBQKHY-QBTcQFghRMAQ&url=https://www.computer.org/csdl/proceedings/wcre/2013/9999/00/06671310.pdf&usg=AFQjCNHpCgPBK9QyELznbuBVbxGNtpkKCQ>


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.veristac.io/pipermail/trustable-software/attachments/20160729/04375977/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <https://lists.veristac.io/pipermail/trustable-software/attachments/20160729/04375977/attachment.sig>


More information about the trustable-software mailing list