Security

As time goes, liberty turns into security, which in turn may guarantee the possibility of new liberties. But beware not to sacrifice liberty for security: you'd jeopardize any further improvement, and make impossible any adaptation to the evolving world, thus ensuring that the system would rot. From Munich 1938 on, the occidental democracies are long known to have made such tragic choice, that they have been long warned against (there's a quote from Benjamin Franklin, but sure there may be older ones).

Such a problem is not out of the scope of the TUNES project: in the computing world, it can be said that those who stick to uneffective static C language and traditional system design are making such a choice.

Security in a dynamic system has the same problems as information in general: to have any validity, it must be constantly confronted to experience and reason. Nothing is 100% secure, and there are always uncheckable assumptions one makes about anything. As security is concerned, such assumptions, that may lead to inconsistency, are called security holes. The size of a hole is inversely proportional to the complexity needed to find such an inconsistency using the assumption. The goal is to have holes so little that we can expect inconsistencies not to happen in any reasonable time.

In traditional systems, all security is based on static, low-level, centralized protection schemes. Each software component is a hole in itself. Assembling software components is done without any security about such components not interacting badly. The paranoid checking that takes place is useless because it's so stupid and the billion dollars spent in having hardware do most of this checking is a shameful waste of resources. Sure this statistically reduces the size of security holes, but all this only postpones crashes, of which the menace is as dreadful as the actual event, because it forces to save and restore everything which we saw was extremely clumsy in these systems. See Persistence.

To solve any security problem, computing systems must stop their flight forward (see Users), and use introduce objective criteria to select the way they can securely assemble components.

Tunes intends to solve this problem by allowing and encouraging the use of formal methods for program specification, making all axioms explicit, so that contractors can know what they exchange. The methods allow for all the formal arguments that men can have, with all the additional rigor and precision that only the machine can provide, plus large databases of programs committed to open development, instead of subjective, almost-blind author-to-author trust communications.

See this Security Taxonomy by Mark Miller (author of a capabilities based programming language E).

Pages in this topic: Capability   Cryptography   Information-Flow Security   Language-Based Security  

Also linked from: Computing Liberalism   Continuation   Correctness   Ethics   Exokernel   GO!   Hermes   Isolation   ITS   Liberty   Microkernel Debate   Monopoly   Multipop   Orthogonal Persistence   Protection   Super-User   Trust   Unity Project   User Rights