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

From: Hamilton Richards <hrichrds_at_swbell_dot_net>
Date: Mon Nov 26 2007 - 15:04:56 CST

Hi, Fred--

At 12:59 PM -0800 2007/11/25, you wrote:
>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.

Was the code being verified designed with verification in mind, or is
the verification being attempted on completed code? The latter is
notoriously more problematic.

If the code to automate the verification is more general than the
code being verified, it's hardly surprising that it's more complex.
The same can be said for compilers, which are more complex than many
of the programs to which they are applied.

>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.

You seem to be referring to a specific system. What you're saying is
no doubt true of that system, but not of all verification systems.
For example, ACL2 <http://en.wikipedia.org/wiki/ACL2>.

>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.

To be sure, most voters can use pen and paper, but electronic ballot
printers have their advantages:

      + there's no expensive inventory of blank ballots to be printed
and securely stored
          before the election

      + disabilities and alternative languages are accommodated more easily

      + overvotes can be prevented, and undervotes can be detected

      + unlike ballots marked by hand, in which the voter's intent can
be obscured by stray marks
         and other mistakes, machine-marked ballots can be read,
manually or by machine, with
         extremely high accuracy

      + machine-printed ballots eliminate a time-honored technique for
fraudulently disqualifying
         ballots by surreptitiously adding stray marks (e.g., using
bits of pencil lead hidden under
         vote counters' fingernails)

Whether these advantages are worth the cost is open to debate, but
they should be debated and not simply ignored.

>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.

Machine-printed ballots would be easy to count manually.

>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.

Voting software is not critical in the same sense as software that
controls medical equipment and aircraft.

Such control software is actually *in control*, and if it screws up
there's often no way for a human to intervene. Voting software, on
the other hand, *can* be used in such a way that screwups can be
detected and corrected before any harm is done.

Note the "*can* be used" in the preceding sentence. If software were
used, as in the first-generation DREs, to count votes with no
meaningful audit, then it would be critical, but I assume that
subscribers to this list agree with me that such systems are totally
unacceptable.

Software that prints ballots which voters inspect before dropping
them in a ballot box is not critical--every voter has an opportunity
to intervene and correct any errors the machine may have made.

Software that runs optical scanners and counts votes is also not
critical, since its operations are subject to audit by manual
recounts of any desired fraction of the printed ballots.

If formal verification technology were more widely practiced and less
expensive than it is, I'd have no objection to applying it to
election software. As things stand, however, requiring formal
verification for election software would be a show-stopper--it would
add tremendously to the cost and time required, and there just aren't
enough people capable of developing formally verified software.

Regards,

--Ham

-- 
------------------------------------------------------------------
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/
==================================================================
= 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:27 2007

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