[Haskell-cafe] How to create an online poll
gwern0 at gmail.com
Thu Feb 19 11:38:37 EST 2009
2009/2/19 Luke Palmer <lrpalmer at gmail.com>:
> 2009/2/19 Rick R <rick.richardson at gmail.com>
>> I think the capabilities community including E and Coyotos/BitC have
>> extensively addressed this topic. Coyotos is taking the correct approach for
>> trusted voting platform. Since, even if your software is trustworthy, it
>> can't be trusted if the OS on which it runs is suspect.
> Woah, that's a pretty interesting question! How do you write software which
> is protected against a malicious operating system (mind -- not erroneous,
> but rather somebody detecting the software you're running and changing your
> vote). Maybe some sort of randomized cryptographic technique, in which,
> with high probability, the OS either runs your program correctly or causes
> it to crash.
Free associating: "Static Typing for a Faulty Lambda Calculus"
"A transient hardware fault occurs when an energetic particle strikes
a transistor, causing it to change state. These faults do not cause
permanent damage, but may result in incorrect program execution by
altering signal transfers or stored values....This paper defines the
first formal, type-theoretic framework for studying reliable
computation in the presence of transient faults. More specifically, it
defines lambda-zap, a lambda calculus that exhibits intermittent data
faults. In order to detect and recover from these faults, lambda-zap
programs replicate intermediate computations and use majority voting,
thereby modeling software-based fault tolerance techniques studied
extensively, but informally.
To ensure that programs maintain the proper invariants and use
lambda-zap primitives correctly, the paper defines a type system for
the language. This type system guarantees that well-typed programs can
tolerate any single data fault. To demonstrate that lambda-zap can
serve as an idealized typed intermediate language, we define a
type-preserving translation from a standard simply-typed lambda
calculus into lambda-zap."
More information about the Haskell-Cafe