Problem (was: Re: need help with tool requirement)

[Bob Bell]

On Wed, Apr 21, 2004 at 01:33:26AM -0400, bmcculley at rcn.com wrote:
> Here's the real problem description.
> 
> Electronic voting machines are feared to be vulnerable to hidden
> malicious code ("Easter eggs") that could subvert voter intentions and
> deliver votes to the wrong candidates.  One proposed solution is to
> require paper ballots be produced by electronic voting machines, but
> this creates other problems.  There is also a practical constraint
> that retrofitting existing systems for paper output will not be
> feasible in the timeframe required for the upcoming election, for
> a variety of reasons (simple installed base logistics among them).
> Thus there is a strong desire and motivation to be able to validate
> the software for systems that are already in the field (it is an
> acceptable constraint to require updating deployed systems to a new
> validated software version).

I believe that in order to validate definitively that there are no
"Easter Eggs", you'd have to explore all *combinations* of branches
taken (or not), not just all branches.  Obviously, that evaluation will
be exponential.

Not to mention that some branches simply may not be taken.  Just
yesterday I was studying papers about "software watermarking" for
a graduate computer science class (which in part actually discusses
hiding "Easter Eggs").  One part of hiding code that implements
a software watermarking is adding "opaque predicates".  These are
predicates to a branch that always evaluate the to same truth value, but
which are "very difficult" to determine that that is the case.  If done
properly, "very difficult" means that you would have to perform global
analysis on the code with relative "smart" algorithms, and your analysis
would take exponential time.  For code of significant size, that
basically means you're not going to get done with today's computing
power.  And taking a branch during testing that in practice won't be
taken (whether done deliberately as part of code obfuscation or just as
a result of the program structure) may put your program into an invalid
state.

-- 
Bob Bell