Tunes and security

[Francois-Rene Rideau]

Dear Tunes people, here is what I wrote about Tunes and security recently.
Parts of the original mail on other subjects have been cut...

------>8------>8------>8------>8------>8------>8------>8------>8------>8------
To: hamdani@indo.net.id (Hamdani)
Date: Fri, 6 Dec 1996 22:04:59 +0100 (MET)

> 	<< Semantics etc>>
> 	How do you handle code security against
> reverse engineering/similar code?
> 	IMO the lawyers & chief of software
> companies will be interested in the matter.
>
This is an issue I've thought about a lot,
and here are my conclusions.
   Firstly, let me state that I don't personally think it any wishable
to protect software code: I am a convinced proponent of free software.
Now, I think that in as much as protecting software
would be wanted by some people, there is no reason why Tunes
couldn't support it better than (at least as well as) any other OS would.
Let's see what are the issues at stake.
   To me, the most important security that Tunes should provide
is that of the customer.
With Tunes, the customer can require from the software provider,
proofs that the software is correct with respect to its specifications,
and correctly implements all the alleged features without any bug,
or at least with potential problems pinpointed.
This means that competition between software providers
can be made on the basis of objective criteria,
instead of subjective arguments and financial threats.
This means that there will be no more $10^9 tax-worth rocket
exploding because of a lame bug in its software.
   Also important to me, the fact that software can migrate seamlessly,
so people are not the hostage of their current computer architecture.
   However, to prove software correct as well as to re-compile it
for optimized use in a different architecture, it requires that
the internals of the software be seen, which software protectors
would not like to be (I think that's bad from them,
but it's their right after all).
   My solution is that a trusted third party
could check proofs and optimize software,
while guaranteeing that nothing would be disclosed to anyone
about the checked or optimized sources (or about the specific
environment for which the sources are optimized).
Of course, it is a threat to have to trust such a third party;
however, people would be able to trust this third party,
because the customer contract would guarantee that
on any failure to respect non-disclosure,
or any incorrect output from the alleged checker or optimizer,
this service provider would pay large compensation to the injured customer.
I can also imagine that some clever guy might invent
a cryptographical "digest" of proofs, so the warrant could
publish a cryptographically-valid warranty that he has done a valid job,
in which case there will not have to be threats of large compensations.
   When it comes to co-optimize several pieces of software,
and/or to prove that the software modules can peacefully live together,
those third parties would provide more service than just hosting
a dumb checker and optimizer, as providing such proof could be
a non-trivial job in the general case, if the available software
specifications are not so complete as should be.
   Hence, the solution to this problem is to promote
new kinds of businesses: software warrants & software mixers.
   The mixers could use arbitrary code manipulation techniques
to make code more difficult to reverse engineer;
most of the time, usual optimization should be enough, though,
all the more when optimized code includes (safe)
run-time code generation and self-modifying code...
   Competition from free software will force those guys to keep prices low,
so they can't end up as another microsoftish monopoly, and everything is fine.
   Of course, it is always simpler and safer to directly
check source code, so customers might demand that they should
be given access to the source code, or else that price for indefinite
checking/mixing be included in the software license.
   Note that availability of source code does not
change anything about the legality of copyrights;
that you publish source doesn't mean that people can freely
infringe your patents and copyrights. So again,
the software hiding&warranting&mixing proponents
will have to keep prices low to be competitive.

> 	Another idea: can you build bullet proof
> anti piracy scheme from the ground? Perhaps
> with timing, central registration etc?
>
Well, depends on what you mean by "bullet proof":
there will always be flaws in just *any* system.
For example, you can kidnap someone who knows the password
and torture him till he admits it,
get a sample of the president's DNA to pass DNA tests,
attack the gold reserve of the bank to seize its gold
rather than pirating its software, etc.
Security is relative concept, and Tunes won't change that.
   What Tunes can do about it is to make you sure what you have,
and what you don't: what you have a proof that you have
relatively to some axioms, that you can trust that you have
in as much as the axioms are valid.
   Hence *if* you can identify class of potential security attacks,
and give a formal specification for software that resist this attack;
if you can make a list of reasonable security assumptions
(like no one can spy the computer using tempest technology,
like no super user will login and leave a security hole behind, etc);
then you can work on software that will comply to this specification,
together with a proof to such compliance assuming those assumptions.
Once done, you can be *sure* that the attack will always be repelled.
Of course, if you write an unsecure specification,
and your program complies to it, you're in trouble rather than safe.
   For instance, if people writing TCP/IP stacks had used
a formal specification for it, and had proved the compliance of
their implementation, then the "ping o' death" attack would
never have been possible.
   Similarly, by using better tools than C,
all the "buffer-overflow" attacks would be eradicated.
   You can also have a hierarchy of stronger assumptions,
with stronger security results everytime.
e.g. the program will run correctly if the remotely connected
object works properly, but even if it doesn't, there will be
no data corruption on the local computer,
just some resource waste and some data exported.
   Typically you would prove that access to some object
only occurs through a rightful set of primitives
that behave according to their specification.
Which means no particular security hole.
   But all your proofs can never prevent someone
from entering the system using super-user passwords,
or from opening the computer case and spying directly the hardware,
then compromise security by making a hole,
leaving open access to the computer.
If you allow remote login for some kind of user,
however double-checked, cryptographically protected, etc,
then you can't escape the possibility that this user
might have been pirated.
   However, you can only prove that *if* only regular access is used,
and *if* there is no hardware failure, and *if* no atomic bomb
explodes near the computer, *then* the system will behave like
specified, which, if you wrote your specification well, means
that everything is ok.
   If no irreversible action is to be taken from
a remote connection (like, well, you know, launching these atomic missiles),
then you can also reverse actions by those remote connections
that you later have identified as being invalid, from the activity log.

> It is possible to put ID code on each individual
> piece of CPU.
   I don't know how much it costs to put serial numbers on each CPU:
you must change the silicon mask everytime,
which might be cheap or expensive.
   Even then, Tunes will not per se make new security problems
or solution appear. What Tunes allows is better, faster, more reliable,
dynamic combination of software modules.
Tunes won't invent any algorithm or computer system feature,
but it will allow seamless safe dynamic integration of these features
in anyone's system, as a set of independently developed modules.
Surely, programming of attack modules might be eased, too,
so this will encourage people to be all the more careful and cautious,
and never ever take any risk.
Overall, Tunes will not provide any really new concept
that wouldn't exist without it,
but it will increase overall software quality
by making these concepts combine instead of just sitting
each in its corner.

[...]

> IMO you should focus on sample everday apps,
> Word Processing, Spreadsheet, Graphics, because
> when you run demo, it is difficult to show
> abstract concept.
Yeah. As soon as I have my beta running,
I'll implement some database and spreadsheet software
as trivial applications.
I expect lots of people from the free software community
to help with Word Processing and Graphics, etc,
as soon as I can prove the interest of my development platform.

> 	The audience only want to see fast, reliable result
> (Response time???)
   As for fast, don't expect the free beta version of Tunes
to be as fast as $multiM worth optimizing compiler benchmark output!
However, reliability should be good, and response time reasonable,
because of clean design.
------>8------>8------>8------>8------>8------>8------>8------>8------>8------
== Fare' -- rideau@ens.fr -- Franc,ois-Rene' Rideau -- DDa(.ng-Vu~ Ba^n ==
Join the TUNES project for a computing system based on computing freedom !
                TUNES is a Useful, Not Expedient System
URL: "http://www.eleves.ens.fr:8080/home/rideau/Tunes/"