Re: How difficult is software? [Re: OVC-discuss Digest, Vol 37, Issue 18]

From: Fred McLain <mclain_at_zipcon_dot_net>
Date: Sun Nov 25 2007 - 14:59:52 CST

Hi Ham,

I'm in the midst of verification via formal methods at work. What I
find astounding is that even in the simplest of security targets the
verification methods seem to increase complexity. In other words, the
code to automate the verification is more complex then the model to be
verified. Furthermore, there seems to be no attempt to verify the
verification code itself. Due to the overall increase of complexity
at each stage I seriously doubt that an end state of a verified system
can be reached.

I am a strong proponent of using existing standards for voting
software, as well as realistic limitation of the use of software
systems in voting. On the limits issue, as has be observed on this
list, HAVA does not require that non-handicapped users us software
intended to enable the handicapped to vote. Given that the vast
majority of voters can use systems like pen and paper, there is no
need to provide a touch screen system for every voter. In most, if
not all, cases the tabulation software can also be eliminated as well
since the overall volume of precinct level votes doesn't rise to the
level of requiring a computer to do that tabulation. If manual
recounts are possible then certainly manual initial counts are
plausible.

On the standards side, I am astounded at the complete lack of
discussion here. I've raised the possibility of using DO-178 (http://en.wikipedia.org/wiki/DO-178B
) and NIST Common Criteria (http://en.wikipedia.org/wiki/
Common_Criteria) as a starting point but haven't had any feedback so
far. Either people are uninterested or simply do not understand how
critical software system verification is done. Having worked in
critical industries with no strict standards (i.e. medical) this is an
issue that should be raised early and applied throughout the
development process. Even the weakest of standards, (i.e. ISO-9000C)
require that the entire development cycle reflects the standard under
which the development was performed.

        -Fred-

On Nov 14, 2007, at 7:58 AM, Hamilton Richards wrote:

> As Danny Swarzman observes, "software isn't witchcraft." Indeed,
> it's pure logic, applied on a large scale. (I say so from the vantage
> point of a 40-year career devoted to practicing that applied logic
> and teaching it to college students.)
>
> It's probably true that "an ordinary person can figure it [i.e.,
> software] out", if "figure it out" means "get a rough idea of what a
> program means, and maybe cobble together a program that seems to
> work."
>
> There is, however, a *huge* gulf between (1) reading and writing
> software and (2) verifying software.
>
> As evidence, consider the software produced by the many "people who
> use computer languages such as Java and xml." Such hard-working and
> well-meaning folks are the ones who produce the vast majority of the
> software sold around the world. With almost no exceptions, that
> software comes with blanket disclaimers which, translated from
> legalese, absolve the vendors of all responsibility for their
> products' correct operation.
>
> Can you name another industry that has such abysmal standards--and
> gets away with it?
>
> If "ordinary people" can observe hand counting of ballots, then they
> outnumber those who can verify open-source software by many orders of
> magnitude.
>
> At this point you may be suspecting that what Mr Swarzman means by
> "verify" and what I mean by it are two quite different notions. I
> don't wish to put words in his mouth, but in commonplace
> software-industry usage, "verify" means something like "inspect the
> source code, and test the corresponding executable until the rate of
> error discovery drops to some acceptable level." Even if the
> "acceptable level" is zero, however, testing cannot ensure that the
> software is error-free--for any program that is not utterly trivial,
> the number of cases to be tested makes exhaustive testing impossible.
> As Edsger W. Dijkstra famously said, "program testing may
> convincingly demonstrate the presence of bugs, but can never
> demonstrate their absence"
> <http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1036.html
> >.
>
> Inspection is actually more promising, but the way it is commonly
> practiced is far from adequate. It usually amounts to no more than
> some combination of line-by-line scrutiny and mental execution. As
> evidence of its inadequacy, consider the phenomenon of "Easter eggs".
> In software, an Easter egg is a hidden feature--often a spectacular
> one--inserted by the programmers as a kind of joke, and as evidence
> of their creativity and cleverness
> <http://en.wikipedia.org/wiki/Easter_egg_(virtual)>. Many software
> companies have stringent policies against Easter eggs and hunt them
> down mercilessly, yet they continue to appear.
>
> To be effective, inspection must rise to the level of formal
> reasoning <http://en.wikipedia.org/wiki/Formal_verification>, i.e.,
> mathematical proofs that programs satisfy given (formal)
> specifications. Such formal methods have been used successfully in
> developing commercial hardware and software since at least as far
> back as 1985, and their use has been spreading gradually
> <http://vl.fmnet.info/companies/>, but it's still far from the norm.
>
> If someone is seriously contemplating the application of such formal
> methods to software used in elections, I say more power to them, but
> I'm not holding my breath.
>
> All the best,
>
> --Ham
>
> At 12:00 PM -0800 2007/11/13, ovc-discuss-request@listman.sonic.net
> wrote:
>> [...]
>> Message: 1
>> Date: Mon, 12 Nov 2007 19:39:32 -0800
>> From: Danny Swarzman <danny@stowlake.com>
>> Subject: [OVC-discuss] Is hand count transparent?
>> To: Open Voting Consortium discussion list
>> <ovc-discuss@listman.sonic.net>
>> Message-ID: <EC3797E4-18E3-4152-8DC0-4DE7D1117C9B@stowlake.com>
>> Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed
>>
>> [...]
>>
>> But, software isn't witchcraft. An ordinary person can figure it out.
>> There are a lot of people who use computer languages such as Java and
>> xml. There' a huge number of books on these subject.
>>
>> If you don't want to read source code, you can get the source code
>> from the internet and follow directions and set up your own elections
>> system. Print some ballots. scan some votes see who wins in your
>> world.
>>
>> Like any human document, source code can be written clearly or not.
>> We hope ours is.
>>
>> There is a lot of talk about how difficult software is. Complex
>> software is tough to get completely correct in every detail. But this
>> isn't that complex. The source code involved is small compared to the
>> documents that describe the applicable regulations.
>>
>> Do you really think there is a larger class of people who can
>> observer hand counting than there is who can verify open source
>> software? They weren't in City Hall last Tuesday round midnight.
>>
>> -Danny
>
> --
> ------------------------------------------------------------------
> Hamilton Richards, PhD Department of Computer Sciences
> Senior Lecturer (retired) The University of Texas at Austin
> ham@cs.utexas.edu hrichrds@swbell.net
> http://www.cs.utexas.edu/users/ham/richards
> ------------------------------------------------------------------
> _______________________________________________
> OVC-discuss mailing list
> OVC-discuss@listman.sonic.net
> http://lists.sonic.net/mailman/listinfo/ovc-discuss
> By sending email to the OVC-discuss list, you thereby agree to
> release the content of your posts to the Public Domain--with the
> exception of copyrighted material quoted according to fair use,
> including publicly archiving at http://gnosis.python-hosting.com/voting-project/
>

_______________________________________________
OVC-discuss mailing list
OVC-discuss@listman.sonic.net
http://lists.sonic.net/mailman/listinfo/ovc-discuss
By sending email to the OVC-discuss list, you thereby agree to release the content of your posts to the Public Domain--with the exception of copyrighted material quoted according to fair use, including publicly archiving at http://gnosis.python-hosting.com/voting-project/
==================================================================
= The content of this message, with the exception of any external
= quotations under fair use, are released to the Public Domain
==================================================================
Received on Fri Nov 30 23:17:26 2007

This archive was generated by hypermail 2.1.8 : Fri Nov 30 2007 - 23:17:32 CST