Improve or Remove "Classification"

[fare]

Current notion of "classified" information doesn't actually help and only makes things more cumbersome for the user.

We should either

1. Improve the notion of "classification", or
2. Remove that notion and accompanying code from our codebase, or
3. Somehow gather evidence that it is useful at all (as opposed to, e.g. being accepted it as useful out of intimidation).

Currently, the use of declassify! is completely redundant with publish!, since there is a one-to-one correspondance between consecutive statements of one and the other, with no use for one without the other. It just makes code heavier to write for no benefit except redundant redundancy. (There is one exception, whereby digests are deemed declassified by default, which is completely misleading. For instance, publishing digest(hand), without salt, or reusing the same salt, is just as good as publishing hand.)

One way to improve classification would be for it to be more like perltaint: private keys and other sensitive material could be marked as "tainted", so they can't leak. Note that tainting in perl is meant to prevent untrusted user-provided data from affecting system state before it was suitably validated, which is a different use case; based on the same flow analysis, many such use cases could be satisfied.

But the entire premise of Alacrity is that the programs will be small enough to fit in a brainful, will express the exact semantics of information flow between participants (no flow outside the program), and will be analyzed using precise logical predicates. In this context, the crude overapproximation of classification offers no advantage, only noise.

Another way to improve on classification would be to replace it with assertions about epistemic propositions, such as "at this point in the program, Bob doesn't know Alice's hand". This would enrich the set of "precise logical predicates" we can express about the information flow, and could be much more useful than classification. The actual difficulty, which is not helped by "classification", is in accounting for indirect ways to decode the data (as in the unsalted or missalted digest, or in commutative encryption, etc.). These indirect ways might or might not be easily modeled into an affordably decidable extension to Z3; or then again might, but it will be non-trivial work to dig into the literature for attacks and build a useful logical model for them.

[fare]

Another good reason I want to get rid of declassify! for now is that it affects our sales pitch regarding how Alacrity saves a 10x factor in lines of code to be written. At the moment, the feature doesn't pull its weight compared to its cost.